equal
deleted
inserted
replaced
575 where |
575 where |
576 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" |
576 "bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" |
577 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))" |
577 | "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (flts (map bsimp rs))" |
578 | "bsimp r = r" |
578 | "bsimp r = r" |
579 |
579 |
580 value "good (AALTs [] [AALTs [] [AONE []]])" |
|
581 value "bsimp (AALTs [] [AONE [], AALTs [] [AONE []]])" |
|
582 |
|
583 |
580 |
584 fun |
581 fun |
585 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
582 bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
586 where |
583 where |
587 "bders_simp r [] = r" |
584 "bders_simp r [] = r" |
1086 apply(auto) |
1083 apply(auto) |
1087 apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5)) |
1084 apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5)) |
1088 by (metis good.simps(4) good.simps(5) neq_Nil_conv) |
1085 by (metis good.simps(4) good.simps(5) neq_Nil_conv) |
1089 |
1086 |
1090 lemma good0: |
1087 lemma good0: |
1091 assumes "rs \<noteq> Nil" |
1088 assumes "rs \<noteq> Nil" |
1092 shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)" |
1089 shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)" |
1093 using assms |
1090 using assms |
1094 apply(induct bs rs rule: bsimp_AALTs.induct) |
1091 apply(induct bs rs rule: bsimp_AALTs.induct) |
1095 apply(auto simp add: good_fuse) |
1092 apply(auto simp add: good_fuse) |
1096 done |
1093 done |
1097 |
1094 |
1098 lemma good0a: |
1095 lemma good0a: |
1099 assumes "flts (map bsimp rs) \<noteq> Nil" |
1096 assumes "flts (map bsimp rs) \<noteq> Nil" |
1100 shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)" |
1097 shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)" |
1101 using assms |
1098 using assms |
1102 apply(simp) |
1099 apply(simp) |
1103 apply(rule good0) |
1100 apply(rule good0) |
1104 apply(simp) |
1101 apply(simp) |
1105 done |
1102 done |
1106 |
1103 |
1107 lemma flts0: |
1104 lemma flts0: |
1108 assumes "r \<noteq> AZERO" "nonalt r" |
1105 assumes "r \<noteq> AZERO" "nonalt r" |
1109 shows "flts [r] \<noteq> []" |
1106 shows "flts [r] \<noteq> []" |
1281 apply(simp) |
1278 apply(simp) |
1282 apply(case_tac list) |
1279 apply(case_tac list) |
1283 apply(simp) |
1280 apply(simp) |
1284 by simp |
1281 by simp |
1285 |
1282 |
1286 lemma flts_idem: |
|
1287 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> |
|
1288 bsimp (bsimp y) = bsimp y" |
|
1289 shows "map bsimp (flts (map bsimp rs)) = flts (map bsimp rs)" |
|
1290 using assms |
|
1291 apply(induct rs) |
|
1292 apply(simp) |
|
1293 apply(simp) |
|
1294 apply(subst k0) |
|
1295 apply(subst (2) k0) |
|
1296 apply(simp add: flts_append) |
|
1297 using good1 |
|
1298 apply - |
|
1299 apply(drule_tac x="a" in meta_spec) |
|
1300 apply(erule disjE) |
|
1301 prefer 2 |
|
1302 apply(simp) |
|
1303 using flts.simps |
|
1304 apply(case_tac a) |
|
1305 apply(simp_all) |
|
1306 defer |
|
1307 apply(drule g1) |
|
1308 apply(erule disjE) |
|
1309 apply(simp) |
|
1310 defer |
|
1311 apply(auto)[1] |
|
1312 |
|
1313 |
|
1314 |
|
1315 lemma flts_idem: |
|
1316 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> |
|
1317 bsimp (bsimp y) = bsimp y" |
|
1318 shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)" |
|
1319 using assms |
|
1320 apply(induct rs) |
|
1321 apply(simp) |
|
1322 apply(simp) |
|
1323 apply(subst k0) |
|
1324 apply(subst (2) k0) |
|
1325 apply(simp add: flts_append) |
|
1326 using good1 |
|
1327 apply - |
|
1328 apply(drule_tac x="a" in meta_spec) |
|
1329 apply(erule disjE) |
|
1330 prefer 2 |
|
1331 apply(simp) |
|
1332 using flts.simps |
|
1333 apply(case_tac a) |
|
1334 apply(simp_all) |
|
1335 defer |
|
1336 apply(drule g1) |
|
1337 apply(erule disjE) |
|
1338 apply(simp) |
|
1339 defer |
|
1340 apply(auto)[1] |
|
1341 |
|
1342 apply(subst g1) |
|
1343 apply(simp) |
|
1344 apply(simp) |
|
1345 apply (me tis (full_types) arexp.inject(4) bsimp_AALTs.simps(2) flts3a fuse_empty g1 list.distinct(1)) |
|
1346 |
|
1347 |
|
1348 |
|
1349 |
|
1350 apply(case_tac "bsimp a = AZERO") |
|
1351 apply(simp) |
|
1352 apply(case_tac "nonalt (bsimp a)") |
|
1353 thm k0 k0a k0b |
|
1354 apply(subst k0b) |
|
1355 apply(simp) |
|
1356 apply(simp) |
|
1357 apply(simp) |
|
1358 apply(subst k0b) |
|
1359 apply(simp) |
|
1360 apply(simp) |
|
1361 apply(simp) |
|
1362 apply(subst k0) |
|
1363 apply(subst k0b) |
|
1364 apply(simp) |
|
1365 apply(simp) |
|
1366 apply(simp) |
|
1367 apply(simp) |
|
1368 apply(simp add: k00) |
|
1369 apply(subst k0a2) |
|
1370 apply(simp) |
|
1371 apply(subst k0a2) |
|
1372 apply(simp) |
|
1373 apply(case_tac a) |
|
1374 apply(simp_all) |
|
1375 oops |
|
1376 |
|
1377 |
1283 |
1378 lemma flts_0: |
1284 lemma flts_0: |
1379 assumes "nonnested (AALTs bs rs)" |
1285 assumes "nonnested (AALTs bs rs)" |
1380 shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO" |
1286 shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO" |
1381 using assms |
1287 using assms |
1440 apply(case_tac rs) |
1346 apply(case_tac rs) |
1441 apply(simp) |
1347 apply(simp) |
1442 apply(simp) |
1348 apply(simp) |
1443 apply(case_tac list) |
1349 apply(case_tac list) |
1444 apply(simp) |
1350 apply(simp) |
1445 |
1351 oops |
1446 |
|
1447 apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO") |
|
1448 prefer 2 |
|
1449 apply(rule_tac bs="bs' @ bs1" in flts_0) |
|
1450 |
|
1451 |
|
1452 thm bsimp_AALTs_qq |
|
1453 apply(case_tac "1 < length rs") |
|
1454 apply(drule_tac bsimp_AALTs_qq) |
|
1455 apply(subgoal_tac "nonnested (AALTs bs rsa)") |
|
1456 prefer 2 |
|
1457 apply (metis nn1b) |
|
1458 apply(rule ballI) |
|
1459 apply(simp) |
|
1460 apply(drule_tac x="r" in meta_spec) |
|
1461 apply(simp) |
|
1462 (* HERE *) |
|
1463 apply(drule flts_0) |
|
1464 |
|
1465 |
|
1466 |
|
1467 apply(simp) |
|
1468 |
|
1469 |
|
1470 |
|
1471 |
|
1472 apply(subst |
|
1473 |
|
1474 apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) |
|
1475 |
|
1476 prefer 2 |
|
1477 |
|
1478 |
|
1479 apply(induct r arbitrary: rs bs bs' rule: bsimp.induct) |
|
1480 apply(auto) |
|
1481 apply(case_tac "bsimp r1 = AZERO") |
|
1482 apply simp |
|
1483 apply(case_tac "bsimp r2 = AZERO") |
|
1484 apply(simp) |
|
1485 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1486 apply(auto) |
|
1487 apply (simp add: bsimp_ASEQ0) |
|
1488 apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'") |
|
1489 apply(auto) |
|
1490 apply (simp add: bsimp_ASEQ2) |
|
1491 using bsimp_fuse apply fast force |
|
1492 apply (simp add: bsimp_ASEQ1) |
|
1493 |
|
1494 |
|
1495 |
|
1496 apply(subst |
|
1497 |
|
1498 apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) |
|
1499 |
|
1500 prefer 2 |
|
1501 |
|
1502 |
1352 |
1503 |
1353 |
1504 lemma ww1: |
1354 lemma ww1: |
1505 assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO" |
1355 assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO" |
1506 shows "r1 = r2" |
1356 shows "r1 = r2" |
1513 prefer 2 |
1363 prefer 2 |
1514 apply(simp) |
1364 apply(simp) |
1515 apply(simp) |
1365 apply(simp) |
1516 apply(auto) |
1366 apply(auto) |
1517 oops |
1367 oops |
|
1368 |
|
1369 fun nonazero :: "arexp \<Rightarrow> bool" |
|
1370 where |
|
1371 "nonazero AZERO = False" |
|
1372 | "nonazero r = True" |
|
1373 |
|
1374 lemma flts_concat: |
|
1375 shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)" |
|
1376 apply(induct rs) |
|
1377 apply(auto) |
|
1378 apply(subst k0) |
|
1379 apply(simp) |
|
1380 done |
|
1381 |
|
1382 lemma flts_single1: |
|
1383 assumes "nonalt r" "nonazero r" |
|
1384 shows "flts [r] = [r]" |
|
1385 using assms |
|
1386 apply(induct r) |
|
1387 apply(auto) |
|
1388 done |
|
1389 |
|
1390 lemma test: |
|
1391 assumes "good r" |
|
1392 shows "bsimp (r) = r" |
|
1393 using assms |
|
1394 apply(induct r) |
|
1395 apply(simp_all) |
|
1396 |
1518 |
1397 |
1519 lemma bsimp_idem: |
1398 lemma bsimp_idem: |
1520 shows "bsimp (bsimp r) = bsimp r" |
1399 shows "bsimp (bsimp r) = bsimp r" |
1521 apply(induct r taking: "asize" rule: measure_induct) |
1400 apply(induct r taking: "asize" rule: measure_induct) |
1522 apply(case_tac x) |
1401 apply(case_tac x) |
1540 apply(simp) |
1419 apply(simp) |
1541 apply(subst k0) |
1420 apply(subst k0) |
1542 apply(simp) |
1421 apply(simp) |
1543 apply(simp add: flts_append) |
1422 apply(simp add: flts_append) |
1544 apply(subst (2) k0) |
1423 apply(subst (2) k0) |
1545 |
1424 apply(subst (asm) k0) |
1546 apply(simp add: flts_append) |
1425 apply(simp) |
|
1426 apply(subgoal_tac "good (bsimp a) \<or> bsimp a = AZERO") |
|
1427 prefer 2 |
|
1428 using good1 apply blast |
|
1429 apply(erule disjE) |
|
1430 prefer 2 |
|
1431 apply(simp) |
|
1432 apply(drule_tac x="AALTs x51 list" in spec) |
|
1433 apply(drule mp) |
|
1434 apply(simp add: asize0) |
|
1435 apply(simp) |
|
1436 apply (simp add: bsimp_AALTs_qq) |
|
1437 apply(case_tac "nonalt (bsimp a)") |
|
1438 apply(subst flts_single1) |
|
1439 apply(simp) |
|
1440 using nonazero.elims(3) apply force |
|
1441 apply(simp) |
|
1442 apply(subst k0b) |
|
1443 apply(simp) |
|
1444 apply(auto)[1] |
|
1445 apply(subst k0b) |
|
1446 apply(simp) |
|
1447 apply(auto)[1] |
|
1448 apply(simp) |
|
1449 (* HERE *) |
|
1450 apply(subst (asm) flts_single1) |
|
1451 apply(simp) |
|
1452 apply(simp) |
|
1453 using nonazero.elims(3) apply force |
|
1454 apply(simp) |
|
1455 apply(subst (2) bsimp_AALTs_qq) |
|
1456 apply(auto)[1] |
|
1457 apply(subst bsimp_AALTs_qq) |
|
1458 apply(auto)[1] |
|
1459 apply(case_tac list) |
|
1460 apply(simp) |
|
1461 apply(simp) |
1547 |
1462 |
1548 prefer 2 |
1463 prefer 2 |
1549 apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> |
1464 apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> |
1550 length (flts (bsimp a # map bsimp list)) = 1") |
1465 length (flts (bsimp a # map bsimp list)) = 1") |
1551 prefer 2 |
1466 prefer 2 |