src/HOL/IMP/Def_Ass_Sound_Small.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45015 fdac1e9880eb child 47818 151d137f1095 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
```     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 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.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.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(induction arbitrary: A' rule:star_induct)
```
```    53 apply (metis progress)
```
```    54 by (metis D_preservation)
```
```    55
```
```    56 end
```