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