src/HOL/IMP/Fold.thy
author nipkow
Tue, 20 Sep 2011 05:48:23 +0200
changeset 45015 fdac1e9880eb
parent 44890 22f665a2e91c
child 45134 9b02f6665fc8
permissions -rw-r--r--
Updated IMP to use new induction method
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     1
header "Constant Folding"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     2
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     3
theory Fold imports Sem_Equiv begin
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     4
44850
a6095c96a89b tuned headers
nipkow
parents: 44070
diff changeset
     5
subsection "Simple folding of arithmetic expressions"
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     6
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     7
types
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     8
  tab = "name \<Rightarrow> val option"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
     9
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    10
(* maybe better as the composition of substitution and the existing simp_const(0) *)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    11
fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    12
"simp_const (N n) _ = N n" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    13
"simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    14
"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    15
  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    16
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    17
definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    18
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    19
theorem aval_simp_const[simp]:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    20
assumes "approx t s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    21
shows "aval (simp_const a t) s = aval a s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    22
  using assms 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    23
  by (induct a) (auto simp: approx_def split: aexp.split option.split)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    24
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    25
theorem aval_simp_const_N:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    26
assumes "approx t s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    27
shows "simp_const a t = N n \<Longrightarrow> aval a s = n"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    28
  using assms
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    29
  by (induct a arbitrary: n)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    30
     (auto simp: approx_def split: aexp.splits option.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    31
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    32
definition
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    33
  "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    34
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    35
primrec lnames :: "com \<Rightarrow> name set" where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    36
"lnames SKIP = {}" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    37
"lnames (x ::= a) = {x}" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    38
"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    39
"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    40
"lnames (WHILE b DO c) = lnames c"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    41
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    42
primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    43
"defs SKIP t = t" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    44
"defs (x ::= a) t =
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    45
  (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    46
"defs (c1;c2) t = (defs c2 o defs c1) t" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    47
"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    48
"defs (WHILE b DO c) t = t |` (-lnames c)" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    49
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    50
primrec fold where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    51
"fold SKIP _ = SKIP" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    52
"fold (x ::= a) t = (x ::= (simp_const a t))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    53
"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    54
"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    55
"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    56
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    57
lemma approx_merge:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    58
  "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44850
diff changeset
    59
  by (fastforce simp: merge_def approx_def)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    60
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    61
lemma approx_map_le:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    62
  "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    63
  by (clarsimp simp: approx_def map_le_def dom_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    64
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    65
lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    66
  by (clarsimp simp: restrict_map_def map_le_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    67
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    68
lemma merge_restrict:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    69
  assumes "t1 |` S = t |` S"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    70
  assumes "t2 |` S = t |` S"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    71
  shows "merge t1 t2 |` S = t |` S"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    72
proof -
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    73
  from assms
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    74
  have "\<forall>x. (t1 |` S) x = (t |` S) x" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    75
   and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    76
  thus ?thesis
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    77
    by (auto simp: merge_def restrict_map_def 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    78
             split: if_splits intro: ext)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    79
qed
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    80
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    81
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    82
lemma defs_restrict:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    83
  "defs c t |` (- lnames c) = t |` (- lnames c)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
    84
proof (induction c arbitrary: t)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    85
  case (Semi c1 c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    86
  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    87
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    88
  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    89
         t |` (- lnames c1) |` (-lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    90
  moreover
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    91
  from Semi
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    92
  have "defs c2 (defs c1 t) |` (- lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    93
        defs c1 t |` (- lnames c2)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    94
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    95
  hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    96
         defs c1 t |` (- lnames c2) |` (- lnames c1)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    97
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    98
  ultimately
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
    99
  show ?case by (clarsimp simp: Int_commute)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   100
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   101
  case (If b c1 c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   102
  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   103
  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   104
         t |` (- lnames c1) |` (-lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   105
  moreover
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   106
  from If
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   107
  have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   108
  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   109
         t |` (- lnames c2) |` (-lnames c1)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   110
  ultimately
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   111
  show ?case by (auto simp: Int_commute intro: merge_restrict)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   112
qed (auto split: aexp.split)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   113
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   114
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   115
lemma big_step_pres_approx:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   116
  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   117
proof (induction arbitrary: t rule: big_step_induct)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   118
  case Skip thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   119
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   120
  case Assign
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   121
  thus ?case
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   122
    by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   123
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   124
  case (Semi c1 s1 s2 c2 s3)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   125
  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   126
  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   127
  thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   128
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   129
  case (IfTrue b s c1 s')
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   130
  hence "approx (defs c1 t) s'" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   131
  thus ?case by (simp add: approx_merge)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   132
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   133
  case (IfFalse b s c2 s')
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   134
  hence "approx (defs c2 t) s'" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   135
  thus ?case by (simp add: approx_merge)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   136
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   137
  case WhileFalse
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   138
  thus ?case by (simp add: approx_def restrict_map_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   139
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   140
  case (WhileTrue b s1 c s2 s3)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   141
  hence "approx (defs c t) s2" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   142
  with WhileTrue
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   143
  have "approx (defs c t |` (-lnames c)) s3" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   144
  thus ?case by (simp add: defs_restrict)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   145
qed
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   146
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   147
corollary approx_defs_inv [simp]:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   148
  "\<Turnstile> {approx t} c {approx (defs c t)}"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   149
  by (simp add: hoare_valid_def big_step_pres_approx)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   150
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   151
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   152
lemma big_step_pres_approx_restrict:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   153
  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   154
proof (induction arbitrary: t rule: big_step_induct)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   155
  case Assign
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   156
  thus ?case by (clarsimp simp: approx_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   157
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   158
  case (Semi c1 s1 s2 c2 s3)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   159
  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   160
    by (simp add: Int_commute)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   161
  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   162
    by (rule Semi)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   163
  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   164
    by (simp add: Int_commute)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   165
  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   166
    by (rule Semi)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   167
  thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   168
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   169
  case (IfTrue b s c1 s' c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   170
  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   171
    by (simp add: Int_commute)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   172
  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   173
    by (rule IfTrue)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   174
  thus ?case by (simp add: Int_commute) 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   175
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   176
  case (IfFalse b s c2 s' c1)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   177
  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   178
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   179
  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   180
    by (rule IfFalse)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   181
  thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   182
qed auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   183
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   184
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   185
lemma approx_restrict_inv:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   186
  "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   187
  by (simp add: hoare_valid_def big_step_pres_approx_restrict)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   188
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   189
declare assign_simp [simp]
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   190
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   191
lemma approx_eq:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   192
  "approx t \<Turnstile> c \<sim> fold c t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   193
proof (induction c arbitrary: t)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   194
  case SKIP show ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   195
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   196
  case Assign
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   197
  show ?case by (simp add: equiv_up_to_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   198
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   199
  case Semi 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   200
  thus ?case by (auto intro!: equiv_up_to_semi)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   201
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   202
  case If
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   203
  thus ?case by (auto intro!: equiv_up_to_if_weak)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   204
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   205
  case (While b c)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   206
  hence "approx (t |` (- lnames c)) \<Turnstile> 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   207
         WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   208
    by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   209
  thus ?case 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   210
    by (auto intro: equiv_up_to_weaken approx_map_le)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   211
qed
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   212
  
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   213
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   214
lemma approx_empty [simp]: 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   215
  "approx empty = (\<lambda>_. True)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   216
  by (auto intro!: ext simp: approx_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   217
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   218
lemma equiv_sym:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   219
  "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   220
  by (auto simp add: equiv_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   221
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   222
theorem constant_folding_equiv:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   223
  "fold c empty \<sim> c"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   224
  using approx_eq [of empty c]
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   225
  by (simp add: equiv_up_to_True equiv_sym)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   226
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   227
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   228
44850
a6095c96a89b tuned headers
nipkow
parents: 44070
diff changeset
   229
subsection {* More ambitious folding including boolean expressions *}
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   230
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   231
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   232
fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   233
"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   234
"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   235
"bsimp_const (Not b) t = not(bsimp_const b t)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   236
"bsimp_const (B bv) _ = B bv"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   237
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   238
theorem bvalsimp_const [simp]:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   239
  assumes "approx t s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   240
  shows "bval (bsimp_const b t) s = bval b s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   241
  using assms by (induct b) auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   242
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   243
lemma not_B [simp]: "not (B v) = B (\<not>v)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   244
  by (cases v) auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   245
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   246
lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   247
  by (cases b) auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   248
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   249
lemma and_B_eq: 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   250
  "(and a b = B v) = (a = B False \<and> \<not>v \<or> 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   251
                      b = B False \<and> \<not>v \<or> 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   252
                      (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   253
  by (rule and.induct) auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   254
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   255
lemma less_B_eq [simp]:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   256
  "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   257
  by (rule less.induct) auto
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   258
    
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   259
theorem bvalsimp_const_B:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   260
assumes "approx t s"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   261
shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   262
  using assms
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   263
  by (induct b arbitrary: v)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   264
     (auto simp: approx_def and_B_eq aval_simp_const_N 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   265
           split: bexp.splits bool.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   266
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   267
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   268
primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   269
"bdefs SKIP t = t" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   270
"bdefs (x ::= a) t =
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   271
  (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   272
"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   273
"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   274
    B True \<Rightarrow> bdefs c1 t
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   275
  | B False \<Rightarrow> bdefs c2 t
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   276
  | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   277
"bdefs (WHILE b DO c) t = t |` (-lnames c)" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   278
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   279
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   280
primrec bfold where
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   281
"bfold SKIP _ = SKIP" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   282
"bfold (x ::= a) t = (x ::= (simp_const a t))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   283
"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   284
"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   285
    B True \<Rightarrow> bfold c1 t
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   286
  | B False \<Rightarrow> bfold c2 t
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   287
  | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   288
"bfold (WHILE b DO c) t = (case bsimp_const b t of
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   289
    B False \<Rightarrow> SKIP
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   290
  | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   291
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   292
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   293
lemma bdefs_restrict:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   294
  "bdefs c t |` (- lnames c) = t |` (- lnames c)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   295
proof (induction c arbitrary: t)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   296
  case (Semi c1 c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   297
  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   298
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   299
  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   300
         t |` (- lnames c1) |` (-lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   301
  moreover
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   302
  from Semi
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   303
  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   304
        bdefs c1 t |` (- lnames c2)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   305
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   306
  hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   307
         bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   308
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   309
  ultimately
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   310
  show ?case by (clarsimp simp: Int_commute)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   311
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   312
  case (If b c1 c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   313
  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   314
  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   315
         t |` (- lnames c1) |` (-lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   316
  moreover
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   317
  from If
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   318
  have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   319
  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) = 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   320
         t |` (- lnames c2) |` (-lnames c1)" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   321
  ultimately
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   322
  show ?case 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   323
    by (auto simp: Int_commute intro: merge_restrict 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   324
             split: bexp.splits bool.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   325
qed (auto split: aexp.split bexp.split bool.split)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   326
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   327
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   328
lemma big_step_pres_approx_b:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   329
  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   330
proof (induction arbitrary: t rule: big_step_induct)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   331
  case Skip thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   332
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   333
  case Assign
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   334
  thus ?case
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   335
    by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   336
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   337
  case (Semi c1 s1 s2 c2 s3)
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   338
  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   339
  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   340
  thus ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   341
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   342
  case (IfTrue b s c1 s')
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   343
  hence "approx (bdefs c1 t) s'" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   344
  thus ?case using `bval b s` `approx t s`
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   345
    by (clarsimp simp: approx_merge bvalsimp_const_B 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   346
                 split: bexp.splits bool.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   347
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   348
  case (IfFalse b s c2 s')
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   349
  hence "approx (bdefs c2 t) s'" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   350
  thus ?case using `\<not>bval b s` `approx t s`
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   351
    by (clarsimp simp: approx_merge bvalsimp_const_B 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   352
                 split: bexp.splits bool.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   353
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   354
  case WhileFalse
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   355
  thus ?case 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   356
    by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   357
                 split: bexp.splits bool.splits)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   358
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   359
  case (WhileTrue b s1 c s2 s3)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   360
  hence "approx (bdefs c t) s2" by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   361
  with WhileTrue
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   362
  have "approx (bdefs c t |` (- lnames c)) s3"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   363
    by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   364
  thus ?case 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   365
    by (simp add: bdefs_restrict)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   366
qed
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   367
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   368
corollary approx_bdefs_inv [simp]:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   369
  "\<Turnstile> {approx t} c {approx (bdefs c t)}"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   370
  by (simp add: hoare_valid_def big_step_pres_approx_b)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   371
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   372
lemma bfold_equiv: 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   373
  "approx t \<Turnstile> c \<sim> bfold c t"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44890
diff changeset
   374
proof (induction c arbitrary: t)
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   375
  case SKIP show ?case by simp
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   376
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   377
  case Assign
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   378
  thus ?case by (simp add: equiv_up_to_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   379
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   380
  case Semi
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   381
  thus ?case by (auto intro!: equiv_up_to_semi)           
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   382
next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   383
  case (If b c1 c2)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   384
  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   385
                   IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   386
    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   387
  thus ?case using If
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44850
diff changeset
   388
    by (fastforce simp: bvalsimp_const_B split: bexp.splits bool.splits 
44070
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   389
                 intro: equiv_up_to_trans)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   390
  next
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   391
  case (While b c)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   392
  hence "approx (t |` (- lnames c)) \<Turnstile> 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   393
                   WHILE b DO c \<sim>
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   394
                   WHILE bsimp_const b (t |` (- lnames c)) 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   395
                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'") 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   396
    by (auto intro: equiv_up_to_while_weak approx_restrict_inv 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   397
             simp: bequiv_up_to_def)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   398
  hence "approx t \<Turnstile> ?W \<sim> ?W'"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   399
    by (auto intro: equiv_up_to_weaken approx_map_le)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   400
  thus ?case
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   401
    by (auto split: bexp.splits bool.splits 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   402
             intro: equiv_up_to_while_False 
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   403
             simp: bvalsimp_const_B)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   404
qed
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   405
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   406
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   407
theorem constant_bfolding_equiv:
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   408
  "bfold c empty \<sim> c"
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   409
  using bfold_equiv [of empty c]
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   410
  by (simp add: equiv_up_to_True equiv_sym)
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   411
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   412
cebb7abb54b1 import constant folding theory into IMP
kleing
parents:
diff changeset
   413
end