src/HOL/IMP/Def_Init_Small.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 53015 a1119cf551e8
child 63540 f8652d0534fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
nipkow@50161
     3
theory Def_Init_Small
nipkow@52726
     4
imports Star Def_Init_Exp Def_Init
kleing@43158
     5
begin
kleing@43158
     6
kleing@43158
     7
subsection "Initialization-Sensitive Small Step Semantics"
kleing@43158
     8
kleing@43158
     9
inductive
kleing@43158
    10
  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
kleing@43158
    11
where
kleing@43158
    12
Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
kleing@43158
    13
nipkow@52046
    14
Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
wenzelm@53015
    15
Seq2:   "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1';;c\<^sub>2,s')" |
kleing@43158
    16
wenzelm@53015
    17
IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" |
wenzelm@53015
    18
IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |
kleing@43158
    19
nipkow@52046
    20
While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
kleing@43158
    21
kleing@43158
    22
lemmas small_step_induct = small_step.induct[split_format(complete)]
kleing@43158
    23
kleing@43158
    24
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
kleing@43158
    25
where "x \<rightarrow>* y == star small_step x y"
kleing@43158
    26
nipkow@52726
    27
nipkow@52726
    28
subsection "Soundness wrt Small Steps"
nipkow@52726
    29
nipkow@52726
    30
theorem progress:
nipkow@52726
    31
  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
nipkow@52726
    32
proof (induction c arbitrary: s A')
nipkow@52726
    33
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
nipkow@52726
    34
next
nipkow@52726
    35
  case (If b c1 c2)
nipkow@52726
    36
  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
nipkow@52726
    37
  then show ?case
nipkow@52726
    38
    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
nipkow@52726
    39
qed (fastforce intro: small_step.intros)+
nipkow@52726
    40
nipkow@52726
    41
lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
nipkow@52726
    42
proof (induction c arbitrary: A A' M)
nipkow@52726
    43
  case Seq thus ?case by auto (metis D.intros(3))
nipkow@52726
    44
next
nipkow@52726
    45
  case (If b c1 c2)
nipkow@52726
    46
  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
nipkow@52726
    47
    by auto
nipkow@52726
    48
  with If.IH `A \<subseteq> A'` obtain M1' M2'
nipkow@52726
    49
    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
nipkow@52726
    50
  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
nipkow@52726
    51
    using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
nipkow@52726
    52
  thus ?case by metis
nipkow@52726
    53
next
nipkow@52726
    54
  case While thus ?case by auto (metis D.intros(5) subset_trans)
nipkow@52726
    55
qed (auto intro: D.intros)
nipkow@52726
    56
nipkow@52726
    57
theorem D_preservation:
nipkow@52726
    58
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
nipkow@52726
    59
proof (induction arbitrary: A rule: small_step_induct)
nipkow@52726
    60
  case (While b c s)
nipkow@52726
    61
  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
nipkow@52726
    62
  moreover
nipkow@52726
    63
  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
nipkow@52726
    64
  ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
nipkow@52726
    65
    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)
nipkow@52726
    66
  thus ?case by (metis D_incr `A = dom s`)
nipkow@52726
    67
next
nipkow@52726
    68
  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
nipkow@52726
    69
qed (auto intro: D.intros)
nipkow@52726
    70
nipkow@52726
    71
theorem D_sound:
nipkow@52726
    72
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
nipkow@52726
    73
   \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
nipkow@52726
    74
apply(induction arbitrary: A' rule:star_induct)
nipkow@52726
    75
apply (metis progress)
nipkow@52726
    76
by (metis D_preservation)
nipkow@52726
    77
kleing@43158
    78
end