111 | "rnullable (RCHAR c) = False" |
143 | "rnullable (RCHAR c) = False" |
112 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
144 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
113 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
145 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
114 | "rnullable (RSTAR r) = True" |
146 | "rnullable (RSTAR r) = True" |
115 |
147 |
|
148 fun convert_cchar_char :: "cchar \<Rightarrow> char" |
|
149 where |
|
150 "convert_cchar_char Achar = (CHR 0x41) " |
|
151 | "convert_cchar_char Bchar = (CHR 0x42) " |
|
152 | "convert_cchar_char Cchar = (CHR 0x43) " |
|
153 | "convert_cchar_char Dchar = (CHR 0x44) " |
116 |
154 |
117 fun |
155 fun |
118 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
156 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
119 where |
157 where |
120 "rder c (RZERO) = RZERO" |
158 "rder c (RZERO) = RZERO" |
121 | "rder c (RONE) = RZERO" |
159 | "rder c (RONE) = RZERO" |
122 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)" |
160 | "rder c (RCHAR d) = (if c = (convert_cchar_char d) then RONE else RZERO)" |
123 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
161 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
124 | "rder c (RSEQ r1 r2) = |
162 | "rder c (RSEQ r1 r2) = |
125 (if rnullable r1 |
163 (if rnullable r1 |
126 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
164 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
127 else RSEQ (rder c r1) r2)" |
165 else RSEQ (rder c r1) r2)" |
422 apply auto |
466 apply auto |
423 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)") |
467 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)") |
424 prefer 2 |
468 prefer 2 |
425 apply auto |
469 apply auto |
426 sorry |
470 sorry |
427 |
471 *) |
428 |
472 |
429 |
473 (* |
430 lemma shape_derssimpseq_onechar2: |
474 lemma shape_derssimpseq_onechar2: |
431 shows "rders_simp (RSEQ r1 r2) [c] = |
475 shows "rders_simp (RSEQ r1 r2) [c] = |
432 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
476 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
433 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
477 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
434 sorry |
478 sorry |
435 |
479 |
|
480 *) |
|
481 |
|
482 lemma shape_derssimpseq_onechar: |
|
483 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
484 and "rders_simp (RSEQ r1 r2) [c] = |
|
485 rsimp (RALTS ((RSEQ (rders r1 [c]) r2) # |
|
486 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
|
487 apply simp |
|
488 apply(simp add: rders.simps) |
|
489 apply(case_tac "rsimp (rder c r1) = RZERO") |
|
490 apply auto |
|
491 apply(case_tac "rsimp (rder c r1) = RONE") |
|
492 apply auto |
|
493 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2") |
|
494 prefer 2 |
|
495 using idiot |
|
496 apply simp |
|
497 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})") |
|
498 prefer 2 |
|
499 apply auto |
|
500 apply(case_tac "rsimp r2") |
|
501 apply auto |
|
502 apply(subgoal_tac "rdistinct x5 {} = x5") |
|
503 prefer 2 |
|
504 using no_further_dB_after_simp |
|
505 apply metis |
|
506 apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5") |
|
507 prefer 2 |
|
508 apply fastforce |
|
509 apply auto |
|
510 apply (metis no_alt_short_list_after_simp) |
|
511 apply (case_tac "rsimp r2 = RZERO") |
|
512 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO") |
|
513 prefer 2 |
|
514 apply(case_tac "rsimp ( rder c r1)") |
|
515 apply auto |
|
516 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)") |
|
517 prefer 2 |
|
518 apply auto |
|
519 sorry |
|
520 |
|
521 lemma shape_derssimpseq_onechar2: |
|
522 shows "rders_simp (RSEQ r1 r2) [c] = |
|
523 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
|
524 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
|
525 sorry |
|
526 |
|
527 (* |
|
528 lemma simp_helps_der_pierce_dB: |
|
529 shows " rsimp |
|
530 (rsimp_ALTs |
|
531 (map (rder x) |
|
532 (rdistinct rs {}))) = |
|
533 rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))" |
|
534 |
|
535 sorry |
|
536 *) |
|
537 (* |
|
538 lemma simp_helps_der_pierce_flts: |
|
539 shows " rsimp |
|
540 (rsimp_ALTs |
|
541 (rdistinct |
|
542 (map (rder x) |
|
543 (rflts rs ) |
|
544 ) {} |
|
545 ) |
|
546 ) = |
|
547 rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}) )" |
|
548 |
|
549 sorry |
|
550 |
|
551 *) |
436 |
552 |
437 lemma rders__onechar: |
553 lemma rders__onechar: |
438 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
554 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
439 by simp |
555 by simp |
440 |
556 |
590 using first_elem_seqder1 rders_simp_append by auto |
683 using first_elem_seqder1 rders_simp_append by auto |
591 |
684 |
592 lemma first_elem_seqder_nullable: |
685 lemma first_elem_seqder_nullable: |
593 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> cond_list r1 r2 (xs @ [x]) = rder x r2 # map (rder x) (cond_list r1 r2 xs)" |
686 shows "rnullable (rders_simp r1 xs) \<Longrightarrow> cond_list r1 r2 (xs @ [x]) = rder x r2 # map (rder x) (cond_list r1 r2 xs)" |
594 sorry |
687 sorry |
|
688 |
|
689 |
|
690 |
|
691 |
|
692 lemma seq_update_seq_ders: |
|
693 shows "rsimp (rder c ( rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
694 (map (rders_simp r2) Ss))))) = |
|
695 rsimp (RALTS ((RSEQ (rders_simp r1 (s @ [c])) r2) # |
|
696 (map (rders_simp r2) (seq_update c (rders_simp r1 s) Ss)))) " |
|
697 sorry |
|
698 |
|
699 lemma seq_ders_closed_form1: |
|
700 shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
|
701 (map ( rders_simp r2 ) Ss)))" |
|
702 apply(case_tac "rnullable r1") |
|
703 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
704 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))") |
|
705 prefer 2 |
|
706 apply (simp add: rsimp_idem) |
|
707 apply(rule_tac x = "[[c]]" in exI) |
|
708 apply simp |
|
709 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
710 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))") |
|
711 apply blast |
|
712 apply(simp add: rsimp_idem) |
|
713 sorry |
|
714 |
|
715 |
|
716 |
|
717 lemma seq_ders_closed_form: |
|
718 shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSEQ r1 r2) s = rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
719 (map ( rders_simp r2 ) Ss)))" |
|
720 apply(induct s rule: rev_induct) |
|
721 apply simp |
|
722 apply(case_tac xs) |
|
723 using seq_ders_closed_form1 apply auto[1] |
|
724 apply(subgoal_tac "\<exists>Ss. rders_simp (RSEQ r1 r2) xs = rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) Ss))") |
|
725 prefer 2 |
|
726 |
|
727 apply blast |
|
728 apply(erule exE) |
|
729 apply(rule_tac x = "seq_update x (rders_simp r1 xs) Ss" in exI) |
|
730 apply(subst rders_simp_append) |
|
731 apply(subgoal_tac "rders_simp (rders_simp (RSEQ r1 r2) xs) [x] = rsimp (rder x (rders_simp (RSEQ r1 r2) xs))") |
|
732 apply(simp only:) |
|
733 apply(subst seq_update_seq_ders) |
|
734 apply blast |
|
735 using rders_simp_one_char by presburger |
|
736 |
595 |
737 |
596 |
738 |
597 (*nullable_seq_with_list1 related *) |
739 (*nullable_seq_with_list1 related *) |
598 lemma LHS0_def_der_alt: |
740 lemma LHS0_def_der_alt: |
599 shows "rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = |
741 shows "rsimp (rder x (RALTS ( (RSEQ (rders_simp r1 xs) r2) # (cond_list r1 r2 xs)))) = |
749 "rexp_encode RZERO = 0" |
865 "rexp_encode RZERO = 0" |
750 |"rexp_encode RONE = 1" |
866 |"rexp_encode RONE = 1" |
751 |"rexp_encode (RCHAR c) = 2" |
867 |"rexp_encode (RCHAR c) = 2" |
752 |"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) " |
868 |"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) " |
753 *) |
869 *) |
754 lemma finite_chars: |
870 |
755 shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)" |
871 |
756 apply(rule_tac x = "Suc 256" in exI) |
872 |
757 sorry |
873 |
758 |
|
759 definition all_chars :: "int \<Rightarrow> char list" |
|
760 where "all_chars n = map char_of [0..n]" |
|
761 (* |
874 (* |
762 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
875 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
763 where |
876 where |
764 "rexp_enum 0 = []" |
877 "rexp_enum 0 = []" |
765 |"rexp_enum (Suc 0) = RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))" |
878 |"rexp_enum (Suc 0) = RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))" |
766 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]" |
879 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]" |
767 |
880 |
768 *) |
881 *) |
769 |
882 context notes rev_conj_cong[fundef_cong] begin |
770 fun rexp_enum :: "nat \<Rightarrow> rrexp set" |
883 function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set" |
771 where |
884 where |
772 "rexp_enum 0 = {}" |
885 "rexp_enum 0 = {}" |
773 |"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in> set (all_chars 255)}" |
886 |"rexp_enum (Suc 0) = {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in>{Achar, Bchar, Cchar, Dchar} }" |
774 |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n}" |
887 |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = n} \<union> |
775 |
888 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union> |
776 |
889 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union> |
777 lemma finite_sized_rexp_forms_finite_set: |
890 (rexp_enum n)" |
778 shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)" |
891 by pat_completeness auto |
779 apply(induct N) |
892 termination |
780 apply simp |
893 by (relation "measure size") auto |
781 apply auto |
894 end |
782 (*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
895 |
783 (* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
896 lemma rexp_enum_inclusion: |
|
897 shows "(rexp_enum n) \<subseteq> (rexp_enum (Suc n))" |
|
898 apply(induct n) |
|
899 apply auto[1] |
|
900 apply(simp) |
|
901 done |
|
902 |
|
903 lemma rexp_enum_mono: |
|
904 shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)" |
|
905 by (simp add: lift_Suc_mono_le rexp_enum_inclusion) |
|
906 |
|
907 lemma enum_inductive_cases: |
|
908 shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n" |
|
909 by (metis Suc_inject rsize.simps(5)) |
|
910 thm rsize.simps(5) |
|
911 |
|
912 lemma enumeration_finite: |
|
913 shows "\<exists>Nn. card (rexp_enum n) < Nn" |
|
914 apply(simp add:no_top_class.gt_ex) |
|
915 done |
|
916 |
|
917 lemma size1_rexps: |
|
918 shows "RCHAR x \<in> rexp_enum 1" |
|
919 apply(cases x) |
|
920 apply auto |
|
921 done |
|
922 |
|
923 lemma non_zero_size: |
|
924 shows "rsize r \<ge> Suc 0" |
|
925 apply(induct r) |
|
926 apply auto done |
|
927 |
|
928 corollary size_geq1: |
|
929 shows "rsize r \<ge> 1" |
|
930 by (simp add: non_zero_size) |
|
931 |
|
932 |
|
933 lemma rexp_size_induct: |
|
934 shows "\<And>N r x5 a list. |
|
935 \<lbrakk> rsize r = Suc N; r = RALTS x5; |
|
936 x5 = a # list\<rbrakk> \<Longrightarrow>\<exists>i j. rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N" |
|
937 apply(rule_tac x = "rsize a" in exI) |
|
938 apply(rule_tac x = "rsize (RALTS list)" in exI) |
|
939 apply(subgoal_tac "rsize a \<ge> 1") |
|
940 prefer 2 |
|
941 using One_nat_def non_zero_size apply presburger |
|
942 apply(subgoal_tac "rsize (RALTS list) \<ge> 1 ") |
|
943 prefer 2 |
|
944 using size_geq1 apply blast |
|
945 apply simp |
|
946 done |
|
947 |
|
948 lemma rexp_enum_case3: |
|
949 shows "N \<ge> Suc 0 \<Longrightarrow> rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union> |
|
950 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N} \<union> |
|
951 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union> |
|
952 (rexp_enum N)" |
|
953 apply(case_tac N) |
|
954 apply simp |
|
955 apply auto |
|
956 done |
|
957 |
|
958 |
|
959 |
|
960 lemma def_enum_alts: |
|
961 shows "\<lbrakk> r = RALTS x5; x5 = a # list; |
|
962 rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> a \<in> (rexp_enum i) \<and> (RALTS list) \<in> (rexp_enum j) \<rbrakk> |
|
963 \<Longrightarrow> r \<in> rexp_enum (Suc N)" |
|
964 apply(subgoal_tac "N \<ge> 1") |
|
965 prefer 2 |
|
966 apply (metis One_nat_def add_is_1 less_Suc0 linorder_le_less_linear non_zero_size) |
|
967 apply(subgoal_tac " rexp_enum (Suc N) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in> (rexp_enum i) \<and> r2 \<in> (rexp_enum j) \<and> i + j = N} \<union> |
|
968 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc N\<and> i \<le> N \<and> j \<le> N} \<union> |
|
969 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union> |
|
970 (rexp_enum N)") |
|
971 prefer 2 |
|
972 using One_nat_def rexp_enum_case3 apply presburger |
|
973 apply(subgoal_tac "i \<le> N \<and> j \<le> N") |
|
974 prefer 2 |
|
975 using non_zero_size apply auto[1] |
|
976 apply(subgoal_tac "r \<in> {uu. |
|
977 \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}") |
|
978 apply auto[1] |
|
979 apply(subgoal_tac "RALTS (a # list) \<in> {uu. |
|
980 \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}") |
|
981 |
|
982 |
|
983 apply fastforce |
|
984 apply(subgoal_tac "a \<in> rexp_enum i") |
|
985 prefer 2 |
|
986 |
|
987 apply linarith |
|
988 by blast |
|
989 |
|
990 lemma rexp_enum_covers: |
|
991 shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)" |
|
992 apply(induct N arbitrary : r) |
|
993 apply simp |
|
994 |
|
995 using rsize.elims apply auto[1] |
|
996 apply(case_tac "rsize r \<le> N") |
|
997 using enumeration_finite |
|
998 |
|
999 apply (meson in_mono rexp_enum_inclusion) |
|
1000 apply(subgoal_tac "rsize r = Suc N") |
|
1001 prefer 2 |
|
1002 using le_Suc_eq apply blast |
|
1003 |
|
1004 apply(case_tac r) |
|
1005 prefer 5 |
|
1006 apply(case_tac x5) |
|
1007 apply(subgoal_tac "rsize r =1") |
|
1008 prefer 2 |
|
1009 using hand_made_def_rlist_size rlist_size.simps(2) rsize.simps(4) apply presburger |
|
1010 apply simp |
|
1011 apply(subgoal_tac "a \<in> rexp_enum (rsize a)") |
|
1012 apply(subgoal_tac "RALTS list \<in> rexp_enum (rsize (RALTS list))") |
|
1013 |
|
1014 apply (meson def_enum_alts rexp_size_induct) |
|
1015 apply(subgoal_tac "rsize (RALTS list) \<le> N") |
|
1016 apply(subgoal_tac "RALTS list \<in> rexp_enum N") |
|
1017 prefer 2 |
|
1018 apply presburger |
|
1019 |
784 sorry |
1020 sorry |
785 |
1021 |
786 |
1022 |
787 lemma finite_size_finite_regx: |
1023 lemma finite_size_finite_regx: |
788 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
1024 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
|
1025 |
789 sorry |
1026 sorry |
790 |
1027 |
791 (*below probably needs proved concurrently*) |
1028 (*below probably needs proved concurrently*) |
792 |
1029 |
793 lemma finite_r1r2_ders_list: |
1030 lemma finite_r1r2_ders_list: |