265 apply simp_all |
267 apply simp_all |
266 apply(case_tac r2) |
268 apply(case_tac r2) |
267 apply simp_all |
269 apply simp_all |
268 done |
270 done |
269 |
271 |
|
272 lemma ralts_cap_mono: |
|
273 shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) " |
|
274 by simp |
|
275 |
|
276 lemma rflts_def_idiot: |
|
277 shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> |
|
278 \<Longrightarrow> rflts (a # rs) = a # rflts rs" |
|
279 apply(case_tac a) |
|
280 apply simp_all |
|
281 done |
|
282 |
|
283 |
|
284 lemma rflts_mono: |
|
285 shows "sum_list (map rsize (rflts rs))\<le> sum_list (map rsize rs)" |
|
286 apply(induct rs) |
|
287 apply simp |
|
288 apply(case_tac "a = RZERO") |
|
289 apply simp |
|
290 apply(case_tac "\<exists>rs1. a = RALTS rs1") |
|
291 apply(erule exE) |
|
292 apply simp |
|
293 apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)") |
|
294 prefer 2 |
|
295 using rflts_def_idiot apply blast |
|
296 apply simp |
|
297 done |
|
298 |
|
299 lemma rdistinct_smaller: shows "sum_list (map rsize (rdistinct rs ss)) \<le> |
|
300 sum_list (map rsize rs )" |
|
301 apply (induct rs arbitrary: ss) |
|
302 apply simp |
|
303 by (simp add: trans_le_add2) |
|
304 |
|
305 lemma rdistinct_phi_smaller: "sum_list (map rsize (rdistinct rs {})) \<le> sum_list (map rsize rs)" |
|
306 by (simp add: rdistinct_smaller) |
|
307 |
|
308 |
|
309 lemma rsimp_alts_mono : |
|
310 shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa) \<Longrightarrow> |
|
311 rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (sum_list (map rsize x))" |
|
312 apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) |
|
313 \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))") |
|
314 prefer 2 |
|
315 using rsimp_aalts_smaller apply auto[1] |
|
316 apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc( sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})))") |
|
317 prefer 2 |
|
318 using ralts_cap_mono apply blast |
|
319 apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})) \<le> |
|
320 sum_list (map rsize ( (rflts (map rsimp x))))") |
|
321 prefer 2 |
|
322 using rdistinct_smaller apply presburger |
|
323 apply(subgoal_tac "sum_list (map rsize (rflts (map rsimp x))) \<le> |
|
324 sum_list (map rsize (map rsimp x))") |
|
325 prefer 2 |
|
326 using rflts_mono apply blast |
|
327 apply(subgoal_tac "sum_list (map rsize (map rsimp x)) \<le> sum_list (map rsize x)") |
|
328 prefer 2 |
|
329 |
|
330 apply (simp add: sum_list_mono) |
|
331 by linarith |
|
332 |
|
333 |
|
334 |
|
335 |
|
336 |
270 lemma rsimp_mono: |
337 lemma rsimp_mono: |
271 shows "rsize (rsimp r) \<le> rsize r" |
338 shows "rsize (rsimp r) \<le> rsize r" |
|
339 |
272 apply(induct r) |
340 apply(induct r) |
273 apply simp_all |
341 apply simp_all |
|
342 |
274 apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))") |
343 apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))") |
275 |
344 |
276 apply force |
345 apply force |
277 using rSEQ_mono |
346 using rSEQ_mono |
278 apply presburger |
347 apply presburger |
279 sorry |
348 using rsimp_alts_mono by auto |
280 |
349 |
281 lemma idiot: |
350 lemma idiot: |
282 shows "rsimp_SEQ RONE r = r" |
351 shows "rsimp_SEQ RONE r = r" |
283 apply(case_tac r) |
352 apply(case_tac r) |
284 apply simp_all |
353 apply simp_all |
285 done |
354 done |
286 |
355 |
287 lemma no_dup_after_simp: |
356 lemma no_alt_short_list_after_simp: |
288 shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs" |
357 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
289 sorry |
358 sorry |
290 |
359 |
291 lemma no_further_dB_after_simp: |
360 lemma no_further_dB_after_simp: |
292 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
361 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
293 sorry |
362 |
294 |
363 sorry |
295 lemma longlist_withstands_rsimp_alts: |
364 |
296 shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
297 sorry |
|
298 |
|
299 lemma no_alt_short_list_after_simp: |
|
300 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
301 sorry |
|
302 |
365 |
303 lemma idiot2: |
366 lemma idiot2: |
304 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
367 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
305 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
368 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
306 apply(case_tac r1) |
369 apply(case_tac r1) |
1015 |
1075 |
1016 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where |
1076 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list => char list list" where |
1017 "star_update c r [] = []" |
1077 "star_update c r [] = []" |
1018 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) |
1078 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) |
1019 then (s@[c]) # [c] # (star_update c r Ss) |
1079 then (s@[c]) # [c] # (star_update c r Ss) |
1020 else s # (star_update c r Ss) )" |
1080 else (s@[c]) # (star_update c r Ss) )" |
1021 |
1081 |
1022 lemma star_update_case1: |
1082 lemma star_update_case1: |
1023 shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" |
1083 shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" |
1024 |
1084 |
1025 by force |
1085 by force |
1026 |
1086 |
1027 lemma star_update_case2: |
1087 lemma star_update_case2: |
1028 shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = s # (star_update c r Ss)" |
1088 shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # (star_update c r Ss)" |
|
1089 by simp |
|
1090 |
|
1091 lemma bubble_break: shows "rflts [r, RZERO] = rflts [r]" |
|
1092 apply(case_tac r) |
|
1093 apply simp+ |
|
1094 done |
|
1095 |
|
1096 lemma rsimp_alts_idem_aux1: |
|
1097 shows "rsimp_ALTs (rdistinct (rflts [rsimp a]) {}) = rsimp (RALTS [a])" |
|
1098 by force |
|
1099 |
|
1100 |
|
1101 |
|
1102 lemma rsimp_alts_idem_aux2: |
|
1103 shows "rsimp a = rsimp (RALTS [a])" |
|
1104 apply(simp) |
|
1105 apply(case_tac "rsimp a") |
|
1106 apply simp+ |
|
1107 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
1029 by simp |
1108 by simp |
1030 |
1109 |
1031 lemma rsimp_alts_idem: |
1110 lemma rsimp_alts_idem: |
1032 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))" |
1111 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))" |
1033 sorry |
1112 apply(induct as) |
|
1113 apply(subgoal_tac "rsimp (rsimp_ALTs [a, rsimp (rsimp_ALTs [])]) = rsimp (rsimp_ALTs [a, RZERO])") |
|
1114 prefer 2 |
|
1115 apply simp |
|
1116 using bubble_break rsimp_alts_idem_aux2 apply auto[1] |
|
1117 apply(case_tac as) |
|
1118 apply(subgoal_tac "rsimp_ALTs( aa # as) = aa") |
|
1119 prefer 2 |
|
1120 apply simp |
|
1121 using head_one_more_simp apply fastforce |
|
1122 apply(subgoal_tac "rsimp_ALTs (aa # as) = RALTS (aa # as)") |
|
1123 prefer 2 |
|
1124 |
|
1125 using rsimp_ALTs.simps(3) apply presburger |
|
1126 |
|
1127 apply(simp only:) |
|
1128 apply(subgoal_tac "rsimp_ALTs (a # aa # aaa # list) = RALTS (a # aa # aaa # list)") |
|
1129 prefer 2 |
|
1130 using rsimp_ALTs.simps(3) apply presburger |
|
1131 apply(simp only:) |
|
1132 apply(subgoal_tac "rsimp_ALTs [a, rsimp (RALTS (aa # aaa # list))] = RALTS (a # [rsimp (RALTS (aa # aaa # list))])") |
|
1133 prefer 2 |
|
1134 |
|
1135 using rsimp_ALTs.simps(3) apply presburger |
|
1136 apply(simp only:) |
|
1137 using simp_flatten2 |
|
1138 apply(subgoal_tac " rsimp (RALT a (rsimp (RALTS (aa # aaa # list)))) = rsimp (RALT a ((RALTS (aa # aaa # list)))) ") |
|
1139 prefer 2 |
|
1140 |
|
1141 apply (metis head_one_more_simp list.simps(9) rsimp.simps(2)) |
|
1142 apply (simp only:) |
|
1143 done |
|
1144 |
1034 |
1145 |
1035 lemma rsimp_alts_idem2: |
1146 lemma rsimp_alts_idem2: |
1036 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))" |
1147 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))" |
1037 sorry |
1148 using head_one_more_simp rsimp_alts_idem by auto |
|
1149 |
1038 |
1150 |
1039 lemma evolution_step1: |
1151 lemma evolution_step1: |
1040 shows "rsimp |
1152 shows "rsimp |
1041 (rsimp_ALTs |
1153 (rsimp_ALTs |
1042 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
1154 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
1054 rsimp |
1166 rsimp |
1055 (rsimp_ALTs |
1167 (rsimp_ALTs |
1056 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) " |
1168 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) " |
1057 by (simp add: assms rsimp_alts_idem) |
1169 by (simp add: assms rsimp_alts_idem) |
1058 |
1170 |
|
1171 lemma rsimp_seq_aux1: |
|
1172 shows "r = RONE \<and> r2 = RSTAR r0 \<Longrightarrow> rsimp_SEQ r r2 = r2" |
|
1173 apply simp |
|
1174 done |
|
1175 |
|
1176 lemma multiple_alts_simp_flatten: |
|
1177 shows "rsimp (RALT (RALT r1 r2) (rsimp_ALTs rs)) = rsimp (RALTS (r1 # r2 # rs))" |
|
1178 by (metis Cons_eq_appendI append_self_conv2 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem simp_flatten) |
|
1179 |
|
1180 |
|
1181 lemma evo3_main_aux1: |
|
1182 shows "rsimp |
|
1183 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1184 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
1185 rsimp |
|
1186 (RALTS |
|
1187 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
1188 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" |
|
1189 apply(subgoal_tac "rsimp |
|
1190 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1191 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
1192 rsimp |
|
1193 (RALT (RALT (RSEQ ( (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1194 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) ") |
|
1195 prefer 2 |
|
1196 apply (simp add: rsimp_idem) |
|
1197 apply (simp only:) |
|
1198 apply(subst multiple_alts_simp_flatten) |
|
1199 by simp |
|
1200 |
|
1201 |
|
1202 lemma evo3_main_nullable: |
|
1203 shows " |
|
1204 \<And>a Ss. |
|
1205 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
1206 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
1207 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; rnullable (rders_simp r a)\<rbrakk> |
|
1208 \<Longrightarrow> rsimp |
|
1209 (rsimp_ALTs |
|
1210 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
1211 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
1212 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
1213 apply(subgoal_tac "rder x (RSEQ (rders_simp r a) (RSTAR r)) |
|
1214 = RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r))") |
|
1215 prefer 2 |
|
1216 apply simp |
|
1217 apply(simp only:) |
|
1218 apply(subgoal_tac "star_update x r (a # Ss) = (a @ [x]) # [x] # (star_update x r Ss)") |
|
1219 prefer 2 |
|
1220 using star_update_case1 apply presburger |
|
1221 apply(simp only:) |
|
1222 apply(subst List.list.map(2))+ |
|
1223 apply(subgoal_tac "rsimp |
|
1224 (rsimp_ALTs |
|
1225 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
1226 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
1227 rsimp |
|
1228 (RALTS |
|
1229 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
1230 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])") |
|
1231 prefer 2 |
|
1232 using rsimp_ALTs.simps(3) apply presburger |
|
1233 apply(simp only:) |
|
1234 apply(subgoal_tac " rsimp |
|
1235 (rsimp_ALTs |
|
1236 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
1237 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) |
|
1238 = |
|
1239 rsimp |
|
1240 (RALTS |
|
1241 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
1242 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
1243 |
|
1244 prefer 2 |
|
1245 using rsimp_ALTs.simps(3) apply presburger |
|
1246 apply (simp only:) |
|
1247 apply(subgoal_tac " rsimp |
|
1248 (RALT (RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ ( (rder x r)) (RSTAR r))) |
|
1249 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
1250 rsimp |
|
1251 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
1252 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
1253 prefer 2 |
|
1254 apply (simp add: rsimp_idem) |
|
1255 apply(simp only:) |
|
1256 apply(subgoal_tac " rsimp |
|
1257 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
1258 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
1259 rsimp |
|
1260 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1261 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
1262 prefer 2 |
|
1263 using rders_simp_append rders_simp_one_char rsimp_idem apply presburger |
|
1264 apply(simp only:) |
|
1265 apply(subgoal_tac " rsimp |
|
1266 (RALTS |
|
1267 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
1268 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) = |
|
1269 rsimp |
|
1270 (RALTS |
|
1271 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
1272 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
1273 prefer 2 |
|
1274 apply (smt (z3) idiot2 list.simps(9) rrexp.distinct(9) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_idem) |
|
1275 apply(simp only:) |
|
1276 apply(subgoal_tac " rsimp |
|
1277 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1278 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
1279 rsimp |
|
1280 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
1281 ( (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) ") |
|
1282 prefer 2 |
|
1283 using rsimp_idem apply force |
|
1284 apply(simp only:) |
|
1285 using evo3_main_aux1 by blast |
|
1286 |
|
1287 |
|
1288 lemma evo3_main_not1: |
|
1289 shows " \<not>rnullable (rders_simp r a) \<Longrightarrow> rder x (RSEQ (rders_simp r a) (RSTAR r)) = RSEQ (rder x (rders_simp r a)) (RSTAR r)" |
|
1290 by fastforce |
|
1291 |
|
1292 |
|
1293 lemma evo3_main_not2: |
|
1294 shows "\<not>rnullable (rders_simp r a) \<Longrightarrow> rsimp |
|
1295 (rsimp_ALTs |
|
1296 (rder x (RSEQ (rders_simp r a) (RSTAR r)) # rs)) = rsimp |
|
1297 (rsimp_ALTs |
|
1298 ((RSEQ (rders_simp r (a @ [x])) (RSTAR r)) # rs))" |
|
1299 by (simp add: rders_simp_append rsimp_alts_idem2 rsimp_idem) |
|
1300 |
|
1301 lemma evo3_main_not3: |
|
1302 shows "rsimp |
|
1303 (rsimp_ALTs |
|
1304 (rsimp_SEQ r1 (RSTAR r) # rs)) = |
|
1305 rsimp (rsimp_ALTs |
|
1306 (RSEQ r1 (RSTAR r) # rs))" |
|
1307 by (metis idiot2 rrexp.distinct(9) rsimp.simps(1) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
1308 |
|
1309 |
|
1310 lemma evo3_main_notnullable: |
|
1311 shows "\<And>a Ss. |
|
1312 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
1313 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
1314 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; \<not>rnullable (rders_simp r a)\<rbrakk> |
|
1315 \<Longrightarrow> rsimp |
|
1316 (rsimp_ALTs |
|
1317 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
1318 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
1319 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
1320 apply(subst star_update_case2) |
|
1321 apply simp |
|
1322 apply(subst List.list.map(2)) |
|
1323 apply(subst evo3_main_not2) |
|
1324 apply simp |
|
1325 apply(subst evo3_main_not3) |
|
1326 using rsimp_alts_idem by presburger |
|
1327 |
|
1328 |
|
1329 lemma evo3_aux2: |
|
1330 shows "rders_simp r a = RONE \<Longrightarrow> rsimp_SEQ (rders_simp (rders_simp r a) [x]) (RSTAR r) = RZERO" |
|
1331 by simp |
|
1332 lemma evo3_aux3: |
|
1333 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
|
1334 by (metis list.simps(8) list.simps(9) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem) |
|
1335 |
|
1336 lemma evo3_aux4: |
|
1337 shows " rsimp |
|
1338 (rsimp_ALTs |
|
1339 [RSEQ (rder x r) (RSTAR r), |
|
1340 rsimp (rsimp_ALTs rs)]) = |
|
1341 rsimp |
|
1342 (rsimp_ALTs |
|
1343 (rsimp_SEQ (rders_simp r [x]) (RSTAR r) # rs))" |
|
1344 by (metis rders_simp_one_char rsimp.simps(1) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
1345 |
|
1346 lemma evo3_aux5: |
|
1347 shows "rders_simp r a \<noteq> RONE \<and> rders_simp r a \<noteq> RZERO \<Longrightarrow> rsimp_SEQ (rders_simp r a) (RSTAR r) = RSEQ (rders_simp r a) (RSTAR r)" |
|
1348 using idiot2 by blast |
|
1349 |
|
1350 |
|
1351 lemma evolution_step3: |
|
1352 shows" \<And>a Ss. |
|
1353 rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
1354 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) \<Longrightarrow> |
|
1355 rsimp |
|
1356 (rsimp_ALTs |
|
1357 [rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)), |
|
1358 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
1359 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
1360 apply(case_tac "rders_simp r a = RONE") |
|
1361 apply(subst rsimp_seq_aux1) |
|
1362 apply simp |
|
1363 apply(subst rder.simps(6)) |
|
1364 apply(subgoal_tac "rnullable (rders_simp r a)") |
|
1365 prefer 2 |
|
1366 using rnullable.simps(2) apply presburger |
|
1367 apply(subst star_update_case1) |
|
1368 apply simp |
|
1369 |
|
1370 apply(subst List.list.map)+ |
|
1371 apply(subst rders_simp_append) |
|
1372 apply(subst evo3_aux2) |
|
1373 apply simp |
|
1374 apply(subst evo3_aux3) |
|
1375 apply(subst evo3_aux4) |
|
1376 apply simp |
|
1377 apply(case_tac "rders_simp r a = RZERO") |
|
1378 |
|
1379 apply (simp add: rsimp_alts_idem2) |
|
1380 apply(subgoal_tac "rders_simp r (a @ [x]) = RZERO") |
|
1381 prefer 2 |
|
1382 using rder.simps(1) rders_simp_append rders_simp_one_char rsimp.simps(3) apply presburger |
|
1383 using rflts.simps(2) rsimp.simps(3) rsimp_SEQ.simps(1) apply presburger |
|
1384 apply(subst evo3_aux5) |
|
1385 apply simp |
|
1386 apply(case_tac "rnullable (rders_simp r a) ") |
|
1387 using evo3_main_nullable apply blast |
|
1388 using evo3_main_notnullable apply blast |
|
1389 done |
1059 |
1390 |
1060 (* |
1391 (* |
1061 proof (prove) |
1392 proof (prove) |
1062 goal (1 subgoal): |
1393 goal (1 subgoal): |
1063 1. map f (a # s) = f a # map f s |
1394 1. map f (a # s) = f a # map f s |
1154 rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))") |
1483 rsimp (RALTS (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))") |
1155 prefer 2 |
1484 prefer 2 |
1156 using star_list_push_der apply presburger |
1485 using star_list_push_der apply presburger |
1157 |
1486 |
1158 |
1487 |
1159 sorry |
1488 by (metis ralts_vs_rsimpalts starseq_list_evolution) |
|
1489 |
|
1490 |
|
1491 lemma starder_is_a_list: |
|
1492 shows " \<exists>Ss. rders_simp (RSTAR r) s = rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) \<or> rders_simp (RSTAR r) s = RSTAR r" |
|
1493 apply(case_tac s) |
|
1494 prefer 2 |
|
1495 apply (metis neq_Nil_conv starder_is_a_list_of_stars_or_starseqs) |
|
1496 apply simp |
|
1497 done |
|
1498 |
|
1499 |
|
1500 (** start about bounds here**) |
|
1501 |
|
1502 |
|
1503 lemma list_simp_size: |
|
1504 shows "rlist_size (map rsimp rs) \<le> rlist_size rs" |
|
1505 apply(induct rs) |
|
1506 apply simp |
|
1507 apply simp |
|
1508 apply (subgoal_tac "rsize (rsimp a) \<le> rsize a") |
|
1509 prefer 2 |
|
1510 using rsimp_mono apply fastforce |
|
1511 using add_le_mono by presburger |
|
1512 |
|
1513 lemma inside_list_simp_inside_list: |
|
1514 shows "r \<in> set rs \<Longrightarrow> rsimp r \<in> set (map rsimp rs)" |
|
1515 apply (induct rs) |
|
1516 apply simp |
|
1517 apply auto |
|
1518 done |
|
1519 |
|
1520 |
|
1521 lemma rsize_star_seq_list: |
|
1522 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow> \<exists>N3.\<forall>Ss. |
|
1523 rlist_size (rdistinct (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3" |
|
1524 sorry |
|
1525 |
|
1526 |
|
1527 lemma rdistinct_bound_by_no_simp: |
|
1528 shows " |
|
1529 |
|
1530 rlist_size (rdistinct (map rsimp rs) (set (map rsimp ss))) |
|
1531 \<le> (rlist_size (rdistinct rs (set ss))) |
|
1532 " |
|
1533 apply(induct rs arbitrary: ss) |
|
1534 apply simp |
|
1535 apply(case_tac "a \<in> set ss") |
|
1536 apply(subgoal_tac "rsimp a \<in> set (map rsimp ss)") |
|
1537 prefer 2 |
|
1538 using inside_list_simp_inside_list apply blast |
|
1539 |
|
1540 apply simp |
|
1541 apply simp |
|
1542 by (metis List.set_insert add_le_mono image_insert insert_absorb rsimp_mono trans_le_add2) |
|
1543 |
|
1544 |
|
1545 lemma starder_closed_form_bound_aux1: |
|
1546 shows |
|
1547 "\<forall>Ss. rsize (rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \<le> |
|
1548 Suc (rlist_size ( (rdistinct ( ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {}))) " |
|
1549 |
|
1550 sorry |
|
1551 |
|
1552 lemma starder_closed_form_bound: |
|
1553 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow> \<exists>N3.\<forall>Ss. |
|
1554 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3" |
|
1555 apply(subgoal_tac " \<exists>N3.\<forall>Ss. |
|
1556 rlist_size (rdistinct (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3") |
|
1557 prefer 2 |
|
1558 |
|
1559 using rsize_star_seq_list apply auto[1] |
|
1560 apply(erule exE) |
|
1561 apply(rule_tac x = "Suc N3" in exI) |
|
1562 apply(subgoal_tac "\<forall>Ss. rsize (rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \<le> |
|
1563 Suc (rlist_size ( (rdistinct ( ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {})))") |
|
1564 prefer 2 |
|
1565 using starder_closed_form_bound_aux1 apply blast |
|
1566 by (meson less_trans_Suc linorder_not_le not_less_eq) |
|
1567 |
|
1568 |
|
1569 thm starder_closed_form_bound_aux1 |
|
1570 |
|
1571 (* |
|
1572 "ralts_vs_rsimpalts", , and "starder_closed_form_bound_aux1", which could be due to a bug in Sledgehammer or to inconsistent axioms (including "sorry"s) |
|
1573 *) |
|
1574 |
|
1575 lemma starder_size_bound: |
|
1576 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) \<Longrightarrow> \<exists>N3.\<forall>Ss. |
|
1577 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \<and> |
|
1578 rsize (RSTAR r0) < N3" |
|
1579 apply(subgoal_tac " \<exists>N3.\<forall>Ss. |
|
1580 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3") |
|
1581 prefer 2 |
|
1582 using starder_closed_form_bound apply blast |
|
1583 apply(erule exE) |
|
1584 apply(rule_tac x = "max N3 (Suc (rsize (RSTAR r0)))" in exI) |
|
1585 using less_max_iff_disj by blast |
|
1586 |
|
1587 |
1160 |
1588 |
1161 |
1589 |
1162 lemma finite_star: |
1590 lemma finite_star: |
1163 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
1591 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
1164 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
1592 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
1165 |
1593 apply(subgoal_tac " \<exists>N3. \<forall>Ss. |
1166 sorry |
1594 rsize(rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \<and> |
|
1595 rsize (RSTAR r0) < N3") |
|
1596 prefer 2 |
|
1597 using starder_size_bound apply blast |
|
1598 apply(erule exE) |
|
1599 apply(rule_tac x = N3 in exI) |
|
1600 by (metis starder_is_a_list) |
1167 |
1601 |
1168 |
1602 |
1169 lemma rderssimp_zero: |
1603 lemma rderssimp_zero: |
1170 shows"rders_simp RZERO s = RZERO" |
1604 shows"rders_simp RZERO s = RZERO" |
1171 apply(induction s) |
1605 apply(induction s) |