43158

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Def_Ass_Sound_Small imports Def_Ass Def_Ass_Small


4 
begin


5 


6 
subsection "Soundness wrt Small Steps"


7 


8 
theorem progress:


9 
"D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"


10 
proof (induct c arbitrary: s A')


11 
case Assign thus ?case by auto (metis aval_Some small_step.Assign)


12 
next


13 
case (If b c1 c2)


14 
then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)


15 
then show ?case


16 
by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)


17 
qed (fastsimp intro: small_step.intros)+


18 


19 
lemma D_mono: "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"


20 
proof (induct c arbitrary: A A' M)


21 
case Semi thus ?case by auto (metis D.intros(3))


22 
next


23 
case (If b c1 c2)


24 
then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"


25 
by auto


26 
with If.hyps `A \<subseteq> A'` obtain M1' M2'


27 
where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis


28 
hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"


29 
using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastsimp intro: D.intros)+


30 
thus ?case by metis


31 
next


32 
case While thus ?case by auto (metis D.intros(5) subset_trans)


33 
qed (auto intro: D.intros)


34 


35 
theorem D_preservation:


36 
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"


37 
proof (induct arbitrary: A rule: small_step_induct)


38 
case (While b c s)


39 
then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast


40 
moreover


41 
then obtain A'' where "D A' c A''" by (metis D_incr D_mono)


42 
ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"


43 
by (metis D.If[OF `vars b \<subseteq> dom s` D.Semi[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)


44 
thus ?case by (metis D_incr `A = dom s`)


45 
next


46 
case Semi2 thus ?case by auto (metis D_mono D.intros(3))


47 
qed (auto intro: D.intros)


48 


49 
theorem D_sound:


50 
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP


51 
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"


52 
apply(induct arbitrary: A' rule:star_induct)


53 
apply (metis progress)


54 
by (metis D_preservation)


55 


56 
end
