538 shows "RALTS rs \<in> set rsb \<Longrightarrow> \<exists>rs1 rs2.( rflts rsb = rs1 @ rs @ rs2)" |
548 shows "RALTS rs \<in> set rsb \<Longrightarrow> \<exists>rs1 rs2.( rflts rsb = rs1 @ rs @ rs2)" |
539 by (metis flts_append rflts.simps(3) split_list_last) |
549 by (metis flts_append rflts.simps(3) split_list_last) |
540 |
550 |
541 lemma flts_gstar: |
551 lemma flts_gstar: |
542 shows "rs \<leadsto>g* rflts rs" |
552 shows "rs \<leadsto>g* rflts rs" |
543 sorry |
553 apply(induct rs) |
544 |
554 apply simp |
545 lemma create_nonexistent_distinct_set: |
555 apply(case_tac "a = RZERO") |
|
556 apply simp |
|
557 using gmany_steps_later grewrite.intros(1) apply blast |
|
558 apply(case_tac "\<exists>rsa. a = RALTS rsa") |
|
559 apply(erule exE) |
|
560 apply simp |
|
561 apply (meson grewrite.intros(2) grewrites.simps grewrites_cons) |
|
562 by (simp add: grewrites_cons rflts_def_idiot) |
|
563 |
|
564 |
|
565 lemma wrong1: |
546 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))" |
566 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct rs (insert a rset)) \<leadsto>g* rs1 @ (rdistinct rs (rset))" |
547 sorry |
567 |
|
568 oops |
|
569 |
|
570 lemma more_distinct1: |
|
571 shows " \<lbrakk>\<And>rsb rset rset2. |
|
572 rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2); |
|
573 rset2 \<subseteq> set rsb; a \<notin> rset; a \<in> rset2\<rbrakk> |
|
574 \<Longrightarrow> rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)" |
|
575 apply(subgoal_tac "rsb @ a # rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (insert a rset)") |
|
576 apply(subgoal_tac "rsb @ rdistinct rs (insert a rset) \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)") |
|
577 apply (meson greal_trans) |
|
578 apply (metis Un_iff Un_insert_left insert_absorb) |
|
579 by (simp add: gr_in_rstar grewrite_variant1 in_mono) |
|
580 |
|
581 |
|
582 |
|
583 |
548 |
584 |
549 lemma grewrites_in_distinct0: |
585 lemma grewrites_in_distinct0: |
550 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)" |
586 shows "a \<in> set rs1 \<Longrightarrow> rs1 @ (rdistinct (a # rs) rset) \<leadsto>g* rs1 @ (rdistinct rs rset)" |
551 apply(case_tac "a \<in> rset") |
587 apply(case_tac "a \<in> rset") |
552 apply simp |
588 apply simp |
696 apply(case_tac "a \<in> rset") |
757 apply(case_tac "a \<in> rset") |
697 apply simp |
758 apply simp |
698 apply (simp add: insert_absorb) |
759 apply (simp add: insert_absorb) |
699 by auto |
760 by auto |
700 |
761 |
|
762 lemma middle_grewrites: |
|
763 "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsa @ rs1 @ rsb \<leadsto>g* rsa @ rs2 @ rsb " |
|
764 by (simp add: grewritess_concat) |
|
765 |
|
766 lemma rdistinct_removes_all: |
|
767 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct rs rset = []" |
|
768 |
|
769 by (metis append.right_neutral rdistinct.simps(1) rdistinct_concat) |
701 |
770 |
702 lemma ends_removal: |
771 lemma ends_removal: |
703 shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc" |
772 shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc" |
704 sorry |
773 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* |
|
774 rsb @ rdistinct rs (set rsb) @ rs @ rsc") |
|
775 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rs @ rsc \<leadsto>g* |
|
776 rsb @ rdistinct rs (set rsb) @ rdistinct rs (set (rsb @ rdistinct rs (set rsb))) @ rsc") |
|
777 apply (metis (full_types) append_Nil2 append_eq_appendI greal_trans list_dlist_union rdistinct_removes_all set_append) |
|
778 apply (metis append.assoc append_Nil gstar_rdistinct_general middle_grewrites) |
|
779 using gr_in_rstar grewrite.intros(2) grewrites_append by presburger |
705 |
780 |
706 lemma grewrites_rev_append: |
781 lemma grewrites_rev_append: |
707 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]" |
782 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]" |
708 using grewritess_concat by auto |
783 using grewritess_concat by auto |
709 |
784 |
765 apply (metis append.assoc grewrites_rev_append) |
840 apply (metis append.assoc grewrites_rev_append) |
766 apply (simp add: insert_absorb) |
841 apply (simp add: insert_absorb) |
767 apply (simp add: distinct_keeps_last)+ |
842 apply (simp add: distinct_keeps_last)+ |
768 done |
843 done |
769 |
844 |
|
845 lemma grewrites_shape2: |
|
846 shows " RALTS rs \<notin> set rsb \<Longrightarrow> |
|
847 rsb @ |
|
848 rdistinct (rs @ rsa) |
|
849 (set rsb) \<leadsto>g* rflts rsb @ |
|
850 rdistinct rs (set rsb) @ |
|
851 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" |
|
852 apply (meson flts_gstar greal_trans grewrites.simps grewrites_shape2_aux grewritess_concat) |
|
853 done |
|
854 |
770 lemma rdistinct_add_acc: |
855 lemma rdistinct_add_acc: |
771 shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)" |
856 shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)" |
772 apply(induct rs arbitrary: rsb rset rset2) |
857 apply(induct rs arbitrary: rsb rset rset2) |
773 apply simp |
858 apply simp |
774 apply (case_tac "a \<in> rset") |
859 apply (case_tac "a \<in> rset") |
775 apply simp |
860 apply simp |
776 apply(case_tac "a \<in> rset2") |
861 apply(case_tac "a \<in> rset2") |
777 apply simp |
862 apply simp |
778 apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono) |
863 apply (simp add: more_distinct1) |
779 apply simp |
864 apply simp |
780 apply(drule_tac x = "rsb @ [a]" in meta_spec) |
865 apply(drule_tac x = "rsb @ [a]" in meta_spec) |
781 by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1) |
866 by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1) |
782 |
867 |
783 |
868 |
1089 |
1164 |
1090 lemma set_inclusion_with_flts: |
1165 lemma set_inclusion_with_flts: |
1091 shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))" |
1166 shows " \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RONE\<rbrakk> \<Longrightarrow> rsimp a \<in> set (rflts (map rsimp as))" |
1092 by (simp add: set_inclusion_with_flts1) |
1167 by (simp add: set_inclusion_with_flts1) |
1093 |
1168 |
1094 lemma "\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk> |
1169 lemma can_spill_lst:"\<And>x5. \<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as); rsimp a = RALTS x5\<rbrakk> |
1095 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = |
1170 \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) = |
1096 rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})" |
1171 rsimp_ALTs (rdistinct (rflts (map rsimp as @ x5)) {})" |
1097 |
1172 |
|
1173 using flts_append rflts_spills_last rsimp_inner_idem4 by presburger |
|
1174 |
|
1175 |
|
1176 |
|
1177 |
|
1178 |
|
1179 lemma common_rewrites_equal: |
|
1180 shows "(rs1 \<leadsto>g* rs3) \<and> (rs2 \<leadsto>g* rs3) \<Longrightarrow> rsimp (rsimp_ALTs rs1 ) = rsimp (rsimp_ALTs rs2)" |
|
1181 using grewrites_simpalts by force |
|
1182 |
|
1183 |
|
1184 lemma basic_regex_property1: |
|
1185 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
1098 sorry |
1186 sorry |
1099 |
1187 |
1100 |
1188 lemma basic_rsimp_SEQ_property1: |
1101 lemma last_elem_dup1: |
1189 shows "rsimp_SEQ RONE r = r" |
1102 shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))" |
1190 by (simp add: idiot) |
1103 apply simp |
1191 |
1104 apply(subgoal_tac "rsimp a \<in> set (map rsimp as)") |
1192 lemma basic_rsimp_SEQ_property3: |
1105 prefer 2 |
1193 shows "rsimp_SEQ r RZERO = RZERO" |
1106 apply simp |
1194 using rsimp_SEQ.elims by blast |
1107 apply(case_tac "rsimp a") |
1195 |
1108 apply simp |
1196 thm rsimp_SEQ.elims |
1109 |
1197 |
1110 using flts_identity3 apply presburger |
1198 |
1111 apply(subst flts_identity2) |
1199 lemma basic_rsimp_SEQ_property2: |
1112 using rrexp.distinct(1) rrexp.distinct(15) apply presburger |
1200 shows "\<lbrakk>r1 \<noteq> RZERO ; r1 \<noteq> RONE; r2 \<noteq> RZERO\<rbrakk> \<Longrightarrow>rsimp_SEQ r1 r2 = RSEQ r1 r2" |
1113 apply(subst distinct_removes_last3[symmetric]) |
1201 apply(case_tac r1) |
1114 using set_inclusion_with_flts apply blast |
1202 apply simp+ |
1115 apply simp |
1203 apply (simp add: idiot2) |
1116 apply (metis distinct_removes_last3 flts_identity10 set_inclusion_with_flts10) |
1204 using idiot2 apply blast |
1117 apply (metis distinct_removes_last3 flts_identity11 set_inclusion_with_flts11) |
1205 using idiot2 apply auto[1] |
|
1206 using idiot2 by blast |
|
1207 |
|
1208 |
|
1209 (* |
|
1210 lemma rderssimp_same_rewrites_rder_induct1: |
|
1211 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ; |
|
1212 ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow> |
|
1213 \<exists>rs3. ([rder x (rsimp (RSEQ r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RSEQ r1 r2)] \<leadsto>g* rs3) " |
1118 sorry |
1214 sorry |
1119 |
1215 |
1120 lemma last_elem_dup: |
1216 lemma rderssimp_same_rewrites_rder_induct2: |
1121 shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))" |
1217 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) \<rbrakk> \<Longrightarrow> |
1122 apply(induct as rule: rev_induct) |
1218 \<exists>rs3. ([rder x (rsimp (RSTAR r1))] \<leadsto>g* rs3) \<and> ([rder x (RSTAR r1)] \<leadsto>g* rs3) " |
1123 apply simp |
|
1124 apply simp |
|
1125 apply(subgoal_tac "xs \<noteq> []") |
|
1126 prefer 2 |
|
1127 |
|
1128 |
|
1129 |
|
1130 |
|
1131 sorry |
1219 sorry |
1132 |
1220 |
1133 lemma appeared_before_remove_later: |
1221 lemma rderssimp_same_rewrites_rder_induct3: |
1134 shows "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))" |
1222 shows "\<lbrakk> ([rder x (rsimp r1)] \<leadsto>g* rs1) \<and> ([rder x r1] \<leadsto>g* rs1) ; |
1135 and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))" |
1223 ([rder x (rsimp r2)] \<leadsto>g* rs2) \<and> ([rder x r2] \<leadsto>g* rs2) \<rbrakk> \<Longrightarrow> |
1136 apply(induct rs arbitrary: as) |
1224 \<exists>rs3. ([rder x (rsimp (RALT r1 r2))] \<leadsto>g* rs3) \<and> ([rder x (RALT r1 r2)] \<leadsto>g* rs3) " |
1137 apply simp |
|
1138 |
|
1139 |
|
1140 sorry |
1225 sorry |
1141 |
1226 |
1142 lemma distinct_remove_later: |
1227 lemma rderssimp_same_rewrites_rder_induct4: |
1143 shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk> |
1228 shows "\<lbrakk>\<forall>r \<in> set rs. \<exists> rsa. ([rder x (rsimp r)] \<leadsto>g* rsa ) \<and> ([rder x r] \<leadsto>g* rsa) \<rbrakk> \<Longrightarrow> |
1144 \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) = |
1229 \<exists>rsb. ([rder x (rsimp (RALTS rs))] \<leadsto>g* rsb) \<and> ([rder x (RALTS rs)] \<leadsto>g* rsb) " |
1145 rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))" |
|
1146 |
|
1147 sorry |
1230 sorry |
1148 |
1231 |
1149 |
1232 lemma rderssimp_same_rewrites_rder_base1: |
1150 lemma distinct_der_general: |
1233 shows "([rder x (rsimp RONE)] \<leadsto>g* [] ) \<and> ([rder x RONE] \<leadsto>g* [])" |
1151 shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) = |
1234 by (simp add: gr_in_rstar grewrite.intros(1)) |
1152 rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )" |
1235 |
1153 apply(induct rs arbitrary: rsa) |
1236 lemma rderssimp_same_rewrites_rder_base2: |
1154 apply simp |
1237 shows " ([rder x (rsimp RZERO)] \<leadsto>g* [] ) \<and> ([rder x RZERO] \<leadsto>g* [])" |
1155 apply(case_tac "a \<in> set rsa") |
1238 using rderssimp_same_rewrites_rder_base1 by auto |
1156 apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)") |
1239 |
1157 apply simp |
1240 lemma rderssimp_same_rewrites_rder_base3: |
1158 apply simp |
1241 shows " ([rder x (rsimp (RCHAR c))] \<leadsto>g* [] ) \<and> ([rder x (RCHAR c)] \<leadsto>g* [])" |
1159 apply(case_tac "rder x a \<notin> set (map (rder x) rsa)") |
1242 sorry |
|
1243 *) |
|
1244 |
|
1245 lemma inside_simp_seq_nullable: |
|
1246 shows |
|
1247 "\<And>r1 r2. |
|
1248 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); |
|
1249 rnullable r1\<rbrakk> |
|
1250 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = |
|
1251 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" |
|
1252 apply(case_tac "rsimp r1 = RONE") |
1160 apply(simp) |
1253 apply(simp) |
1161 apply(subst map_concat_cons)+ |
1254 apply(subst basic_rsimp_SEQ_property1) |
1162 apply(drule_tac x = "rsa @ [a]" in meta_spec) |
1255 apply (simp add: idem_after_simp1) |
1163 apply simp |
1256 apply(case_tac "rsimp r1 = RZERO") |
1164 apply(drule neg_removal_element_of) |
1257 |
1165 apply simp |
1258 using basic_regex_property1 apply blast |
1166 apply(subst distinct_remove_later) |
1259 apply(case_tac "rsimp r2 = RZERO") |
1167 apply simp |
1260 |
1168 apply(drule_tac x = "rsa" in meta_spec) |
1261 apply (simp add: basic_rsimp_SEQ_property3) |
1169 by blast |
1262 apply(subst basic_rsimp_SEQ_property2) |
1170 |
1263 apply simp+ |
1171 |
1264 apply(subgoal_tac "rnullable (rsimp r1)") |
|
1265 apply simp |
|
1266 using rsimp_idem apply presburger |
|
1267 |
|
1268 sorry |
|
1269 |
|
1270 |
|
1271 lemma inside_simp_removal: |
|
1272 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
|
1273 apply(induct r) |
|
1274 apply simp+ |
|
1275 apply(case_tac "rnullable r1") |
|
1276 apply simp |
|
1277 |
|
1278 using inside_simp_seq_nullable apply blast |
|
1279 sorry |
|
1280 |
|
1281 |
|
1282 lemma rders_simp_same_simpders: |
|
1283 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
|
1284 apply(induct s rule: rev_induct) |
|
1285 apply simp |
|
1286 apply(case_tac "xs = []") |
|
1287 apply simp |
|
1288 apply(simp add: rders_append rders_simp_append) |
|
1289 using inside_simp_removal by blast |
|
1290 |
|
1291 |
1172 |
1292 |
1173 |
1293 |
1174 lemma distinct_der: |
1294 lemma distinct_der: |
1175 shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) {}))" |
1295 shows "rsimp (rsimp_ALTs (map (rder x) (rdistinct rs {}))) = |
1176 by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty) |
1296 rsimp (rsimp_ALTs (rdistinct (map (rder x) rs) {}))" |
|
1297 by (metis grewrites_simpalts gstar_rdistinct inside_simp_removal rder_rsimp_ALTs_commute) |
|
1298 |
1177 |
1299 |
1178 |
1300 |
1179 |
1301 |
1180 |
1302 |
1181 lemma rders_simp_lambda: |
1303 lemma rders_simp_lambda: |