theory sol08_2 imports "~~/src/HOL/IMP/Com" "~~/src/HOL/IMP/Def_Init_Exp" "~~/src/HOL/IMP/Def_Init" "~~/src/HOL/IMP/Vars" begin subsection "Initialization-Sensitive Small Step Semantics" inductive small_step :: "(com \ state) \ (com \ state) \ bool" (infix "\" 55) where Assign: "aval a s = Some i \ (x ::= a, s) \ (SKIP, s(x := Some i))" | Semi1: "(SKIP;;c,s) \ (c,s)" | Semi2: "(c\<^sub>1,s) \ (c\<^sub>1',s') \ (c\<^sub>1;;c\<^sub>2,s) \ (c\<^sub>1';;c\<^sub>2,s')" | IfTrue: "bval b s = Some True \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>1,s)" | IfFalse: "bval b s = Some False \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \ (c\<^sub>2,s)" | While: "(WHILE b DO c,s) \ (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" lemmas small_step_induct = small_step.induct[split_format(complete)] inductive small_steps :: "com * state \ com * state \ bool" (infix "\*" 55) where refl: "cs \* cs" | step: "cs \ cs' \ cs' \* cs'' \ cs \* cs''" lemmas small_steps_induct = small_steps.induct[split_format(complete)] subsection "Definite Initialization Analysis 2" fun AA :: "com \ vname set" where "AA SKIP = {}" | "AA (x ::= a) = {x}" | "AA (c1;; c2) = AA c1 \ AA c2" | "AA (IF b THEN c1 ELSE c2) = AA c1 \ AA c2" | "AA (WHILE b DO c) = {}" fun D :: "vname set \ com \ bool" where "D _ SKIP = True" | "D A (x ::= a) = (vars a \ A)" | "D A (c1;; c2) = (D A c1 \ D (A \ AA c1) c2)" | "D A (IF b THEN c1 ELSE c2) = (vars b \ A \ D A c1 \ D A c2)" | "D A (WHILE b DO c) = (vars b \ A \ D A c)" subsection "Soundness wrt Small Steps" theorem progress: "D (dom s) c \ c \ SKIP \ \ cs'. (c,s) \ cs'" proof (induct c arbitrary: s) case Assign thus ?case by simp (metis aval_Some small_step.Assign) next case (If b c1 c2) then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some) then show ?case by (cases bv) (auto intro: small_step.IfTrue small_step.IfFalse) qed (fastforce intro: small_step.intros)+ lemma D_incr: "(c,s) \ (c',s') \ dom s \ AA c \ dom s' \ AA c'" by (induct rule: small_step_induct) auto lemma D_mono: "A \ A' \ D A c \ D A' c" apply (induct c arbitrary: A A') apply auto by (metis order_refl sup_mono) theorem D_preservation: "(c,s) \ (c',s') \ D (dom s) c \ D (dom s') c'" proof (induct rule: small_step_induct) case (Semi2 c1 s c1' s' c2) hence "dom s \ AA c1 \ dom s' \ AA c1'" using D_incr by simp moreover from Semi2 have "D (dom s \ AA c1) c2" by simp ultimately have "D (dom s' \ AA c1') c2" by (rule D_mono) with Semi2 show ?case by simp next case While thus ?case by auto (metis D_mono Un_commute Un_upper2) qed auto theorem D_sound: "(c,s) \* (c',s') \ D (dom s) c \ c' \ SKIP \ \cs''. (c',s') \ cs''" by (induct rule:small_steps_induct) (metis progress D_preservation)+ (* The equivalence *) lemma aux: "Def_Init.D A c A' \ A' = A \ AA c" by (induct rule: Def_Init.D.induct) auto lemma "D A c \ Def_Init.D A c (A \ AA c)" apply rule apply (induct c arbitrary: A) apply (auto intro: Def_Init.D.intros) apply (rule Def_Init.D.intros) apply (auto) apply (metis Un_assoc) thm Def_Init.D.intros apply (simp add: Un_Int_distrib) apply (rule Def_Init.D.intros) apply (auto) apply (induct A'\"A\AA c" rule: Def_Init.D.induct) apply (auto dest: aux) done end