author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45015  fdac1e9880eb 
child 47818  151d137f1095 
permissions  rwrr 
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'" 

45015  10 
proof (induction c arbitrary: s A') 
43158  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) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43158
diff
changeset

17 
qed (fastforce intro: small_step.intros)+ 
43158  18 

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

45015  20 
proof (induction c arbitrary: A A' M) 
43158  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 

45015  26 
with If.IH `A \<subseteq> A'` obtain M1' M2' 
43158  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'" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
43158
diff
changeset

29 
using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+ 
43158  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'" 

45015  37 
proof (induction arbitrary: A rule: small_step_induct) 
43158  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''" 

45015  52 
apply(induction arbitrary: A' rule:star_induct) 
43158  53 
apply (metis progress) 
54 
by (metis D_preservation) 

55 

56 
end 