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