theory Exercise09
imports "HOL-IMP.Small_Step" "HOL-IMP.Def_Init"
begin
section "Definite initialization analysis"
(* fun ivars :: "com \ vname set" where *)
(* fun ok :: "vname set \ com \ bool" where *)
lemma "D A c A' \ A' = A \ ivars c \ ok A c"
oops
lemma "ok A c \ D A c (A \ ivars c)"
oops
section "Dependencies"
(* the following function checks whether a specific variable gets assigned in a command *)
fun assigned :: "com \ vname \ bool" where
"assigned SKIP x \ False"
| "assigned (x ::= a) y \ (x = y)"
| "assigned (c1;; c2) x \ assigned c1 x \ assigned c2 x"
| "assigned (IF b THEN c1 ELSE c2) x \ assigned c1 x \ assigned c2 x"
| "assigned (WHILE b DO c) x \ assigned c x"
lemma unassigned_implies_equal: "\ (c, s) \ t; \ assigned c x \ \ s x = t x"
by (induction c s t rule: big_step_induct) auto
(* this is the inductive definition we're interested in *)
inductive influences :: "vname \ com \ vname \ bool" where
Skip: "influences v SKIP v"
(* add the remaining cases, you're going to need at least one per command type *)
(* we compute the set of dependencies of x as all variables y that influence it *)
abbreviation deps :: "com \ vname \ vname set" where
"deps c x \ {y. influences y c x}"
(* prove the following lemma *)
lemma deps_unassigned_keep: "\ assigned c x \ x \ deps c x"
(* hint: this lemma should go through with the following invocation: *)
(* by (induction c) (auto intro: influences.intros) *)
oops
(* this is the final statement *)
(* Hints:
- obviously, this should be proved by induction big_step_induct
- hence, there are 7 cases to consider
- it is sufficient to prove 4 out of the remaining 6 cases
- don't hesitate to use Sledgehammer
*)
lemma deps_sound:
"\ (c, s) \ t; s = s' on deps c x; (c, s') \ t' \
\ t x = t' x"
proof (induction c s t arbitrary: s' t' x rule: big_step_induct)
case Skip thus ?case by (auto intro: influences.intros)
oops
end