1158 theorem blexersimp_correctness: |
1158 theorem blexersimp_correctness: |
1159 shows "lexer r s = blexer_simp r s" |
1159 shows "lexer r s = blexer_simp r s" |
1160 using blexer_correctness main_blexer_simp by simp |
1160 using blexer_correctness main_blexer_simp by simp |
1161 |
1161 |
1162 |
1162 |
1163 |
1163 fun |
1164 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
1164 rerase :: "arexp \<Rightarrow> rrexp" |
1165 |
1165 where |
1166 |
1166 "rerase AZERO = RZERO" |
1167 unused_thms |
1167 | "rerase (AONE _) = RONE" |
1168 |
1168 | "rerase (ACHAR _ c) = RCHAR c" |
1169 |
1169 | "rerase (AALTs bs rs) = RALTS (map rerase rs)" |
1170 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
1170 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" |
|
1171 | "rerase (ASTAR _ r) = RSTAR (rerase r)" |
|
1172 |
|
1173 |
|
1174 |
|
1175 lemma asize_rsize: |
|
1176 shows "rsize (rerase r) = asize r" |
|
1177 apply(induct r) |
|
1178 apply simp+ |
|
1179 |
|
1180 apply (metis (mono_tags, lifting) comp_apply map_eq_conv) |
|
1181 by simp |
|
1182 |
|
1183 lemma rb_nullability: |
|
1184 shows " rnullable (rerase a) = bnullable a" |
|
1185 apply(induct a) |
|
1186 apply simp+ |
|
1187 done |
|
1188 |
|
1189 lemma fuse_anything_doesnt_matter: |
|
1190 shows "rerase a = rerase (fuse bs a)" |
|
1191 by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6)) |
|
1192 |
|
1193 |
|
1194 lemma rerase_preimage: |
|
1195 shows "rerase r = RZERO \<Longrightarrow> r = AZERO" |
|
1196 apply(case_tac r) |
|
1197 apply simp+ |
|
1198 done |
|
1199 |
|
1200 lemma rerase_preimage2: |
|
1201 shows "rerase r = RONE \<Longrightarrow> \<exists>bs. r = AONE bs" |
|
1202 apply(case_tac r) |
|
1203 apply simp+ |
|
1204 done |
|
1205 |
|
1206 lemma rerase_preimage3: |
|
1207 shows "rerase r= RCHAR c \<Longrightarrow> \<exists>bs. r = ACHAR bs c" |
|
1208 apply(case_tac r) |
|
1209 apply simp+ |
|
1210 done |
|
1211 |
|
1212 lemma rerase_preimage4: |
|
1213 shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2" |
|
1214 apply(case_tac r) |
|
1215 apply(simp)+ |
|
1216 done |
|
1217 |
|
1218 lemma rerase_preimage5: |
|
1219 shows "rerase r = RALTS rs \<Longrightarrow> \<exists>bs as. r = AALTs bs as \<and> map rerase as = rs" |
|
1220 apply(case_tac r) |
|
1221 apply(simp)+ |
|
1222 done |
|
1223 |
|
1224 lemma rerase_preimage6: |
|
1225 shows "rerase r = RSTAR r0 \<Longrightarrow> \<exists>bs a0. r = ASTAR bs a0 \<and> rerase a0 = r0 " |
|
1226 apply(case_tac r) |
|
1227 apply(simp)+ |
|
1228 done |
|
1229 |
|
1230 lemma map_rder_bder: |
|
1231 shows "\<lbrakk> \<And>xa a. \<lbrakk>xa \<in> set x; rerase a = xa\<rbrakk> \<Longrightarrow> rerase (bder c a) = rder c xa; |
|
1232 map rerase as = x\<rbrakk> \<Longrightarrow> |
|
1233 map rerase (map (bder c) as) = map (rder c) x" |
|
1234 apply(induct x arbitrary: as) |
|
1235 apply simp+ |
|
1236 by force |
|
1237 |
|
1238 |
|
1239 lemma der_rerase: |
|
1240 shows "rerase a = r \<Longrightarrow> rerase (bder c a) = rder c r" |
|
1241 apply(induct r arbitrary: a) |
|
1242 apply simp |
|
1243 using rerase_preimage apply fastforce |
|
1244 using rerase_preimage2 apply force |
|
1245 apply (metis bder.simps(3) rder.simps(3) rerase.simps(1) rerase.simps(2) rerase_preimage3) |
|
1246 apply(insert rerase_preimage4)[1] |
|
1247 apply(subgoal_tac " \<exists>bs a1 a2. a = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2") |
|
1248 prefer 2 |
|
1249 apply presburger |
|
1250 apply(erule exE)+ |
|
1251 apply(erule conjE)+ |
|
1252 apply(subgoal_tac " rerase (bder c a1) = rder c r1") |
|
1253 prefer 2 |
|
1254 apply blast |
|
1255 apply(subgoal_tac " rerase (bder c a2) = rder c r2") |
|
1256 prefer 2 |
|
1257 apply blast |
|
1258 apply(case_tac "rnullable r1") |
|
1259 apply(subgoal_tac "bnullable a1") |
|
1260 apply simp |
|
1261 using fuse_anything_doesnt_matter apply presburger |
|
1262 using rb_nullability apply blast |
|
1263 apply (metis bder.simps(5) rb_nullability rder.simps(5) rerase.simps(5)) |
|
1264 apply simp |
|
1265 apply(insert rerase_preimage5)[1] |
|
1266 apply(subgoal_tac "\<exists>bs as. a = AALTs bs as \<and> map rerase as = x") |
|
1267 prefer 2 |
|
1268 |
|
1269 apply blast |
|
1270 apply(erule exE)+ |
|
1271 apply(erule conjE)+ |
|
1272 apply(subgoal_tac "map rerase (map (bder c) as) = map (rder c) x") |
|
1273 using bder.simps(4) rerase.simps(4) apply presburger |
|
1274 using map_rder_bder apply blast |
|
1275 using fuse_anything_doesnt_matter rerase_preimage6 by force |
|
1276 |
|
1277 lemma der_rerase2: |
|
1278 shows "rerase (bder c a) = rder c (rerase a)" |
|
1279 using der_rerase by force |
|
1280 |
|
1281 lemma ders_rerase: |
|
1282 shows "rerase (bders a s) = rders (rerase a) s" |
|
1283 apply(induct s rule: rev_induct) |
|
1284 apply simp |
|
1285 by (simp add: bders_append der_rerase rders_append) |
|
1286 |
|
1287 lemma rerase_bsimp_ASEQ: |
|
1288 shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)" |
|
1289 by (smt (verit, ccfv_SIG) SizeBound3.bsimp_ASEQ0 SizeBound3.bsimp_ASEQ2 basic_rsimp_SEQ_property1 basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 bsimp_ASEQ.simps(1) bsimp_ASEQ1 fuse_anything_doesnt_matter rerase.simps(1) rerase.simps(2) rerase.simps(5) rerase_preimage rerase_preimage2 rsimp_SEQ.simps(1)) |
|
1290 |
|
1291 lemma rerase_bsimp_AALTs: |
|
1292 shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)" |
|
1293 apply(induct rs arbitrary: bs) |
|
1294 apply simp+ |
|
1295 by (smt (verit, ccfv_threshold) Cons_eq_map_conv bsimp_AALTs.elims fuse_anything_doesnt_matter list.discI list.inject list.simps(9) rerase.simps(4) rsimp_ALTs.elims) |
|
1296 |
|
1297 |
|
1298 fun anonalt :: "arexp \<Rightarrow> bool" |
1171 where |
1299 where |
1172 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
1300 "anonalt (AALTs bs2 rs) = False" |
1173 |
1301 | "anonalt r = True" |
1174 |
1302 |
|
1303 |
|
1304 fun agood :: "arexp \<Rightarrow> bool" where |
|
1305 "agood AZERO = False" |
|
1306 | "agood (AONE cs) = True" |
|
1307 | "agood (ACHAR cs c) = True" |
|
1308 | "agood (AALTs cs []) = False" |
|
1309 | "agood (AALTs cs [r]) = False" |
|
1310 | "agood (AALTs cs (r1#r2#rs)) = (distinct (map erase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))" |
|
1311 | "agood (ASEQ _ AZERO _) = False" |
|
1312 | "agood (ASEQ _ (AONE _) _) = False" |
|
1313 | "agood (ASEQ _ _ AZERO) = False" |
|
1314 | "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)" |
|
1315 | "agood (ASTAR cs r) = True" |
|
1316 |
|
1317 |
|
1318 fun anonnested :: "arexp \<Rightarrow> bool" |
|
1319 where |
|
1320 "anonnested (AALTs bs2 []) = True" |
|
1321 | "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" |
|
1322 | "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)" |
|
1323 | "anonnested r = True" |
|
1324 |
|
1325 |
|
1326 lemma k0: |
|
1327 shows "flts (r # rs1) = flts [r] @ flts rs1" |
|
1328 apply(induct r arbitrary: rs1) |
|
1329 apply(auto) |
|
1330 done |
|
1331 |
|
1332 lemma k00: |
|
1333 shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2" |
|
1334 apply(induct rs1 arbitrary: rs2) |
|
1335 apply(auto) |
|
1336 by (metis append.assoc k0) |
|
1337 |
|
1338 |
|
1339 lemma bbbbs: |
|
1340 assumes "agood r" "r = AALTs bs1 rs" |
|
1341 shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)" |
|
1342 using assms |
|
1343 by (smt (verit, ccfv_SIG) Cons_eq_map_conv agood.simps(4) agood.simps(5) append.right_neutral bsimp_AALTs.elims flts.simps(1) flts.simps(3) list.map_disc_iff) |
|
1344 |
|
1345 lemma bbbbs1: |
|
1346 shows "anonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)" |
|
1347 by (meson anonalt.elims(3)) |
|
1348 |
|
1349 |
|
1350 |
|
1351 lemma good_fuse: |
|
1352 shows "agood (fuse bs r) = agood r" |
|
1353 apply(induct r arbitrary: bs) |
|
1354 apply(auto) |
|
1355 apply(case_tac r1) |
|
1356 apply(simp_all) |
|
1357 apply(case_tac r2) |
|
1358 apply(simp_all) |
|
1359 apply(case_tac r2) |
|
1360 apply(simp_all) |
|
1361 apply(case_tac r2) |
|
1362 apply(simp_all) |
|
1363 apply(case_tac r2) |
|
1364 apply(simp_all) |
|
1365 apply(case_tac r1) |
|
1366 apply(simp_all) |
|
1367 apply(case_tac r2) |
|
1368 apply(simp_all) |
|
1369 apply(case_tac r2) |
|
1370 apply(simp_all) |
|
1371 apply(case_tac r2) |
|
1372 apply(simp_all) |
|
1373 apply(case_tac r2) |
|
1374 apply(simp_all) |
|
1375 apply(case_tac x2a) |
|
1376 apply(simp_all) |
|
1377 apply(case_tac list) |
|
1378 apply(simp_all) |
|
1379 apply(case_tac x2a) |
|
1380 apply(simp_all) |
|
1381 apply(case_tac list) |
|
1382 apply(simp_all) |
|
1383 done |
|
1384 |
|
1385 lemma good0: |
|
1386 assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. anonalt r" "distinct (map erase rs)" |
|
1387 shows "agood (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. agood r)" |
|
1388 using assms |
|
1389 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
1390 apply simp+ |
|
1391 apply (simp add: good_fuse) |
|
1392 apply(subgoal_tac "bsimp_AALTs bs1 (v # vb # vc) = AALTs bs1 (v # vb # vc)") |
|
1393 prefer 2 |
|
1394 |
|
1395 |
|
1396 using bsimp_AALTs.simps(3) apply presburger |
|
1397 apply(simp only:) |
|
1398 apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\<forall>r \<in> (set (v # vb # vc)). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc)))") |
|
1399 prefer 2 |
|
1400 using agood.simps(6) apply blast |
|
1401 apply(simp only:) |
|
1402 apply(subgoal_tac "((\<forall>r\<in>set (v # vb # vc). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc))) = ((\<forall>r\<in>set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc)))") |
|
1403 prefer 2 |
|
1404 apply blast |
|
1405 apply(simp only:) |
|
1406 apply(subgoal_tac "((\<forall>r \<in> set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc))) = (\<forall> r \<in> set (v # vb # vc). agood r) ") |
|
1407 prefer 2 |
|
1408 apply(subgoal_tac "distinct (map erase (v # vb # vc)) = True") |
|
1409 prefer 2 |
|
1410 apply blast |
|
1411 prefer 2 |
|
1412 apply force |
|
1413 apply simp |
|
1414 done |
|
1415 |
|
1416 |
|
1417 lemma nn11a: |
|
1418 assumes "anonalt r" |
|
1419 shows "anonalt (fuse bs r)" |
|
1420 using assms |
|
1421 apply(induct r) |
|
1422 apply(auto) |
|
1423 done |
|
1424 |
|
1425 |
|
1426 |
|
1427 |
|
1428 lemma flts0: |
|
1429 assumes "r \<noteq> AZERO" "anonalt r" |
|
1430 shows "flts [r] \<noteq> []" |
|
1431 using assms |
|
1432 apply(induct r) |
|
1433 apply(simp_all) |
|
1434 done |
|
1435 |
|
1436 lemma flts1: |
|
1437 assumes "agood r" |
|
1438 shows "flts [r] \<noteq> []" |
|
1439 using assms |
|
1440 apply(induct r) |
|
1441 apply(simp_all) |
|
1442 apply(case_tac x2a) |
|
1443 apply(simp) |
|
1444 apply(simp) |
|
1445 done |
|
1446 |
|
1447 lemma flts2: |
|
1448 assumes "agood r" |
|
1449 shows "\<forall>r' \<in> set (flts [r]). agood r' \<and> anonalt r'" |
|
1450 using assms |
|
1451 apply(induct r) |
|
1452 apply(simp) |
|
1453 apply(simp) |
|
1454 apply(simp) |
|
1455 prefer 2 |
|
1456 apply(simp) |
|
1457 apply(auto)[1] |
|
1458 apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) good_fuse) |
|
1459 apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) nn11a) |
|
1460 apply fastforce |
|
1461 apply(simp) |
|
1462 done |
|
1463 |
|
1464 |
|
1465 lemma flts3: |
|
1466 assumes "\<forall>r \<in> set rs. agood r \<or> r = AZERO" |
|
1467 shows "\<forall>r \<in> set (flts rs). agood r" |
|
1468 using assms |
|
1469 apply(induct rs arbitrary: rule: flts.induct) |
|
1470 apply(simp_all) |
|
1471 by (metis SizeBound3.flts2 UnE append.right_neutral flts.simps(1) flts.simps(3) list.set_map) |
|
1472 |
|
1473 |
|
1474 lemma flts3b: |
|
1475 assumes "\<exists>r\<in>set rs. agood r" |
|
1476 shows "flts rs \<noteq> []" |
|
1477 using assms |
|
1478 apply(induct rs arbitrary: rule: flts.induct) |
|
1479 apply(simp) |
|
1480 apply(simp) |
|
1481 apply(simp) |
|
1482 apply(auto) |
|
1483 done |
|
1484 |
|
1485 lemma k0a: |
|
1486 shows "flts [AALTs bs rs] = map (fuse bs) rs" |
|
1487 apply(simp) |
|
1488 done |
|
1489 |
|
1490 |
|
1491 lemma k0b: |
|
1492 assumes "anonalt r" "r \<noteq> AZERO" |
|
1493 shows "flts [r] = [r]" |
|
1494 using assms |
|
1495 apply(case_tac r) |
|
1496 apply(simp_all) |
|
1497 done |
|
1498 |
|
1499 lemma flts4_nogood: |
|
1500 shows "bsimp_AALTs bs0 rs = AZERO \<Longrightarrow> \<forall>r \<in> set rs. \<not> agood r" |
|
1501 by (metis SizeBound3.flts3b arexp.distinct(7) bsimp_AALTs.elims flts.simps(1) flts.simps(2) fuse_anything_doesnt_matter rerase.simps(1) rerase_preimage) |
|
1502 |
|
1503 lemma flts4_append: |
|
1504 shows "bsimp_AALTs bs0 (rs @ flts rsa) = AZERO \<Longrightarrow> bsimp_AALTs bs0 rs = AZERO" |
|
1505 by (metis append_is_Nil_conv arexp.simps(13) bsimp_AALTs.elims bsimp_AALTs.simps(1) butlast_append butlast_snoc) |
|
1506 |
|
1507 lemma flts4: |
|
1508 assumes "bsimp_AALTs bs (flts rs) = AZERO" |
|
1509 shows "\<forall>r \<in> set rs. \<not> agood r" |
|
1510 using assms |
|
1511 apply(induct rs arbitrary: bs rule: flts.induct) |
|
1512 apply(auto) |
|
1513 defer |
|
1514 apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b anonalt.simps(1) anonalt.simps(2)) |
|
1515 apply (metis agood.simps(1) agood.simps(2) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject) |
|
1516 apply (metis agood.simps(1) agood.simps(3) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject) |
|
1517 apply (metis agood.simps(1) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject) |
|
1518 apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject) |
|
1519 apply (metis agood.simps(1) agood.simps(33) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject) |
|
1520 by (metis SizeBound3.bbbbs SizeBound3.k0a arexp.simps(13) flts4_append) |
|
1521 |
|
1522 |
|
1523 lemma flts_nil: |
|
1524 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> |
|
1525 agood (bsimp y) \<or> bsimp y = AZERO" |
|
1526 and "\<forall>r\<in>set rs. \<not> agood (bsimp r)" |
|
1527 shows "flts (map bsimp rs) = []" |
|
1528 using assms |
|
1529 apply(induct rs) |
|
1530 apply(simp) |
|
1531 apply(simp) |
|
1532 apply(subst k0) |
|
1533 apply(simp) |
|
1534 by force |
|
1535 |
|
1536 lemma flts_nil2: |
|
1537 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> |
|
1538 agood (bsimp y) \<or> bsimp y = AZERO" |
|
1539 and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO" |
|
1540 shows "flts (map bsimp rs) = []" |
|
1541 using assms |
|
1542 apply(induct rs arbitrary: bs) |
|
1543 apply(simp) |
|
1544 apply(simp) |
|
1545 apply(subst k0) |
|
1546 apply(simp) |
|
1547 apply(subst (asm) k0) |
|
1548 apply(auto) |
|
1549 apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1)) |
|
1550 by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1)) |
|
1551 |
|
1552 |
|
1553 |
|
1554 lemma good_SEQ: |
|
1555 assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs" |
|
1556 shows "agood (ASEQ bs r1 r2) = (agood r1 \<and> agood r2)" |
|
1557 using assms |
|
1558 apply(case_tac r1) |
|
1559 apply(simp_all) |
|
1560 apply(case_tac r2) |
|
1561 apply(simp_all) |
|
1562 apply(case_tac r2) |
|
1563 apply(simp_all) |
|
1564 apply(case_tac r2) |
|
1565 apply(simp_all) |
|
1566 apply(case_tac r2) |
|
1567 apply(simp_all) |
|
1568 done |
|
1569 |
|
1570 lemma asize0: |
|
1571 shows "0 < asize r" |
|
1572 apply(induct r) |
|
1573 apply(auto) |
|
1574 done |
|
1575 |
|
1576 lemma nn1qq: |
|
1577 assumes "anonnested (AALTs bs rs)" |
|
1578 shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs" |
|
1579 using assms |
|
1580 apply(induct rs rule: flts.induct) |
|
1581 apply(auto) |
|
1582 done |
|
1583 |
|
1584 lemma nn1c: |
|
1585 assumes "\<forall>r \<in> set rs. anonnested r" |
|
1586 shows "\<forall>r \<in> set (flts rs). anonalt r" |
|
1587 using assms |
|
1588 apply(induct rs rule: flts.induct) |
|
1589 apply(auto) |
|
1590 apply(rule nn11a) |
|
1591 by (metis nn1qq anonalt.elims(3)) |
|
1592 |
|
1593 lemma n0: |
|
1594 shows "anonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. anonalt r)" |
|
1595 apply(induct rs arbitrary: bs) |
|
1596 apply(auto) |
|
1597 apply (metis SizeBound3.nn1qq anonalt.elims(3) list.set_intros(1)) |
|
1598 apply (metis SizeBound3.bbbbs1 SizeBound3.nn1qq list.set_intros(2)) |
|
1599 by (metis anonalt.elims(2) anonnested.simps(3) anonnested.simps(4) anonnested.simps(5) anonnested.simps(6) anonnested.simps(7)) |
|
1600 |
|
1601 |
|
1602 |
|
1603 lemma nn1bb: |
|
1604 assumes "\<forall>r \<in> set rs. anonalt r" |
|
1605 shows "anonnested (bsimp_AALTs bs rs)" |
|
1606 using assms |
|
1607 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
1608 apply(auto) |
|
1609 apply (metis nn11a anonalt.simps(1) anonnested.elims(3)) |
|
1610 using n0 by auto |
|
1611 |
|
1612 lemma nn10: |
|
1613 assumes "anonnested (AALTs cs rs)" |
|
1614 shows "anonnested (AALTs (bs @ cs) rs)" |
|
1615 using assms |
|
1616 apply(induct rs arbitrary: cs bs) |
|
1617 apply(simp_all) |
|
1618 apply(case_tac a) |
|
1619 apply(simp_all) |
|
1620 done |
|
1621 |
|
1622 lemma nn1a: |
|
1623 assumes "anonnested r" |
|
1624 shows "anonnested (fuse bs r)" |
|
1625 using assms |
|
1626 apply(induct bs r arbitrary: rule: fuse.induct) |
|
1627 apply(simp_all add: nn10) |
|
1628 done |
|
1629 |
|
1630 lemma dB_keeps_property: |
|
1631 shows "(\<forall>r \<in> set rs. P r) \<longrightarrow> (\<forall>r \<in> set (distinctBy rs erase rset). P r)" |
|
1632 apply(induct rs arbitrary: rset) |
|
1633 apply simp+ |
|
1634 done |
|
1635 |
|
1636 lemma dB_filters_out: |
|
1637 shows "erase a \<in> rset \<Longrightarrow> a \<notin> set (distinctBy rs erase (rset))" |
|
1638 apply(induct rs arbitrary: rset) |
|
1639 apply simp |
|
1640 apply(case_tac "a = aa") |
|
1641 apply simp+ |
|
1642 done |
|
1643 |
|
1644 lemma dB_will_be_distinct: |
|
1645 shows "distinct (distinctBy rs erase (insert (erase a) rset)) \<Longrightarrow> distinct (a # (distinctBy rs erase (insert (erase a) rset)))" |
|
1646 using dB_filters_out by force |
|
1647 |
|
1648 |
|
1649 |
|
1650 lemma dB_does_the_job2: |
|
1651 shows "distinct (distinctBy rs erase rset)" |
|
1652 apply(induct rs arbitrary: rset) |
|
1653 apply simp |
|
1654 apply(case_tac "erase a \<in> rset") |
|
1655 apply simp |
|
1656 apply(drule_tac x = "insert (erase a) rset" in meta_spec) |
|
1657 apply(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)") |
|
1658 apply(simp only:) |
|
1659 using dB_will_be_distinct apply presburger |
|
1660 by auto |
|
1661 |
|
1662 lemma dB_does_more_job: |
|
1663 shows "distinct (map erase (distinctBy rs erase rset))" |
|
1664 apply(induct rs arbitrary:rset) |
|
1665 apply simp |
|
1666 apply(case_tac "erase a \<in> rset") |
|
1667 apply simp+ |
|
1668 using dB_filters_out by force |
|
1669 |
|
1670 lemma dB_mono2: |
|
1671 shows "rset \<subseteq> rset' \<Longrightarrow> distinctBy rs erase rset = [] \<Longrightarrow> distinctBy rs erase rset' = []" |
|
1672 apply(induct rs arbitrary: rset rset') |
|
1673 apply simp+ |
|
1674 by (meson in_mono list.discI) |
|
1675 |
|
1676 |
|
1677 lemma nn1b: |
|
1678 shows "anonnested (bsimp r)" |
|
1679 apply(induct r) |
|
1680 apply(simp_all) |
|
1681 apply(case_tac "bsimp r1 = AZERO") |
|
1682 apply(simp) |
|
1683 apply(case_tac "bsimp r2 = AZERO") |
|
1684 apply(simp) |
|
1685 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1686 apply(auto)[1] |
|
1687 apply (simp add: nn1a) |
|
1688 apply(subst bsimp_ASEQ1) |
|
1689 apply(auto) |
|
1690 apply(rule nn1bb) |
|
1691 apply(auto) |
|
1692 apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r") |
|
1693 prefer 2 |
|
1694 apply (metis (mono_tags, lifting) SizeBound3.nn1c image_iff list.set_map) |
|
1695 apply(subgoal_tac "\<forall>r \<in> set (distinctBy (flts (map bsimp x2a)) erase {}). anonalt r") |
|
1696 prefer 2 |
|
1697 using dB_keeps_property apply presburger |
|
1698 by blast |
|
1699 |
|
1700 |
|
1701 lemma induct_smaller_elem_list: |
|
1702 shows "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))" |
|
1703 apply(induct list) |
|
1704 apply simp+ |
|
1705 by fastforce |
|
1706 |
|
1707 lemma no0s_fltsbsimp: |
|
1708 shows "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO" |
|
1709 oops |
|
1710 |
|
1711 lemma flts_all0s: |
|
1712 shows "\<forall>r \<in> set rs. r = AZERO \<Longrightarrow> flts rs = []" |
|
1713 apply(induct rs) |
|
1714 apply simp+ |
|
1715 done |
|
1716 |
|
1717 |
|
1718 |
|
1719 |
|
1720 |
|
1721 lemma good1: |
|
1722 shows "agood (bsimp a) \<or> bsimp a = AZERO" |
|
1723 apply(induct a taking: asize rule: measure_induct) |
|
1724 apply(case_tac x) |
|
1725 apply(simp) |
|
1726 apply(simp) |
|
1727 apply(simp) |
|
1728 prefer 3 |
|
1729 apply(simp) |
|
1730 prefer 2 |
|
1731 (* AALTs case *) |
|
1732 apply(simp only:) |
|
1733 apply(case_tac "x52") |
|
1734 apply(simp) |
|
1735 (* AALTs list at least one - case *) |
|
1736 apply(simp only: ) |
|
1737 apply(frule_tac x="a" in spec) |
|
1738 apply(drule mp) |
|
1739 apply(simp) |
|
1740 (* either first element is agood, or AZERO *) |
|
1741 apply(erule disjE) |
|
1742 prefer 2 |
|
1743 apply(simp) |
|
1744 (* in the AZERO case, the size is smaller *) |
|
1745 apply(drule_tac x="AALTs x51 list" in spec) |
|
1746 apply(drule mp) |
|
1747 apply(simp add: asize0) |
|
1748 apply(subst (asm) bsimp.simps) |
|
1749 apply(subst (asm) bsimp.simps) |
|
1750 apply(assumption) |
|
1751 (* in the agood case *) |
|
1752 apply(frule_tac x="AALTs x51 list" in spec) |
|
1753 apply(drule mp) |
|
1754 apply(simp add: asize0) |
|
1755 apply(erule disjE) |
|
1756 apply(rule disjI1) |
|
1757 apply(simp add: good0) |
|
1758 apply(subst good0) |
|
1759 using SizeBound3.flts3b distinctBy.elims apply force |
|
1760 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt") |
|
1761 prefer 2 |
|
1762 apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) |
|
1763 using dB_keeps_property apply presburger |
|
1764 using dB_does_more_job apply presburger |
|
1765 apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood") |
|
1766 using dB_keeps_property apply presburger |
|
1767 apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)") |
|
1768 using SizeBound3.flts3 apply blast |
|
1769 |
|
1770 apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (asize a + sum_list (map asize list))") |
|
1771 |
|
1772 apply simp |
|
1773 |
|
1774 apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))") |
|
1775 |
|
1776 apply fastforce |
|
1777 using induct_smaller_elem_list apply blast |
|
1778 |
|
1779 |
|
1780 |
|
1781 |
|
1782 apply simp |
|
1783 apply(subgoal_tac "agood (bsimp a)") |
|
1784 prefer 2 |
|
1785 apply blast |
|
1786 apply(subgoal_tac "\<forall>r \<in> (set (map bsimp list)). r = AZERO \<or> agood r") |
|
1787 prefer 2 |
|
1788 apply (metis add_Suc_right image_iff induct_smaller_elem_list list.set_map trans_less_add2) |
|
1789 apply(subgoal_tac "\<not>(\<exists> r\<in>set (map bsimp list). agood r)") |
|
1790 prefer 2 |
|
1791 apply (metis SizeBound3.flts3 SizeBound3.flts3b distinctBy.elims empty_iff flts4_nogood list.set_intros(1)) |
|
1792 apply(subgoal_tac "\<forall>r \<in> set (map bsimp list). r = AZERO") |
|
1793 prefer 2 |
|
1794 apply blast |
|
1795 apply(subgoal_tac "flts (map bsimp list) = []") |
|
1796 prefer 2 |
|
1797 using flts_all0s apply presburger |
|
1798 apply (smt (verit, del_insts) SizeBound3.flts2 SizeBound3.good0 SizeBound3.k0 dB_does_more_job dB_keeps_property distinctBy.simps(1) flts.simps(1)) |
|
1799 apply(subgoal_tac "agood (bsimp x42) \<or> bsimp x42 = AZERO") |
|
1800 apply(subgoal_tac "agood (bsimp x43) \<or> bsimp x43 = AZERO") |
|
1801 apply(case_tac "bsimp x42 = AZERO") |
|
1802 apply simp |
|
1803 apply(case_tac "bsimp x43 = AZERO") |
|
1804 apply simp |
|
1805 apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'") |
|
1806 apply(erule exE) |
|
1807 apply simp |
|
1808 using good_fuse apply presburger |
|
1809 apply simp |
|
1810 apply(subgoal_tac "bsimp_ASEQ x41 (bsimp x42) (bsimp x43) = ASEQ x41 (bsimp x42) (bsimp x43)") |
|
1811 prefer 2 |
|
1812 using bsimp_ASEQ1 apply presburger |
|
1813 using SizeBound3.good_SEQ apply presburger |
|
1814 using asize.simps(5) less_add_Suc2 apply presburger |
|
1815 by simp |
|
1816 |
|
1817 |
|
1818 |
|
1819 |
|
1820 |
|
1821 |
|
1822 lemma good1a: |
|
1823 assumes "L (erase a) \<noteq> {}" |
|
1824 shows "agood (bsimp a)" |
|
1825 using good1 assms |
|
1826 using L_bsimp_erase by force |
|
1827 |
|
1828 |
|
1829 |
|
1830 lemma flts_append: |
|
1831 "flts (xs1 @ xs2) = flts xs1 @ flts xs2" |
|
1832 apply(induct xs1 arbitrary: xs2 rule: rev_induct) |
|
1833 apply(auto) |
|
1834 apply(case_tac xs) |
|
1835 apply(auto) |
|
1836 apply(case_tac x) |
|
1837 apply(auto) |
|
1838 apply(case_tac x) |
|
1839 apply(auto) |
|
1840 done |
|
1841 |
|
1842 lemma g1: |
|
1843 assumes "agood (bsimp_AALTs bs rs)" |
|
1844 shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)" |
|
1845 using assms |
|
1846 apply(induct rs arbitrary: bs) |
|
1847 apply(simp) |
|
1848 apply(case_tac rs) |
|
1849 apply(simp only:) |
|
1850 apply(simp) |
|
1851 apply(case_tac list) |
|
1852 apply(simp) |
|
1853 by simp |
|
1854 |
|
1855 lemma flts_0: |
|
1856 assumes "anonnested (AALTs bs rs)" |
|
1857 shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO" |
|
1858 using assms |
|
1859 apply(induct rs arbitrary: bs rule: flts.induct) |
|
1860 apply(simp) |
|
1861 apply(simp) |
|
1862 defer |
|
1863 apply(simp) |
|
1864 apply(simp) |
|
1865 apply(simp) |
|
1866 apply(simp) |
|
1867 apply(rule ballI) |
|
1868 apply(simp) |
|
1869 done |
|
1870 |
|
1871 lemma flts_0a: |
|
1872 assumes "anonnested (AALTs bs rs)" |
|
1873 shows "AZERO \<notin> set (flts rs)" |
|
1874 using assms |
|
1875 using flts_0 by blast |
|
1876 |
|
1877 lemma qqq1: |
|
1878 shows "AZERO \<notin> set (flts (map bsimp rs))" |
|
1879 by (metis ex_map_conv flts3 agood.simps(1) good1) |
|
1880 |
|
1881 |
|
1882 fun nonazero :: "arexp \<Rightarrow> bool" |
|
1883 where |
|
1884 "nonazero AZERO = False" |
|
1885 | "nonazero r = True" |
|
1886 |
|
1887 lemma flts_concat: |
|
1888 shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)" |
|
1889 apply(induct rs) |
|
1890 apply(auto) |
|
1891 apply(subst k0) |
|
1892 apply(simp) |
|
1893 done |
|
1894 |
|
1895 lemma flts_single1: |
|
1896 assumes "anonalt r" "nonazero r" |
|
1897 shows "flts [r] = [r]" |
|
1898 using assms |
|
1899 apply(induct r) |
|
1900 apply(auto) |
|
1901 done |
|
1902 |
|
1903 lemma flts_qq: |
|
1904 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> agood y \<longrightarrow> bsimp y = y" |
|
1905 "\<forall>r'\<in>set rs. agood r' \<and> anonalt r'" |
|
1906 shows "flts (map bsimp rs) = rs" |
|
1907 using assms |
|
1908 apply(induct rs) |
|
1909 apply(simp) |
|
1910 apply(simp) |
|
1911 apply(subst k0) |
|
1912 apply(subgoal_tac "flts [bsimp a] = [a]") |
|
1913 prefer 2 |
|
1914 apply(drule_tac x="a" in spec) |
|
1915 apply(drule mp) |
|
1916 apply(simp) |
|
1917 apply(auto)[1] |
|
1918 using agood.simps(1) k0b apply blast |
|
1919 apply(auto)[1] |
|
1920 done |
|
1921 |
|
1922 lemma test: |
|
1923 assumes "agood r" |
|
1924 shows "bsimp r = r" |
|
1925 using assms |
|
1926 apply(induct r taking: "asize" rule: measure_induct) |
|
1927 apply(erule agood.elims) |
|
1928 apply(simp_all) |
|
1929 apply(subst k0) |
|
1930 apply(subst (2) k0) |
|
1931 apply(subst flts_qq) |
|
1932 apply(auto)[1] |
|
1933 apply(auto)[1] |
|
1934 oops |
|
1935 |
|
1936 |
|
1937 |
|
1938 lemma bsimp_idem: |
|
1939 shows "bsimp (bsimp r) = bsimp r" |
|
1940 using test good1 |
|
1941 oops |
|
1942 |
|
1943 |
|
1944 lemma erase_preimage1: |
|
1945 assumes "anonalt r" |
|
1946 shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs" |
|
1947 apply(case_tac r) |
|
1948 apply simp+ |
|
1949 using anonalt.simps(1) assms apply presburger |
|
1950 by fastforce |
|
1951 |
|
1952 lemma erase_preimage_char: |
|
1953 assumes "anonalt r" |
|
1954 shows "erase r = CH c \<Longrightarrow> \<exists>bs. r = ACHAR bs c" |
|
1955 apply(case_tac r) |
|
1956 apply simp+ |
|
1957 using assms apply fastforce |
|
1958 by simp |
|
1959 |
|
1960 lemma erase_preimage_seq: |
|
1961 assumes "anonalt r" |
|
1962 shows "erase r = SEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> erase a1 = r1 \<and> erase a2 = r2" |
|
1963 apply(case_tac r) |
|
1964 apply simp+ |
|
1965 using assms apply fastforce |
|
1966 by simp |
|
1967 |
|
1968 lemma rerase_preimage_seq: |
|
1969 assumes "anonalt r" |
|
1970 shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2 " |
|
1971 using rerase_preimage4 by presburger |
|
1972 |
|
1973 lemma seq_recursive_equality: |
|
1974 shows "\<lbrakk>r1 = a1; r2 = a2\<rbrakk> \<Longrightarrow> SEQ r1 r2 = SEQ a1 a2" |
|
1975 by meson |
|
1976 |
|
1977 lemma almost_identical_image: |
|
1978 assumes "agood r" "\<forall>r \<in> rset. agood r" |
|
1979 shows "erase r \<in> erase ` rset \<Longrightarrow> \<exists>r' \<in> rset. erase r' = erase r" |
|
1980 by auto |
|
1981 |
|
1982 lemma goodalts_never_change: |
|
1983 assumes "r = AALTs bs rs" "agood r" |
|
1984 shows "\<exists>r1 r2. erase r = ALT r1 r2" |
|
1985 by (metis agood.simps(4) agood.simps(5) assms(1) assms(2) bmkepss.cases erase.simps(6)) |
|
1986 |
|
1987 |
|
1988 fun shape_preserving :: "arexp \<Rightarrow> bool" where |
|
1989 "shape_preserving AZERO = True" |
|
1990 | "shape_preserving (AONE bs) = True" |
|
1991 | "shape_preserving (ACHAR bs c) = True" |
|
1992 | "shape_preserving (AALTs bs []) = False" |
|
1993 | "shape_preserving (AALTs bs [a]) = False" |
|
1994 | "shape_preserving (AALTs bs (a1 # a2 # rs)) = (\<forall>r \<in> set (a1 # a2 # rs). shape_preserving r)" |
|
1995 | "shape_preserving (ASEQ bs r1 r2) = (shape_preserving r1 \<and> shape_preserving r2)" |
|
1996 | "shape_preserving (ASTAR bs r) = shape_preserving r" |
|
1997 |
|
1998 |
|
1999 lemma good_shape_preserving: |
|
2000 assumes "\<nexists>bs r0. r = ASTAR bs r0" |
|
2001 shows "agood r \<Longrightarrow> shape_preserving r" |
|
2002 using assms |
|
2003 |
|
2004 apply(induct r) |
|
2005 prefer 6 |
|
2006 |
|
2007 apply blast |
|
2008 apply simp |
|
2009 |
|
2010 oops |
|
2011 |
|
2012 |
|
2013 |
|
2014 |
|
2015 |
|
2016 lemma shadow_arexp_rerase_erase: |
|
2017 shows "\<lbrakk>agood r; agood r'; erase r = erase r'\<rbrakk> \<Longrightarrow> rerase r = rerase r'" |
|
2018 apply(induct r ) |
|
2019 apply simp |
|
2020 apply(induct r') |
|
2021 apply simp+ |
|
2022 apply (metis goodalts_never_change rexp.distinct(15)) |
|
2023 apply simp+ |
|
2024 apply (metis anonalt.elims(3) erase_preimage_char goodalts_never_change rerase.simps(3) rexp.distinct(21)) |
|
2025 apply(induct r') |
|
2026 apply simp |
|
2027 apply simp |
|
2028 apply simp |
|
2029 apply(subgoal_tac "agood r1") |
|
2030 prefer 2 |
|
2031 apply (metis SizeBound3.good_SEQ agood.simps(10) agood.simps(11) agood.simps(2) agood.simps(3) agood.simps(33) agood.simps(7) bsimp.cases) |
|
2032 apply(subgoal_tac "agood r2") |
|
2033 apply(subgoal_tac "agood r'1") |
|
2034 apply(subgoal_tac "agood r'2") |
|
2035 apply(subgoal_tac "rerase r'1 = rerase r1") |
|
2036 apply(subgoal_tac "rerase r'2 = rerase r2") |
|
2037 |
|
2038 using rerase.simps(5) apply presburger |
|
2039 sledgehammer |
|
2040 |
|
2041 |
|
2042 lemma rerase_erase_good: |
|
2043 assumes "agood r" "\<forall>r \<in> rset. agood r" |
|
2044 shows "erase r \<in> erase ` rset \<Longrightarrow> rerase r \<in> rerase ` rset" |
|
2045 using assms |
|
2046 apply(case_tac r) |
|
2047 apply simp+ |
|
2048 oops |
|
2049 |
|
2050 lemma rerase_erase_both: |
|
2051 assumes "\<forall>r \<in> rset. agood r" "agood r" |
|
2052 shows "(rerase r \<in> (rerase ` rset)) \<longleftrightarrow> (erase r \<in> (erase ` rset))" |
|
2053 using assms |
|
2054 apply(induct r ) |
|
2055 apply force |
|
2056 apply simp |
|
2057 apply(case_tac "RONE \<in> rerase ` rset") |
|
2058 apply(subgoal_tac "\<exists>bs. (AONE bs) \<in> rset") |
|
2059 apply (metis erase.simps(2) rev_image_eqI) |
|
2060 apply (metis image_iff rerase_preimage2) |
|
2061 apply(subgoal_tac "\<nexists>bs. (AONE bs) \<in> rset") |
|
2062 apply(subgoal_tac "ONE \<notin> erase ` rset") |
|
2063 |
|
2064 apply blast |
|
2065 sledgehammer |
|
2066 apply (metis erase_preimage1 image_iff) |
|
2067 apply (metis rerase.simps(2) rev_image_eqI) |
|
2068 apply (smt (verit, best) erase.simps(3) erase_preimage_char image_iff rerase.simps(3) rerase_preimage3) |
|
2069 (* apply simp |
|
2070 apply(subgoal_tac "(RSEQ (rerase r1) (rerase r2) \<in> rerase ` rset) \<Longrightarrow> (SEQ (erase r1) (erase r2) \<in> erase ` rset)") |
|
2071 prefer 2 |
|
2072 apply(subgoal_tac "\<exists>bs a1 a2. (ASEQ bs a1 a2) \<in> rset \<and> rerase a1 = rerase r1 \<and> rerase a2 = rerase r2") |
|
2073 prefer 2 |
|
2074 apply (metis (full_types) image_iff rerase_preimage4) |
|
2075 apply(erule exE)+ |
|
2076 apply(subgoal_tac "erase (ASEQ bs a1 a2) \<in> (erase ` rset) ") |
|
2077 apply(subgoal_tac "SEQ (erase a1) (erase a2) \<in> (erase ` rset)") |
|
2078 apply(subgoal_tac "SEQ (erase a1) (erase a2) = SEQ (erase r1) (erase r2)") |
|
2079 apply metis |
|
2080 apply(erule conjE)+*) |
|
2081 apply(drule_tac x = "rset" in meta_spec)+ |
|
2082 |
|
2083 |
|
2084 |
|
2085 |
|
2086 oops |
|
2087 |
|
2088 |
|
2089 lemma rerase_pushin1_general: |
|
2090 assumes "\<forall>r \<in> set rs. agood r" |
|
2091 shows "map rerase (distinctBy rs erase (erase ` rset)) = rdistinct (map rerase rs) (rerase ` rset)" |
|
2092 apply(induct rs arbitrary: rset) |
|
2093 apply simp+ |
|
2094 apply(case_tac "erase a \<in> erase ` rset") |
|
2095 apply simp |
|
2096 |
|
2097 |
|
2098 |
|
2099 oops |
|
2100 |
|
2101 lemma rerase_erase: |
|
2102 assumes "\<forall>r \<in> set as. agood r \<and> anonalt r" |
|
2103 shows "rdistinct (map rerase as) (rerase ` rset) = map rerase (distinctBy as erase (erase ` rset))" |
|
2104 using assms |
|
2105 apply(induct as) |
|
2106 apply simp+ |
|
2107 |
|
2108 sorry |
|
2109 |
|
2110 |
|
2111 lemma rerase_pushin1: |
|
2112 assumes "\<forall>r \<in> set rs. anonalt r \<and> agood r" |
|
2113 shows "map rerase (distinctBy rs erase {}) = rdistinct (map rerase rs) {}" |
|
2114 apply(insert rerase_erase) |
|
2115 by (metis assms image_empty) |
|
2116 |
|
2117 |
|
2118 |
|
2119 |
|
2120 |
|
2121 |
|
2122 |
|
2123 lemma nonalt_flts : shows |
|
2124 "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO" |
|
2125 using SizeBound3.qqq1 by force |
|
2126 |
|
2127 |
|
2128 |
|
2129 |
|
2130 lemma rerase_list_ders: |
|
2131 shows "\<And>x1 x2a. |
|
2132 (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> rerase (bsimp x2aa) = rsimp (rerase x2aa)) \<Longrightarrow> |
|
2133 (map rerase (distinctBy (flts (map bsimp x2a)) erase {})) = (rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {})" |
|
2134 apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r ") |
|
2135 prefer 2 |
|
2136 apply (metis SizeBound3.nn1b SizeBound3.nn1c ex_map_conv) |
|
2137 sledgehammer |
|
2138 |
|
2139 sorry |
|
2140 |
|
2141 |
|
2142 lemma simp_rerase: |
|
2143 shows "rerase (bsimp a) = rsimp (rerase a)" |
|
2144 apply(induct a) |
|
2145 apply simp+ |
|
2146 using rerase_bsimp_ASEQ apply presburger |
|
2147 apply simp |
|
2148 apply(subst rerase_bsimp_AALTs) |
|
2149 apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) erase {}) = rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {}") |
|
2150 apply simp |
|
2151 using rerase_list_ders apply blast |
|
2152 by simp |
|
2153 |
|
2154 lemma rders_simp_size: |
|
2155 shows " rders_simp (rerase r) s = rerase (bders_simp r s)" |
|
2156 apply(induct s rule: rev_induct) |
|
2157 apply simp |
|
2158 apply(subst rders_simp_append) |
|
2159 apply(subst bders_simp_append) |
|
2160 apply(subgoal_tac "rders_simp (rerase r ) xs = rerase (bders_simp r xs)") |
|
2161 apply(simp only:) |
|
2162 apply simp |
|
2163 apply (simp add: der_rerase2 simp_rerase) |
|
2164 by simp |
|
2165 |
|
2166 |
|
2167 |
|
2168 |
|
2169 corollary aders_simp_finiteness: |
|
2170 assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N" |
|
2171 shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N" |
|
2172 using assms |
|
2173 apply(subgoal_tac "\<forall>s. asize (bders_simp r s) = rsize (rerase (bders_simp r s))") |
|
2174 apply(erule exE) |
|
2175 apply(rule_tac x = "N" in exI) |
|
2176 using rders_simp_size apply auto[1] |
|
2177 using asize_rsize by auto |
|
2178 |
|
2179 theorem annotated_size_bound: |
|
2180 shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N" |
|
2181 apply(insert aders_simp_finiteness) |
|
2182 by (simp add: rders_simp_bounded) |
1175 |
2183 |
1176 end |
2184 end |