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 (induction 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 (fastforce 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 (induction c arbitrary: A A' M) |
|
21 case Seq 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.IH `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(fastforce 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 (induction 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.Seq[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 Seq2 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(induction arbitrary: A' rule:star_induct) |
|
53 apply (metis progress) |
|
54 by (metis D_preservation) |
|
55 |
|
56 end |
|