1621 shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})" |
1611 shows "rsimp_SEQ (rsimp r1) (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp r1) (rsimp r2)]) {})" |
1622 by (metis idem_after_simp1 rsimp.simps(1)) |
1612 by (metis idem_after_simp1 rsimp.simps(1)) |
1623 |
1613 |
1624 |
1614 |
1625 |
1615 |
1626 lemma vsuf_der_stepwise: |
|
1627 shows "rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1))) = |
|
1628 rsimp (rder x (rsimp (RALTS (RSEQ (rders_simp r1 xs) r2 # map (rders_simp r2) (vsuf xs r1)))))" |
|
1629 apply simp |
|
1630 apply(subst rders_simp_append) |
|
1631 |
|
1632 oops |
|
1633 |
|
1634 inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where |
|
1635 "RALTS rs \<leadsto>o rs" |
|
1636 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
|
1637 |
1616 |
1638 |
1617 |
1639 fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where |
1618 fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where |
1640 "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs" |
1619 "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs" |
1641 | "sflat_aux (RALTS []) = []" |
1620 | "sflat_aux (RALTS []) = []" |
1885 |
1857 |
1886 |
1858 |
1887 |
1859 |
1888 |
1860 |
1889 lemma sflat_rsimpeq: |
1861 lemma sflat_rsimpeq: |
1890 shows "sflat_aux r1 = sflat_aux r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1862 shows "created_by_seq r1 \<Longrightarrow> sflat_aux r1 = rs \<Longrightarrow> rsimp r1 = rsimp (RALTS rs)" |
1891 apply(cases r1 ) |
1863 apply(induct r1 arbitrary: rs rule: created_by_seq.induct) |
1892 apply(cases r2) |
1864 apply simp |
1893 apply simp+ |
1865 using rsimp_seq_equal1 apply force |
1894 apply(case_tac x5) |
1866 by (metis head_one_more_simp rsimp.simps(2) sflat_aux.simps(1) simp_flatten) |
1895 apply simp |
|
1896 apply(case_tac list) |
|
1897 apply simp |
|
1898 |
|
1899 |
|
1900 |
|
1901 sorry |
|
1902 |
1867 |
1903 |
1868 |
1904 |
1869 |
1905 lemma seq_closed_form_general: |
1870 lemma seq_closed_form_general: |
1906 shows "rsimp (rders (RSEQ r1 r2) s) = |
1871 shows "rsimp (rders (RSEQ r1 r2) s) = |
1907 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1872 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1908 apply(case_tac "s \<noteq> []") |
1873 apply(case_tac "s \<noteq> []") |
1909 apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = sflat_aux (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))") |
1874 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) s)") |
|
1875 apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))") |
1910 using sflat_rsimpeq apply blast |
1876 using sflat_rsimpeq apply blast |
1911 using seq_sfau0 apply blast |
1877 apply (simp add: seq_sfau0) |
|
1878 using recursively_derseq1 apply blast |
1912 apply simp |
1879 apply simp |
1913 by (metis idem_after_simp1 rsimp.simps(1)) |
1880 by (metis idem_after_simp1 rsimp.simps(1)) |
1914 |
1881 |
|
1882 |
1915 |
1883 |
1916 lemma seq_closed_form_aux1: |
1884 lemma seq_closed_form_aux1: |
1917 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
1885 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
1918 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1886 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1919 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem) |
1887 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem) |
1984 apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x])) |
1952 apply(subgoal_tac "rsimp (rders_simp (RSEQ r1 r2) (xs @ [x])) |
1985 = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))") |
1953 = rsimp (RALTS (RSEQ (rders_simp r1 (xs @ [x])) r2 # map (rders_simp r2) (vsuf (xs @ [x]) r1)))") |
1986 apply force |
1954 apply force |
1987 by presburger |
1955 by presburger |
1988 |
1956 |
|
1957 |
|
1958 lemma star_closed_form_seq1: |
|
1959 shows "sflat_aux (rders (RSTAR r0) (c # s)) = |
|
1960 RSEQ (rders (rder c r0) s) (RSTAR r0) # |
|
1961 map (rders (RSTAR r0)) (vsuf s (rder c r0))" |
|
1962 apply simp |
|
1963 using seq_sfau0 by blast |
|
1964 |
|
1965 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where |
|
1966 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" |
|
1967 | "hflat_aux r = [r]" |
|
1968 |
|
1969 |
|
1970 fun hflat :: "rrexp \<Rightarrow> rrexp" where |
|
1971 "hflat (RALT r1 r2) = RALTS ((hflat_aux r1) @ (hflat_aux r2))" |
|
1972 | "hflat r = r" |
|
1973 |
|
1974 inductive created_by_star :: "rrexp \<Rightarrow> bool" where |
|
1975 "created_by_star (RSEQ ra (RSTAR rb))" |
|
1976 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)" |
|
1977 |
|
1978 fun hElem :: "rrexp \<Rightarrow> rrexp list" where |
|
1979 "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)" |
|
1980 | "hElem r = [r]" |
|
1981 |
|
1982 |
|
1983 |
|
1984 |
|
1985 lemma cbs_ders_cbs: |
|
1986 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)" |
|
1987 apply(induct r rule: created_by_star.induct) |
|
1988 apply simp |
|
1989 using created_by_star.intros(1) created_by_star.intros(2) apply auto[1] |
|
1990 by (metis (mono_tags, lifting) created_by_star.simps list.simps(8) list.simps(9) rder.simps(4)) |
|
1991 |
|
1992 lemma star_ders_cbs: |
|
1993 shows "created_by_star (rders (RSEQ r1 (RSTAR r2)) s)" |
|
1994 apply(induct s rule: rev_induct) |
|
1995 apply simp |
|
1996 apply (simp add: created_by_star.intros(1)) |
|
1997 apply(subst rders_append) |
|
1998 apply simp |
|
1999 using cbs_ders_cbs by auto |
|
2000 |
|
2001 lemma created_by_star_cases: |
|
2002 shows "created_by_star r \<Longrightarrow> \<exists>ra rb. (r = RALT ra rb \<and> created_by_star ra \<and> created_by_star rb) \<or> r = RSEQ ra rb " |
|
2003 by (meson created_by_star.cases) |
|
2004 |
|
2005 |
|
2006 |
|
2007 lemma hfau_pushin: |
|
2008 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))" |
|
2009 apply(induct r rule: created_by_star.induct) |
|
2010 apply simp |
|
2011 apply(subgoal_tac "created_by_star (rder c r1)") |
|
2012 prefer 2 |
|
2013 apply(subgoal_tac "created_by_star (rder c r2)") |
|
2014 using cbs_ders_cbs apply blast |
|
2015 using cbs_ders_cbs apply auto[1] |
|
2016 apply simp |
|
2017 done |
|
2018 |
|
2019 lemma stupdate_induct1: |
|
2020 shows " concat (map (hElem \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
|
2021 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
|
2022 apply(induct Ss) |
|
2023 apply simp+ |
|
2024 by (simp add: rders_append) |
|
2025 |
|
2026 |
|
2027 |
|
2028 lemma stupdates_join_general: |
|
2029 shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) = |
|
2030 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" |
|
2031 apply(induct xs arbitrary: Ss) |
|
2032 apply (simp) |
|
2033 prefer 2 |
|
2034 apply auto[1] |
|
2035 using stupdate_induct1 by blast |
|
2036 |
|
2037 |
|
2038 |
|
2039 |
|
2040 lemma stupdates_join: |
|
2041 shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) = |
|
2042 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 [[c]])" |
|
2043 using stupdates_join_general by auto |
|
2044 |
|
2045 |
|
2046 |
|
2047 lemma star_hfau_induct: |
|
2048 shows "hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) s) = |
|
2049 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])" |
|
2050 apply(induct s rule: rev_induct) |
|
2051 apply simp |
|
2052 apply(subst rders_append)+ |
|
2053 apply simp |
|
2054 apply(subst stupdates_append) |
|
2055 apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)") |
|
2056 prefer 2 |
|
2057 apply (simp add: star_ders_cbs) |
|
2058 apply(subst hfau_pushin) |
|
2059 apply simp |
|
2060 apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = |
|
2061 concat (map hElem (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") |
|
2062 apply(simp only:) |
|
2063 prefer 2 |
|
2064 apply presburger |
|
2065 apply(subst stupdates_append[symmetric]) |
|
2066 using stupdates_join_general by blast |
|
2067 |
|
2068 |
|
2069 |
|
2070 lemma star_closed_form_seq2: |
|
2071 shows "RSEQ (rders (rder c r0) s) (RSTAR r0) # map (rders (RSTAR r0)) (vsuf s (rder c r0)) = |
|
2072 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])" |
|
2073 apply(induct s rule: rev_induct) |
|
2074 apply simp |
|
2075 apply(subst rders_append)+ |
|
2076 apply(case_tac "rnullable (rder c r0)") |
|
2077 apply simp |
|
2078 |
|
2079 sorry |
|
2080 |
|
2081 |
|
2082 lemma star_closed_form1: |
|
2083 shows "rders (RSTAR r0) (c#s) = |
|
2084 ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
|
2085 |
|
2086 |
|
2087 sorry |
|
2088 |
|
2089 lemma star_closed_form: |
|
2090 shows "rders_simp (RSTAR r0) (c#s) = |
|
2091 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
|
2092 apply(induct s) |
|
2093 apply simp |
|
2094 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) |
|
2095 |
|
2096 |
|
2097 sorry |
|
2098 |
|
2099 |
1989 lemma simp_helps_der_pierce: |
2100 lemma simp_helps_der_pierce: |
1990 shows " rsimp |
2101 shows " rsimp |
1991 (rder x |
2102 (rder x |
1992 (rsimp_ALTs rs)) = |
2103 (rsimp_ALTs rs)) = |
1993 rsimp |
2104 rsimp |