1722 where |
1722 where |
1723 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
1723 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
1724 |"nullable_bools r [] = []" |
1724 |"nullable_bools r [] = []" |
1725 |
1725 |
1726 |
1726 |
1727 lemma ders_simp_commute: |
1727 lemma shape_derssimp_seq: |
1728 shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase (bders_simp r s) = rerase (bsimp (bders r s))" |
1728 shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase (bders_simp r s) = rerase (bsimp (bders r s))" |
1729 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1729 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1730 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1730 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1731 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
1731 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
1732 apply(induct s arbitrary: r r1 r2 rule: rev_induct) |
1732 apply(induct s arbitrary: r r1 r2 rule: rev_induct) |
1743 apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))") |
1743 apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))") |
1744 prefer 2 |
1744 prefer 2 |
1745 apply presburger |
1745 apply presburger |
1746 sorry |
1746 sorry |
1747 |
1747 |
|
1748 lemma shape_derssimp_alts: |
|
1749 shows "rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))" |
|
1750 |
|
1751 |
1748 lemma finite_size_finite_regx: |
1752 lemma finite_size_finite_regx: |
1749 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
1753 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
1750 sorry |
1754 sorry |
1751 |
1755 |
1752 |
1756 |
1761 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1765 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1762 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
1766 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
1763 sorry |
1767 sorry |
1764 |
1768 |
1765 |
1769 |
|
1770 lemma finite_star: |
|
1771 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
|
1772 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
|
1773 sorry |
|
1774 |
|
1775 |
|
1776 lemma rderssimp_zero: |
|
1777 shows"rders_simp RZERO s = RZERO" |
|
1778 apply(induction s) |
|
1779 apply simp |
|
1780 by simp |
|
1781 |
|
1782 lemma rderssimp_one: |
|
1783 shows"rders_simp RONE (a # s) = RZERO" |
|
1784 apply(induction s) |
|
1785 apply simp |
|
1786 by simp |
|
1787 |
|
1788 lemma rderssimp_char: |
|
1789 shows "rders_simp (RCHAR c) s = RONE \<or> rders_simp (RCHAR c) s = RZERO \<or> rders_simp (RCHAR c) s = (RCHAR c)" |
|
1790 apply auto |
|
1791 by (metis rder.simps(2) rder.simps(3) rders_simp.elims rders_simp.simps(2) rderssimp_one rsimp.simps(4)) |
|
1792 |
1766 lemma finite_size_ders: |
1793 lemma finite_size_ders: |
1767 shows "\<forall>r. \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr" |
1794 shows " \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr" |
|
1795 apply(induct r rule: rrexp.induct) |
|
1796 apply auto |
|
1797 apply(rule_tac x = "2" in exI) |
|
1798 using rderssimp_zero rsize.simps(1) apply presburger |
|
1799 apply(rule_tac x = "2" in exI) |
|
1800 apply (metis Suc_1 lessI rders_simp.elims rderssimp_one rsize.simps(1) rsize.simps(2)) |
|
1801 apply(rule_tac x = "2" in meta_spec) |
|
1802 apply (metis lessI rderssimp_char rsize.simps(1) rsize.simps(2) rsize.simps(3)) |
|
1803 |
|
1804 using finite_seq apply blast |
|
1805 prefer 2 |
|
1806 |
|
1807 apply (simp add: finite_star) |
|
1808 sledgehammer |
1768 sorry |
1809 sorry |
1769 |
1810 |
1770 |
1811 |
1771 unused_thms |
1812 unused_thms |
1772 lemma seq_ders_shape: |
1813 lemma seq_ders_shape: |