theory ex07_tmpl 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))" | Seq1: "(SKIP;;c,s) \ (c,s)" | Seq2: "(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" fun AA :: "com \ vname set" where "AA c = undefined" (* provide a suitable definition *) fun D :: "vname set \ com \ bool" where "D A c = undefined" (* provide a suitable definition *) subsection "Soundness wrt Small Steps" theorem progress: "D (dom s) c \ c \ SKIP \ \ cs'. (c,s) \ cs'" sorry lemma D_incr: "(c,s) \ (c',s') \ dom s \ AA c \ dom s' \ AA c'" sorry lemma D_mono: "A \ A' \ D A c \ D A' c" sorry theorem D_preservation: "(c,s) \ (c',s') \ D (dom s) c \ D (dom s') c'" sorry theorem D_sound: "(c,s) \* (c',s') \ D (dom s) c \ c' \ SKIP \ \cs''. (c',s') \ cs''" sorry end