1552 apply simp |
1552 apply simp |
1553 apply(subst rders_simp_append) |
1553 apply(subst rders_simp_append) |
1554 |
1554 |
1555 oops |
1555 oops |
1556 |
1556 |
|
1557 inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where |
|
1558 "RALTS rs \<leadsto>o rs" |
|
1559 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
|
1560 |
|
1561 |
1557 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
1562 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
1558 "sflat (RALT r1 r2) = sflat r1 @ [r2]" |
1563 "sflat (RALT r1 r2) = sflat r1 @ [r2]" |
1559 | "sflat (RALTS rs) = rs" |
1564 | "sflat (RALTS rs) = rs" |
1560 | "sflat r = [r]" |
1565 | "sflat r = [r]" |
|
1566 |
|
1567 lemma softrewrite_flat: |
|
1568 shows "r \<leadsto>o sflat r" |
|
1569 |
1561 |
1570 |
1562 lemma seq_sflat0: |
1571 lemma seq_sflat0: |
1563 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1572 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1564 (map (rders r2) (vsuf s r1))) )" |
1573 (map (rders r2) (vsuf s r1))) )" |
1565 |
1574 |
1578 ) ) = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) # |
1587 ) ) = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) # |
1579 (map (rders r2) (vsuf s r1)) |
1588 (map (rders r2) (vsuf s r1)) |
1580 )) )" |
1589 )) )" |
1581 sorry |
1590 sorry |
1582 |
1591 |
|
1592 lemma sflat_elemnum: |
|
1593 shows "sflat (RALTS [a1, a2, a3]) = [a1, a2, a3]" |
|
1594 sorry |
|
1595 |
|
1596 lemma sflat_emptyalts: |
|
1597 shows "sflat (RALTS xs) = [] \<Longrightarrow> xs = []" |
|
1598 using sflat.elims by auto |
|
1599 |
|
1600 lemma ralt_sflat_gte2: |
|
1601 shows "\<exists>ra rb rsc. sflat (RALT r1 r2) = ra # rb # rsc" |
|
1602 apply(case_tac r1) |
|
1603 apply simp+ |
|
1604 |
|
1605 oops |
|
1606 |
|
1607 lemma sflat_singleton: |
|
1608 shows "sflat (RALTS xs) = [a] \<Longrightarrow> xs = [a]" |
|
1609 apply(case_tac xs) |
|
1610 apply simp |
|
1611 apply(case_tac list) |
|
1612 apply simp |
|
1613 apply simp |
|
1614 oops |
|
1615 |
|
1616 thm sflat.elims |
|
1617 |
|
1618 |
|
1619 lemma sflat_ralts: |
|
1620 shows "sflat (RALTS xs) = sflat (RALTS xs') |
|
1621 \<Longrightarrow> rsimp (RALTS xs) = rsimp (RALTS xs')" |
|
1622 apply(induct xs) |
|
1623 |
|
1624 apply(case_tac xs) |
|
1625 apply simp |
|
1626 apply (metis list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp_ALTs.simps(1) sflat_emptyalts) |
|
1627 apply(case_tac list) |
|
1628 apply simp |
|
1629 apply |
|
1630 sledgehammer |
|
1631 |
|
1632 |
1583 |
1633 |
1584 |
1634 |
1585 lemma sflat_rsimpeq: |
1635 lemma sflat_rsimpeq: |
1586 shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1636 shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
|
1637 apply(cases r1 ) |
|
1638 apply(cases r2) |
|
1639 apply simp+ |
|
1640 apply(case_tac x5) |
|
1641 apply simp |
|
1642 apply(case_tac list) |
|
1643 apply simp |
|
1644 apply(case_tac lista) |
|
1645 apply simp |
|
1646 |
|
1647 |
1587 sorry |
1648 sorry |
1588 |
1649 |
1589 |
1650 |
1590 |
1651 |
1591 lemma seq_closed_form_general: |
1652 lemma seq_closed_form_general: |