1 theory BasicIdentities |
1 theory BasicIdentities |
2 imports "RfltsRdistinctProps" |
2 imports "Lexer" |
3 begin |
3 begin |
4 |
4 |
|
5 datatype rrexp = |
|
6 RZERO |
|
7 | RONE |
|
8 | RCHAR char |
|
9 | RSEQ rrexp rrexp |
|
10 | RALTS "rrexp list" |
|
11 | RSTAR rrexp |
|
12 | RNTIMES rrexp nat |
|
13 |
|
14 abbreviation |
|
15 "RALT r1 r2 \<equiv> RALTS [r1, r2]" |
|
16 |
|
17 |
|
18 fun |
|
19 rnullable :: "rrexp \<Rightarrow> bool" |
|
20 where |
|
21 "rnullable (RZERO) = False" |
|
22 | "rnullable (RONE) = True" |
|
23 | "rnullable (RCHAR c) = False" |
|
24 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
|
25 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
|
26 | "rnullable (RSTAR r) = True" |
|
27 | "rnullable (RNTIMES r n) = (if n = 0 then True else rnullable r)" |
|
28 |
|
29 fun |
|
30 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
31 where |
|
32 "rder c (RZERO) = RZERO" |
|
33 | "rder c (RONE) = RZERO" |
|
34 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)" |
|
35 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
|
36 | "rder c (RSEQ r1 r2) = |
|
37 (if rnullable r1 |
|
38 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
|
39 else RSEQ (rder c r1) r2)" |
|
40 | "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" |
|
41 | "rder c (RNTIMES r n) = (if n = 0 then RZERO else RSEQ (rder c r) (RNTIMES r (n - 1)))" |
|
42 |
|
43 fun |
|
44 rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
45 where |
|
46 "rders r [] = r" |
|
47 | "rders r (c#s) = rders (rder c r) s" |
|
48 |
|
49 fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list" |
|
50 where |
|
51 "rdistinct [] acc = []" |
|
52 | "rdistinct (x#xs) acc = |
|
53 (if x \<in> acc then rdistinct xs acc |
|
54 else x # (rdistinct xs ({x} \<union> acc)))" |
|
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 |
|
65 lemma rdistinct_does_the_job: |
|
66 shows "distinct (rdistinct rs s)" |
|
67 apply(induct rs s rule: rdistinct.induct) |
|
68 apply(auto simp add: rdistinct1) |
|
69 done |
|
70 |
|
71 |
|
72 |
|
73 lemma rdistinct_concat: |
|
74 assumes "set rs \<subseteq> rset" |
|
75 shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
76 using assms |
|
77 apply(induct rs) |
|
78 apply simp+ |
|
79 done |
|
80 |
|
81 lemma distinct_not_exist: |
|
82 assumes "a \<notin> set rs" |
|
83 shows "rdistinct rs rset = rdistinct rs (insert a rset)" |
|
84 using assms |
|
85 apply(induct rs arbitrary: rset) |
|
86 apply(auto) |
|
87 done |
|
88 |
|
89 lemma rdistinct_on_distinct: |
|
90 shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs" |
|
91 apply(induct rs) |
|
92 apply simp |
|
93 using distinct_not_exist by fastforce |
|
94 |
|
95 lemma distinct_rdistinct_append: |
|
96 assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc" |
|
97 shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))" |
|
98 using assms |
|
99 apply(induct rs1 arbitrary: rsa acc) |
|
100 apply(auto)[1] |
|
101 apply(auto)[1] |
|
102 apply(drule_tac x="rsa" in meta_spec) |
|
103 apply(drule_tac x="{a} \<union> acc" in meta_spec) |
|
104 apply(simp) |
|
105 apply(drule meta_mp) |
|
106 apply(auto)[1] |
|
107 apply(simp) |
|
108 done |
|
109 |
|
110 |
|
111 lemma rdistinct_set_equality1: |
|
112 shows "set (rdistinct rs acc) = set rs - acc" |
|
113 apply(induct rs acc rule: rdistinct.induct) |
|
114 apply(auto) |
|
115 done |
|
116 |
|
117 |
|
118 lemma rdistinct_set_equality: |
|
119 shows "set (rdistinct rs {}) = set rs" |
|
120 by (simp add: rdistinct_set_equality1) |
|
121 |
|
122 |
|
123 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
|
124 where |
|
125 "rflts [] = []" |
|
126 | "rflts (RZERO # rs) = rflts rs" |
|
127 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
|
128 | "rflts (r1 # rs) = r1 # rflts rs" |
|
129 |
|
130 |
|
131 lemma rflts_def_idiot: |
|
132 shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs" |
|
133 apply(case_tac a) |
|
134 apply simp_all |
|
135 done |
|
136 |
|
137 lemma rflts_def_idiot2: |
|
138 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)" |
|
139 apply(induct rs rule: rflts.induct) |
|
140 apply(auto) |
|
141 done |
|
142 |
|
143 lemma flts_append: |
|
144 shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2" |
|
145 apply(induct rs1) |
|
146 apply simp |
|
147 apply(case_tac a) |
|
148 apply simp+ |
|
149 done |
|
150 |
|
151 |
|
152 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
|
153 where |
|
154 "rsimp_ALTs [] = RZERO" |
|
155 | "rsimp_ALTs [r] = r" |
|
156 | "rsimp_ALTs rs = RALTS rs" |
|
157 |
|
158 lemma rsimpalts_conscons: |
|
159 shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)" |
|
160 by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3)) |
|
161 |
|
162 lemma rsimp_alts_equal: |
|
163 shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) " |
|
164 by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons) |
|
165 |
|
166 |
|
167 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
168 where |
|
169 "rsimp_SEQ RZERO _ = RZERO" |
|
170 | "rsimp_SEQ _ RZERO = RZERO" |
|
171 | "rsimp_SEQ RONE r2 = r2" |
|
172 | "rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
173 |
|
174 |
|
175 fun rsimp :: "rrexp \<Rightarrow> rrexp" |
|
176 where |
|
177 "rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)" |
|
178 | "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) " |
|
179 | "rsimp r = r" |
|
180 |
|
181 |
|
182 fun |
|
183 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
184 where |
|
185 "rders_simp r [] = r" |
|
186 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
|
187 |
|
188 fun rsize :: "rrexp \<Rightarrow> nat" where |
|
189 "rsize RZERO = 1" |
|
190 | "rsize (RONE) = 1" |
|
191 | "rsize (RCHAR c) = 1" |
|
192 | "rsize (RALTS rs) = Suc (sum_list (map rsize rs))" |
|
193 | "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)" |
|
194 | "rsize (RSTAR r) = Suc (rsize r)" |
|
195 | "rsize (RNTIMES r n) = Suc (rsize r) + n" |
|
196 |
|
197 abbreviation rsizes where |
|
198 "rsizes rs \<equiv> sum_list (map rsize rs)" |
5 |
199 |
6 |
200 |
7 lemma rder_rsimp_ALTs_commute: |
201 lemma rder_rsimp_ALTs_commute: |
8 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
202 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
9 apply(induct rs) |
203 apply(induct rs) |
10 apply simp |
204 apply simp |
11 apply(case_tac rs) |
205 apply(case_tac rs) |
12 apply simp |
206 apply simp |
13 apply auto |
207 apply auto |
14 done |
208 done |
15 |
|
16 |
209 |
17 |
210 |
18 lemma rsimp_aalts_smaller: |
211 lemma rsimp_aalts_smaller: |
19 shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)" |
212 shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)" |
20 apply(induct rs) |
213 apply(induct rs) |
394 apply simp |
638 apply simp |
395 apply (metis bsimp_ASEQ2 good_SEQ idiot2) |
639 apply (metis bsimp_ASEQ2 good_SEQ idiot2) |
396 apply blast |
640 apply blast |
397 apply fastforce |
641 apply fastforce |
398 using less_add_Suc2 apply blast |
642 using less_add_Suc2 apply blast |
399 using less_iff_Suc_add by blast |
643 using less_iff_Suc_add apply blast |
|
644 using good.simps(45) rsimp.simps(7) by presburger |
|
645 |
|
646 |
|
647 |
|
648 fun |
|
649 RL :: "rrexp \<Rightarrow> string set" |
|
650 where |
|
651 "RL (RZERO) = {}" |
|
652 | "RL (RONE) = {[]}" |
|
653 | "RL (RCHAR c) = {[c]}" |
|
654 | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)" |
|
655 | "RL (RALTS rs) = (\<Union> (set (map RL rs)))" |
|
656 | "RL (RSTAR r) = (RL r)\<star>" |
|
657 | "RL (RNTIMES r n) = (RL r) ^^ n" |
|
658 |
|
659 lemma pow_rempty_iff: |
|
660 shows "[] \<in> (RL r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (RL r))" |
|
661 by (induct n) (auto simp add: Sequ_def) |
400 |
662 |
401 lemma RL_rnullable: |
663 lemma RL_rnullable: |
402 shows "rnullable r = ([] \<in> RL r)" |
664 shows "rnullable r = ([] \<in> RL r)" |
403 apply(induct r) |
665 apply(induct r) |
404 apply(auto simp add: Sequ_def) |
666 apply(auto simp add: Sequ_def pow_rempty_iff) |
405 done |
667 done |
|
668 |
|
669 lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A ;; B" |
|
670 by (metis append_Nil concI) |
|
671 |
|
672 |
|
673 lemma empty_pow_add: |
|
674 fixes A::"string set" |
|
675 assumes "[] \<in> A" "s \<in> A ^^ n" |
|
676 shows "s \<in> A ^^ (n + m)" |
|
677 using assms |
|
678 apply(induct m arbitrary: n) |
|
679 apply(auto simp add: Sequ_def) |
|
680 done |
|
681 |
|
682 (* |
|
683 lemma der_pow: |
|
684 shows "Der c (A ^^ n) = (if n = 0 then {} else (Der c A) ;; (A ^^ (n - 1)))" |
|
685 apply(induct n arbitrary: A) |
|
686 apply(auto) |
|
687 by (smt (verit, best) Suc_pred concE concI concI_if_Nil2 conc_pow_comm lang_pow.simps(2)) |
|
688 *) |
406 |
689 |
407 lemma RL_rder: |
690 lemma RL_rder: |
408 shows "RL (rder c r) = Der c (RL r)" |
691 shows "RL (rder c r) = Der c (RL r)" |
409 apply(induct r) |
692 apply(induct r) |
410 apply(auto simp add: Sequ_def Der_def) |
693 apply(auto simp add: Sequ_def Der_def)[5] |
411 apply (metis append_Cons) |
694 apply (metis append_Cons) |
412 using RL_rnullable apply blast |
695 using RL_rnullable apply blast |
413 apply (metis append_eq_Cons_conv) |
696 apply (metis append_eq_Cons_conv) |
414 apply (metis append_Cons) |
697 apply (metis append_Cons) |
415 apply (metis RL_rnullable append_eq_Cons_conv) |
698 apply (metis RL_rnullable append_eq_Cons_conv) |
416 apply (metis Star.step append_Cons) |
699 apply simp |
417 using Star_decomp by auto |
700 apply(simp) |
418 |
701 done |
419 |
|
420 |
|
421 |
702 |
422 lemma RL_rsimp_RSEQ: |
703 lemma RL_rsimp_RSEQ: |
423 shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" |
704 shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)" |
424 apply(induct r1 r2 rule: rsimp_SEQ.induct) |
705 apply(induct r1 r2 rule: rsimp_SEQ.induct) |
425 apply(simp_all) |
706 apply(simp_all) |
426 done |
707 done |
427 |
|
428 |
|
429 |
708 |
430 lemma RL_rsimp_RALTS: |
709 lemma RL_rsimp_RALTS: |
431 shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))" |
710 shows "RL (rsimp_ALTs rs) = (\<Union> (set (map RL rs)))" |
432 apply(induct rs rule: rsimp_ALTs.induct) |
711 apply(induct rs rule: rsimp_ALTs.induct) |
433 apply(simp_all) |
712 apply(simp_all) |
603 lemma idem_after_simp1: |
873 lemma idem_after_simp1: |
604 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
874 shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa" |
605 apply(case_tac "rsimp aa") |
875 apply(case_tac "rsimp aa") |
606 apply simp+ |
876 apply simp+ |
607 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
877 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
608 by simp |
878 apply(simp) |
609 |
879 apply(simp) |
610 |
880 done |
611 |
881 |
612 |
|
613 |
|
614 (*equalities with rsimp *) |
|
615 lemma identity_wwo0: |
882 lemma identity_wwo0: |
616 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
883 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
617 by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
884 apply (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
618 |
885 done |
619 |
886 |
620 |
887 lemma distinct_removes_last: |
621 |
888 shows "\<lbrakk>a \<in> set as\<rbrakk> |
622 |
889 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
623 |
890 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1" |
|
891 apply(induct as arbitrary: rset ab rset1 a) |
|
892 apply simp |
|
893 apply simp |
|
894 apply(case_tac "aa \<in> rset") |
|
895 apply(case_tac "a = aa") |
|
896 apply (metis append_Cons) |
|
897 apply simp |
|
898 apply(case_tac "a \<in> set as") |
|
899 apply (metis append_Cons rdistinct.simps(2) set_ConsD) |
|
900 apply(case_tac "a = aa") |
|
901 prefer 2 |
|
902 apply simp |
|
903 apply (metis append_Cons) |
|
904 apply(case_tac "ab \<in> rset1") |
|
905 prefer 2 |
|
906 apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = |
|
907 ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))") |
|
908 prefer 2 |
|
909 apply force |
|
910 apply(simp only:) |
|
911 apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))") |
|
912 apply(simp only:) |
|
913 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)") |
|
914 apply blast |
|
915 apply(case_tac "a \<in> insert ab rset1") |
|
916 apply simp |
|
917 apply (metis insertI1) |
|
918 apply simp |
|
919 apply (meson insertI1) |
|
920 apply simp |
|
921 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
|
922 apply simp |
|
923 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
|
924 |
|
925 |
|
926 lemma distinct_removes_middle: |
|
927 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
928 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
929 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
930 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
931 apply simp |
|
932 apply simp |
|
933 apply(case_tac "a \<in> rset") |
|
934 apply simp |
|
935 apply metis |
|
936 apply simp |
|
937 apply (metis insertI1) |
|
938 apply(case_tac "a = ab") |
|
939 apply simp |
|
940 apply(case_tac "ab \<in> rset") |
|
941 apply simp |
|
942 apply presburger |
|
943 apply (meson insertI1) |
|
944 apply(case_tac "a \<in> rset") |
|
945 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
946 apply(case_tac "ab \<in> rset") |
|
947 apply simp |
|
948 apply (meson insert_iff) |
|
949 apply simp |
|
950 by (metis insertI1) |
|
951 |
|
952 |
|
953 lemma distinct_removes_middle3: |
|
954 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
955 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
956 using distinct_removes_middle(1) by fastforce |
|
957 |
|
958 |
|
959 lemma distinct_removes_list: |
|
960 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
|
961 apply(induct rs) |
|
962 apply simp+ |
|
963 apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}") |
|
964 prefer 2 |
|
965 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
|
966 by presburger |
|
967 |
|
968 |
|
969 lemma spawn_simp_rsimpalts: |
|
970 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))" |
|
971 apply(cases rs) |
|
972 apply simp |
|
973 apply(case_tac list) |
|
974 apply simp |
|
975 apply(subst rsimp_idem[symmetric]) |
|
976 apply simp |
|
977 apply(subgoal_tac "rsimp_ALTs rs = RALTS rs") |
|
978 apply(simp only:) |
|
979 apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)") |
|
980 apply(simp only:) |
|
981 prefer 2 |
|
982 apply simp |
|
983 prefer 2 |
|
984 using rsimp_ALTs.simps(3) apply presburger |
|
985 apply auto |
|
986 apply(subst rsimp_idem)+ |
|
987 by (metis comp_apply rsimp_idem) |
|
988 |
|
989 |
|
990 lemma simp_singlealt_flatten: |
|
991 shows "rsimp (RALTS [RALTS rsa]) = rsimp (RALTS (rsa @ []))" |
|
992 apply(induct rsa) |
|
993 apply simp |
|
994 apply simp |
|
995 by (metis idem_after_simp1 list.simps(9) rsimp.simps(2)) |
|
996 |
|
997 |
|
998 lemma good1_rsimpalts: |
|
999 shows "rsimp r = RALTS rs \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
1000 by (metis no_alt_short_list_after_simp) |
|
1001 |
|
1002 |
|
1003 |
|
1004 |
|
1005 lemma good1_flatten: |
|
1006 shows "\<lbrakk> rsimp r = (RALTS rs1)\<rbrakk> |
|
1007 \<Longrightarrow> rflts (rsimp_ALTs rs1 # map rsimp rsb) = rflts (rs1 @ map rsimp rsb)" |
|
1008 apply(subst good1_rsimpalts) |
|
1009 apply simp+ |
|
1010 apply(subgoal_tac "rflts (rs1 @ map rsimp rsb) = rs1 @ rflts (map rsimp rsb)") |
|
1011 apply simp |
|
1012 using flts_append rsimp_inner_idem4 by presburger |
|
1013 |
|
1014 |
|
1015 lemma flatten_rsimpalts: |
|
1016 shows "rflts (rsimp_ALTs (rdistinct (rflts (map rsimp rsa)) {}) # map rsimp rsb) = |
|
1017 rflts ( (rdistinct (rflts (map rsimp rsa)) {}) @ map rsimp rsb)" |
|
1018 apply(case_tac "map rsimp rsa") |
|
1019 apply simp |
|
1020 apply(case_tac "list") |
|
1021 apply simp |
|
1022 apply(case_tac a) |
|
1023 apply simp+ |
|
1024 apply(rename_tac rs1) |
|
1025 apply (metis good1_flatten map_eq_Cons_D no_further_dB_after_simp) |
|
1026 |
|
1027 apply simp |
|
1028 |
|
1029 apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r") |
|
1030 apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}") |
|
1031 apply simp |
|
1032 apply auto[1] |
|
1033 apply simp |
|
1034 apply(simp) |
|
1035 apply(case_tac "lista") |
|
1036 apply simp_all |
|
1037 |
|
1038 apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
|
1039 by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims) |
|
1040 |
|
1041 lemma last_elem_out: |
|
1042 shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" |
|
1043 apply(induct xs arbitrary: rset) |
|
1044 apply simp+ |
|
1045 done |
|
1046 |
|
1047 |
|
1048 |
|
1049 |
|
1050 lemma rdistinct_concat_general: |
|
1051 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
1052 apply(induct rs1 arbitrary: rs2 rule: rev_induct) |
|
1053 apply simp |
|
1054 apply(drule_tac x = "x # rs2" in meta_spec) |
|
1055 apply simp |
|
1056 apply(case_tac "x \<in> set xs") |
|
1057 apply simp |
|
1058 |
|
1059 apply (simp add: distinct_removes_middle3 insert_absorb) |
|
1060 apply simp |
|
1061 by (simp add: last_elem_out) |
|
1062 |
|
1063 |
|
1064 |
|
1065 |
|
1066 lemma distinct_once_enough: |
|
1067 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
1068 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
1069 apply(subgoal_tac |
|
1070 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
1071 apply(simp only:) |
|
1072 using rdistinct_concat_general apply blast |
|
1073 apply (simp add: distinct_rdistinct_append rdistinct_set_equality1) |
|
1074 by (simp add: rdistinct_does_the_job) |
|
1075 |
|
1076 |
|
1077 lemma simp_flatten: |
|
1078 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
1079 apply simp |
|
1080 apply(subst flatten_rsimpalts) |
|
1081 apply(simp add: flts_append) |
|
1082 by (metis Diff_empty distinct_once_enough flts_append nonalt0_fltseq nonalt_flts_rd qqq1 rdistinct_set_equality1) |
|
1083 |
|
1084 lemma basic_rsimp_SEQ_property1: |
|
1085 shows "rsimp_SEQ RONE r = r" |
|
1086 by (simp add: idiot) |
|
1087 |
|
1088 |
|
1089 |
|
1090 lemma basic_rsimp_SEQ_property3: |
|
1091 shows "rsimp_SEQ r RZERO = RZERO" |
|
1092 using rsimp_SEQ.elims by blast |
|
1093 |
|
1094 |
|
1095 |
|
1096 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where |
|
1097 "vsuf [] _ = []" |
|
1098 |"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] |
|
1099 else (vsuf cs (rder c r1)) |
|
1100 ) " |
|
1101 |
|
1102 |
|
1103 |
|
1104 |
|
1105 |
|
1106 |
|
1107 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
|
1108 "star_update c r [] = []" |
|
1109 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) |
|
1110 then (s@[c]) # [c] # (star_update c r Ss) |
|
1111 else (s@[c]) # (star_update c r Ss) )" |
|
1112 |
|
1113 |
|
1114 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
|
1115 where |
|
1116 "star_updates [] r Ss = Ss" |
|
1117 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
1118 |
|
1119 lemma stupdates_append: shows |
|
1120 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" |
|
1121 apply(induct s arbitrary: Ss) |
|
1122 apply simp |
|
1123 apply simp |
|
1124 done |
|
1125 |
|
1126 lemma flts_removes0: |
|
1127 shows " rflts (rs @ [RZERO]) = |
|
1128 rflts rs" |
|
1129 apply(induct rs) |
|
1130 apply simp |
|
1131 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
1132 |
|
1133 |
|
1134 lemma rflts_spills_last: |
|
1135 shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs" |
|
1136 apply (induct rs1 rule: rflts.induct) |
|
1137 apply(auto) |
|
1138 done |
|
1139 |
|
1140 lemma flts_keeps1: |
|
1141 shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]" |
|
1142 apply (induct rs rule: rflts.induct) |
|
1143 apply(auto) |
|
1144 done |
|
1145 |
|
1146 lemma flts_keeps_others: |
|
1147 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]" |
|
1148 apply(induct rs rule: rflts.induct) |
|
1149 apply(auto) |
|
1150 by (meson k0b nonalt.elims(3)) |
|
1151 |
|
1152 lemma spilled_alts_contained: |
|
1153 shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)" |
|
1154 apply(induct rs1) |
|
1155 apply simp |
|
1156 apply(case_tac "a = aa") |
|
1157 apply simp |
|
1158 apply(subgoal_tac " a \<in> set rs1") |
|
1159 prefer 2 |
|
1160 apply (meson set_ConsD) |
|
1161 apply(case_tac aa) |
|
1162 using rflts.simps(2) apply presburger |
|
1163 apply fastforce |
|
1164 apply fastforce |
|
1165 apply fastforce |
|
1166 apply fastforce |
|
1167 apply fastforce |
|
1168 by simp |
|
1169 |
|
1170 |
|
1171 lemma distinct_removes_duplicate_flts: |
|
1172 shows " a \<in> set rsa |
|
1173 \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
1174 rdistinct (rflts (map rsimp rsa)) {}" |
|
1175 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)") |
|
1176 prefer 2 |
|
1177 apply simp |
|
1178 apply(induct "rsimp a") |
|
1179 apply simp |
|
1180 using flts_removes0 apply presburger |
|
1181 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
1182 rdistinct (rflts (map rsimp rsa @ [RONE])) {}") |
|
1183 apply (simp only:) |
|
1184 apply(subst flts_keeps1) |
|
1185 apply (metis distinct_removes_last(1) flts_append in_set_conv_decomp rflts.simps(4)) |
|
1186 apply presburger |
|
1187 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
1188 rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") |
|
1189 apply (simp only:) |
|
1190 prefer 2 |
|
1191 apply (metis flts_append rflts.simps(1) rflts.simps(5)) |
|
1192 apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(3)) |
|
1193 apply (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(6) rflts_def_idiot2 rrexp.distinct(31) rrexp.distinct(5)) |
|
1194 apply (metis distinct_removes_list rflts_spills_last spilled_alts_contained) |
|
1195 apply (metis distinct_removes_last(1) flts_append good.simps(1) good.simps(44) rflts.simps(1) rflts.simps(7) rflts_def_idiot2 rrexp.distinct(37)) |
|
1196 by (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(8) rflts_def_idiot2 rrexp.distinct(11) rrexp.distinct(39)) |
624 |
1197 |
625 (*some basic facts about rsimp*) |
1198 (*some basic facts about rsimp*) |
626 |
1199 |
627 unused_thms |
1200 unused_thms |
628 |
1201 |