1 theory BlexerSimp |
1 theory BlexerSimp |
2 imports Blexer |
2 imports Blexer |
3 begin |
3 begin |
4 |
4 |
|
5 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list" |
|
6 where |
|
7 "distinctWith [] eq acc = []" |
|
8 | "distinctWith (x # xs) eq acc = |
|
9 (if (\<exists> y \<in> acc. eq x y) then distinctWith xs eq acc |
|
10 else x # (distinctWith xs eq ({x} \<union> acc)))" |
|
11 |
|
12 |
|
13 fun eq1 ("_ ~1 _" [80, 80] 80) where |
|
14 "AZERO ~1 AZERO = True" |
|
15 | "(AONE bs1) ~1 (AONE bs2) = True" |
|
16 | "(ACHAR bs1 c) ~1 (ACHAR bs2 d) = (if c = d then True else False)" |
|
17 | "(ASEQ bs1 ra1 ra2) ~1 (ASEQ bs2 rb1 rb2) = (ra1 ~1 rb1 \<and> ra2 ~1 rb2)" |
|
18 | "(AALTs bs1 []) ~1 (AALTs bs2 []) = True" |
|
19 | "(AALTs bs1 (r1 # rs1)) ~1 (AALTs bs2 (r2 # rs2)) = (r1 ~1 r2 \<and> (AALTs bs1 rs1) ~1 (AALTs bs2 rs2))" |
|
20 | "(ASTAR bs1 r1) ~1 (ASTAR bs2 r2) = r1 ~1 r2" |
|
21 | "(ANTIMES bs1 r1 n1) ~1 (ANTIMES bs2 r2 n2) = (r1 ~1 r2 \<and> n1 = n2)" |
|
22 | "_ ~1 _ = False" |
|
23 |
|
24 |
|
25 |
|
26 lemma eq1_L: |
|
27 assumes "x ~1 y" |
|
28 shows "L (erase x) = L (erase y)" |
|
29 using assms |
|
30 apply(induct rule: eq1.induct) |
|
31 apply(auto elim: eq1.elims) |
|
32 apply presburger |
|
33 done |
5 |
34 |
6 fun flts :: "arexp list \<Rightarrow> arexp list" |
35 fun flts :: "arexp list \<Rightarrow> arexp list" |
7 where |
36 where |
8 "flts [] = []" |
37 "flts [] = []" |
9 | "flts (AZERO # rs) = flts rs" |
38 | "flts (AZERO # rs) = flts rs" |
40 where |
69 where |
41 "bsimp_AALTs _ [] = AZERO" |
70 "bsimp_AALTs _ [] = AZERO" |
42 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
71 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
43 | "bsimp_AALTs bs1 rs = AALTs bs1 rs" |
72 | "bsimp_AALTs bs1 rs = AALTs bs1 rs" |
44 |
73 |
|
74 |
|
75 |
|
76 |
|
77 fun bsimp :: "arexp \<Rightarrow> arexp" |
|
78 where |
|
79 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
80 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) " |
|
81 | "bsimp r = r" |
|
82 |
|
83 |
|
84 fun |
|
85 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
86 where |
|
87 "bders_simp r [] = r" |
|
88 | "bders_simp r (c # s) = bders_simp (bsimp (bder c r)) s" |
|
89 |
|
90 definition blexer_simp where |
|
91 "blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then |
|
92 decode (bmkeps (bders_simp (intern r) s)) r else None" |
|
93 |
|
94 |
|
95 |
|
96 lemma bders_simp_append: |
|
97 shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2" |
|
98 apply(induct s1 arbitrary: r s2) |
|
99 apply(simp_all) |
|
100 done |
|
101 |
45 lemma bmkeps_fuse: |
102 lemma bmkeps_fuse: |
46 assumes "bnullable r" |
103 assumes "bnullable r" |
47 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
104 shows "bmkeps (fuse bs r) = bs @ bmkeps r" |
48 using assms |
105 using assms |
49 by (induct r rule: bnullable.induct) (auto) |
106 apply(induct r rule: bnullable.induct) |
|
107 apply(auto) |
|
108 apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
109 done |
50 |
110 |
51 lemma bmkepss_fuse: |
111 lemma bmkepss_fuse: |
52 assumes "bnullables rs" |
112 assumes "bnullables rs" |
53 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
113 shows "bmkepss (map (fuse bs) rs) = bs @ bmkepss rs" |
54 using assms |
114 using assms |
60 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
120 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
61 apply(induct a arbitrary: bs c) |
121 apply(induct a arbitrary: bs c) |
62 apply(simp_all) |
122 apply(simp_all) |
63 done |
123 done |
64 |
124 |
65 |
|
66 |
|
67 |
|
68 fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where |
|
69 "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c" |
|
70 |
|
71 fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and |
|
72 turnIntoTerms :: "rexp \<Rightarrow> rexp list " |
|
73 where |
|
74 "furtherSEQ ONE r2 = turnIntoTerms r2 " |
|
75 | "furtherSEQ r11 r2 = [SEQ r11 r2]" |
|
76 | "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" |
|
77 | "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))" |
|
78 | "turnIntoTerms r = [r]" |
|
79 |
|
80 abbreviation "tint \<equiv> turnIntoTerms" |
|
81 |
|
82 fun seqFold :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where |
|
83 "seqFold acc [] = acc" |
|
84 | "seqFold ONE (r # rs1) = seqFold r rs1" |
|
85 | "seqFold acc (r # rs1) = seqFold (SEQ acc r) rs1" |
|
86 |
|
87 |
|
88 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where |
|
89 "attachCtx r ctx = set (turnIntoTerms (seqFold (erase r) ctx))" |
|
90 |
|
91 |
|
92 fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where |
|
93 "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)" |
|
94 |
|
95 |
|
96 fun notZero :: "arexp \<Rightarrow> bool" where |
|
97 "notZero AZERO = True" |
|
98 | "notZero _ = False" |
|
99 |
|
100 |
|
101 fun tset :: "arexp list \<Rightarrow> rexp set" where |
|
102 "tset rs = set (concat (map turnIntoTerms (map erase rs)))" |
|
103 |
|
104 |
|
105 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
|
106 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
|
107 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
|
108 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0)) |
|
109 | r \<Rightarrow> r |
|
110 ) |
|
111 ) |
|
112 " |
|
113 |
|
114 abbreviation |
|
115 "p6 acc r \<equiv> prune6 (tset acc) r Nil" |
|
116 |
|
117 |
|
118 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
|
119 "dB6 [] acc = []" |
|
120 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
|
121 else (let pruned = prune6 acc a [] in |
|
122 (case pruned of |
|
123 AZERO \<Rightarrow> dB6 as acc |
|
124 |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) " |
|
125 |
|
126 |
|
127 fun bsimpStrong6 :: "arexp \<Rightarrow> arexp" |
|
128 where |
|
129 "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" |
|
130 | "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) " |
|
131 | "bsimpStrong6 r = r" |
|
132 |
|
133 |
|
134 fun |
|
135 bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
136 where |
|
137 "bdersStrong6 r [] = r" |
|
138 | "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s" |
|
139 |
|
140 definition blexerStrong where |
|
141 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
|
142 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
|
143 |
125 |
144 |
126 |
145 |
127 |
146 inductive |
128 inductive |
147 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
129 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
225 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
207 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto>* (rs @ rs2)" |
226 apply(induct rs1 rs2 rule: srewrites.induct) |
208 apply(induct rs1 rs2 rule: srewrites.induct) |
227 apply(auto) |
209 apply(auto) |
228 using srewrite1 by blast |
210 using srewrite1 by blast |
229 |
211 |
230 lemma srewrites_prepend: |
|
231 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (r # rs1) s\<leadsto>* (r # rs2)" |
|
232 by (metis append_Cons append_Nil srewrites1) |
|
233 |
|
234 lemma srewrite2: |
212 lemma srewrite2: |
235 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
213 shows "r1 \<leadsto> r2 \<Longrightarrow> True" |
236 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
214 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
237 apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts) |
215 apply(induct rule: rrewrite_srewrite.inducts) |
238 apply simp+ |
216 apply(auto) |
239 using srewrites_prepend apply force |
217 apply (metis append_Cons append_Nil srewrites1) |
240 apply (simp add: rs_in_rstar ss3) |
218 apply(meson srewrites.simps ss3) |
241 using ss4 apply force |
219 apply (meson srewrites.simps ss4) |
242 using rs_in_rstar ss5 apply auto[1] |
220 apply (meson srewrites.simps ss5) |
243 using rs_in_rstar ss6 apply auto[1] |
221 by (metis append_Cons append_Nil srewrites.simps ss6) |
244 using rs_in_rstar ss7 by force |
222 |
245 |
|
246 |
|
247 |
|
248 |
223 |
249 lemma srewrites3: |
224 lemma srewrites3: |
250 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
225 shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)" |
251 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
226 apply(induct rs1 rs2 arbitrary: rs rule: srewrites.induct) |
252 apply(auto) |
227 apply(auto) |
253 by (meson srewrite2(2) srewrites_trans) |
228 by (meson srewrite2(2) srewrites_trans) |
254 |
229 |
|
230 (* |
|
231 lemma srewrites4: |
|
232 assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" |
|
233 shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)" |
|
234 using assms |
|
235 apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct) |
|
236 apply (simp add: srewrites3) |
|
237 using srewrite1 by blast |
|
238 *) |
255 |
239 |
256 lemma srewrites6: |
240 lemma srewrites6: |
257 assumes "r1 \<leadsto>* r2" |
241 assumes "r1 \<leadsto>* r2" |
258 shows "[r1] s\<leadsto>* [r2]" |
242 shows "[r1] s\<leadsto>* [r2]" |
259 using assms |
243 using assms |
265 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
249 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
266 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
250 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
267 using assms |
251 using assms |
268 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
252 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
269 |
253 |
270 (*harmless sorry*) |
254 lemma ss6_stronger_aux: |
271 lemma existing_preimage : |
255 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctWith rs2 eq1 (set rs1))" |
272 shows "f a \<in> f ` set rs1 \<Longrightarrow> \<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> f x = f a " |
256 apply(induct rs2 arbitrary: rs1) |
273 apply(induct rs1) |
257 apply(auto) |
274 apply simp |
|
275 apply(case_tac "f a = f aa") |
|
276 |
|
277 sorry |
|
278 |
|
279 |
|
280 lemma deletes_dB: |
|
281 shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)" |
|
282 apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a") |
|
283 prefer 2 |
258 prefer 2 |
284 apply (meson existing_preimage) |
259 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
|
260 apply(simp) |
|
261 apply(drule_tac x="rs1" in meta_spec) |
|
262 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
263 using srewrites_trans apply blast |
|
264 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
|
265 prefer 2 |
|
266 apply (simp add: split_list) |
285 apply(erule exE)+ |
267 apply(erule exE)+ |
286 apply simp |
268 apply(simp) |
287 apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\<leadsto> (rs1a @ [x] @ rs1b @ rs2)") |
269 using eq1_L rs_in_rstar ss6 by force |
288 apply (simp add: rs_in_rstar) |
|
289 apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)") |
|
290 using ss6 apply presburger |
|
291 by simp |
|
292 |
|
293 |
|
294 |
|
295 lemma ss6_realistic: |
|
296 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (tset rs1))" |
|
297 apply(induct rs2 arbitrary: rs1) |
|
298 apply simp |
|
299 apply(rename_tac cc' cc) |
|
300 apply(subgoal_tac "(cc @ a # cc') s\<leadsto>* (cc @ a # dB6 cc' (tset (cc @ [a])))") |
|
301 prefer 2 |
|
302 apply (metis append.assoc append.left_neutral append_Cons) |
|
303 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") |
|
304 sorry |
|
305 |
|
306 |
|
307 |
|
308 |
270 |
309 lemma ss6_stronger: |
271 lemma ss6_stronger: |
310 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
272 shows "rs1 s\<leadsto>* distinctWith rs1 eq1 {}" |
311 using ss6 |
273 by (metis append_Nil list.set(1) ss6_stronger_aux) |
312 by (metis append_Nil concat.simps(1) list.set(1) list.simps(8) ss6_realistic tset.simps) |
274 |
313 |
|
314 |
|
315 lemma tint_fuse: |
|
316 shows "tint (erase a) = tint (erase (fuse bs a))" |
|
317 by (simp add: erase_fuse) |
|
318 |
|
319 lemma tint_fuse2: |
|
320 shows " set (tint (erase a)) = |
|
321 set (tint (erase (fuse bs a)))" |
|
322 using tint_fuse by auto |
|
323 |
|
324 lemma fused_bits_at_head: |
|
325 shows "fuse bs a = ASEQ bs1 a1 a2 \<Longrightarrow> \<exists>bs2. bs1 = bs @ bs2" |
|
326 |
|
327 (* by (smt (verit) arexp.distinct(13) arexp.distinct(19) arexp.distinct(25) arexp.distinct(27) arexp.distinct(5) arexp.inject(3) fuse.elims) |
|
328 harmless sorry |
|
329 *) |
|
330 |
|
331 |
|
332 sorry |
|
333 |
|
334 thm seqFold.simps |
|
335 |
|
336 lemma seqFold_concats: |
|
337 shows "r \<noteq> ONE \<Longrightarrow> seqFold r [r1] = SEQ r r1" |
|
338 apply(case_tac r) |
|
339 apply simp+ |
|
340 done |
|
341 |
|
342 |
|
343 lemma tint_seqFold_eq: shows |
|
344 "set (tint (seqFold (erase x42) [erase x43])) = |
|
345 set (tint (SEQ (erase x42) (erase x43)))" |
|
346 apply(case_tac "erase x42 = ONE") |
|
347 apply simp |
|
348 using seqFold_concats |
|
349 apply simp |
|
350 done |
|
351 |
|
352 fun top :: "arexp \<Rightarrow> bit list" where |
|
353 "top AZERO = []" |
|
354 | "top (AONE bs) = bs" |
|
355 | "top (ASEQ bs r1 r2) = bs" |
|
356 | "top (ACHAR v va) = v" |
|
357 | "top (AALTs v va) = v" |
|
358 | "top (ASTAR v va) = v " |
|
359 |
|
360 |
|
361 |
|
362 |
|
363 lemma p6fa_aux: |
|
364 shows " fuse bs |
|
365 (bsimp_AALTs bs\<^sub>0 as) = |
|
366 |
|
367 (bsimp_AALTs (bs @ bs\<^sub>0) as)" |
|
368 by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv) |
|
369 |
|
370 |
|
371 lemma p6pfuse_alts: |
|
372 shows |
|
373 " \<And>bs\<^sub>0 as\<^sub>0. |
|
374 \<lbrakk>\<And>a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\<rbrakk> |
|
375 \<Longrightarrow> \<not> set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<longrightarrow> |
|
376 fuse bs |
|
377 (case a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa |
|
378 | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2 |
|
379 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa) |
|
380 = |
|
381 (case fuse bs a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa |
|
382 | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2 |
|
383 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)" |
|
384 apply simp |
|
385 using p6fa_aux by presburger |
|
386 |
|
387 |
|
388 |
|
389 |
|
390 lemma prune6_preserves_fuse: |
|
391 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
|
392 using tint_fuse2 |
|
393 apply simp |
|
394 apply(case_tac a) |
|
395 apply simp |
|
396 apply simp |
|
397 apply simp |
|
398 |
|
399 using fused_bits_at_head |
|
400 |
|
401 apply simp |
|
402 using tint_seqFold_eq |
|
403 apply simp |
|
404 apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append) |
|
405 using p6pfuse_alts apply presburger |
|
406 by simp |
|
407 |
|
408 |
|
409 (* |
|
410 The top-level bitlist stays the same: |
|
411 \<^sub>b\<^sub>sa ------pruning-----> \<^sub>b\<^sub>s\<^sub>' b \<Longrightarrow> \<exists>bs3. bs' = bs @ bs3 |
|
412 *) |
|
413 lemma top_bitcodes_preserved_p6: |
|
414 shows "top r = bs \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)" |
|
415 |
|
416 |
|
417 apply(induct r arbitrary: as) |
|
418 |
|
419 (*this sorry requires more care *) |
|
420 |
|
421 sorry |
|
422 |
|
423 |
|
424 |
|
425 corollary prune6_preserves_fuse_srewrite: |
|
426 shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)" |
|
427 apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") |
|
428 apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)") |
|
429 using prune6_preserves_fuse apply auto[1] |
|
430 using rs_in_rstar ss7 apply presburger |
|
431 by simp |
|
432 |
|
433 lemma prune6_invariant_fuse: |
|
434 shows "p6 as a = p6 (map (fuse bs) as) a" |
|
435 apply simp |
|
436 using erase_fuse by presburger |
|
437 |
|
438 |
|
439 lemma p6pfs_cor: |
|
440 shows "(map (fuse bs) as @ map (fuse bs) [a] @ map (fuse bs) as1) s\<leadsto>* (map (fuse bs) as @ map (fuse bs) [p6 as a] @ map (fuse bs) as1)" |
|
441 by (metis prune6_invariant_fuse prune6_preserves_fuse_srewrite) |
|
442 |
275 |
443 lemma rewrite_preserves_fuse: |
276 lemma rewrite_preserves_fuse: |
444 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
277 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
445 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
278 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
446 proof(induct rule: rrewrite_srewrite.inducts) |
279 proof(induct rule: rrewrite_srewrite.inducts) |
505 lemma continuous_rewrite: |
332 lemma continuous_rewrite: |
506 assumes "r1 \<leadsto>* AZERO" |
333 assumes "r1 \<leadsto>* AZERO" |
507 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
334 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
508 using assms bs1 star_seq by blast |
335 using assms bs1 star_seq by blast |
509 |
336 |
510 |
337 (* |
|
338 lemma continuous_rewrite2: |
|
339 assumes "r1 \<leadsto>* AONE bs" |
|
340 shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)" |
|
341 using assms by (meson bs3 rrewrites.simps star_seq) |
|
342 *) |
511 |
343 |
512 lemma bsimp_aalts_simpcases: |
344 lemma bsimp_aalts_simpcases: |
513 shows "AONE bs \<leadsto>* bsimpStrong6 (AONE bs)" |
345 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
514 and "AZERO \<leadsto>* bsimpStrong6 AZERO" |
346 and "AZERO \<leadsto>* bsimp AZERO" |
515 and "ACHAR bs c \<leadsto>* bsimpStrong6 (ACHAR bs c)" |
347 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
516 by (simp_all) |
348 by (simp_all) |
517 |
349 |
518 lemma bsimp_AALTs_rewrites: |
350 lemma bsimp_AALTs_rewrites: |
519 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
351 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
520 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
352 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
533 apply(auto intro: rrewrite_srewrite.intros) |
365 apply(auto intro: rrewrite_srewrite.intros) |
534 apply (meson srewrites.simps srewrites1 ss5) |
366 apply (meson srewrites.simps srewrites1 ss5) |
535 using rs1 srewrites7 apply presburger |
367 using rs1 srewrites7 apply presburger |
536 using srewrites7 apply force |
368 using srewrites7 apply force |
537 apply (simp add: srewrites7) |
369 apply (simp add: srewrites7) |
|
370 apply(simp add: srewrites7) |
538 by (simp add: srewrites7) |
371 by (simp add: srewrites7) |
|
372 |
539 |
373 |
540 lemma bnullable0: |
374 lemma bnullable0: |
541 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
375 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
542 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
376 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
543 apply(induct rule: rrewrite_srewrite.inducts) |
377 apply(induct rule: rrewrite_srewrite.inducts) |
544 apply simp |
378 apply(auto simp add: bnullable_fuse) |
545 apply simp |
379 apply (meson UnCI bnullable_fuse imageI) |
546 apply (simp add: bnullable_fuse) |
380 using bnullable_correctness nullable_correctness by blast |
547 using bnullable.simps(5) apply presburger |
|
548 apply simp |
|
549 apply simp |
|
550 sorry |
|
551 |
|
552 |
381 |
553 |
382 |
554 lemma rewritesnullable: |
383 lemma rewritesnullable: |
555 assumes "r1 \<leadsto>* r2" |
384 assumes "r1 \<leadsto>* r2" |
556 shows "bnullable r1 = bnullable r2" |
385 shows "bnullable r1 = bnullable r2" |
557 using assms |
386 using assms |
558 apply(induction r1 r2 rule: rrewrites.induct) |
387 apply(induction r1 r2 rule: rrewrites.induct) |
559 apply simp |
388 apply simp |
560 using bnullable0(1) by presburger |
389 using bnullable0(1) by auto |
561 |
390 |
562 lemma rewrite_bmkeps_aux: |
391 lemma rewrite_bmkeps_aux: |
563 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
392 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
564 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
393 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
565 proof (induct rule: rrewrite_srewrite.inducts) |
394 proof (induct rule: rrewrite_srewrite.inducts) |
573 then show ?case |
402 then show ?case |
574 using bmkepss.simps bnullable0(1) by presburger |
403 using bmkepss.simps bnullable0(1) by presburger |
575 next |
404 next |
576 case (ss5 bs1 rs1 rsb) |
405 case (ss5 bs1 rs1 rsb) |
577 then show ?case |
406 then show ?case |
578 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
407 apply (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
|
408 apply(case_tac rs1) |
|
409 apply(auto simp add: bnullable_fuse) |
|
410 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
411 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
412 apply (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
|
413 by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
579 next |
414 next |
580 case (ss6 a1 a2 rsa rsb rsc) |
415 case (ss6 a1 a2 rsa rsb rsc) |
581 then show ?case |
416 then show ?case |
582 by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) |
417 by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) |
583 next |
418 next |
584 prefer 10 |
419 case (bs10 rs1 rs2 bs) |
585 case (ss7 as a as1) |
420 then show ?case |
586 then show ?case |
421 by (metis bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4)) |
587 |
422 qed (auto) |
588 (*this sorry requires more effort*) |
|
589 sorry |
|
590 qed(auto) |
|
591 |
423 |
592 lemma rewrites_bmkeps: |
424 lemma rewrites_bmkeps: |
593 assumes "r1 \<leadsto>* r2" "bnullable r1" |
425 assumes "r1 \<leadsto>* r2" "bnullable r1" |
594 shows "bmkeps r1 = bmkeps r2" |
426 shows "bmkeps r1 = bmkeps r2" |
595 using assms |
427 using assms |
607 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
439 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
608 then show "bmkeps r1 = bmkeps r3" using IH by simp |
440 then show "bmkeps r1 = bmkeps r3" using IH by simp |
609 qed |
441 qed |
610 |
442 |
611 |
443 |
|
444 lemma rewrites_to_bsimp: |
|
445 shows "r \<leadsto>* bsimp r" |
|
446 proof (induction r rule: bsimp.induct) |
|
447 case (1 bs1 r1 r2) |
|
448 have IH1: "r1 \<leadsto>* bsimp r1" by fact |
|
449 have IH2: "r2 \<leadsto>* bsimp r2" by fact |
|
450 { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO" |
|
451 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
452 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
453 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
454 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto |
|
455 } |
|
456 moreover |
|
457 { assume "\<exists>bs. bsimp r1 = AONE bs" |
|
458 then obtain bs where as: "bsimp r1 = AONE bs" by blast |
|
459 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
460 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
461 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)" |
|
462 using rewrites_fuse by (meson rrewrites_trans) |
|
463 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp |
|
464 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) |
|
465 } |
|
466 moreover |
|
467 { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" |
|
468 then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
469 by (simp add: bsimp_ASEQ1) |
|
470 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 |
|
471 by (metis rrewrites_trans star_seq star_seq2) |
|
472 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp |
|
473 } |
|
474 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast |
|
475 next |
|
476 case (2 bs1 rs) |
|
477 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact |
|
478 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) |
|
479 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) |
|
480 also have "... s\<leadsto>* distinctWith (flts (map bsimp rs)) eq1 {}" by (simp add: ss6_stronger) |
|
481 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
482 using contextrewrites0 by auto |
|
483 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
484 by (simp add: bsimp_AALTs_rewrites) |
|
485 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp |
|
486 qed (simp_all) |
|
487 |
612 |
488 |
613 lemma to_zero_in_alt: |
489 lemma to_zero_in_alt: |
614 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
490 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
615 by (simp add: bs1 bs10 ss3) |
491 by (simp add: bs1 bs10 ss3) |
616 |
492 |
705 apply(rule srewrites_trans) |
575 apply(rule srewrites_trans) |
706 apply(rule rs_in_rstar) |
576 apply(rule rs_in_rstar) |
707 apply(rule_tac rrewrite_srewrite.ss6) |
577 apply(rule_tac rrewrite_srewrite.ss6) |
708 using Der_def der_correctness apply auto[1] |
578 using Der_def der_correctness apply auto[1] |
709 by blast |
579 by blast |
710 next |
|
711 case (ss7 as a as1) |
|
712 then show ?case |
|
713 apply simp |
|
714 sorry |
|
715 qed |
580 qed |
716 |
581 |
717 lemma rewrites_preserves_bder: |
582 lemma rewrites_preserves_bder: |
718 assumes "r1 \<leadsto>* r2" |
583 assumes "r1 \<leadsto>* r2" |
719 shows "bder c r1 \<leadsto>* bder c r2" |
584 shows "bder c r1 \<leadsto>* bder c r2" |
720 using assms |
585 using assms |
721 apply(induction r1 r2 rule: rrewrites.induct) |
586 apply(induction r1 r2 rule: rrewrites.induct) |
722 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
587 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
723 done |
588 done |
724 |
589 |
725 |
590 |
726 |
591 lemma central: |
727 lemma bders_simp_appendStrong : |
592 shows "bders r s \<leadsto>* bders_simp r s" |
728 shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" |
|
729 apply(induct s1 arbitrary: s2 rule: rev_induct) |
|
730 apply simp |
|
731 apply auto |
|
732 done |
|
733 |
|
734 |
|
735 |
|
736 |
|
737 lemma rewrites_to_bsimpStrong: |
|
738 shows "r \<leadsto>* bsimpStrong6 r" |
|
739 proof (induction r rule: bsimpStrong6.induct) |
|
740 case (1 bs1 r1 r2) |
|
741 have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact |
|
742 have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact |
|
743 { assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO" |
|
744 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
745 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
746 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
747 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto |
|
748 } |
|
749 moreover |
|
750 { assume "\<exists>bs. bsimpStrong6 r1 = AONE bs" |
|
751 then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast |
|
752 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
753 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
754 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)" |
|
755 using rewrites_fuse by (meson rrewrites_trans) |
|
756 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp |
|
757 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as) |
|
758 } |
|
759 moreover |
|
760 { assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)" |
|
761 then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" |
|
762 by (simp add: bsimp_ASEQ1) |
|
763 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 |
|
764 by (metis rrewrites_trans star_seq star_seq2) |
|
765 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp |
|
766 } |
|
767 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" |
|
768 by blast |
|
769 next |
|
770 case (2 bs1 rs) |
|
771 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact |
|
772 then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) |
|
773 also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) |
|
774 also have "... s\<leadsto>* dB6 (flts (map bsimpStrong6 rs)) {}" by (simp add: ss6_stronger) |
|
775 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" |
|
776 using contextrewrites0 by auto |
|
777 also have "... \<leadsto>* bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" |
|
778 by (simp add: bsimp_AALTs_rewrites) |
|
779 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" |
|
780 using bsimpStrong6.simps(2) by presburger |
|
781 qed (simp_all) |
|
782 |
|
783 |
|
784 |
|
785 |
|
786 lemma centralStrong: |
|
787 shows "bders r s \<leadsto>* bdersStrong6 r s" |
|
788 proof(induct s arbitrary: r rule: rev_induct) |
593 proof(induct s arbitrary: r rule: rev_induct) |
789 case Nil |
594 case Nil |
790 then show "bders r [] \<leadsto>* bdersStrong6 r []" by simp |
595 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
791 next |
596 next |
792 case (snoc x xs) |
597 case (snoc x xs) |
793 have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact |
598 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
794 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
599 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
795 also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH |
600 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
796 by (simp add: rewrites_preserves_bder) |
601 by (simp add: rewrites_preserves_bder) |
797 also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH |
602 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
798 by (simp add: rewrites_to_bsimpStrong) |
603 by (simp add: rewrites_to_bsimp) |
799 finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])" |
604 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
800 by (simp add: bders_simp_appendStrong) |
605 by (simp add: bders_simp_append) |
801 qed |
606 qed |
802 |
607 |
803 lemma mainStrong: |
608 lemma main_aux: |
804 assumes "bnullable (bders r s)" |
609 assumes "bnullable (bders r s)" |
805 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
610 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
806 proof - |
611 proof - |
807 have "bders r s \<leadsto>* bdersStrong6 r s" |
612 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
808 using centralStrong by force |
|
809 then |
613 then |
810 show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
614 show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms |
811 using assms rewrites_bmkeps by blast |
615 by (rule rewrites_bmkeps) |
812 qed |
616 qed |
813 |
617 |
814 |
618 |
815 |
619 |
816 |
620 |
817 theorem blexerStrong_correct : |
621 theorem main_blexer_simp: |
818 shows "blexerStrong r s = blexer r s" |
622 shows "blexer r s = blexer_simp r s" |
819 unfolding blexerStrong_def blexer_def |
623 unfolding blexer_def blexer_simp_def |
820 by (metis centralStrong mainStrong rewritesnullable) |
624 by (metis central main_aux rewritesnullable) |
821 |
625 |
822 |
626 theorem blexersimp_correctness: |
|
627 shows "lexer r s = blexer_simp r s" |
|
628 using blexer_correctness main_blexer_simp by simp |
|
629 |
|
630 |
|
631 unused_thms |
823 |
632 |
824 end |
633 end |