1440 lemma bsimp_idem: |
1440 lemma bsimp_idem: |
1441 shows "bsimp (bsimp r) = bsimp r" |
1441 shows "bsimp (bsimp r) = bsimp r" |
1442 apply(induct r rule: bsimp.induct) |
1442 apply(induct r rule: bsimp.induct) |
1443 apply(auto) |
1443 apply(auto) |
1444 using bsimp_ASEQ_idem apply presburger |
1444 using bsimp_ASEQ_idem apply presburger |
1445 oops |
1445 sorry |
|
1446 |
1446 |
1447 |
1447 lemma neg: |
1448 lemma neg: |
1448 shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and> (r2 \<leadsto>* bsimp r1) )" |
1449 shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and> (r2 \<leadsto>* bsimp r1) )" |
1449 apply(rule notI) |
1450 apply(rule notI) |
1450 apply(erule exE) |
1451 apply(erule exE) |
1451 apply(erule conjE) |
1452 apply(erule conjE) |
1452 oops |
1453 oops |
1453 |
1454 |
1454 |
1455 |
1455 |
1456 |
1456 |
|
1457 lemma reduction_always_in_bsimp: |
1457 lemma reduction_always_in_bsimp: |
1458 shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False" |
1458 shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False" |
1459 apply(erule rrewrite.cases) |
1459 apply(erule rrewrite.cases) |
1460 apply simp |
1460 apply simp |
1461 apply auto |
1461 apply auto |
1462 |
1462 |
1463 oops |
1463 oops |
1464 |
1464 |
|
1465 |
|
1466 |
1465 (* |
1467 (* |
1466 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] |
1468 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] |
1467 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto> |
1469 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto> |
1468 fuse [] (AALTs bs1, [a, b]) |
1470 fuse [] (AALTs bs1, [a, b]) |
1469 rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ] |
1471 rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ] |
1476 |
1478 |
1477 (*r' size bsimp r > size r' |
1479 (*r' size bsimp r > size r' |
1478 r' \<leadsto>* bsimp bsimp r |
1480 r' \<leadsto>* bsimp bsimp r |
1479 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1481 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1480 |
1482 |
1481 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
1483 fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
|
1484 where |
|
1485 "orderedSufAux (Suc 0) ss = Nil" |
|
1486 |"orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)" |
|
1487 |"orderedSufAux 0 ss = Nil" |
|
1488 |
|
1489 fun |
|
1490 orderedSuf :: "char list \<Rightarrow> char list list" |
|
1491 where |
|
1492 "orderedSuf s = orderedSufAux (length s) s" |
|
1493 |
|
1494 lemma shape_of_suf_2list: |
|
1495 shows "orderedSuf [c1, c2] = [[c2]]" |
|
1496 apply auto |
|
1497 done |
|
1498 |
|
1499 |
|
1500 lemma shape_of_suf_3list: |
|
1501 shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3]]" |
|
1502 apply auto |
|
1503 done |
|
1504 |
|
1505 |
|
1506 |
|
1507 datatype rrexp = |
|
1508 RZERO |
|
1509 | RONE |
|
1510 | RCHAR char |
|
1511 | RSEQ rrexp rrexp |
|
1512 | RALTS "rrexp list" |
|
1513 | RSTAR rrexp |
|
1514 |
|
1515 abbreviation |
|
1516 "RALT r1 r2 \<equiv> RALTS [r1, r2]" |
|
1517 |
|
1518 fun |
|
1519 rerase :: "arexp \<Rightarrow> rrexp" |
|
1520 where |
|
1521 "rerase AZERO = RZERO" |
|
1522 | "rerase (AONE _) = RONE" |
|
1523 | "rerase (ACHAR _ c) = RCHAR c" |
|
1524 | "rerase (AALTs bs rs) = RALTS (map rerase rs)" |
|
1525 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" |
|
1526 | "rerase (ASTAR _ r) = RSTAR (rerase r)" |
|
1527 |
|
1528 |
|
1529 |
|
1530 |
|
1531 fun |
|
1532 rnullable :: "rrexp \<Rightarrow> bool" |
|
1533 where |
|
1534 "rnullable (RZERO) = False" |
|
1535 | "rnullable (RONE ) = True" |
|
1536 | "rnullable (RCHAR c) = False" |
|
1537 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
|
1538 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
|
1539 | "rnullable (RSTAR r) = True" |
|
1540 |
|
1541 |
|
1542 fun |
|
1543 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
1544 where |
|
1545 "rder c (RZERO) = RZERO" |
|
1546 | "rder c (RONE) = RZERO" |
|
1547 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)" |
|
1548 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
|
1549 | "rder c (RSEQ r1 r2) = |
|
1550 (if rnullable r1 |
|
1551 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
|
1552 else RSEQ (rder c r1) r2)" |
|
1553 | "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" |
|
1554 |
|
1555 |
|
1556 fun |
|
1557 rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
1558 where |
|
1559 "rders r [] = r" |
|
1560 | "rders r (c#s) = rders (rder c r) s" |
|
1561 |
|
1562 fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list" |
|
1563 where |
|
1564 "rdistinct [] acc = []" |
|
1565 | "rdistinct (x#xs) acc = |
|
1566 (if x \<in> acc then rdistinct xs acc |
|
1567 else x # (rdistinct xs ({x} \<union> acc)))" |
|
1568 |
|
1569 |
|
1570 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
|
1571 where |
|
1572 "rflts [] = []" |
|
1573 | "rflts (RZERO # rs) = rflts rs" |
|
1574 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
|
1575 | "rflts (r1 # rs) = r1 # rflts rs" |
|
1576 |
|
1577 |
|
1578 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
|
1579 where |
|
1580 "rsimp_ALTs [] = RZERO" |
|
1581 | "rsimp_ALTs [r] = r" |
|
1582 | "rsimp_ALTs rs = RALTS rs" |
|
1583 |
|
1584 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
1585 where |
|
1586 "rsimp_SEQ RZERO _ = RZERO" |
|
1587 | "rsimp_SEQ _ RZERO = RZERO" |
|
1588 | "rsimp_SEQ RONE r2 = r2" |
|
1589 | "rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
1590 |
|
1591 |
|
1592 fun rsimp :: "rrexp \<Rightarrow> rrexp" |
|
1593 where |
|
1594 "rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)" |
|
1595 | "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) " |
|
1596 | "rsimp r = r" |
|
1597 |
|
1598 |
|
1599 fun |
|
1600 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
1601 where |
|
1602 "rders_simp r [] = r" |
|
1603 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
|
1604 |
|
1605 |
|
1606 lemma rerase_bsimp: |
|
1607 shows "rerase (bsimp r) = rsimp (rerase r)" |
|
1608 apply(induct r) |
|
1609 apply auto |
|
1610 |
|
1611 |
|
1612 sorry |
|
1613 |
|
1614 lemma rerase_bder: |
|
1615 shows "rerase (bder c r) = rder c (rerase r)" |
|
1616 apply(induct r) |
|
1617 apply auto |
|
1618 sorry |
|
1619 |
|
1620 lemma rders_shape: |
|
1621 shows "rders_simp (RSEQ r1 r2) s = |
|
1622 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
|
1623 (map (rders r2) (orderedSuf s))) )" |
|
1624 sorry |
|
1625 |
|
1626 |
|
1627 lemma ders_simp_commute: |
|
1628 shows "rerase (bsimp (bders_simp r s)) = rerase (bsimp (bders r s))" |
|
1629 apply(induct s arbitrary: r rule: rev_induct) |
|
1630 apply simp |
|
1631 apply (simp add: bders_simp_append bders_append ) |
|
1632 apply (simp add: rerase_bsimp) |
|
1633 apply (simp add: rerase_bder) |
|
1634 apply (simp add: rders_shape) |
|
1635 sledgehammer |
|
1636 oops |
|
1637 |
1482 |
1638 |
1483 |
1639 |
1484 unused_thms |
1640 unused_thms |
|
1641 lemma seq_ders_shape: |
|
1642 shows "E" |
|
1643 |
|
1644 oops |
|
1645 |
|
1646 (*rsimp (rders (RSEQ r1 r2) s) = |
|
1647 rsimp RALT [RSEQ (rders r1 s) r2, rders r2 si, ...] |
|
1648 where si is the i-th shortest suffix of s such that si \<in> L r2" |
|
1649 *) |
1485 |
1650 |
1486 |
1651 |
1487 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
1652 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
1488 where |
1653 where |
1489 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
1654 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |