src/HOL/IMP/Def_Init_Sound_Small.thy
author kleing
Thu May 23 11:39:40 2013 +1000 (2013-05-23)
changeset 52120 e6433b34364b
parent 52046 bc01725d7918
permissions -rw-r--r--
slightly clearer formulation
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
nipkow@50161
     3
theory Def_Init_Sound_Small
nipkow@50161
     4
imports Def_Init Def_Init_Small
kleing@43158
     5
begin
kleing@43158
     6
kleing@43158
     7
subsection "Soundness wrt Small Steps"
kleing@43158
     8
kleing@43158
     9
theorem progress:
kleing@43158
    10
  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
nipkow@45015
    11
proof (induction c arbitrary: s A')
kleing@43158
    12
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
kleing@43158
    13
next
kleing@43158
    14
  case (If b c1 c2)
kleing@43158
    15
  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
kleing@43158
    16
  then show ?case
kleing@43158
    17
    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
nipkow@44890
    18
qed (fastforce intro: small_step.intros)+
kleing@43158
    19
kleing@43158
    20
lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
nipkow@45015
    21
proof (induction c arbitrary: A A' M)
nipkow@47818
    22
  case Seq thus ?case by auto (metis D.intros(3))
kleing@43158
    23
next
kleing@43158
    24
  case (If b c1 c2)
kleing@43158
    25
  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
kleing@43158
    26
    by auto
nipkow@45015
    27
  with If.IH `A \<subseteq> A'` obtain M1' M2'
kleing@43158
    28
    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
kleing@43158
    29
  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
nipkow@44890
    30
    using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
kleing@43158
    31
  thus ?case by metis
kleing@43158
    32
next
kleing@43158
    33
  case While thus ?case by auto (metis D.intros(5) subset_trans)
kleing@43158
    34
qed (auto intro: D.intros)
kleing@43158
    35
kleing@43158
    36
theorem D_preservation:
kleing@43158
    37
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
nipkow@45015
    38
proof (induction arbitrary: A rule: small_step_induct)
kleing@43158
    39
  case (While b c s)
kleing@43158
    40
  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
kleing@43158
    41
  moreover
kleing@43158
    42
  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
nipkow@52046
    43
  ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
nipkow@47818
    44
    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)
kleing@43158
    45
  thus ?case by (metis D_incr `A = dom s`)
kleing@43158
    46
next
nipkow@47818
    47
  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
kleing@43158
    48
qed (auto intro: D.intros)
kleing@43158
    49
kleing@43158
    50
theorem D_sound:
kleing@51466
    51
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
kleing@52120
    52
   \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
nipkow@45015
    53
apply(induction arbitrary: A' rule:star_induct)
kleing@43158
    54
apply (metis progress)
kleing@43158
    55
by (metis D_preservation)
kleing@43158
    56
kleing@43158
    57
end