157 lemma pders_Set_snoc: |
157 lemma pders_Set_snoc: |
158 shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))" |
158 shows "pders_Set (PSuf s ;; {[c]}) r = (pder_set c (pders_Set (PSuf s) r))" |
159 unfolding pders_Set_def |
159 unfolding pders_Set_def |
160 by (simp add: PSuf_Union pders_snoc) |
160 by (simp add: PSuf_Union pders_snoc) |
161 |
161 |
162 lemma pderivs_SEQ: |
162 lemma pders_SEQ: |
163 shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
163 shows "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
164 proof (induct s rule: rev_induct) |
164 proof (induct s rule: rev_induct) |
165 case (snoc c s) |
165 case (snoc c s) |
166 have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
166 have ih: "pders s (SEQ r1 r2) \<subseteq> SEQs (pders s r1) r2 \<union> (pders_Set (PSuf s) r2)" |
167 by fact |
167 by fact |
338 also have "... \<le> awidth r + 1" |
340 also have "... \<le> awidth r + 1" |
339 by (rule card_pders_set_UNIV_le_awidth) |
341 by (rule card_pders_set_UNIV_le_awidth) |
340 finally show "card (pders_Set A r) \<le> awidth r + 1" by simp |
342 finally show "card (pders_Set A r) \<le> awidth r + 1" by simp |
341 qed |
343 qed |
342 |
344 |
343 (* tests *) |
345 (* other result by antimirov *) |
344 |
346 |
345 lemma b: |
347 fun subs :: "rexp \<Rightarrow> rexp set" where |
346 assumes "rd \<in> pder c r" |
348 "subs ZERO = {ZERO}" | |
347 shows "size rd \<le> (Suc (size r)) * (Suc (size r))" |
349 "subs ONE = {ONE}" | |
348 using assms |
350 "subs (CHAR a) = {CHAR a, ONE}" | |
349 apply(induct r arbitrary: rd) |
351 "subs (ALT r1 r2) = (subs r1 \<union> subs r2 \<union> {ALT r1 r2})" | |
350 apply(auto)[3] |
352 "subs (SEQ r1 r2) = (subs r1 \<union> subs r2 \<union> {SEQ r1 r2} \<union> SEQs (subs r1) r2)" | |
351 apply(case_tac "c = x") |
353 "subs (STAR r1) = (subs r1 \<union> {STAR r1} \<union> SEQs (subs r1) (STAR r1))" |
352 apply(auto)[2] |
354 |
353 prefer 2 |
355 lemma pders_subs: |
|
356 shows "pders s r \<subseteq> subs r" |
|
357 apply(induct r arbitrary: s) |
|
358 apply(simp) |
|
359 apply(simp) |
|
360 apply(simp add: pders_CHAR) |
|
361 apply(simp) |
|
362 apply(rule subset_trans) |
|
363 apply(rule pders_SEQ) |
|
364 defer |
|
365 apply(simp) |
|
366 apply(rule impI) |
|
367 apply(rule conjI) |
|
368 apply blast |
|
369 apply blast |
|
370 apply(case_tac s) |
|
371 apply(simp) |
|
372 apply(rule subset_trans) |
|
373 thm pders_STAR |
|
374 apply(rule pders_STAR) |
|
375 apply(simp) |
|
376 apply(simp) |
|
377 apply (smt UN_I UN_least Un_iff insertCI pders_Set_def subsetCE subsetI) |
|
378 apply(simp) |
|
379 apply(rule conjI) |
|
380 apply blast |
|
381 by (metis Un_insert_right le_supI1 pders_Set_subsetI subset_trans sup_ge2) |
|
382 |
|
383 fun size2 :: "rexp \<Rightarrow> nat" where |
|
384 "size2 ZERO = 1" | |
|
385 "size2 ONE = 1" | |
|
386 "size2 (CHAR c) = 1" | |
|
387 "size2 (ALT r1 r2) = Suc (size2 r1 + size2 r2)" | |
|
388 "size2 (SEQ r1 r2) = Suc (size2 r1 + size2 r2)" | |
|
389 "size2 (STAR r1) = Suc (size2 r1)" |
|
390 |
|
391 |
|
392 lemma size_rexp: |
|
393 fixes r :: rexp |
|
394 shows "1 \<le> size2 r" |
|
395 apply(induct r) |
|
396 apply(simp) |
|
397 apply(simp_all) |
|
398 done |
|
399 |
|
400 lemma |
|
401 shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
|
402 apply(induct r) |
|
403 apply(simp) |
|
404 apply(simp) |
|
405 apply(simp) |
|
406 apply(simp) |
354 apply(auto)[1] |
407 apply(auto)[1] |
355 oops |
408 apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
356 |
409 apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2) |
357 |
410 apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
358 |
|
359 lemma a: |
|
360 assumes "rd \<in> pders s (SEQ r1 r2)" |
|
361 shows "size rd \<le> Suc (size r1 + size r2)" |
|
362 using assms |
|
363 apply(induct s arbitrary: r1 r2 rd) |
|
364 apply(simp) |
|
365 apply(auto) |
|
366 apply(case_tac "nullable r1") |
|
367 apply(auto) |
|
368 oops |
|
369 |
|
370 |
|
371 lemma |
|
372 shows "\<forall>rd \<in> (pders_Set UNIV r). size rd \<le> size r" |
|
373 apply(induct r) |
|
374 apply(auto)[1] |
|
375 apply(simp add: pders_Set_def) |
|
376 apply(simp add: pders_Set_def) |
|
377 apply(simp add: pders_Set_def pders_CHAR) |
|
378 using pders_CHAR apply fastforce |
|
379 prefer 2 |
|
380 apply(simp add: pders_Set_def) |
|
381 apply (meson Un_iff le_SucI trans_le_add1 trans_le_add2) |
|
382 apply(simp add: pders_Set_def) |
|
383 apply(auto)[1] |
|
384 apply(case_tac y) |
|
385 apply(simp) |
|
386 apply(simp) |
411 apply(simp) |
387 apply(auto)[1] |
412 apply(auto)[1] |
388 apply(case_tac "nullable r1") |
413 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum) |
389 apply(simp) |
414 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1) |
390 apply(auto)[1] |
415 apply(auto)[1] |
391 prefer 3 |
416 apply(drule_tac x="r'" in bspec) |
392 apply(simp) |
417 apply(simp) |
393 apply(auto)[1] |
418 apply(rule le_trans) |
394 apply(subgoal_tac "size xa \<le> size r1") |
419 apply(assumption) |
395 prefer 2 |
420 apply(simp) |
396 apply (metis UN_I pders.simps(1) pders_snoc singletonI) |
421 using size_rexp |
397 oops |
422 apply(simp) |
|
423 done |
398 |
424 |
|
425 fun height :: "rexp \<Rightarrow> nat" where |
|
426 "height ZERO = 1" | |
|
427 "height ONE = 1" | |
|
428 "height (CHAR c) = 1" | |
|
429 "height (ALT r1 r2) = Suc (max (height r1) (height r2))" | |
|
430 "height (SEQ r1 r2) = Suc (max (height r1) (height r2))" | |
|
431 "height (STAR r1) = Suc (height r1)" |
|
432 |
|
433 lemma height_rexp: |
|
434 fixes r :: rexp |
|
435 shows "1 \<le> height r" |
|
436 apply(induct r) |
|
437 apply(simp_all) |
|
438 done |
|
439 |
|
440 lemma |
|
441 shows "\<forall>r1 \<in> subs r. height r1 \<le> Suc (height r)" |
|
442 apply(induct r) |
|
443 apply(auto)+ |
|
444 done |
399 |
445 |
|
446 |
|
447 |
|
448 (* tests *) |
|
449 |
400 |
450 |
401 |
|
402 |
451 |
403 end |
452 end |