src/HOL/IMP/Def_Ass_Sound_Small.thy
author kleing
Mon, 06 Jun 2011 16:29:38 +0200
changeset 43158 686fa0a0696e
child 44890 22f665a2e91c
permissions -rw-r--r--
imported rest of new IMP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
theory Def_Ass_Sound_Small imports Def_Ass Def_Ass_Small
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
subsection "Soundness wrt Small Steps"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
theorem progress:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
proof (induct c arbitrary: s A')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
  case (If b c1 c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    14
  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
  then show ?case
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    17
qed (fastsimp intro: small_step.intros)+
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
proof (induct c arbitrary: A A' M)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
  case Semi thus ?case by auto (metis D.intros(3))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
  case (If b c1 c2)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
    by auto
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
  with If.hyps `A \<subseteq> A'` obtain M1' M2'
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
    using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastsimp intro: D.intros)+
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
  thus ?case by metis
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
  case While thus ?case by auto (metis D.intros(5) subset_trans)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
qed (auto intro: D.intros)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
theorem D_preservation:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
proof (induct arbitrary: A rule: small_step_induct)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
  case (While b c s)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
  moreover
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
  ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    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)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
  thus ?case by (metis D_incr `A = dom s`)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
next
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
  case Semi2 thus ?case by auto (metis D_mono D.intros(3))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
qed (auto intro: D.intros)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
theorem D_sound:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    52
apply(induct arbitrary: A' rule:star_induct)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
apply (metis progress)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
by (metis D_preservation)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
end