1385 using assms |
1422 using assms |
1386 apply(induct r) |
1423 apply(induct r) |
1387 apply(auto) |
1424 apply(auto) |
1388 done |
1425 done |
1389 |
1426 |
|
1427 lemma flts_qq: |
|
1428 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" |
|
1429 "\<forall>r'\<in>set rs. good r' \<and> nonalt r'" |
|
1430 shows "flts (map bsimp rs) = rs" |
|
1431 using assms |
|
1432 apply(induct rs) |
|
1433 apply(simp) |
|
1434 apply(simp) |
|
1435 apply(subst k0) |
|
1436 apply(subgoal_tac "flts [bsimp a] = [a]") |
|
1437 prefer 2 |
|
1438 apply(drule_tac x="a" in spec) |
|
1439 apply(drule mp) |
|
1440 apply(simp) |
|
1441 apply(auto)[1] |
|
1442 using good.simps(1) k0b apply blast |
|
1443 apply(auto)[1] |
|
1444 done |
|
1445 |
1390 lemma test: |
1446 lemma test: |
1391 assumes "good r" |
1447 assumes "good r" |
1392 shows "bsimp (r) = r" |
1448 shows "bsimp r = r" |
1393 using assms |
1449 using assms |
1394 apply(induct r) |
1450 apply(induct r taking: "asize" rule: measure_induct) |
|
1451 apply(erule good.elims) |
1395 apply(simp_all) |
1452 apply(simp_all) |
|
1453 apply(subst k0) |
|
1454 apply(subst (2) k0) |
|
1455 apply(subst flts_qq) |
|
1456 apply(auto)[1] |
|
1457 apply(auto)[1] |
|
1458 apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b) |
|
1459 apply force+ |
|
1460 apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2) |
|
1461 apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2) |
|
1462 apply force+ |
|
1463 apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2) |
|
1464 apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2) |
|
1465 apply force+ |
|
1466 done |
|
1467 |
|
1468 lemma test2: |
|
1469 assumes "good r" |
|
1470 shows "bsimp r = r" |
|
1471 using assms |
|
1472 apply(induct r taking: "asize" rule: measure_induct) |
|
1473 apply(case_tac x) |
|
1474 apply(simp_all) |
|
1475 defer |
|
1476 (* AALT case *) |
|
1477 apply(subgoal_tac "1 < length x52") |
|
1478 prefer 2 |
|
1479 apply(case_tac x52) |
|
1480 apply(simp) |
|
1481 apply(simp) |
|
1482 apply(case_tac list) |
|
1483 apply(simp) |
|
1484 apply(simp) |
|
1485 apply(subst bsimp_AALTs_qq) |
|
1486 prefer 2 |
|
1487 apply(subst flts_qq) |
|
1488 apply(auto)[1] |
|
1489 apply(auto)[1] |
|
1490 apply(case_tac x52) |
|
1491 apply(simp) |
|
1492 apply(simp) |
|
1493 apply(case_tac list) |
|
1494 apply(simp) |
|
1495 apply(simp) |
|
1496 apply(auto)[1] |
|
1497 apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff) |
|
1498 apply(simp) |
|
1499 apply(case_tac x52) |
|
1500 apply(simp) |
|
1501 apply(simp) |
|
1502 apply(case_tac list) |
|
1503 apply(simp) |
|
1504 apply(simp) |
|
1505 apply(subst k0) |
|
1506 apply(simp) |
|
1507 apply(subst (2) k0) |
|
1508 apply(simp) |
|
1509 apply (simp add: Suc_lessI flts1 one_is_add) |
|
1510 (* SEQ case *) |
|
1511 apply(case_tac "bsimp x42 = AZERO") |
|
1512 apply simp |
|
1513 apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1) |
|
1514 apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'") |
|
1515 apply(auto)[1] |
|
1516 defer |
|
1517 apply(case_tac "bsimp x43 = AZERO") |
|
1518 apply(simp) |
|
1519 apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2) |
|
1520 apply(auto) |
|
1521 apply (subst bsimp_ASEQ1) |
|
1522 apply(auto)[3] |
|
1523 apply(auto)[1] |
|
1524 apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1) |
|
1525 apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2) |
|
1526 apply (subst bsimp_ASEQ2) |
|
1527 apply(drule_tac x="x42" in spec) |
|
1528 apply(drule mp) |
|
1529 apply(simp) |
|
1530 apply(drule mp) |
|
1531 apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ) |
|
1532 apply(simp) |
|
1533 done |
1396 |
1534 |
1397 |
1535 |
1398 lemma bsimp_idem: |
1536 lemma bsimp_idem: |
1399 shows "bsimp (bsimp r) = bsimp r" |
1537 shows "bsimp (bsimp r) = bsimp r" |
1400 apply(induct r taking: "asize" rule: measure_induct) |
1538 using test good1 |
1401 apply(case_tac x) |
1539 by force |
1402 apply(simp) |
|
1403 apply(simp) |
|
1404 apply(simp) |
|
1405 prefer 3 |
|
1406 apply(simp) |
|
1407 apply(simp) |
|
1408 apply (simp add: bsimp_ASEQ_idem) |
|
1409 apply(clarify) |
|
1410 apply(case_tac x52) |
|
1411 apply(simp) |
|
1412 (* AALT case where rs is of the form _ # _ *) |
|
1413 apply(clarify) |
|
1414 apply(simp) |
|
1415 apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1") |
|
1416 prefer 2 |
|
1417 apply(subst bsimp_AALTs_qq) |
|
1418 apply(auto)[1] |
|
1419 apply(simp) |
|
1420 apply(subst k0) |
|
1421 apply(simp) |
|
1422 apply(simp add: flts_append) |
|
1423 apply(subst (2) k0) |
|
1424 apply(subst (asm) k0) |
|
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) |
|
1462 |
|
1463 prefer 2 |
|
1464 apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> |
|
1465 length (flts (bsimp a # map bsimp list)) = 1") |
|
1466 prefer 2 |
|
1467 apply(auto)[1] |
|
1468 using le_SucE apply blast |
|
1469 apply(erule disjE) |
|
1470 apply(simp) |
|
1471 apply(simp) |
|
1472 apply(subst k0) |
|
1473 apply(subst (2) k0) |
|
1474 apply(subst (asm) k0) |
|
1475 apply(simp) |
|
1476 apply(subgoal_tac "length (flts [bsimp a]) = 1 \<or> |
|
1477 length (flts (map bsimp list)) = 1") |
|
1478 prefer 2 |
|
1479 apply linarith |
|
1480 apply(erule disjE) |
|
1481 apply(simp) |
|
1482 prefer 2 |
|
1483 apply(simp) |
|
1484 apply(drule_tac x="AALTs x51 list" in spec) |
|
1485 apply(drule mp) |
|
1486 apply(simp) |
|
1487 using asize0 apply blast |
|
1488 apply(simp) |
|
1489 apply(frule_tac x="a" in spec) |
|
1490 apply(drule mp) |
|
1491 apply(simp) |
|
1492 apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]") |
|
1493 prefer 2 |
|
1494 apply (simp add: length_Suc_conv) |
|
1495 apply(clarify) |
|
1496 apply(simp only: ) |
|
1497 apply(case_tac "bsimp a = AZERO") |
|
1498 apply simp |
|
1499 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
1500 apply(clarify) |
|
1501 apply(simp) |
|
1502 apply(drule_tac x="AALTs bs rs" in spec) |
|
1503 apply(drule mp) |
|
1504 apply(simp) |
|
1505 apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1) |
|
1506 apply(simp) |
|
1507 |
|
1508 apply(subst ww) |
|
1509 apply(subst ww) |
|
1510 apply(frule_tac x="fuse x51 r" in spec) |
|
1511 apply(drule mp) |
|
1512 apply(simp) |
|
1513 apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons) |
|
1514 apply(case_tac "bsimp a = AZERO") |
|
1515 apply simp |
|
1516 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
1517 apply(clarify) |
|
1518 |
|
1519 defer |
|
1520 |
|
1521 apply( |
|
1522 apply(case_tac a) |
|
1523 apply(simp_all) |
|
1524 apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]") |
|
1525 prefer 2 |
|
1526 apply (simp add: length_Suc_conv) |
|
1527 apply auto[1] |
|
1528 apply(case_tac |
|
1529 apply(clarify) |
|
1530 |
|
1531 defer |
|
1532 apply(auto)[1] |
|
1533 |
|
1534 |
|
1535 apply(subst k0) |
|
1536 apply(subst (2) k0) |
|
1537 apply(case_tac "bsimp a = AZERO") |
|
1538 apply(simp) |
|
1539 apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec) |
|
1540 apply(drule mp) |
|
1541 apply(simp) |
|
1542 apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2) |
|
1543 apply(simp) |
|
1544 apply(subst (asm) flts_idem) |
|
1545 apply(auto)[1] |
|
1546 apply(drule_tac x="r" in spec) |
|
1547 apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1) |
|
1548 apply(simp) |
|
1549 apply(subst flts_idem) |
|
1550 apply(auto)[1] |
|
1551 apply(drule_tac x="r" in spec) |
|
1552 apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1) |
|
1553 apply(simp) |
|
1554 apply(case_tac "nonalt (bsimp a)") |
|
1555 apply(subst k0b) |
|
1556 apply(simp) |
|
1557 apply(simp) |
|
1558 apply(subst k0b) |
|
1559 apply(simp) |
|
1560 apply(simp) |
|
1561 apply(auto)[1] |
|
1562 apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec) |
|
1563 apply(drule mp) |
|
1564 apply(simp) |
|
1565 prefer 2 |
|
1566 apply(simp) |
|
1567 apply(subst (asm) k0) |
|
1568 apply(subst (asm) flts_idem) |
|
1569 apply(auto)[1] |
|
1570 apply (simp add: sum_list_map_remove1) |
|
1571 apply(subst (asm) k0b) |
|
1572 apply(simp) |
|
1573 apply(simp) |
|
1574 apply(simp) |
|
1575 apply(subst k0) |
|
1576 apply(subst flts_idem) |
|
1577 apply(auto)[1] |
|
1578 apply (simp add: sum_list_map_remove1) |
|
1579 apply(subst k0b) |
|
1580 apply(simp) |
|
1581 apply(simp) |
|
1582 apply(simp) |
|
1583 lemma XX_bder: |
|
1584 shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r" |
|
1585 apply(induct r) |
|
1586 apply(simp) |
|
1587 apply(simp) |
|
1588 apply(simp) |
|
1589 prefer 3 |
|
1590 apply(simp) |
|
1591 prefer 2 |
|
1592 apply(simp) |
|
1593 apply(case_tac x2a) |
|
1594 apply(simp) |
|
1595 apply(simp) |
|
1596 apply(auto)[1] |
|
1597 |
1540 |
1598 |
1541 |
1599 lemma q3a: |
1542 lemma q3a: |
1600 assumes "\<exists>r \<in> set rs. bnullable r" |
1543 assumes "\<exists>r \<in> set rs. bnullable r" |
1601 shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)" |
1544 shows "bmkeps (AALTs bs (map (fuse bs1) rs)) = bmkeps (AALTs (bs@bs1) rs)" |
1758 apply(simp) |
1701 apply(simp) |
1759 apply(case_tac rs) |
1702 apply(case_tac rs) |
1760 apply(simp_all) |
1703 apply(simp_all) |
1761 done |
1704 done |
1762 |
1705 |
1763 |
|
1764 fun extr :: "arexp \<Rightarrow> (bit list) set" where |
|
1765 "extr (AONE bs) = {bs}" |
|
1766 | "extr (ACHAR bs c) = {bs}" |
|
1767 | "extr (AALTs bs (r#rs)) = |
|
1768 {bs @ bs' | bs'. bs' \<in> extr r} \<union> |
|
1769 {bs @ bs' | bs'. bs' \<in> extr (AALTs [] rs)}" |
|
1770 | "extr (ASEQ bs r1 r2) = |
|
1771 {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}" |
|
1772 | "extr (ASTAR bs r) = {bs @ [S]} \<union> |
|
1773 {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR [] r)}" |
|
1774 |
|
1775 |
|
1776 lemma MAIN_decode: |
|
1777 assumes "\<Turnstile> v : ders s r" |
|
1778 shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r" |
|
1779 using assms |
|
1780 proof (induct s arbitrary: v rule: rev_induct) |
|
1781 case Nil |
|
1782 have "\<Turnstile> v : ders [] r" by fact |
|
1783 then have "\<Turnstile> v : r" by simp |
|
1784 then have "Some v = decode (retrieve (intern r) v) r" |
|
1785 using decode_code retrieve_code by auto |
|
1786 then show "Some (flex r id [] v) = decode (retrieve (bders_simp (intern r) []) v) r" |
|
1787 by simp |
|
1788 next |
|
1789 case (snoc c s v) |
|
1790 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
|
1791 Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r" by fact |
|
1792 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
|
1793 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
|
1794 by(simp add: Prf_injval ders_append) |
|
1795 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
|
1796 by (simp add: flex_append) |
|
1797 also have "... = decode (retrieve (bders_simp (intern r) s) (injval (ders s r) c v)) r" |
|
1798 using asm2 IH by simp |
|
1799 also have "... = decode (retrieve (bder c (bders_simp (intern r) s)) v) r" |
|
1800 using asm bder_retrieve ders_append |
|
1801 apply - |
|
1802 apply(drule_tac x="v" in meta_spec) |
|
1803 apply(drule_tac x="c" in meta_spec) |
|
1804 apply(drule_tac x="bders_simp (intern r) s" in meta_spec) |
|
1805 apply(drule_tac meta_mp) |
|
1806 apply(simp add: ders_append) |
|
1807 defer |
|
1808 apply(simp) |
|
1809 oops |
|
1810 |
|
1811 fun vsimp :: "arexp \<Rightarrow> val \<Rightarrow> val" |
|
1812 where |
|
1813 "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1" |
|
1814 | "vsimp _ v = v" |
|
1815 |
|
1816 lemma fuse_vsimp: |
|
1817 assumes "\<Turnstile> v : (erase r)" |
|
1818 shows "vsimp (fuse bs r) v = vsimp r v" |
|
1819 using assms |
|
1820 apply(induct r arbitrary: v bs) |
|
1821 apply(simp_all) |
|
1822 apply(case_tac "\<exists>bs. r1 = AONE bs") |
|
1823 apply(auto) |
|
1824 apply (metis Prf_elims(2) vsimp.simps(1)) |
|
1825 apply(erule Prf_elims) |
|
1826 apply(auto) |
|
1827 apply(case_tac r1) |
|
1828 apply(auto) |
|
1829 done |
|
1830 |
|
1831 |
|
1832 lemma retrieve_XXX0: |
|
1833 assumes "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow> |
|
1834 \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v" |
|
1835 "\<Turnstile> v : erase (AALTs bs rs)" |
|
1836 shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and> |
|
1837 retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v" |
|
1838 using assms |
|
1839 apply(induct rs arbitrary: bs v taking: size rule: measure_induct) |
|
1840 apply(case_tac x) |
|
1841 apply(simp) |
|
1842 using Prf_elims(1) apply blast |
|
1843 apply(simp) |
|
1844 apply(case_tac list) |
|
1845 apply(simp_all) |
|
1846 apply(case_tac a) |
|
1847 apply(simp_all) |
|
1848 using Prf_elims(1) apply blast |
|
1849 apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2) |
|
1850 using Prf_elims(5) apply force |
|
1851 apply(erule Prf_elims) |
|
1852 apply(auto)[1] |
|
1853 |
|
1854 |
|
1855 |
|
1856 |
|
1857 apply(simp) |
|
1858 apply(erule Prf_elims) |
|
1859 using Prf_elims(1) apply b last |
|
1860 apply(auto) |
|
1861 apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2) |
|
1862 apply(case_tac rs) |
|
1863 apply(auto) |
|
1864 |
|
1865 |
|
1866 oops |
|
1867 |
|
1868 fun get where |
|
1869 "get (Some v) = v" |
|
1870 |
|
1871 |
|
1872 lemma retrieve_XXX: |
|
1873 assumes "\<Turnstile> v : erase r" |
|
1874 shows "\<Turnstile> get (decode (code v) (erase (bsimp r))) : erase (bsimp r)" |
|
1875 using assms |
|
1876 apply(induct r arbitrary: v) |
|
1877 apply(simp) |
|
1878 using Prf_elims(1) apply auto[1] |
|
1879 apply(simp) |
|
1880 apply (simp add: decode_code) |
|
1881 apply(simp) |
|
1882 apply (simp add: decode_code) |
|
1883 apply(simp) |
|
1884 apply(erule Prf_elims) |
|
1885 apply(simp) |
|
1886 apply(case_tac "r1 = AZERO") |
|
1887 apply(simp) |
|
1888 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1889 apply(case_tac "r2 = AZERO") |
|
1890 apply(simp) |
|
1891 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1892 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1893 apply(clarify) |
|
1894 apply(simp) |
|
1895 apply(subst bsimp_ASEQ2) |
|
1896 apply(subst bsimp_ASEQ2) |
|
1897 apply(simp add: erase_fuse) |
|
1898 apply(case_tac r1) |
|
1899 apply(simp_all) |
|
1900 using Prf_elims(4) apply fastforce |
|
1901 apply(erule Prf_elims) |
|
1902 apply(simp) |
|
1903 |
|
1904 apply(simp) |
|
1905 |
|
1906 |
|
1907 defer |
|
1908 apply(subst bsimp_ASEQ1) |
|
1909 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force |
|
1910 using L_bsimp_erase L_ |
|
1911 |
|
1912 lemma retrieve_XXX: |
|
1913 assumes "\<Turnstile> v : erase r" |
|
1914 shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r) \<and> retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v" |
|
1915 using assms |
|
1916 apply(induct r arbitrary: v) |
|
1917 apply(simp) |
|
1918 using Prf_elims(1) apply blast |
|
1919 apply(simp) |
|
1920 using Prf_elims(4) apply fastforce |
|
1921 apply(simp) |
|
1922 apply blast |
|
1923 apply simp |
|
1924 apply(case_tac "r1 = AZERO") |
|
1925 apply(simp) |
|
1926 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1927 apply(case_tac "r2 = AZERO") |
|
1928 apply(simp) |
|
1929 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1930 apply(erule Prf_elims) |
|
1931 apply(simp) |
|
1932 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1933 apply(clarify) |
|
1934 apply(simp) |
|
1935 apply(subst bsimp_ASEQ2) |
|
1936 defer |
|
1937 apply(subst bsimp_ASEQ1) |
|
1938 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1939 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1940 apply(simp) |
|
1941 apply(simp) |
|
1942 apply(drule_tac x="v1" in meta_spec) |
|
1943 apply(drule_tac x="v2" in meta_spec) |
|
1944 apply(simp) |
|
1945 apply(clarify) |
|
1946 apply(rule_tac x="Seq v' v'a" in exI) |
|
1947 apply(simp) |
|
1948 apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6)) |
|
1949 prefer 3 |
|
1950 apply(drule_tac x="v1" in meta_spec) |
|
1951 apply(drule_tac x="v2" in meta_spec) |
|
1952 apply(simp) |
|
1953 apply(clarify) |
|
1954 apply(rule_tac x="v'a" in exI) |
|
1955 apply(subst bsimp_ASEQ2) |
|
1956 apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2) |
|
1957 prefer 2 |
|
1958 apply(auto) |
|
1959 apply(case_tac "x2a") |
|
1960 apply(simp) |
|
1961 using Prf_elims(1) apply blast |
|
1962 apply(simp) |
|
1963 apply(case_tac "list") |
|
1964 apply(simp) |
|
1965 sorry |
|
1966 |
|
1967 |
|
1968 lemma retrieve_XXX: |
|
1969 assumes "\<Turnstile> v : erase r" |
|
1970 shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v" |
|
1971 using assms |
|
1972 apply(induct r arbitrary: v) |
|
1973 apply(simp) |
|
1974 using Prf_elims(1) apply blast |
|
1975 apply(simp) |
|
1976 using Prf_elims(4) apply fastforce |
|
1977 apply(simp) |
|
1978 apply blast |
|
1979 apply simp |
|
1980 apply(case_tac "r1 = AZERO") |
|
1981 apply(simp) |
|
1982 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1983 apply(case_tac "r2 = AZERO") |
|
1984 apply(simp) |
|
1985 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1986 apply(erule Prf_elims) |
|
1987 apply(simp) |
|
1988 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1989 apply(clarify) |
|
1990 apply(simp) |
|
1991 apply(subst bsimp_ASEQ2) |
|
1992 defer |
|
1993 apply(subst bsimp_ASEQ1) |
|
1994 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1995 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1996 apply(simp) |
|
1997 apply(simp) |
|
1998 apply(drule_tac x="v1" in meta_spec) |
|
1999 apply(drule_tac x="v2" in meta_spec) |
|
2000 apply(simp) |
|
2001 apply(clarify) |
|
2002 apply(rule_tac x="Seq v' v'a" in exI) |
|
2003 apply(simp) |
|
2004 apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6)) |
|
2005 prefer 3 |
|
2006 apply(drule_tac x="v1" in meta_spec) |
|
2007 apply(drule_tac x="v2" in meta_spec) |
|
2008 apply(simp) |
|
2009 apply(clarify) |
|
2010 apply(rule_tac x="v'a" in exI) |
|
2011 apply(subst bsimp_ASEQ2) |
|
2012 apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2) |
|
2013 prefer 2 |
|
2014 apply(auto) |
|
2015 apply(case_tac "x2a") |
|
2016 apply(simp) |
|
2017 using Prf_elims(1) apply blast |
|
2018 apply(simp) |
|
2019 apply(case_tac "list") |
|
2020 apply(simp) |
|
2021 sorry |
|
2022 |
|
2023 |
|
2024 lemma TEST: |
|
2025 assumes "\<Turnstile> v : ders s r" |
|
2026 shows "\<exists>v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v" |
|
2027 using assms |
|
2028 apply(induct s arbitrary: r v rule: rev_induct) |
|
2029 apply(simp) |
|
2030 |
|
2031 defer |
|
2032 apply(simp add: ders_append) |
|
2033 apply(frule Prf_injval) |
|
2034 apply(drule_tac x="r" in meta_spec) |
|
2035 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
|
2036 apply(simp) |
|
2037 apply(simp add: bders_append) |
|
2038 apply(subst bder_retrieve) |
|
2039 apply(simp) |
|
2040 apply(simp) |
|
2041 thm bder_retrieve |
|
2042 thm bmkeps_retrieve |
|
2043 |
|
2044 |
|
2045 lemma bmkeps_simp2: |
|
2046 assumes "bnullable (bder c r)" |
|
2047 shows "bmkeps (bder c (bsimp r)) = bmkeps (bder c r)" |
|
2048 using assms |
|
2049 apply(induct r) |
|
2050 apply(simp) |
|
2051 apply(simp) |
|
2052 apply(simp) |
|
2053 prefer 3 |
|
2054 apply(simp) |
|
2055 apply(simp) |
|
2056 apply(auto)[1] |
|
2057 prefer 2 |
|
2058 apply(case_tac "r1 = AZERO") |
|
2059 apply(simp) |
|
2060 apply(case_tac "r2 = AZERO") |
|
2061 apply(simp) |
|
2062 apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs") |
|
2063 apply(clarify) |
|
2064 apply(simp) |
|
2065 apply(subst bsimp_ASEQ2) |
|
2066 |
|
2067 apply(simp add: bmkeps_simp) |
|
2068 apply(simp add: bders_append) |
|
2069 apply(drule_tac x="bder a r" in meta_spec) |
|
2070 apply(simp) |
|
2071 apply(simp) |
|
2072 apply(simp) |
|
2073 prefer 3 |
|
2074 apply(simp) |
|
2075 prefer 2 |
|
2076 apply(simp) |
|
2077 apply(case_tac x2a) |
|
2078 apply(simp) |
|
2079 apply(simp add: ) |
|
2080 apply(subst k0) |
|
2081 apply(auto)[1] |
|
2082 apply(case_tac list) |
|
2083 apply(simp) |
|
2084 |
|
2085 |
|
2086 apply(case_tac "r1=AZERO") |
|
2087 apply(simp) |
|
2088 apply(case_tac "r2=AZERO") |
|
2089 apply(simp) |
|
2090 apply(auto)[1] |
|
2091 apply(case_tac "\<exists>bs. r1=AONE bs") |
|
2092 apply(simp) |
|
2093 apply(auto)[1] |
|
2094 apply(subst bsimp_ASEQ2) |
|
2095 |
|
2096 |
|
2097 prefer 2 |
|
2098 apply(simp) |
|
2099 apply(subst bmkeps_bder_AALTs) |
|
2100 apply(case_tac x2a) |
|
2101 apply(simp) |
|
2102 apply(simp) |
|
2103 apply(auto)[1] |
|
2104 apply(subst bmkeps_bder_AALTs) |
|
2105 |
|
2106 apply(case_tac a) |
|
2107 apply(simp_all) |
|
2108 apply(auto)[1] |
|
2109 apply(case_tac list) |
|
2110 apply(simp) |
|
2111 apply(simp) |
|
2112 |
|
2113 prefer 2 |
|
2114 apply(simp) |
|
2115 |
|
2116 |
|
2117 lemma bbs0: |
1706 lemma bbs0: |
2118 shows "blexer_simp r [] = blexer r []" |
1707 shows "blexer_simp r [] = blexer r []" |
2119 apply(simp add: blexer_def blexer_simp_def) |
1708 apply(simp add: blexer_def blexer_simp_def) |
2120 done |
1709 done |
2121 |
1710 |
2128 using b3 apply auto[1] |
1717 using b3 apply auto[1] |
2129 apply(subst bmkeps_simp[symmetric]) |
1718 apply(subst bmkeps_simp[symmetric]) |
2130 apply(simp) |
1719 apply(simp) |
2131 apply(simp) |
1720 apply(simp) |
2132 done |
1721 done |
2133 |
|
2134 lemma bbs1: |
|
2135 shows "blexer_simp r [c1, c2] = blexer r [c1, c2]" |
|
2136 apply(simp add: blexer_def blexer_simp_def) |
|
2137 apply(auto) |
|
2138 defer |
|
2139 apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1)) |
|
2140 apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1)) |
|
2141 apply(subst bmkeps_simp[symmetric]) |
|
2142 using b3 apply auto[1] |
|
2143 apply(subst bmkeps_retrieve) |
|
2144 using b3 bnullable_correctness apply blast |
|
2145 apply(subst bder_retrieve) |
|
2146 using b3 bnullable_correctness mkeps_nullable apply fastforce |
|
2147 apply(subst bmkeps_retrieve) |
|
2148 using bnullable_correctness apply blast |
|
2149 apply(subst bder_retrieve) |
|
2150 using bnullable_correctness mkeps_nullable apply force |
|
2151 |
|
2152 using bder_retrieve bmkeps_simp bmkeps_retrieve |
|
2153 |
|
2154 |
|
2155 |
|
2156 lemma bsimp_retrieve_bder: |
|
2157 assumes "\<Turnstile> v : der c (erase r)" |
|
2158 shows "retrieve (bder c r) v = retrieve (bsimp (bder c r)) v" |
|
2159 thm bder_retrieve bmkeps_simp |
|
2160 apply(induct r arbitrary: c v) |
|
2161 apply(simp) |
|
2162 apply(simp) |
|
2163 apply(simp) |
|
2164 apply(auto)[1] |
|
2165 apply(case_tac "bsimp (bder c r1) = AZERO") |
|
2166 apply(simp) |
|
2167 |
|
2168 prefer 3 |
|
2169 apply(simp) |
|
2170 apply(auto elim!: Prf_elims)[1] |
|
2171 apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO") |
|
2172 apply(simp) |
|
2173 apply (met is L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse) |
|
2174 apply(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs") |
|
2175 apply(clarify) |
|
2176 apply(subgoal_tac "L (der c (erase r)) = {[]}") |
|
2177 prefer 2 |
|
2178 apply (metis L.simps(2) L_bsimp_erase erase.simps(2) erase_bder erase_fuse) |
|
2179 apply(simp) |
|
2180 |
|
2181 |
|
2182 |
|
2183 apply(subst bsimp_ASEQ1) |
|
2184 apply(simp) |
|
2185 apply(simp) |
|
2186 apply(auto)[1] |
|
2187 |
|
2188 prefer 2 |
|
2189 |
|
2190 |
1722 |
2191 lemma oo: |
1723 lemma oo: |
2192 shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)" |
1724 shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)" |
2193 apply(simp add: blexer_correctness) |
1725 apply(simp add: blexer_correctness) |
2194 done |
1726 done |
2195 |
1727 |
2196 lemma oo2a: |
|
2197 assumes "\<forall>r. bmkeps (bders_simp r s) = bmkeps (bders r s)" "c # s \<in> L r" |
|
2198 "bnullable (bders_simp (bsimp (bder c (intern r))) s)" |
|
2199 shows "(case (blexer_simp (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer_simp r (c # s)" |
|
2200 using assms |
|
2201 apply(simp add: blexer_simp_def) |
|
2202 apply(auto split: option.split) |
|
2203 apply (metis blexer_correctness blexer_def lexer.simps(2) lexer_correct_None option.simps(4)) |
|
2204 prefer 2 |
|
2205 apply (metis L_bders_simp L_bsimp_erase Posix1(1) Posix_mkeps bnullable_correctness ders_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None) |
|
2206 apply(subst bmkeps_retrieve) |
|
2207 using L_bders_simp bnullable_correctness nullable_correctness apply blast |
|
2208 |
|
2209 thm bder_retrieve |
|
2210 |
|
2211 |
|
2212 apply(subst bder_retrieve[symmetric]) |
|
2213 |
|
2214 |
|
2215 |
|
2216 apply(drule_tac x="bsimp (bder c (intern r))" in spec) |
|
2217 apply(drule sym) |
|
2218 apply(simp) |
|
2219 apply(subst blexer_simp_def) |
|
2220 apply(case_tac "bnullable (bders_simp (intern (der c r)) s)") |
|
2221 apply(simp) |
|
2222 apply(auto split: option.split) |
|
2223 apply(subst oo) |
|
2224 apply(simp) |
|
2225 done |
|
2226 |
|
2227 |
|
2228 |
|
2229 lemma oo3: |
|
2230 assumes "\<forall>r. bders r s = bders_simp r s" |
|
2231 shows "blexer_simp r (s @ [c]) = blexer r (s @ [c])" |
|
2232 using assms |
|
2233 apply(simp (no_asm) add: blexer_simp_def) |
|
2234 apply(auto) |
|
2235 prefer 2 |
|
2236 apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1)) |
|
2237 apply(simp add: bders_simp_append) |
|
2238 apply(subst bmkeps_simp[symmetric]) |
|
2239 using b3 apply auto[1] |
|
2240 apply(simp add: blexer_def) |
|
2241 apply(auto)[1] |
|
2242 prefer 2 |
|
2243 apply (metis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1)) |
|
2244 apply(simp add: bders_append) |
|
2245 done |
|
2246 |
|
2247 lemma oo4: |
|
2248 assumes "\<forall>r. bmkeps (bders r s) = bmkeps (bders_simp r s)" "bnullable (bder c (bders r s))" |
|
2249 shows "bmkeps (bders_simp r (s @ [c])) = bmkeps (bders r (s @ [c]))" |
|
2250 using assms |
|
2251 apply(simp add: bders_simp_append) |
|
2252 apply(subst bmkeps_simp[symmetric]) |
|
2253 apply (metis L_bders_simp bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1)) |
|
2254 apply(simp add: bders_append) |
|
2255 done |
|
2256 |
|
2257 lemma oo4: |
|
2258 shows "blexer_simp r s = blexer r s" |
|
2259 apply(induct s arbitrary: r rule: rev_induct) |
|
2260 apply(simp only: blexer_simp_def blexer_def) |
|
2261 apply(simp) |
|
2262 apply(simp only: blexer_simp_def blexer_def) |
|
2263 apply(subgoal_tac "bnullable (bders_simp (intern r) (xs @ [x])) = bnullable (bders (intern r) (xs @ [x]))") |
|
2264 prefer 2 |
|
2265 apply (simp add: b4) |
|
2266 apply(simp) |
|
2267 apply(rule impI) |
|
2268 apply(simp add: bders_simp_append) |
|
2269 apply(subst bmkeps_simp[symmetric]) |
|
2270 using b3 apply auto[1] |
|
2271 apply(subst bmkeps_retrieve) |
|
2272 using b3 bnullable_correctness apply blast |
|
2273 apply(subst bder_retrieve) |
|
2274 using b3 bnullable_correctness mkeps_nullable apply fastforce |
|
2275 apply(simp add: bders_append) |
|
2276 apply(subst bmkeps_retrieve) |
|
2277 using bnullable_correctness apply blast |
|
2278 apply(subst bder_retrieve) |
|
2279 using bnullable_correctness mkeps_nullable apply fastforce |
|
2280 apply(subst erase_bder) |
|
2281 apply(case_tac "xs \<in> L") |
|
2282 apply(subst (asm) (2) bmkeps_retrieve) |
|
2283 |
|
2284 |
|
2285 thm bmkeps_retrieve bmkeps_retrieve |
|
2286 apply(subst bmkeps_retrieve[symmetric]) |
|
2287 |
|
2288 apply (simp add: bnullable_correctness) |
|
2289 apply(simp add: bders_simp_append) |
|
2290 |
|
2291 |
|
2292 apply(induct s arbitrary: r rule: rev_induct) |
|
2293 apply(simp add: blexer_def blexer_simp_def) |
|
2294 apply(rule oo3) |
|
2295 apply(simp (no_asm) add: blexer_simp_def) |
|
2296 apply(auto) |
|
2297 prefer 2 |
|
2298 apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1)) |
|
2299 apply(simp add: bders_simp_append) |
|
2300 apply(subst bmkeps_simp[symmetric]) |
|
2301 using b3 apply auto[1] |
|
2302 apply(simp add: blexer_def) |
|
2303 apply(auto)[1] |
|
2304 prefer 2 |
|
2305 apply (m etis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1)) |
|
2306 apply(simp add: bders_append) |
|
2307 oops |
|
2308 |
|
2309 |
|
2310 lemma bnullable_simp: |
|
2311 assumes "s \<in> L (erase r)" |
|
2312 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
|
2313 using assms |
|
2314 apply(induct s arbitrary: r rule: rev_induct) |
|
2315 apply(simp) |
|
2316 apply(simp add: bders_append bders_simp_append) |
|
2317 apply(subst bmkeps_simp[symmetric]) |
|
2318 apply (metis L_bders_simp b3 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correct_Some lexer_correctness(1)) |
|
2319 apply(subst bmkeps_retrieve) |
|
2320 apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer_correct_Some option.distinct(1)) |
|
2321 apply(subst bmkeps_retrieve) |
|
2322 apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2)) |
|
2323 apply(subst bder_retrieve) |
|
2324 apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer_correct_Some mkeps_nullable option.distinct(1)) |
|
2325 apply(subst bder_retrieve) |
|
2326 apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2) mkeps_nullable) |
|
2327 |
|
2328 apply(drule_tac x="bder a r" in meta_spec) |
|
2329 apply(drule_tac meta_mp) |
|
2330 apply (me tis erase_bder lexer.simps(2) lexer_correct_None option.simps(4)) |
|
2331 apply(simp) |
|
2332 oops |
|
2333 |
|
2334 |
|
2335 lemma |
|
2336 shows "blexer r s = blexer_simp r s" |
|
2337 apply(induct s arbitrary: r rule: rev_induct) |
|
2338 apply(simp add: blexer_def blexer_simp_def) |
|
2339 apply(case_tac "xs @ [x] \<in> L r") |
|
2340 defer |
|
2341 apply(subgoal_tac "blexer (ders xs r) [x] = None") |
|
2342 prefer 2 |
|
2343 apply(subst blexer_correctness) |
|
2344 apply(simp (no_asm) add: lexer_correct_None) |
|
2345 apply(simp add: nullable_correctness) |
|
2346 apply(simp add: der_correctness ders_correctness) |
|
2347 apply(simp add: Der_def Ders_def) |
|
2348 apply(subgoal_tac "blexer r (xs @ [x]) = None") |
|
2349 prefer 2 |
|
2350 apply (simp add: blexer_correctness) |
|
2351 using lexer_correct_None apply auto[1] |
|
2352 apply(simp) |
|
2353 apply(subgoal_tac "blexer_simp (ders xs r) [x] = None") |
|
2354 prefer 2 |
|
2355 apply (metis L_bders_simp Posix_injval Posix_mkeps bders.simps(2) blexer_correctness blexer_simp_def bnullable_correctness ders.simps(1) erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2)) |
|
2356 apply(subgoal_tac "[] \<notin> L (erase (bders_simp (intern r) (xs @ [x])))") |
|
2357 prefer 2 |
|
2358 apply(metis L_bders_simp Posix_injval bders.simps(2) blexer_correctness ders.simps(1) ders_append erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2)) |
|
2359 using blexer_simp_def bnullable_correctness lexer_correct_None apply auto[1] |
|
2360 (* case xs @ [x] \<in> L r *) |
|
2361 apply(subgoal_tac "\<exists>v. blexer (ders xs r) [x] = Some v \<and> [x] \<in> (ders xs r) \<rightarrow> v") |
|
2362 prefer 2 |
|
2363 using blexer_correctness lexer_correct_Some apply auto[1] |
|
2364 apply (simp add: Posix_injval Posix_mkeps) |
|
2365 apply (metis ders.simps(1) ders.simps(2) ders_append lexer_correct_None lexer_flex) |
|
2366 apply(clarify) |
|
2367 apply(subgoal_tac "blexer_simp (ders xs r) [x] = Some v") |
|
2368 prefer 2 |
|
2369 apply(simp add: blexer_simp_def) |
|
2370 apply(auto)[1] |
|
2371 apply (metis bders.simps(1) bders.simps(2) blexer_def bmkeps_simp option.simps(3)) |
|
2372 using b3 blexer_def apply fastforce |
|
2373 apply(subgoal_tac "blexer_simp (ders xs r) [x] = blexer_simp r (xs @ [x])") |
|
2374 prefer 2 |
|
2375 apply(simp add: blexer_simp_def) |
|
2376 |
|
2377 apply(simp) |
|
2378 |
|
2379 |
|
2380 |
|
2381 apply(simp) |
|
2382 apply(subst blexer_simp_def) |
|
2383 apply(simp) |
|
2384 apply(auto) |
|
2385 apply(drule_tac x="der a r" in meta_spec) |
|
2386 apply(subst blexer_def) |
|
2387 apply(subgoal_tac "bnullable (bders (intern r) (a # s))") |
|
2388 prefer 2 |
|
2389 apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2)) |
|
2390 apply(simp) |
|
2391 |
|
2392 |
|
2393 |
|
2394 lemma |
|
2395 shows "blexer r s = blexer_simp r s" |
|
2396 apply(induct s arbitrary: r) |
|
2397 apply(simp add: blexer_def blexer_simp_def) |
|
2398 apply(case_tac "s \<in> L (der a r)") |
|
2399 defer |
|
2400 apply(subgoal_tac "blexer (der a r) s = None") |
|
2401 prefer 2 |
|
2402 apply (simp add: blexer_correctness lexer_correct_None) |
|
2403 apply(subgoal_tac "blexer r (a # s) = None") |
|
2404 prefer 2 |
|
2405 apply (simp add: blexer_correctness) |
|
2406 apply(simp) |
|
2407 |
|
2408 apply(subst blexer_simp_def) |
|
2409 apply(simp) |
|
2410 apply(drule_tac x="der a r" in meta_spec) |
|
2411 apply(subgoal_tac "s \<notin> L(erase (bder a (intern r)))") |
|
2412 prefer 2 |
|
2413 apply simp |
|
2414 |
|
2415 apply(simp only:) |
|
2416 apply(subst blexer_simp_def) |
|
2417 apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))") |
|
2418 apply(simp) |
|
2419 apply(subst bnullable_correctness[symmetric]) |
|
2420 apply(simp) |
|
2421 oops |
|
2422 |
|
2423 |
|
2424 lemma flts_bsimp: |
|
2425 "flts (map bsimp rs) = map bsimp (flts rs)" |
|
2426 apply(induct rs taking: size rule: measure_induct) |
|
2427 apply(case_tac x) |
|
2428 apply(simp) |
|
2429 apply(simp) |
|
2430 apply(induct rs rule: flts.induct) |
|
2431 apply(simp) |
|
2432 apply(simp) |
|
2433 defer |
|
2434 apply(simp) |
|
2435 apply(simp) |
|
2436 defer |
|
2437 apply(simp) |
|
2438 apply(subst List.list.map(2)) |
|
2439 apply(simp only: flts.simps) |
|
2440 apply(subst k0) |
|
2441 apply(subst map_append) |
|
2442 apply(simp only:) |
|
2443 apply(simp del: bsimp.simps) |
|
2444 apply(case_tac rs1) |
|
2445 apply(simp) |
|
2446 apply(simp) |
|
2447 apply(case_tac list) |
|
2448 apply(simp_all) |
|
2449 thm map |
|
2450 apply(subst map.simps) |
|
2451 apply(auto) |
|
2452 defer |
|
2453 apply(case_tac "(bsimp va) = AZERO") |
|
2454 apply(simp) |
|
2455 |
|
2456 using b3 apply for ce |
|
2457 apply(case_tac "(bsimp a2) = AZERO") |
|
2458 apply(simp) |
|
2459 apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) |
|
2460 apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs") |
|
2461 apply(clarify) |
|
2462 apply(simp) |
|
2463 |
|
2464 |
|
2465 lemma XXX: |
|
2466 shows "bsimp (bsimp a) = bsimp a" |
|
2467 sorry |
|
2468 |
1728 |
2469 lemma bder_fuse: |
1729 lemma bder_fuse: |
2470 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
1730 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
2471 apply(induct a arbitrary: bs c) |
1731 apply(induct a arbitrary: bs c) |
2472 apply(simp_all) |
1732 apply(simp_all) |
2473 done |
1733 done |
2474 |
1734 |
2475 lemma XXX2: |
1735 lemma XXX2_helper: |
|
1736 assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" |
|
1737 "\<forall>r'\<in>set rs. good r' \<and> nonalt r'" |
|
1738 shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)" |
|
1739 using assms |
|
1740 apply(induct rs arbitrary: c) |
|
1741 apply(simp) |
|
1742 apply(simp) |
|
1743 apply(subst k0) |
|
1744 apply(simp add: flts_append) |
|
1745 apply(subst (2) k0) |
|
1746 apply(simp add: flts_append) |
|
1747 apply(subgoal_tac "flts [a] = [a]") |
|
1748 prefer 2 |
|
1749 using good.simps(1) k0b apply blast |
|
1750 apply(simp) |
|
1751 done |
|
1752 |
|
1753 lemma bmkeps_good: |
|
1754 assumes "good a" |
|
1755 shows "bmkeps (bsimp a) = bmkeps a" |
|
1756 using assms |
|
1757 using test2 by auto |
|
1758 |
|
1759 |
|
1760 lemma xxx_bder: |
|
1761 assumes "good r" |
|
1762 shows "L (erase r) \<noteq> {}" |
|
1763 using assms |
|
1764 apply(induct r rule: good.induct) |
|
1765 apply(auto simp add: Sequ_def) |
|
1766 done |
|
1767 |
|
1768 lemma xxx_bder2: |
|
1769 assumes "L (erase (bsimp r)) = {}" |
|
1770 shows "bsimp r = AZERO" |
|
1771 using assms xxx_bder test2 good1 |
|
1772 by blast |
|
1773 |
|
1774 lemma XXX2aa: |
|
1775 assumes "good a" |
2476 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
1776 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2477 apply(induct a arbitrary: c) |
1777 using assms |
|
1778 by (simp add: test2) |
|
1779 |
|
1780 lemma XXX2aa_ders: |
|
1781 assumes "good a" |
|
1782 shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)" |
|
1783 using assms |
|
1784 by (simp add: test2) |
|
1785 |
|
1786 lemma XXX4a: |
|
1787 shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO" |
|
1788 apply(induct s arbitrary: r rule: rev_induct) |
|
1789 apply(simp) |
|
1790 apply (simp add: good1) |
|
1791 apply(simp add: bders_simp_append) |
|
1792 apply (simp add: good1) |
|
1793 done |
|
1794 |
|
1795 lemma XXX4a_good: |
|
1796 assumes "good a" |
|
1797 shows "good (bders_simp a s) \<or> bders_simp a s = AZERO" |
|
1798 using assms |
|
1799 apply(induct s arbitrary: a rule: rev_induct) |
|
1800 apply(simp) |
|
1801 apply(simp add: bders_simp_append) |
|
1802 apply (simp add: good1) |
|
1803 done |
|
1804 |
|
1805 lemma XXX4a_good_cons: |
|
1806 assumes "s \<noteq> []" |
|
1807 shows "good (bders_simp a s) \<or> bders_simp a s = AZERO" |
|
1808 using assms |
|
1809 apply(case_tac s) |
|
1810 apply(auto) |
|
1811 using XXX4a by blast |
|
1812 |
|
1813 lemma XXX4b: |
|
1814 assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}" |
|
1815 shows "good (bders_simp a s)" |
|
1816 using assms |
|
1817 apply(induct s arbitrary: a) |
|
1818 apply(simp) |
|
1819 apply(simp) |
|
1820 apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}") |
|
1821 prefer 2 |
|
1822 apply(auto)[1] |
|
1823 apply(erule disjE) |
|
1824 apply(subgoal_tac "bsimp (bder a aa) = AZERO") |
|
1825 prefer 2 |
|
1826 using L_bsimp_erase xxx_bder2 apply auto[1] |
|
1827 apply(simp) |
|
1828 apply (metis L.simps(1) XXX4a erase.simps(1)) |
|
1829 apply(drule_tac x="bsimp (bder a aa)" in meta_spec) |
|
1830 apply(drule meta_mp) |
|
1831 apply simp |
|
1832 apply(rule good1a) |
|
1833 apply(auto) |
|
1834 done |
|
1835 |
|
1836 lemma bders_AZERO: |
|
1837 shows "bders AZERO s = AZERO" |
|
1838 and "bders_simp AZERO s = AZERO" |
|
1839 apply (induct s) |
|
1840 apply(auto) |
|
1841 done |
|
1842 |
|
1843 lemma ZZ0: |
|
1844 assumes "bsimp a = AALTs bs rs" |
|
1845 shows "bsimp (bder c a) = AALTs bs (map (bder c) rs)" |
|
1846 using assms |
|
1847 apply(induct a arbitrary: rs bs c) |
|
1848 apply(simp_all) |
|
1849 apply(auto)[1] |
|
1850 prefer 2 |
|
1851 apply (metis arexp.distinct(25) arexp.distinct(7) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1) |
|
1852 prefer 2 |
|
1853 oops |
|
1854 |
|
1855 |
|
1856 lemma ZZZ: |
|
1857 assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)" |
|
1858 shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))" |
|
1859 using assms |
|
1860 apply(induct x52) |
|
1861 apply(simp) |
|
1862 apply(simp) |
|
1863 apply(case_tac "bsimp a = AZERO") |
|
1864 apply(simp) |
|
1865 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
1866 prefer 2 |
|
1867 using less_add_Suc1 apply fastforce |
|
1868 apply(simp) |
|
1869 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
1870 apply(clarify) |
|
1871 apply(simp) |
|
1872 apply(subst k0) |
|
1873 apply(case_tac "rs = []") |
|
1874 apply(simp) |
|
1875 apply(subgoal_tac "bsimp (bder c a) = AALTs bs []") |
|
1876 apply(simp) |
|
1877 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
1878 oops |
|
1879 |
|
1880 |
|
1881 |
|
1882 |
|
1883 lemma bders_snoc: |
|
1884 "bder c (bders a s) = bders a (s @ [c])" |
|
1885 apply(simp add: bders_append) |
|
1886 done |
|
1887 |
|
1888 lemma |
|
1889 assumes "bnullable (bders a s)" "good a" |
|
1890 shows "bmkeps (bders_simp a s) = bmkeps (bders a s)" |
|
1891 using assms |
|
1892 apply(induct s arbitrary: a) |
|
1893 apply(simp) |
|
1894 apply(simp add: bders_append bders_simp_append) |
|
1895 apply(drule_tac x="bsimp (bsimp (bder a aa))" in meta_spec) |
|
1896 apply(drule meta_mp) |
|
1897 apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem) |
|
1898 apply(subgoal_tac "good (bsimp (bder a aa)) \<or> bsimp (bder a aa) = AZERO") |
|
1899 apply(auto simp add: bders_AZERO) |
|
1900 prefer 2 |
|
1901 apply (metis b4 bders.simps(2) bders_AZERO(2) bders_simp.simps(2) bnullable.simps(1)) |
|
1902 prefer 2 |
|
1903 using good1 apply auto[1] |
|
1904 apply(drule meta_mp) |
|
1905 apply (simp add: bsimp_idem) |
|
1906 apply (subst (asm) (1) bsimp_idem) |
|
1907 apply(simp) |
|
1908 apply(subst (asm) (2) bmkeps_simp) |
|
1909 apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem) |
|
1910 apply (subst (asm) (1) bsimp_idem) |
|
1911 apply(simp) |
|
1912 defer |
|
1913 oops |
|
1914 |
|
1915 |
|
1916 lemma |
|
1917 shows "bmkeps (bders (bders_simp a s2) s1) = bmkeps (bders_simp a (s2 @ s1))" |
|
1918 apply(induct s2 arbitrary: a s1) |
|
1919 apply(simp) |
|
1920 defer |
|
1921 apply(simp add: bders_append bders_simp_append) |
|
1922 oops |
|
1923 |
|
1924 lemma QQ1: |
|
1925 shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []" |
|
1926 apply(simp) |
|
1927 apply(simp add: bsimp_idem) |
|
1928 done |
|
1929 |
|
1930 lemma QQ2: |
|
1931 shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]" |
|
1932 apply(simp) |
|
1933 done |
|
1934 |
|
1935 lemma QQ3: |
|
1936 assumes "good a" |
|
1937 shows "bmkeps (bsimp (bders (bsimp a) [c1, c2])) = bmkeps (bders_simp (bsimp a) [c1, c2])" |
|
1938 using assms |
|
1939 apply(simp) |
|
1940 |
|
1941 oops |
|
1942 |
|
1943 lemma QQ4: |
|
1944 shows "bmkeps (bsimp (bders (bsimp a) [c1, c2, c3])) = bmkeps (bders_simp (bsimp a) [c1, c2, c3])" |
|
1945 apply(simp) |
|
1946 oops |
|
1947 |
|
1948 lemma QQ3: |
|
1949 assumes "good a" |
|
1950 shows "bsimp (bders (bders_simp a s2) s1)= bders_simp a (s1 @ s2)" |
|
1951 using assms |
|
1952 apply(induct s2 arbitrary: a s1) |
|
1953 apply(simp) |
|
1954 oops |
|
1955 |
|
1956 lemma XXX2a_long: |
|
1957 assumes "good a" |
|
1958 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
1959 using assms |
|
1960 apply(induct a arbitrary: c taking: asize rule: measure_induct) |
|
1961 apply(case_tac x) |
2478 apply(simp) |
1962 apply(simp) |
2479 apply(simp) |
1963 apply(simp) |
2480 apply(simp) |
1964 apply(simp) |
2481 prefer 3 |
1965 prefer 3 |
2482 apply(simp) |
1966 apply(simp) |
|
1967 apply(simp) |
2483 apply(auto)[1] |
1968 apply(auto)[1] |
2484 apply(case_tac "(bsimp a1) = AZERO") |
1969 apply(case_tac "x42 = AZERO") |
2485 apply(simp) |
1970 apply(simp) |
|
1971 apply(case_tac "x43 = AZERO") |
|
1972 apply(simp) |
|
1973 using test2 apply force |
|
1974 apply(case_tac "\<exists>bs. x42 = AONE bs") |
|
1975 apply(clarify) |
|
1976 apply(simp) |
|
1977 apply(subst bsimp_ASEQ1) |
|
1978 apply(simp) |
2486 using b3 apply force |
1979 using b3 apply force |
2487 apply(case_tac "(bsimp a2) = AZERO") |
1980 using bsimp_ASEQ0 test2 apply force |
2488 apply(simp) |
1981 thm good_SEQ test2 |
2489 apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) |
1982 apply (simp add: good_SEQ test2) |
2490 apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs") |
1983 apply (simp add: good_SEQ test2) |
|
1984 apply(case_tac "x42 = AZERO") |
|
1985 apply(simp) |
|
1986 apply(case_tac "x43 = AZERO") |
|
1987 apply(simp) |
|
1988 apply (simp add: bsimp_ASEQ0) |
|
1989 apply(case_tac "\<exists>bs. x42 = AONE bs") |
2491 apply(clarify) |
1990 apply(clarify) |
2492 apply(simp) |
1991 apply(simp) |
2493 apply(subst bsimp_ASEQ2) |
1992 apply(subst bsimp_ASEQ1) |
2494 apply(subgoal_tac "bmkeps a1 = bs") |
1993 apply(simp) |
|
1994 using bsimp_ASEQ0 test2 apply force |
|
1995 apply (simp add: good_SEQ test2) |
|
1996 apply (simp add: good_SEQ test2) |
|
1997 apply (simp add: good_SEQ test2) |
|
1998 (* AALTs case *) |
|
1999 apply(simp) |
|
2000 using test2 by fastforce |
|
2001 |
|
2002 lemma XXX2a_long_without_good: |
|
2003 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
2004 apply(induct a arbitrary: c taking: asize rule: measure_induct) |
|
2005 apply(case_tac x) |
|
2006 apply(simp) |
|
2007 apply(simp) |
|
2008 apply(simp) |
|
2009 prefer 3 |
|
2010 apply(simp) |
|
2011 apply(simp) |
|
2012 apply(auto)[1] |
|
2013 apply(case_tac "x42 = AZERO") |
|
2014 apply(simp) |
|
2015 apply(case_tac "bsimp x43 = AZERO") |
|
2016 apply(simp) |
|
2017 apply (simp add: bsimp_ASEQ0) |
|
2018 apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO") |
|
2019 apply(simp) |
|
2020 apply (metis bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2) |
|
2021 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
|
2022 apply(clarify) |
|
2023 apply(simp) |
|
2024 apply(subst bsimp_ASEQ2) |
|
2025 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |
|
2026 apply(simp) |
|
2027 prefer 2 |
|
2028 using less_add_Suc1 apply fastforce |
|
2029 apply(subgoal_tac "bmkeps x42 = bs") |
2495 prefer 2 |
2030 prefer 2 |
2496 apply (simp add: bmkeps_simp) |
2031 apply (simp add: bmkeps_simp) |
2497 apply(simp) |
2032 apply(simp) |
2498 apply(subst (1) bsimp_fuse[symmetric]) |
2033 apply(case_tac "nonalt (bsimp (bder c x43))") |
2499 defer |
2034 apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a) |
2500 apply(subst bsimp_ASEQ1) |
2035 apply(subgoal_tac "nonnested (bsimp (bder c x43))") |
|
2036 prefer 2 |
|
2037 using nn1b apply blast |
|
2038 apply(case_tac x43) |
|
2039 apply(simp) |
|
2040 apply(simp) |
2501 apply(simp) |
2041 apply(simp) |
|
2042 prefer 3 |
2502 apply(simp) |
2043 apply(simp) |
2503 apply(simp) |
2044 apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6)) |
|
2045 apply(simp) |
|
2046 apply(auto)[1] |
|
2047 apply(case_tac "(bsimp (bder c x42a)) = AZERO") |
|
2048 apply(simp) |
|
2049 |
|
2050 apply(simp) |
|
2051 |
|
2052 |
|
2053 |
|
2054 apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) = AALTs bs1 rs1 ) \<or> |
|
2055 (\<exists>bs1 r. bsimp (bder c x43) = fuse bs1 r)") |
|
2056 prefer 2 |
|
2057 apply (metis fuse_empty) |
|
2058 apply(erule disjE) |
|
2059 prefer 2 |
|
2060 apply(clarify) |
|
2061 apply(simp only:) |
|
2062 apply(simp) |
|
2063 apply(simp add: fuse_append) |
|
2064 apply(subst bder_fuse) |
|
2065 apply(subst bsimp_fuse[symmetric]) |
|
2066 apply(subst bder_fuse) |
|
2067 apply(subst bsimp_fuse[symmetric]) |
|
2068 apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)") |
|
2069 prefer 2 |
|
2070 using less_add_Suc2 apply blast |
|
2071 apply(simp only: ) |
|
2072 apply(subst bsimp_fuse[symmetric]) |
|
2073 apply(simp only: ) |
|
2074 |
|
2075 apply(simp only: fuse.simps) |
|
2076 apply(simp) |
|
2077 apply(case_tac rs1) |
|
2078 apply(simp) |
|
2079 apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse) |
|
2080 apply(simp) |
|
2081 apply(case_tac list) |
|
2082 apply(simp) |
|
2083 apply (metis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse) |
|
2084 apply(simp only: bsimp_AALTs.simps map_cons.simps) |
2504 apply(auto)[1] |
2085 apply(auto)[1] |
2505 apply (metis XXX bmkeps_simp bsimp_fuse) |
2086 |
2506 using b3 apply blast |
2087 |
2507 apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1) |
2088 |
2508 apply(simp) |
2089 apply(subst bsimp_fuse[symmetric]) |
|
2090 apply(subgoal_tac "bmkeps x42 = bs") |
|
2091 prefer 2 |
|
2092 apply (simp add: bmkeps_simp) |
|
2093 |
|
2094 |
|
2095 apply(simp) |
|
2096 |
|
2097 using b3 apply force |
|
2098 using bsimp_ASEQ0 test2 apply force |
|
2099 thm good_SEQ test2 |
|
2100 apply (simp add: good_SEQ test2) |
|
2101 apply (simp add: good_SEQ test2) |
|
2102 apply(case_tac "x42 = AZERO") |
|
2103 apply(simp) |
|
2104 apply(case_tac "x43 = AZERO") |
|
2105 apply(simp) |
|
2106 apply (simp add: bsimp_ASEQ0) |
|
2107 apply(case_tac "\<exists>bs. x42 = AONE bs") |
|
2108 apply(clarify) |
|
2109 apply(simp) |
|
2110 apply(subst bsimp_ASEQ1) |
|
2111 apply(simp) |
|
2112 using bsimp_ASEQ0 test2 apply force |
|
2113 apply (simp add: good_SEQ test2) |
|
2114 apply (simp add: good_SEQ test2) |
|
2115 apply (simp add: good_SEQ test2) |
|
2116 (* AALTs case *) |
|
2117 apply(simp) |
|
2118 using test2 by fastforce |
|
2119 |
|
2120 |
|
2121 lemma XXX4ab: |
|
2122 shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO" |
|
2123 apply(induct s arbitrary: r rule: rev_induct) |
|
2124 apply(simp) |
|
2125 apply (simp add: good1) |
|
2126 apply(simp add: bders_simp_append) |
|
2127 apply (simp add: good1) |
|
2128 done |
|
2129 |
|
2130 lemma XXX4: |
|
2131 assumes "good a" |
|
2132 shows "bders_simp a s = bsimp (bders a s)" |
|
2133 using assms |
|
2134 apply(induct s arbitrary: a rule: rev_induct) |
|
2135 apply(simp) |
|
2136 apply (simp add: test2) |
|
2137 apply(simp add: bders_append bders_simp_append) |
|
2138 oops |
|
2139 |
|
2140 |
|
2141 lemma MAINMAIN: |
|
2142 "blexer r s = blexer_simp r s" |
|
2143 apply(induct s arbitrary: r) |
|
2144 apply(simp add: blexer_def blexer_simp_def) |
|
2145 apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps) |
|
2146 apply(auto simp del: bders.simps bders_simp.simps) |
|
2147 prefer 2 |
|
2148 apply (metis b4 bders.simps(2) bders_simp.simps(2)) |
2509 prefer 2 |
2149 prefer 2 |
2510 apply(subst bder_fuse) |
2150 apply (metis b4 bders.simps(2)) |
2511 apply(subst bsimp_fuse[symmetric]) |
2151 apply(subst bmkeps_simp) |
2512 apply(simp) |
2152 apply(simp) |
2513 sorry |
2153 apply(case_tac s) |
2514 |
2154 apply(simp only: bders.simps) |
2515 |
2155 apply(subst bders_simp.simps) |
2516 thm bsimp_AALTs.simps |
2156 apply(simp) |
2517 thm bsimp.simps |
2157 |
2518 thm flts.simps |
|
2519 |
|
2520 lemma XXX3: |
|
2521 "bsimp (bders (bsimp r) s) = bsimp (bders r s)" |
|
2522 apply(induct s arbitrary: r rule: rev_induct) |
|
2523 apply(simp) |
|
2524 apply (simp add: XXX) |
|
2525 apply(simp add: bders_append) |
|
2526 apply(subst (2) XXX2[symmetric]) |
|
2527 apply(subst XXX2[symmetric]) |
|
2528 apply(drule_tac x="r" in meta_spec) |
|
2529 apply(simp) |
|
2530 done |
|
2531 |
|
2532 lemma XXX4: |
|
2533 "bders_simp (bsimp r) s = bsimp (bders r s)" |
|
2534 apply(induct s arbitrary: r) |
|
2535 apply(simp) |
|
2536 apply(simp) |
|
2537 by (metis XXX2) |
|
2538 |
|
2539 |
|
2540 lemma |
|
2541 assumes "bnullable (bder c r)" "bnullable (bder c (bsimp r))" |
|
2542 shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))" |
|
2543 using assms |
|
2544 apply(induct r arbitrary: c) |
|
2545 apply(simp) |
|
2546 apply(simp) |
|
2547 apply(simp) |
|
2548 prefer 3 |
|
2549 apply(simp) |
|
2550 apply(auto)[1] |
|
2551 apply(case_tac "(bsimp r1) = AZERO") |
|
2552 apply(simp) |
|
2553 apply(case_tac "(bsimp r2) = AZERO") |
|
2554 apply(simp) |
|
2555 apply (simp add: bsimp_ASEQ0) |
|
2556 apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs") |
|
2557 apply(clarify) |
|
2558 apply(simp) |
|
2559 apply(subgoal_tac "bnullable r1") |
|
2560 prefer 2 |
|
2561 using b3 apply force |
|
2562 apply(simp) |
|
2563 apply(simp add: bsimp_ASEQ2) |
|
2564 prefer 2 |
|
2565 |
|
2566 |
|
2567 |
|
2568 apply(subst bsimp_ASEQ2) |
|
2569 |
|
2570 |
|
2571 |
|
2572 |
|
2573 |
|
2574 |
|
2575 lemma |
|
2576 assumes "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)" |
|
2577 shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)" |
|
2578 using assms |
|
2579 apply(induct s2 arbitrary: a s1) |
|
2580 apply(simp) |
|
2581 using bmkeps_simp apply blast |
|
2582 apply(simp add: bders_append) |
|
2583 apply(drule_tac x="aa" in meta_spec) |
|
2584 apply(drule_tac x="s1 @ [a]" in meta_spec) |
|
2585 apply(drule meta_mp) |
|
2586 apply(simp add: bders_append) |
|
2587 apply(simp add: bders_append) |
|
2588 apply(drule meta_mp) |
|
2589 apply (metis b4 bders.simps(2) bders_simp.simps(2)) |
|
2590 apply(simp) |
|
2591 |
|
2592 apply (met is b4 bders.simps(2) bders_simp.simps(2)) |
|
2593 |
|
2594 |
|
2595 |
|
2596 using b3 apply blast |
|
2597 using b3 apply auto[1] |
|
2598 apply(auto simp add: blex_def) |
|
2599 prefer 3 |
|
2600 |
|
2601 |
|
2602 |
|
2603 |
|
2604 |
2158 |
2605 end |
2159 end |