30 fun simp_ALT where |
30 fun simp_ALT where |
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
31 "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" |
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
32 | "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" |
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
33 | "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" |
34 |
34 |
|
35 (* where is ZERO *) |
35 fun simp_SEQ where |
36 fun simp_SEQ where |
36 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
37 "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" |
37 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" |
38 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
39 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" |
39 |
40 |
225 then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp |
226 then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp |
226 then have "slexer (fst (simp (der c r))) s = None" using IH by simp |
227 then have "slexer (fst (simp (der c r))) s = None" using IH by simp |
227 ultimately show "slexer r (c # s) = lexer r (c # s)" |
228 ultimately show "slexer r (c # s) = lexer r (c # s)" |
228 by (simp del: slexer.simps add: slexer_better_simp) |
229 by (simp del: slexer.simps add: slexer_better_simp) |
229 qed |
230 qed |
230 qed |
231 qed |
|
232 |
|
233 |
|
234 fun simp2_ALT where |
|
235 "simp2_ALT ZERO r2 seen = (r2, seen)" |
|
236 | "simp2_ALT r1 ZERO seen = (r1, seen)" |
|
237 | "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)" |
|
238 |
|
239 fun simp2_SEQ where |
|
240 "simp2_SEQ ZERO r2 seen = (ZERO, seen)" |
|
241 | "simp2_SEQ r1 ZERO seen = (ZERO, seen)" |
|
242 | "simp2_SEQ ONE r2 seen = (r2, seen \<union> {r2})" |
|
243 | "simp2_SEQ r1 ONE seen = (r1, seen \<union> {r1})" |
|
244 | "simp2_SEQ r1 r2 seen = (SEQ r1 r2, seen \<union> {SEQ r1 r2})" |
|
245 |
|
246 |
|
247 |
|
248 |
|
249 fun |
|
250 simp2 :: "rexp \<Rightarrow> rexp set \<Rightarrow> rexp * rexp set" |
|
251 where |
|
252 "simp2 (ALT r1 r2) seen = |
|
253 (let (r1s, seen1) = simp2 r1 seen in |
|
254 let (r2s, seen2) = simp2 r2 seen1 |
|
255 in simp2_ALT r1s r2s seen2)" |
|
256 | "simp2 (SEQ r1 r2) seen = |
|
257 (let (r1s, _) = simp2 r1 {} in |
|
258 let (r2s, _) = simp2 r2 {} |
|
259 in if (SEQ r1s r2s \<in> seen) then (ZERO, seen) |
|
260 else simp2_SEQ r1s r2s seen)" |
|
261 | "simp2 r seen = (if r \<in> seen then (ZERO, seen) else (r, seen \<union> {r}))" |
|
262 |
|
263 |
|
264 lemma simp2_ALT[simp]: |
|
265 shows "L (fst (simp2_ALT r1 r2 seen)) = L r1 \<union> L r2" |
|
266 apply(induct r1 r2 seen rule: simp2_ALT.induct) |
|
267 apply(simp_all) |
|
268 done |
|
269 |
|
270 lemma test1: |
|
271 shows "snd (simp2_ALT r1 r2 rs) = rs" |
|
272 apply(induct r1 r2 rs rule: simp2_ALT.induct) |
|
273 apply(auto) |
|
274 done |
|
275 |
|
276 lemma test2: |
|
277 shows "rs \<subseteq> snd (simp2_SEQ r1 r2 rs)" |
|
278 apply(induct r1 r2 rs rule: simp2_SEQ.induct) |
|
279 apply(auto) |
|
280 done |
|
281 |
|
282 lemma test3: |
|
283 shows "rs \<subseteq> snd (simp2 r rs)" |
|
284 apply(induct r rs rule: simp2.induct) |
|
285 apply(auto split: prod.split) |
|
286 apply (metis set_mp test1) |
|
287 by (meson set_mp test2) |
|
288 |
|
289 lemma test3a: |
|
290 shows "\<Union>(L ` snd (simp2 r rs)) \<subseteq> L(r) \<union> (\<Union> (L ` rs))" |
|
291 apply(induct r rs rule: simp2.induct) |
|
292 apply(auto split: prod.split simp add: Sequ_def) |
|
293 apply (smt UN_iff Un_iff set_mp test1) |
|
294 |
|
295 |
|
296 lemma test: |
|
297 assumes "(\<Union>r' \<in> rs. L r') \<subseteq> L r" |
|
298 shows "L(fst (simp2 r rs)) \<subseteq> L(r)" |
|
299 using assms |
|
300 apply(induct r arbitrary: rs) |
|
301 apply(simp only: simp2.simps) |
|
302 apply(simp) |
|
303 apply(simp only: simp2.simps) |
|
304 apply(simp) |
|
305 apply(simp only: simp2.simps) |
|
306 apply(simp) |
|
307 prefer 3 |
|
308 apply(simp only: simp2.simps) |
|
309 apply(simp) |
|
310 prefer 2 |
|
311 apply(simp only: simp2.simps) |
|
312 apply(simp) |
|
313 apply(subst prod.split) |
|
314 apply(rule allI)+ |
|
315 apply(rule impI) |
|
316 apply(subst prod.split) |
|
317 apply(rule allI)+ |
|
318 apply(rule impI) |
|
319 apply(simp) |
|
320 apply(drule_tac x="rs" in meta_spec) |
|
321 apply(simp) |
|
322 apply(drule_tac x="x2" in meta_spec) |
|
323 apply(simp) |
|
324 apply(auto)[1] |
|
325 apply(subgoal_tac "rs \<subseteq> x2a") |
|
326 prefer 2 |
|
327 apply (metis order_trans prod.sel(2) test3) |
|
328 |
|
329 |
|
330 apply(rule antisym) |
|
331 prefer 2 |
|
332 apply(simp) |
|
333 apply(rule conjI) |
|
334 apply(drule meta_mp) |
|
335 prefer 2 |
|
336 apply(simp) |
|
337 apply(auto)[1] |
|
338 apply(auto)[1] |
|
339 |
|
340 thm prod.split |
|
341 apply(auto split: prod.split)[1] |
|
342 apply(drule_tac x="rs" in meta_spec) |
|
343 apply(drule_tac x="rs" in meta_spec) |
|
344 apply(simp) |
|
345 apply(rule_tac x="SEQ x1 x1a" in bexI) |
|
346 apply(simp add: Sequ_def) |
|
347 |
|
348 apply(auto)[1] |
|
349 apply(simp) |
|
350 apply(subgoal_tac "L (fst (simp2_SEQ x1 x1a rs)) \<subseteq> L x1 \<union> L x1a") |
|
351 apply(frule_tac x="{}" in meta_spec) |
|
352 apply(rotate_tac 1) |
|
353 apply(frule_tac x="{}" in meta_spec) |
|
354 apply(simp) |
|
355 |
|
356 |
|
357 apply(rule_tac x="SEQ x1 x1a" in bexI) |
|
358 apply(simp add: Sequ_def) |
|
359 apply(auto)[1] |
|
360 apply(simp) |
|
361 using L.simps(2) apply blast |
|
362 prefer 3 |
|
363 apply(simp only: simp2.simps) |
|
364 apply(simp) |
|
365 using L.simps(3) apply blast |
|
366 prefer 2 |
|
367 apply(simp add: Sequ_def) |
|
368 apply(auto)[1] |
|
369 oops |
231 |
370 |
232 end |
371 end |