# Theory Def_Init_Sound_Small

Up to index of Isabelle/HOL/HOL-IMP

theory Def_Init_Sound_Small
imports Def_Init Def_Init_Small
`(* Author: Tobias Nipkow *)theory Def_Init_Sound_Smallimports Def_Init Def_Init_Smallbeginsubsection "Soundness wrt Small Steps"theorem progress:  "D (dom s) c A' ==> c ≠ SKIP ==> EX cs'. (c,s) -> cs'"proof (induction c arbitrary: s A')  case Assign thus ?case by auto (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_mono:  "D A c M ==> A ⊆ A' ==> EX M'. D A' c M' & M <= M'"proof (induction c arbitrary: A A' M)  case Seq thus ?case by auto (metis D.intros(3))next  case (If b c1 c2)  then obtain M1 M2 where "vars b ⊆ A" "D A c1 M1" "D A c2 M2" "M = M1 ∩ M2"    by auto  with If.IH `A ⊆ A'` obtain M1' M2'    where "D A' c1 M1'" "D A' c2 M2'" and "M1 ⊆ M1'" "M2 ⊆ M2'" by metis  hence "D A' (IF b THEN c1 ELSE c2) (M1' ∩ M2')" and "M ⊆ M1' ∩ M2'"    using `vars b ⊆ A` `A ⊆ A'` `M = M1 ∩ M2` by(fastforce intro: D.intros)+  thus ?case by metisnext  case While thus ?case by auto (metis D.intros(5) subset_trans)qed (auto intro: D.intros)theorem D_preservation:  "(c,s) -> (c',s') ==> D (dom s) c A ==> EX A'. D (dom s') c' A' & A <= A'"proof (induction arbitrary: A rule: small_step_induct)  case (While b c s)  then obtain A' where "vars b ⊆ dom s" "A = dom s" "D (dom s) c A'" by blast  moreover  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)  ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"    by (metis D.If[OF `vars b ⊆ dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)  thus ?case by (metis D_incr `A = dom s`)next  case Seq2 thus ?case by auto (metis D_mono D.intros(3))qed (auto intro: D.intros)theorem D_sound:  "(c,s) ->* (c',s') ==> D (dom s) c A' ==> c' ≠ SKIP   ==> ∃cs''. (c',s') -> cs''"apply(induction arbitrary: A' rule:star_induct)apply (metis progress)by (metis D_preservation)end`