author | nipkow |
Mon, 11 Nov 2013 10:23:01 +0100 | |
changeset 54297 | 3fc1b77ef750 |
parent 52825 | 71fef62c4213 |
child 55583 | a0134252ac29 |
permissions | -rw-r--r-- |
52072 | 1 |
theory Fold imports Sem_Equiv Vars begin |
44070 | 2 |
|
44850 | 3 |
subsection "Simple folding of arithmetic expressions" |
44070 | 4 |
|
45134 | 5 |
type_synonym |
45212 | 6 |
tab = "vname \<Rightarrow> val option" |
44070 | 7 |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
8 |
fun afold :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
9 |
"afold (N n) _ = N n" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
10 |
"afold (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
11 |
"afold (Plus e1 e2) t = (case (afold e1 t, afold e2 t) of |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
12 |
(N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')" |
44070 | 13 |
|
14 |
definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)" |
|
15 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
16 |
theorem aval_afold[simp]: |
44070 | 17 |
assumes "approx t s" |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
18 |
shows "aval (afold a t) s = aval a s" |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
19 |
using assms |
44070 | 20 |
by (induct a) (auto simp: approx_def split: aexp.split option.split) |
21 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
22 |
theorem aval_afold_N: |
44070 | 23 |
assumes "approx t s" |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
24 |
shows "afold a t = N n \<Longrightarrow> aval a s = n" |
51573 | 25 |
by (metis assms aval.simps(1) aval_afold) |
44070 | 26 |
|
27 |
definition |
|
28 |
"merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)" |
|
29 |
||
30 |
primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where |
|
31 |
"defs SKIP t = t" | |
|
32 |
"defs (x ::= a) t = |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
33 |
(case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51573
diff
changeset
|
34 |
"defs (c1;;c2) t = (defs c2 o defs c1) t" | |
44070 | 35 |
"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" | |
52072 | 36 |
"defs (WHILE b DO c) t = t |` (-lvars c)" |
44070 | 37 |
|
38 |
primrec fold where |
|
39 |
"fold SKIP _ = SKIP" | |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
40 |
"fold (x ::= a) t = (x ::= (afold a t))" | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51573
diff
changeset
|
41 |
"fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" | |
44070 | 42 |
"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" | |
52072 | 43 |
"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lvars c))" |
44070 | 44 |
|
45 |
lemma approx_merge: |
|
46 |
"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
|
47 |
by (fastforce simp: merge_def approx_def) |
44070 | 48 |
|
49 |
lemma approx_map_le: |
|
50 |
"approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s" |
|
51 |
by (clarsimp simp: approx_def map_le_def dom_def) |
|
52 |
||
53 |
lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t" |
|
54 |
by (clarsimp simp: restrict_map_def map_le_def) |
|
55 |
||
56 |
lemma merge_restrict: |
|
57 |
assumes "t1 |` S = t |` S" |
|
58 |
assumes "t2 |` S = t |` S" |
|
59 |
shows "merge t1 t2 |` S = t |` S" |
|
60 |
proof - |
|
61 |
from assms |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
62 |
have "\<forall>x. (t1 |` S) x = (t |` S) x" |
44070 | 63 |
and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto |
64 |
thus ?thesis |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
65 |
by (auto simp: merge_def restrict_map_def |
51506 | 66 |
split: if_splits) |
44070 | 67 |
qed |
68 |
||
69 |
||
70 |
lemma defs_restrict: |
|
52072 | 71 |
"defs c t |` (- lvars c) = t |` (- lvars c)" |
45015 | 72 |
proof (induction c arbitrary: t) |
47818 | 73 |
case (Seq c1 c2) |
52072 | 74 |
hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" |
44070 | 75 |
by simp |
52072 | 76 |
hence "defs c1 t |` (- lvars c1) |` (-lvars c2) = |
77 |
t |` (- lvars c1) |` (-lvars c2)" by simp |
|
44070 | 78 |
moreover |
47818 | 79 |
from Seq |
52072 | 80 |
have "defs c2 (defs c1 t) |` (- lvars c2) = |
81 |
defs c1 t |` (- lvars c2)" |
|
44070 | 82 |
by simp |
52072 | 83 |
hence "defs c2 (defs c1 t) |` (- lvars c2) |` (- lvars c1) = |
84 |
defs c1 t |` (- lvars c2) |` (- lvars c1)" |
|
44070 | 85 |
by simp |
86 |
ultimately |
|
87 |
show ?case by (clarsimp simp: Int_commute) |
|
88 |
next |
|
89 |
case (If b c1 c2) |
|
52072 | 90 |
hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp |
91 |
hence "defs c1 t |` (- lvars c1) |` (-lvars c2) = |
|
92 |
t |` (- lvars c1) |` (-lvars c2)" by simp |
|
44070 | 93 |
moreover |
94 |
from If |
|
52072 | 95 |
have "defs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp |
96 |
hence "defs c2 t |` (- lvars c2) |` (-lvars c1) = |
|
97 |
t |` (- lvars c2) |` (-lvars c1)" by simp |
|
44070 | 98 |
ultimately |
99 |
show ?case by (auto simp: Int_commute intro: merge_restrict) |
|
100 |
qed (auto split: aexp.split) |
|
101 |
||
102 |
||
103 |
lemma big_step_pres_approx: |
|
104 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'" |
|
45015 | 105 |
proof (induction arbitrary: t rule: big_step_induct) |
44070 | 106 |
case Skip thus ?case by simp |
107 |
next |
|
108 |
case Assign |
|
109 |
thus ?case |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
110 |
by (clarsimp simp: aval_afold_N approx_def split: aexp.split) |
44070 | 111 |
next |
47818 | 112 |
case (Seq c1 s1 s2 c2 s3) |
113 |
have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems]) |
|
114 |
hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2)) |
|
44070 | 115 |
thus ?case by simp |
116 |
next |
|
117 |
case (IfTrue b s c1 s') |
|
118 |
hence "approx (defs c1 t) s'" by simp |
|
119 |
thus ?case by (simp add: approx_merge) |
|
120 |
next |
|
121 |
case (IfFalse b s c2 s') |
|
122 |
hence "approx (defs c2 t) s'" by simp |
|
123 |
thus ?case by (simp add: approx_merge) |
|
124 |
next |
|
125 |
case WhileFalse |
|
126 |
thus ?case by (simp add: approx_def restrict_map_def) |
|
127 |
next |
|
128 |
case (WhileTrue b s1 c s2 s3) |
|
129 |
hence "approx (defs c t) s2" by simp |
|
130 |
with WhileTrue |
|
52072 | 131 |
have "approx (defs c t |` (-lvars c)) s3" by simp |
44070 | 132 |
thus ?case by (simp add: defs_restrict) |
133 |
qed |
|
134 |
||
135 |
||
136 |
lemma big_step_pres_approx_restrict: |
|
52072 | 137 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lvars c)) s \<Longrightarrow> approx (t |` (-lvars c)) s'" |
45015 | 138 |
proof (induction arbitrary: t rule: big_step_induct) |
44070 | 139 |
case Assign |
140 |
thus ?case by (clarsimp simp: approx_def) |
|
141 |
next |
|
47818 | 142 |
case (Seq c1 s1 s2 c2 s3) |
52072 | 143 |
hence "approx (t |` (-lvars c2) |` (-lvars c1)) s1" |
44070 | 144 |
by (simp add: Int_commute) |
52072 | 145 |
hence "approx (t |` (-lvars c2) |` (-lvars c1)) s2" |
47818 | 146 |
by (rule Seq) |
52072 | 147 |
hence "approx (t |` (-lvars c1) |` (-lvars c2)) s2" |
44070 | 148 |
by (simp add: Int_commute) |
52072 | 149 |
hence "approx (t |` (-lvars c1) |` (-lvars c2)) s3" |
47818 | 150 |
by (rule Seq) |
44070 | 151 |
thus ?case by simp |
152 |
next |
|
153 |
case (IfTrue b s c1 s' c2) |
|
52072 | 154 |
hence "approx (t |` (-lvars c2) |` (-lvars c1)) s" |
44070 | 155 |
by (simp add: Int_commute) |
52072 | 156 |
hence "approx (t |` (-lvars c2) |` (-lvars c1)) s'" |
44070 | 157 |
by (rule IfTrue) |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
158 |
thus ?case by (simp add: Int_commute) |
44070 | 159 |
next |
160 |
case (IfFalse b s c2 s' c1) |
|
52072 | 161 |
hence "approx (t |` (-lvars c1) |` (-lvars c2)) s" |
44070 | 162 |
by simp |
52072 | 163 |
hence "approx (t |` (-lvars c1) |` (-lvars c2)) s'" |
44070 | 164 |
by (rule IfFalse) |
165 |
thus ?case by simp |
|
166 |
qed auto |
|
167 |
||
168 |
||
169 |
declare assign_simp [simp] |
|
170 |
||
171 |
lemma approx_eq: |
|
172 |
"approx t \<Turnstile> c \<sim> fold c t" |
|
45015 | 173 |
proof (induction c arbitrary: t) |
44070 | 174 |
case SKIP show ?case by simp |
175 |
next |
|
176 |
case Assign |
|
177 |
show ?case by (simp add: equiv_up_to_def) |
|
178 |
next |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
179 |
case Seq |
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
180 |
thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx) |
44070 | 181 |
next |
182 |
case If |
|
183 |
thus ?case by (auto intro!: equiv_up_to_if_weak) |
|
184 |
next |
|
185 |
case (While b c) |
|
52072 | 186 |
hence "approx (t |` (- lvars c)) \<Turnstile> |
187 |
WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lvars c))" |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
188 |
by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict) |
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
189 |
thus ?case |
44070 | 190 |
by (auto intro: equiv_up_to_weaken approx_map_le) |
191 |
qed |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
192 |
|
44070 | 193 |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
194 |
lemma approx_empty [simp]: |
44070 | 195 |
"approx empty = (\<lambda>_. True)" |
51506 | 196 |
by (auto simp: approx_def) |
44070 | 197 |
|
198 |
||
199 |
theorem constant_folding_equiv: |
|
200 |
"fold c empty \<sim> c" |
|
201 |
using approx_eq [of empty c] |
|
52825 | 202 |
by (simp add: equiv_up_to_True sim_sym) |
44070 | 203 |
|
204 |
||
205 |
||
44850 | 206 |
subsection {* More ambitious folding including boolean expressions *} |
44070 | 207 |
|
208 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
209 |
fun bfold :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
210 |
"bfold (Less a1 a2) t = less (afold a1 t) (afold a2 t)" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
211 |
"bfold (And b1 b2) t = and (bfold b1 t) (bfold b2 t)" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
212 |
"bfold (Not b) t = not(bfold b t)" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
213 |
"bfold (Bc bc) _ = Bc bc" |
44070 | 214 |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
215 |
theorem bval_bfold [simp]: |
44070 | 216 |
assumes "approx t s" |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
217 |
shows "bval (bfold b t) s = bval b s" |
44070 | 218 |
using assms by (induct b) auto |
219 |
||
45200 | 220 |
lemma not_Bc [simp]: "not (Bc v) = Bc (\<not>v)" |
44070 | 221 |
by (cases v) auto |
222 |
||
45200 | 223 |
lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))" |
44070 | 224 |
by (cases b) auto |
225 |
||
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
226 |
lemma and_Bc_eq: |
45200 | 227 |
"(and a b = Bc v) = |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
228 |
(a = Bc False \<and> \<not>v \<or> b = Bc False \<and> \<not>v \<or> |
45200 | 229 |
(\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))" |
44070 | 230 |
by (rule and.induct) auto |
231 |
||
45200 | 232 |
lemma less_Bc_eq [simp]: |
233 |
"(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))" |
|
44070 | 234 |
by (rule less.induct) auto |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
235 |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
236 |
theorem bval_bfold_Bc: |
44070 | 237 |
assumes "approx t s" |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
238 |
shows "bfold b t = Bc v \<Longrightarrow> bval b s = v" |
44070 | 239 |
using assms |
240 |
by (induct b arbitrary: v) |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
241 |
(auto simp: approx_def and_Bc_eq aval_afold_N |
44070 | 242 |
split: bexp.splits bool.splits) |
243 |
||
244 |
||
245 |
primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where |
|
246 |
"bdefs SKIP t = t" | |
|
247 |
"bdefs (x ::= a) t = |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
248 |
(case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51573
diff
changeset
|
249 |
"bdefs (c1;;c2) t = (bdefs c2 o bdefs c1) t" | |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
250 |
"bdefs (IF b THEN c1 ELSE c2) t = (case bfold b t of |
45200 | 251 |
Bc True \<Rightarrow> bdefs c1 t |
252 |
| Bc False \<Rightarrow> bdefs c2 t |
|
44070 | 253 |
| _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" | |
52072 | 254 |
"bdefs (WHILE b DO c) t = t |` (-lvars c)" |
44070 | 255 |
|
256 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
257 |
primrec fold' where |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
258 |
"fold' SKIP _ = SKIP" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
259 |
"fold' (x ::= a) t = (x ::= (afold a t))" | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51573
diff
changeset
|
260 |
"fold' (c1;;c2) t = (fold' c1 t;; fold' c2 (bdefs c1 t))" | |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
261 |
"fold' (IF b THEN c1 ELSE c2) t = (case bfold b t of |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
262 |
Bc True \<Rightarrow> fold' c1 t |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
263 |
| Bc False \<Rightarrow> fold' c2 t |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
264 |
| _ \<Rightarrow> IF bfold b t THEN fold' c1 t ELSE fold' c2 t)" | |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
265 |
"fold' (WHILE b DO c) t = (case bfold b t of |
45200 | 266 |
Bc False \<Rightarrow> SKIP |
52072 | 267 |
| _ \<Rightarrow> WHILE bfold b (t |` (-lvars c)) DO fold' c (t |` (-lvars c)))" |
44070 | 268 |
|
269 |
||
270 |
lemma bdefs_restrict: |
|
52072 | 271 |
"bdefs c t |` (- lvars c) = t |` (- lvars c)" |
45015 | 272 |
proof (induction c arbitrary: t) |
47818 | 273 |
case (Seq c1 c2) |
52072 | 274 |
hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)" |
44070 | 275 |
by simp |
52072 | 276 |
hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) = |
277 |
t |` (- lvars c1) |` (-lvars c2)" by simp |
|
44070 | 278 |
moreover |
47818 | 279 |
from Seq |
52072 | 280 |
have "bdefs c2 (bdefs c1 t) |` (- lvars c2) = |
281 |
bdefs c1 t |` (- lvars c2)" |
|
44070 | 282 |
by simp |
52072 | 283 |
hence "bdefs c2 (bdefs c1 t) |` (- lvars c2) |` (- lvars c1) = |
284 |
bdefs c1 t |` (- lvars c2) |` (- lvars c1)" |
|
44070 | 285 |
by simp |
286 |
ultimately |
|
287 |
show ?case by (clarsimp simp: Int_commute) |
|
288 |
next |
|
289 |
case (If b c1 c2) |
|
52072 | 290 |
hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp |
291 |
hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) = |
|
292 |
t |` (- lvars c1) |` (-lvars c2)" by simp |
|
44070 | 293 |
moreover |
294 |
from If |
|
52072 | 295 |
have "bdefs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp |
296 |
hence "bdefs c2 t |` (- lvars c2) |` (-lvars c1) = |
|
297 |
t |` (- lvars c2) |` (-lvars c1)" by simp |
|
44070 | 298 |
ultimately |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
299 |
show ?case |
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
300 |
by (auto simp: Int_commute intro: merge_restrict |
44070 | 301 |
split: bexp.splits bool.splits) |
302 |
qed (auto split: aexp.split bexp.split bool.split) |
|
303 |
||
304 |
||
305 |
lemma big_step_pres_approx_b: |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
306 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" |
45015 | 307 |
proof (induction arbitrary: t rule: big_step_induct) |
44070 | 308 |
case Skip thus ?case by simp |
309 |
next |
|
310 |
case Assign |
|
311 |
thus ?case |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
312 |
by (clarsimp simp: aval_afold_N approx_def split: aexp.split) |
44070 | 313 |
next |
47818 | 314 |
case (Seq c1 s1 s2 c2 s3) |
315 |
have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems]) |
|
316 |
hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2)) |
|
44070 | 317 |
thus ?case by simp |
318 |
next |
|
319 |
case (IfTrue b s c1 s') |
|
320 |
hence "approx (bdefs c1 t) s'" by simp |
|
321 |
thus ?case using `bval b s` `approx t s` |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
322 |
by (clarsimp simp: approx_merge bval_bfold_Bc |
44070 | 323 |
split: bexp.splits bool.splits) |
324 |
next |
|
325 |
case (IfFalse b s c2 s') |
|
326 |
hence "approx (bdefs c2 t) s'" by simp |
|
327 |
thus ?case using `\<not>bval b s` `approx t s` |
|
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
328 |
by (clarsimp simp: approx_merge bval_bfold_Bc |
44070 | 329 |
split: bexp.splits bool.splits) |
330 |
next |
|
331 |
case WhileFalse |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
332 |
thus ?case |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
333 |
by (clarsimp simp: bval_bfold_Bc approx_def restrict_map_def |
44070 | 334 |
split: bexp.splits bool.splits) |
335 |
next |
|
336 |
case (WhileTrue b s1 c s2 s3) |
|
337 |
hence "approx (bdefs c t) s2" by simp |
|
338 |
with WhileTrue |
|
52072 | 339 |
have "approx (bdefs c t |` (- lvars c)) s3" |
44070 | 340 |
by simp |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
341 |
thus ?case |
44070 | 342 |
by (simp add: bdefs_restrict) |
343 |
qed |
|
344 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
345 |
lemma fold'_equiv: |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
346 |
"approx t \<Turnstile> c \<sim> fold' c t" |
45015 | 347 |
proof (induction c arbitrary: t) |
44070 | 348 |
case SKIP show ?case by simp |
349 |
next |
|
350 |
case Assign |
|
351 |
thus ?case by (simp add: equiv_up_to_def) |
|
352 |
next |
|
47818 | 353 |
case Seq |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
354 |
thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx_b) |
44070 | 355 |
next |
356 |
case (If b c1 c2) |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
357 |
hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
358 |
IF bfold b t THEN fold' c1 t ELSE fold' c2 t" |
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
359 |
by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) |
44070 | 360 |
thus ?case using If |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
361 |
by (fastforce simp: bval_bfold_Bc split: bexp.splits bool.splits |
44070 | 362 |
intro: equiv_up_to_trans) |
363 |
next |
|
364 |
case (While b c) |
|
52072 | 365 |
hence "approx (t |` (- lvars c)) \<Turnstile> |
44070 | 366 |
WHILE b DO c \<sim> |
52072 | 367 |
WHILE bfold b (t |` (- lvars c)) |
368 |
DO fold' c (t |` (- lvars c))" (is "_ \<Turnstile> ?W \<sim> ?W'") |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
369 |
by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict |
44070 | 370 |
simp: bequiv_up_to_def) |
371 |
hence "approx t \<Turnstile> ?W \<sim> ?W'" |
|
372 |
by (auto intro: equiv_up_to_weaken approx_map_le) |
|
373 |
thus ?case |
|
48909
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
374 |
by (auto split: bexp.splits bool.splits |
b2dea007e55e
remove Hoare dependency from Fold.thy
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
47818
diff
changeset
|
375 |
intro: equiv_up_to_while_False |
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
376 |
simp: bval_bfold_Bc) |
44070 | 377 |
qed |
378 |
||
379 |
||
51514
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
380 |
theorem constant_folding_equiv': |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
381 |
"fold' c empty \<sim> c" |
9bed72e55475
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
kleing
parents:
51506
diff
changeset
|
382 |
using fold'_equiv [of empty c] |
52825 | 383 |
by (simp add: equiv_up_to_True sim_sym) |
44070 | 384 |
|
385 |
||
386 |
end |