51 "rdistinct [] acc = []" |
51 "rdistinct [] acc = []" |
52 | "rdistinct (x#xs) acc = |
52 | "rdistinct (x#xs) acc = |
53 (if x \<in> acc then rdistinct xs acc |
53 (if x \<in> acc then rdistinct xs acc |
54 else x # (rdistinct xs ({x} \<union> acc)))" |
54 else x # (rdistinct xs ({x} \<union> acc)))" |
55 |
55 |
|
56 lemma rdistinct1: |
|
57 assumes "a \<in> acc" |
|
58 shows "a \<notin> set (rdistinct rs acc)" |
|
59 using assms |
|
60 apply(induct rs arbitrary: acc a) |
|
61 apply(auto) |
|
62 done |
|
63 |
|
64 |
56 lemma rdistinct_does_the_job: |
65 lemma rdistinct_does_the_job: |
57 shows "distinct (rdistinct rs s)" |
66 shows "distinct (rdistinct rs s)" |
58 apply(induct rs arbitrary: s) |
67 apply(induct rs arbitrary: s) |
59 apply simp |
68 apply simp |
60 apply simp |
69 apply simp |
61 sorry |
70 apply(auto) |
|
71 by (simp add: rdistinct1) |
|
72 |
|
73 |
62 |
74 |
63 |
75 |
64 lemma rdistinct_concat: |
76 lemma rdistinct_concat: |
65 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
77 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
66 apply(induct rs) |
78 apply(induct rs) |
108 apply(auto)[1] |
120 apply(auto)[1] |
109 apply(simp) |
121 apply(simp) |
110 done |
122 done |
111 |
123 |
112 |
124 |
113 lemma rdistinct_concat_general: |
125 |
114 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
126 |
115 sorry |
127 |
|
128 lemma rdistinct_set_equality1: |
|
129 shows "set (rdistinct rs acc) = set rs - acc" |
|
130 apply(induct rs acc rule: rdistinct.induct) |
|
131 apply(auto) |
|
132 done |
116 |
133 |
117 lemma rdistinct_set_equality: |
134 lemma rdistinct_set_equality: |
118 shows "set (rdistinct rs {}) = set rs" |
135 shows "set (rdistinct rs {}) = set rs" |
119 sorry |
136 by (simp add: rdistinct_set_equality1) |
120 |
|
121 lemma distinct_once_enough: |
|
122 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
123 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
124 apply(subgoal_tac |
|
125 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
126 apply(simp only:) |
|
127 using rdistinct_concat_general apply blast |
|
128 apply (simp add: distinct_rdistinct_append rdistinct_set_equality) |
|
129 by (simp add: rdistinct_does_the_job) |
|
130 |
|
131 |
137 |
132 |
138 |
133 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
139 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
134 where |
140 where |
135 "rflts [] = []" |
141 "rflts [] = []" |
427 shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)" |
433 shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)" |
428 using head_one_more_simp rders_simp_append rders_simp_one_char by presburger |
434 using head_one_more_simp rders_simp_append rders_simp_one_char by presburger |
429 |
435 |
430 |
436 |
431 |
437 |
|
438 fun |
|
439 RL :: "rrexp \<Rightarrow> string set" |
|
440 where |
|
441 "RL (RZERO) = {}" |
|
442 | "RL (RONE) = {[]}" |
|
443 | "RL (RCHAR c) = {[c]}" |
|
444 | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)" |
|
445 | "RL (RALTS rs) = (\<Union> (set (map RL rs)))" |
|
446 | "RL (RSTAR r) = (RL r)\<star>" |
|
447 |
|
448 |
|
449 lemma RL_rnullable: |
|
450 shows "rnullable r = ([] \<in> RL r)" |
|
451 apply(induct r) |
|
452 apply(auto simp add: Sequ_def) |
|
453 done |
|
454 |
|
455 lemma RL_rder: |
|
456 shows "RL (rder c r) = Der c (RL r)" |
|
457 apply(induct r) |
|
458 apply(auto simp add: Sequ_def Der_def) |
|
459 apply (metis append_Cons) |
|
460 using RL_rnullable apply blast |
|
461 apply (metis append_eq_Cons_conv) |
|
462 apply (metis append_Cons) |
|
463 apply (metis RL_rnullable append_eq_Cons_conv) |
|
464 apply (metis Star.step append_Cons) |
|
465 using Star_decomp by auto |
|
466 |
|
467 |
|
468 |
|
469 |
|
470 lemma RL_rsimp_RSEQ: |
|
471 shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" |
|
472 apply(induct r1 r2 rule: rsimp_SEQ.induct) |
|
473 apply(simp_all) |
|
474 done |
|
475 |
|
476 lemma RL_rsimp_RALTS: |
|
477 shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))" |
|
478 apply(induct rs rule: rsimp_ALTs.induct) |
|
479 apply(simp_all) |
|
480 done |
|
481 |
|
482 lemma RL_rsimp_rdistinct: |
|
483 shows "(\<Union> (set (map RL (rdistinct rs {})))) = (\<Union> (set (map RL rs)))" |
|
484 apply(auto) |
|
485 apply (metis rdistinct_set_equality) |
|
486 by (metis rdistinct_set_equality) |
|
487 |
|
488 lemma RL_rsimp_rflts: |
|
489 shows "(\<Union> (set (map RL (rflts rs)))) = (\<Union> (set (map RL rs)))" |
|
490 apply(induct rs rule: rflts.induct) |
|
491 apply(simp_all) |
|
492 done |
|
493 |
|
494 lemma RL_rsimp: |
|
495 shows "RL r = RL (rsimp r)" |
|
496 apply(induct r rule: rsimp.induct) |
|
497 apply(auto simp add: Sequ_def RL_rsimp_RSEQ) |
|
498 using RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts apply auto[1] |
|
499 by (smt (verit, del_insts) RL_rsimp_RALTS RL_rsimp_rdistinct RL_rsimp_rflts UN_E image_iff list.set_map) |
|
500 |
|
501 lemma RL_rders: |
|
502 shows "RL (rders_simp r s) = RL (rders r s)" |
|
503 apply(induct s arbitrary: r rule: rev_induct) |
|
504 apply(simp) |
|
505 apply(simp add: rders_append rders_simp_append) |
|
506 apply(subst RL_rsimp[symmetric]) |
|
507 using RL_rder by force |
|
508 |
|
509 |
|
510 lemma der_simp_nullability: |
|
511 shows "rnullable r = rnullable (rsimp r)" |
|
512 using RL_rnullable RL_rsimp by auto |
|
513 |
432 |
514 |
433 lemma ders_simp_nullability: |
515 lemma ders_simp_nullability: |
434 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
516 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
435 sorry |
517 apply(induct s arbitrary: r rule: rev_induct) |
436 |
518 apply(simp) |
437 lemma der_simp_nullability: |
519 apply(simp add: rders_append rders_simp_append) |
438 shows "rnullable r = rnullable (rsimp r)" |
520 apply(simp only: RL_rnullable) |
439 sorry |
521 apply(simp only: RL_rder) |
|
522 apply(subst RL_rsimp[symmetric]) |
|
523 apply(simp only: RL_rder) |
|
524 by (simp add: RL_rders) |
|
525 |
|
526 |
|
527 |
|
528 |
440 |
529 |
441 |
530 |
442 lemma first_elem_seqder: |
531 lemma first_elem_seqder: |
443 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
532 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
444 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
533 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
457 |
546 |
458 |
547 |
459 |
548 |
460 |
549 |
461 |
550 |
462 lemma seq_ders_closed_form1: |
|
463 shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
|
464 (map ( rders_simp r2 ) Ss)))" |
|
465 apply(case_tac "rnullable r1") |
|
466 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
467 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))") |
|
468 prefer 2 |
|
469 apply (simp add: rsimp_idem) |
|
470 apply(rule_tac x = "[[c]]" in exI) |
|
471 apply simp |
|
472 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
473 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))") |
|
474 apply blast |
|
475 apply(simp add: rsimp_idem) |
|
476 sorry |
|
477 |
551 |
478 |
552 |
479 |
553 |
480 lemma idem_after_simp1: |
554 lemma idem_after_simp1: |
481 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
555 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
630 using good1.simps goods.cases apply auto[1] |
704 using good1.simps goods.cases apply auto[1] |
631 apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD) |
705 apply (metis good1.cases good1.intros(1) goods.intros(2) rrexp.distinct(15) rrexp.distinct(21) rrexp.distinct(25) rrexp.distinct(29) rrexp.distinct(7) rrexp.distinct(9) rrexp.inject(3) set_ConsD) |
632 apply simp |
706 apply simp |
633 by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30)) |
707 by (metis good1.cases good1.intros(1) goods.cases list.distinct(1) list.inject list.set_intros(2) rrexp.distinct(15) rrexp.distinct(29) rrexp.distinct(7) rrexp.inject(3) rrexp.simps(26) rrexp.simps(30)) |
634 |
708 |
|
709 lemma rsimp_good10: |
|
710 shows "good1 (rsimp r)" |
|
711 apply(induct r) |
|
712 apply simp |
|
713 |
|
714 apply (simp add: good1.intros(2)) |
|
715 apply simp |
|
716 |
|
717 apply (simp add: good1.intros(3)) |
|
718 |
|
719 apply (simp add: good1.intros(4)) |
|
720 sledgehammer |
|
721 |
|
722 sorry |
|
723 |
635 lemma rsimp_good1: |
724 lemma rsimp_good1: |
636 shows "rsimp r = r1 \<Longrightarrow> good1 r1" |
725 shows "rsimp r = r1 \<Longrightarrow> good1 r1" |
637 |
726 using rsimp_good10 by blast |
638 sorry |
727 |
|
728 |
639 |
729 |
640 lemma rsimp_no_dup: |
730 lemma rsimp_no_dup: |
641 shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs" |
731 shows "rsimp r = RALTS rs \<Longrightarrow> distinct rs" |
642 sorry |
732 sorry |
643 |
733 |
737 lemma simp_flatten_aux: |
827 lemma simp_flatten_aux: |
738 shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})" |
828 shows "\<forall>r \<in> set rs. good1 r \<Longrightarrow> rflts (rdistinct (rflts rs) {}) = (rdistinct (rflts rs) {})" |
739 sorry |
829 sorry |
740 |
830 |
741 |
831 |
|
832 |
|
833 lemma rdistinct_concat_general: |
|
834 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
835 |
|
836 sorry |
|
837 |
|
838 lemma distinct_once_enough: |
|
839 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
840 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
841 apply(subgoal_tac |
|
842 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
843 apply(simp only:) |
|
844 using rdistinct_concat_general apply blast |
|
845 apply (simp add: distinct_rdistinct_append rdistinct_set_equality) |
|
846 by (simp add: rdistinct_does_the_job) |
|
847 |
742 |
848 |
743 lemma simp_flatten: |
849 lemma simp_flatten: |
744 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
850 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
745 apply simp |
851 apply simp |
746 apply(subst flatten_rsimpalts) |
852 apply(subst flatten_rsimpalts) |