(*<*)
theory tut09
imports Main "~~/src/HOL/IMP/Vars" "~~/src/HOL/IMP/Small_Step"
begin
(*>*)
text {* \ExerciseSheet{9}{8.~12.~2015} *}
text {*
\Exercise{Available Expressions}
*}
text {*
Regard the following function @{text "AA"}, which computes the {\em
available assignments} of a command. An available assignment is a
pair of a variable and an expression such that the variable holds
the value of the expression in the current state. The function
@{text "AA c A"} computes the available assignments after executing
command @{text "c"}, assuming that @{text "A"} is the set of
available assignments for the initial state.
Note that available assignments can be used for program
optimization, by avoiding recomputation of expressions whose value
is already available in some variable.
*}
fun AA :: "com \ (vname \ aexp) set \ (vname \ aexp) set" where
"AA SKIP A = A" |
"AA (x ::= a) A = (if x \ vars a then {} else {(x, a)})
\ {(x', a'). (x', a') \ A \ x \ {x'} \ vars a'}" |
"AA (c\<^sub>1;; c\<^sub>2) A = (AA c\<^sub>2 \ AA c\<^sub>1) A" |
"AA (IF b THEN c\<^sub>1 ELSE c\<^sub>2) A = AA c\<^sub>1 A \ AA c\<^sub>2 A" |
"AA (WHILE b DO c) A = A \ AA c A"
(*
abbreviation setminus :: "'a set \ 'a set \ 'a set" (infixl "\" 65)
where "setminus \ op -"
*)
term "{(x,e). P x e}"
term "{f x e | e. P e}"
fun kill :: "com \ (vname\aexp) set"
and gen :: "com \ (vname\aexp) set"
where
"kill SKIP = {}"
| "kill (x ::= e) = {(x',e'). x'=x \ e'\e \ x\vars e' }"
| "kill (c1;;c2) = (kill c1 - gen c2) \ kill c2"
| "kill (IF b THEN c1 ELSE c2) = kill c1 \ kill c2"
| "kill (WHILE b DO c) = kill c"
| "gen SKIP = {}"
| "gen (x ::= e) = {(x,e)}"
| "gen (c1;;c2) = gen c1 \ gen c2"
| "gen (IF b THEN c1 ELSE c2) = gen c1 \ gen c2"
| "gen (WHILE b DO c) = {}"
lemma AA_gen_kill: "AA c A = (A \ gen c) - kill c"
apply (induction c arbitrary: A)
apply auto
done
lemma AA_sound_aux:
assumes "(c,s) \ s'"
assumes "\(x,e)\A. s x = aval e s"
shows "\(x,e)\AA c A. s' x = aval e s'"
using assms
(* unfolding AA_gen_kill *)
proof (induction arbitrary: A rule: big_step_induct)
case (WhileTrue b s1 c s2 s3) show ?case
using WhileTrue.IH(2)[OF WhileTrue.IH(1)[OF WhileTrue.prems]]
by (simp add: AA_gen_kill)
have ?case
proof clarsimp
fix x e
assume "(x, e) \ A" "(x, e) \ AA c A"
from WhileTrue.IH(1)[OF WhileTrue.prems] have
"\a\AA c A. case a of (x, e) \ s2 x = aval e s2" .
from WhileTrue.IH(2)[OF this, simplified] have
"\x\AA c A \ AA c (AA c A). case x of (x, e) \ s3 x = aval e s3" .
also have "AA c A \ AA c (AA c A) = AA c A" by (auto simp add: AA_gen_kill)
finally show "s3 x = aval e s3" using \(x, e) \ AA c A\ by blast
qed
qed (auto, fastforce)
lemma AA_sound: "(c,s) \ s' \ (x,e)\AA c {} \ s' x = aval e s'"
using AA_sound_aux by blast
lemma "n+m = (0::nat)"
apply (induction n)
apply (induction m)
end