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