1864 and "bders_simp AZERO s = AZERO" |
1889 and "bders_simp AZERO s = AZERO" |
1865 apply (induct s) |
1890 apply (induct s) |
1866 apply(auto) |
1891 apply(auto) |
1867 done |
1892 done |
1868 |
1893 |
|
1894 lemma LA: |
|
1895 assumes "\<Turnstile> v : ders s (erase r)" |
|
1896 shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)" |
|
1897 using assms |
|
1898 apply(induct s arbitrary: r v rule: rev_induct) |
|
1899 apply(simp) |
|
1900 apply(simp add: bders_append ders_append) |
|
1901 apply(subst bder_retrieve) |
|
1902 apply(simp) |
|
1903 apply(drule Prf_injval) |
|
1904 by (simp add: flex_append) |
|
1905 |
|
1906 |
|
1907 lemma LB: |
|
1908 assumes "s \<in> (erase r) \<rightarrow> v" |
|
1909 shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" |
|
1910 using assms |
|
1911 apply(induct s arbitrary: r v rule: rev_induct) |
|
1912 apply(simp) |
|
1913 apply(subgoal_tac "v = mkeps (erase r)") |
|
1914 prefer 2 |
|
1915 apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness) |
|
1916 apply(simp) |
|
1917 apply(simp add: flex_append ders_append) |
|
1918 by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex) |
|
1919 |
|
1920 lemma LB_sym: |
|
1921 assumes "s \<in> (erase r) \<rightarrow> v" |
|
1922 shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))" |
|
1923 using assms |
|
1924 by (simp add: LB) |
|
1925 |
|
1926 |
|
1927 lemma LC: |
|
1928 assumes "s \<in> (erase r) \<rightarrow> v" |
|
1929 shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))" |
|
1930 apply(simp) |
|
1931 by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable) |
|
1932 |
|
1933 |
|
1934 lemma L0: |
|
1935 assumes "bnullable a" |
|
1936 shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))" |
|
1937 using assms |
|
1938 by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness) |
|
1939 |
|
1940 thm bmkeps_retrieve |
|
1941 |
|
1942 lemma L0a: |
|
1943 assumes "s \<in> L(erase a)" |
|
1944 shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) = |
|
1945 retrieve (bders a s) (mkeps (erase (bders a s)))" |
|
1946 using assms |
|
1947 by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex) |
|
1948 |
|
1949 lemma L0aa: |
|
1950 assumes "s \<in> L (erase a)" |
|
1951 shows "[] \<in> erase (bsimp (bders a s)) \<rightarrow> mkeps (erase (bsimp (bders a s)))" |
|
1952 using assms |
|
1953 by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex) |
|
1954 |
|
1955 lemma L0aaa: |
|
1956 assumes "[c] \<in> L (erase a)" |
|
1957 shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bder c a)))" |
|
1958 using assms |
|
1959 by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject) |
|
1960 |
|
1961 lemma L0aaaa: |
|
1962 assumes "[c] \<in> L (erase a)" |
|
1963 shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bders a [c])))" |
|
1964 using assms |
|
1965 using L0aaa by auto |
|
1966 |
|
1967 |
|
1968 lemma L02: |
|
1969 assumes "bnullable (bder c a)" |
|
1970 shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) = |
|
1971 retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))" |
|
1972 using assms |
|
1973 apply(simp) |
|
1974 using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0 LA LB |
|
1975 apply(subst bder_retrieve[symmetric]) |
|
1976 apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness) |
|
1977 apply(simp) |
|
1978 done |
|
1979 |
|
1980 lemma L02_bders: |
|
1981 assumes "bnullable (bders a s)" |
|
1982 shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = |
|
1983 retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))" |
|
1984 using assms |
|
1985 by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness) |
|
1986 |
|
1987 |
|
1988 |
|
1989 |
|
1990 lemma L03: |
|
1991 assumes "bnullable (bder c a)" |
|
1992 shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = |
|
1993 bmkeps (bsimp (bder c (bsimp a)))" |
|
1994 using assms |
|
1995 by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) |
|
1996 |
|
1997 lemma L04: |
|
1998 assumes "bnullable (bder c a)" |
|
1999 shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = |
|
2000 retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" |
|
2001 using assms |
|
2002 by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness) |
|
2003 |
|
2004 lemma L05: |
|
2005 assumes "bnullable (bder c a)" |
|
2006 shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) = |
|
2007 retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" |
|
2008 using assms |
|
2009 using L04 by auto |
|
2010 |
|
2011 lemma L06: |
|
2012 assumes "bnullable (bder c a)" |
|
2013 shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))" |
|
2014 using assms |
|
2015 by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) |
|
2016 |
|
2017 lemma L07: |
|
2018 assumes "s \<in> L (erase r)" |
|
2019 shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) |
|
2020 = retrieve (bders r s) (mkeps (erase (bders r s)))" |
|
2021 using assms |
|
2022 using LB LC lexer_correct_Some by auto |
|
2023 |
|
2024 lemma LXXX: |
|
2025 assumes "s \<in> (erase r) \<rightarrow> v" "s \<in> (erase (bsimp r)) \<rightarrow> v'" |
|
2026 shows "retrieve r v = retrieve (bsimp r) v'" |
|
2027 using assms |
|
2028 apply - |
|
2029 thm LC |
|
2030 apply(subst LC) |
|
2031 apply(assumption) |
|
2032 apply(subst L0[symmetric]) |
|
2033 using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce |
|
2034 apply(subst (2) LC) |
|
2035 apply(assumption) |
|
2036 apply(subst (2) L0[symmetric]) |
|
2037 using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce |
|
2038 |
|
2039 oops |
|
2040 |
|
2041 |
|
2042 lemma L07a: |
|
2043 assumes "s \<in> L (erase r)" |
|
2044 shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r))))) |
|
2045 = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))" |
|
2046 using assms |
|
2047 apply(induct s arbitrary: r) |
|
2048 apply(simp) |
|
2049 using L0a apply force |
|
2050 apply(drule_tac x="(bder a r)" in meta_spec) |
|
2051 apply(drule meta_mp) |
|
2052 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2053 apply(drule sym) |
|
2054 apply(simp) |
|
2055 apply(subst (asm) bder_retrieve) |
|
2056 apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex) |
|
2057 apply(simp only: flex_fun_apply) |
|
2058 apply(simp) |
|
2059 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2060 |
|
2061 |
|
2062 lemma L08: |
|
2063 assumes "s \<in> L (erase r)" |
|
2064 shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s))) |
|
2065 = retrieve (bders r s) (mkeps (erase (bders r s)))" |
|
2066 using assms |
|
2067 apply(induct s arbitrary: r) |
|
2068 apply(simp) |
|
2069 using L0 bnullable_correctness nullable_correctness apply blast |
|
2070 apply(simp add: bders_append) |
|
2071 apply(drule_tac x="(bder a (bsimp r))" in meta_spec) |
|
2072 apply(drule meta_mp) |
|
2073 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2074 apply(drule sym) |
|
2075 apply(simp) |
|
2076 apply(subst LA) |
|
2077 apply (metis L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness) |
|
2078 apply(subst LA) |
|
2079 using lexer_correct_None lexer_flex mkeps_nullable apply force |
|
2080 |
|
2081 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2082 |
|
2083 thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars] |
|
2084 oops |
|
2085 |
|
2086 lemma test: |
|
2087 assumes "s = [c]" |
|
2088 shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)" |
|
2089 using assms |
|
2090 apply(simp only: bders.simps) |
|
2091 defer |
|
2092 using assms |
|
2093 apply(simp only: flex.simps id_simps) |
|
2094 using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] |
|
2095 find_theorems "retrieve (bders _ _) _" |
|
2096 find_theorems "retrieve _ (mkeps _)" |
|
2097 oops |
|
2098 |
|
2099 lemma L06X: |
|
2100 assumes "bnullable (bder c a)" |
|
2101 shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)" |
|
2102 using assms |
|
2103 apply(induct a arbitrary: c) |
|
2104 apply(simp) |
|
2105 apply(simp) |
|
2106 apply(simp) |
|
2107 prefer 3 |
|
2108 apply(simp) |
|
2109 prefer 2 |
|
2110 apply(simp) |
|
2111 |
|
2112 defer |
|
2113 apply(simp only: bnullable.simps) |
|
2114 oops |
|
2115 |
|
2116 lemma L06_2: |
|
2117 assumes "bnullable (bders a [c,d])" |
|
2118 shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))" |
|
2119 using assms |
|
2120 apply(simp) |
|
2121 by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness) |
|
2122 |
|
2123 lemma L06_bders: |
|
2124 assumes "bnullable (bders a s)" |
|
2125 shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))" |
|
2126 using assms |
|
2127 by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness) |
|
2128 |
|
2129 lemma LLLL: |
|
2130 shows "L (erase a) = L (erase (bsimp a))" |
|
2131 and "L (erase a) = {flat v | v. \<Turnstile> v: (erase a)}" |
|
2132 and "L (erase a) = {flat v | v. \<Turnstile> v: (erase (bsimp a))}" |
|
2133 using L_bsimp_erase apply(blast) |
|
2134 apply (simp add: L_flat_Prf) |
|
2135 using L_bsimp_erase L_flat_Prf apply(auto)[1] |
|
2136 done |
|
2137 |
|
2138 |
|
2139 |
|
2140 lemma LXX_bders: |
|
2141 assumes "" |
|
2142 shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" |
|
2143 using assms |
|
2144 apply(induct s arbitrary: a rule: rev_induct) |
|
2145 apply(simp add: bmkeps_simp) |
|
2146 apply(simp add: bders_append) |
|
2147 |
|
2148 |
|
2149 |
|
2150 lemma L07: |
|
2151 assumes "s \<in> L (erase a)" |
|
2152 shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))" |
|
2153 using assms |
|
2154 by (meson lexer_correct_None lexer_correctness(1) lexer_flex) |
|
2155 |
|
2156 lemma LX0: |
|
2157 assumes "s \<in> L r" |
|
2158 shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))" |
|
2159 by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex) |
|
2160 |
|
2161 |
|
2162 lemma L02_bders2: |
|
2163 assumes "bnullable (bders a s)" "s = [c]" |
|
2164 shows "retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s))) = |
|
2165 retrieve (bders a s) (mkeps (erase (bders a s)))" |
|
2166 using assms |
|
2167 apply(simp) |
|
2168 |
|
2169 apply(induct s arbitrary: a) |
|
2170 apply(simp) |
|
2171 using L0 apply auto[1] |
|
2172 apply(simp) |
|
2173 |
|
2174 thm bmkeps_retrieve bmkeps_simp Posix_mkeps |
|
2175 |
|
2176 lemma WQ1: |
|
2177 assumes "s \<in> L (der c r)" |
|
2178 shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))" |
|
2179 using assms |
|
2180 sorry |
|
2181 |
|
2182 lemma L02_bsimp: |
|
2183 assumes "bnullable (bders a s)" |
|
2184 shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = |
|
2185 retrieve a (flex (erase a) id s (mkeps (erase (bders a s))))" |
|
2186 using assms |
|
2187 apply(induct s arbitrary: a) |
|
2188 apply(simp) |
|
2189 apply (simp add: L0) |
|
2190 apply(simp) |
|
2191 apply(drule_tac x="bder a aa" in meta_spec) |
|
2192 apply(simp) |
|
2193 apply(subst (asm) bder_retrieve) |
|
2194 using Posix_Prf Posix_flex Posix_mkeps bnullable_correctness apply fastforce |
|
2195 apply(simp add: flex_fun_apply) |
|
2196 apply(drule sym) |
|
2197 apply(simp) |
|
2198 apply(subst flex_injval) |
|
2199 apply(subst bder_retrieve[symmetric]) |
|
2200 apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps bders.simps(2) bnullable_correctness ders.simps(2) erase_bders lexer_correct_None lexer_flex option.distinct(1)) |
|
2201 apply(simp only: erase_bder[symmetric] erase_bders[symmetric]) |
|
2202 apply(subst LB_sym[symmetric]) |
|
2203 apply(simp) |
|
2204 apply(rule WQ1) |
|
2205 apply(simp only: erase_bder[symmetric]) |
|
2206 apply(rule L07) |
|
2207 apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder erase_bders lexer_correct_None lexer_flex option.simps(3)) |
|
2208 |
|
2209 apply(simp) |
|
2210 (*sledgehammer [timeout = 6000]*) |
|
2211 |
|
2212 |
|
2213 using bder_retrieve |
|
2214 |
|
2215 |
|
2216 |
|
2217 lemma LX0MAIN: |
|
2218 assumes "s \<in> r \<rightarrow> v" |
|
2219 shows "decode (bmkeps (bders_simp (intern r) s)) r = Some(flex r id s v)" |
|
2220 using assms |
|
2221 apply(induct s arbitrary: r v) |
|
2222 apply(simp) |
|
2223 apply (metis LX0 Posix1(1) bders.simps(1) lexer_correctness(1) lexer_flex option.simps(3)) |
|
2224 apply(simp add: bders_simp_append ders_append flex_append) |
|
2225 apply(subst bmkeps_simp[symmetric]) |
|
2226 apply (met is L_bders_simp Posix1(1) bnullable_correctness der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) |
|
2227 (*apply(subgoal_tac "v = flex r id xs (injval (ders xs r) x (mkeps (ders (xs @ [x]) r)))") |
|
2228 prefer 2 |
|
2229 apply (metis Posix1(1) flex.simps(1) flex.simps(2) flex_append lexer_correct_None lexer_correctness(1) lexer_flex option.inject) |
|
2230 *) apply(drule_tac x="r" in meta_spec) |
|
2231 apply(drule_tac x="(mkeps (ders xs r))" in meta_spec) |
|
2232 apply(drule meta_mp) |
|
2233 |
|
2234 defer |
|
2235 apply(simp) |
|
2236 apply(drule sym) |
|
2237 apply(simp) |
|
2238 using bder_retrieve MAIN_decode |
|
2239 oops |
|
2240 |
|
2241 lemma LXaa: |
|
2242 assumes "s \<in> L (erase a)" |
|
2243 shows "decode (bmkeps (bsimp (bders (bsimp a) s))) (erase a) = decode (bmkeps (bders a s)) (erase a)" |
|
2244 using assms |
|
2245 apply(induct s arbitrary: a) |
|
2246 apply(simp) |
|
2247 using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1] |
|
2248 apply(simp) |
|
2249 apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec) |
|
2250 apply(drule meta_mp) |
|
2251 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2252 apply(subst (asm) bsimp_idem) |
|
2253 apply(subst bmkeps_simp[symmetric]) |
|
2254 apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness) |
|
2255 apply(subst (asm) bmkeps_simp[symmetric]) |
|
2256 apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness) |
|
2257 apply(subst bmkeps_retrieve) |
|
2258 apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) nullable_correctness) |
|
2259 apply(subst LA) |
|
2260 apply(simp) |
|
2261 apply (metis L_bsimp_erase ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable) |
|
2262 |
|
2263 |
|
2264 |
|
2265 lemma LXaa: |
|
2266 assumes "s \<in> L (erase a)" |
|
2267 shows "bmkeps (bsimp (bders (bsimp a) s)) = bmkeps (bders a s)" |
|
2268 using assms |
|
2269 apply(induct s arbitrary: a) |
|
2270 apply(simp) |
|
2271 using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1] |
|
2272 apply(simp) |
|
2273 apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec) |
|
2274 apply(drule meta_mp) |
|
2275 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2276 apply(subst (asm) bsimp_idem) |
|
2277 apply(subst bmkeps_simp[symmetric]) |
|
2278 apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness) |
|
2279 apply(subst (asm) bmkeps_simp[symmetric]) |
|
2280 apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness) |
|
2281 |
|
2282 |
|
2283 lemma LXaa: |
|
2284 assumes "s \<in> L (erase a)" |
|
2285 shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" |
|
2286 using assms |
|
2287 apply(induct s arbitrary: a) |
|
2288 apply(simp) |
|
2289 using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1] |
|
2290 apply(simp) |
|
2291 apply(drule_tac x="bder a aa" in meta_spec) |
|
2292 apply(drule meta_mp) |
|
2293 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2294 apply(drule sym) |
|
2295 apply(simp) |
|
2296 (* transformation to retrieve *) |
|
2297 apply(subst bmkeps_retrieve) |
|
2298 apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) ders_correctness erase_bders nullable_correctness) |
|
2299 apply(subst bmkeps_retrieve) |
|
2300 apply (metis b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer_correct_None lexer_flex) |
|
2301 apply(subst (2) LC[symmetric]) |
|
2302 prefer 2 |
|
2303 apply(subst L0) |
|
2304 apply(subst LA) |
|
2305 apply(simp) |
|
2306 apply (m etis L_bsimp_erase bders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable) |
|
2307 apply(subst LA) |
|
2308 apply(simp) |
|
2309 apply (m etis L0aa b3 b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer.simps(1) lexer_correctness(2) mkeps_nullable) |
|
2310 apply(subst (2) LB_sym[symmetric]) |
|
2311 prefer 2 |
|
2312 apply(subst L0) |
|
2313 apply(simp) |
|
2314 using lexer_correct_None lexer_flex apply fastforce |
|
2315 apply(subst (asm) bmkeps_retrieve) |
|
2316 apply (metis L_bsimp_erase bders.simps(2) erase_bders lexer_correct_None lexer_flex) |
|
2317 apply(subst (asm) bmkeps_retrieve) |
|
2318 apply (metis L0aa L_bsimp_erase b3 b4 bders_simp.simps(2) bnullable_correctness lexer.simps(1) lexer_correctness(2)) |
|
2319 apply(subst LA) |
|
2320 apply (met is L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness) |
|
2321 apply(subst LA) |
|
2322 using lexer_correct_None lexer_flex mkeps_nullable apply force |
|
2323 |
|
2324 using L0aaaa LB[OF L0aaaa] |
|
2325 apply(subst LB[OF L0aaaa]) |
|
2326 using L0aaaa |
|
2327 apply(rule L0aaaa) |
|
2328 |
|
2329 |
|
2330 |
|
2331 |
|
2332 |
|
2333 |
|
2334 |
|
2335 |
|
2336 lemma L00: |
|
2337 assumes "s \<in> L (erase a)" |
|
2338 shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = |
|
2339 retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))" |
|
2340 using assms |
|
2341 apply(induct s arbitrary: a taking: length rule: measure_induct) |
|
2342 apply(case_tac x) |
|
2343 apply(simp) |
|
2344 using L0 b3 bnullable_correctness nullable_correctness apply blast |
|
2345 apply(simp) |
|
2346 apply(drule_tac x="[]" in spec) |
|
2347 apply(simp) |
|
2348 apply(drule_tac x="bders (bsimp a) (aa#list)" in spec) |
|
2349 apply(simp) |
|
2350 apply(drule mp) |
|
2351 apply (metis L_bsimp_erase ders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness) |
|
2352 using bder_retrieve bmkeps_simp bmkeps_retrieve L0 LA LB LC L02 L03 L04 L05 |
|
2353 |
|
2354 oops |
|
2355 |
|
2356 lemma L00: |
|
2357 assumes "s \<in> L (erase (bsimp a))" |
|
2358 shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = |
|
2359 retrieve a (flex (erase a) id s (mkeps (ders s (erase a))))" |
|
2360 using assms |
|
2361 apply(induct s arbitrary: a) |
|
2362 apply(simp) |
|
2363 using L0 b3 bnullable_correctness nullable_correctness apply blast |
|
2364 apply(simp add: flex_append) |
|
2365 apply(drule_tac x="bder a aa" in meta_spec) |
|
2366 apply(drule meta_mp) |
|
2367 apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2368 apply(simp) |
|
2369 |
|
2370 (*using bmkeps_retrieve bder_retrieve*) |
|
2371 apply(subst (asm) bder_retrieve) |
|
2372 apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex) |
|
2373 apply(simp add: flex_fun_apply) |
|
2374 apply(drule sym) |
|
2375 apply(simp) |
|
2376 using bmkeps_retrieve bder_retrieve |
|
2377 oops |
|
2378 |
|
2379 lemma L0a: |
|
2380 assumes "s \<in> L (erase a)" |
|
2381 shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = |
|
2382 retrieve (bders a s) (mkeps (erase (bders a s)))" |
|
2383 using assms |
|
2384 apply(induct s arbitrary: a) |
|
2385 apply(simp) |
|
2386 apply(simp) |
|
2387 apply(drule_tac x="bsimp (bder a aa)" in meta_spec) |
|
2388 apply(drule meta_mp) |
|
2389 using L_bsimp_erase lexer_correct_None apply fastforce |
|
2390 apply(simp) |
|
2391 apply(subst LA) |
|
2392 apply (metis L_bsimp_erase ders.simps(2) ders_correctness erase_bder lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) |
|
2393 apply(subst LA) |
|
2394 apply(simp) |
|
2395 apply (metis ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable) |
|
2396 |
|
2397 apply(simp) |
|
2398 (* MAIN *) |
|
2399 |
|
2400 apply(subst L00) |
|
2401 apply (met is L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1)) |
|
2402 apply(simp) |
|
2403 done |
|
2404 |
|
2405 lemma L0a: |
|
2406 assumes "s \<in> L (erase a)" |
|
2407 shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = |
|
2408 retrieve (bders a s) (mkeps (erase (bders a s)))" |
|
2409 using assms |
|
2410 apply(induct s arbitrary: a rule: rev_induct) |
|
2411 apply(simp) |
|
2412 apply(simp add: bders_simp_append) |
|
2413 apply(subst L0) |
|
2414 apply (metis L_bders_simp bnullable_correctness der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness) |
|
2415 apply(subst bder_retrieve) |
|
2416 apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) |
|
2417 apply(simp add: bders_append) |
|
2418 apply(subst bder_retrieve) |
|
2419 apply (metis ders_snoc erase_bders lexer_correct_None lexer_flex mkeps_nullable) |
|
2420 apply(simp add: ders_append) |
|
2421 using bder_retrieve |
|
2422 |
|
2423 find_theorems "retrieve _ (injval _ _ _)" |
|
2424 find_theorems "mkeps (erase _)" |
|
2425 |
|
2426 |
|
2427 lemma L1: |
|
2428 assumes "s \<in> r \<rightarrow> v" |
|
2429 shows "decode (bmkeps (bders (intern r) s)) r = Some v" |
|
2430 using assms |
|
2431 by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1)) |
|
2432 |
|
2433 lemma L2: |
|
2434 assumes "s \<in> (der c r) \<rightarrow> v" |
|
2435 shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)" |
|
2436 using assms |
|
2437 apply(subst bmkeps_retrieve) |
|
2438 using Posix1(1) lexer_correct_None lexer_flex apply fastforce |
|
2439 using MAIN_decode |
|
2440 apply(subst MAIN_decode[symmetric]) |
|
2441 apply(simp) |
|
2442 apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable) |
|
2443 apply(simp) |
|
2444 apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))") |
|
2445 prefer 2 |
|
2446 apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1)) |
|
2447 apply(simp) |
|
2448 apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) = |
|
2449 (flex (der c r) ((\<lambda>v. injval r c v) o id) s (mkeps (ders s (der c r))))") |
|
2450 apply(simp) |
|
2451 using flex_fun_apply by blast |
|
2452 |
|
2453 lemma L3: |
|
2454 assumes "s2 \<in> (ders s1 r) \<rightarrow> v" |
|
2455 shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)" |
|
2456 using assms |
|
2457 apply(induct s1 arbitrary: r s2 v rule: rev_induct) |
|
2458 apply(simp) |
|
2459 using L1 apply blast |
|
2460 apply(simp add: ders_append) |
|
2461 apply(drule_tac x="r" in meta_spec) |
|
2462 apply(drule_tac x="x # s2" in meta_spec) |
|
2463 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
|
2464 apply(drule meta_mp) |
|
2465 defer |
|
2466 apply(simp) |
|
2467 apply(simp add: flex_append) |
|
2468 by (simp add: Posix_injval) |
|
2469 |
|
2470 lemma L4: |
|
2471 assumes "[c] \<in> r \<rightarrow> v" |
|
2472 shows "bmkeps (bder c (bsimp (intern r))) = code (flex r id [c] v)" |
|
2473 using assms |
|
2474 apply(subst bmkeps_retrieve) |
|
2475 apply (metis L_bsimp_erase Posix1(1) bders.simps(1) bders.simps(2) erase_bders erase_intern lexer_correct_None lexer_flex) |
|
2476 apply(subst bder_retrieve) |
|
2477 apply (metis L_bsimp_erase Posix1(1) bders.simps(1) bders.simps(2) erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable) |
|
2478 apply(simp) |
|
2479 |
|
2480 |
|
2481 |
|
2482 |
|
2483 |
|
2484 lemma |
|
2485 assumes "s \<in> L r" |
|
2486 shows "bmkeps (bders_simp (intern r) s) = bmkeps (bders (intern r) s)" |
|
2487 using assms |
|
2488 apply(induct s arbitrary: r rule: rev_induct) |
|
2489 apply(simp) |
|
2490 apply(simp add: bders_simp_append bders_append) |
|
2491 apply(subst bmkeps_simp[symmetric]) |
|
2492 apply (metis b4 bders.simps(1) bders.simps(2) bders_simp_append blexer_correctness blexer_def lexer_correct_None) |
|
2493 apply(subst bmkeps_retrieve) |
|
2494 apply(simp) |
|
2495 apply (metis L_bders_simp der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) |
|
2496 apply(subst bmkeps_retrieve) |
|
2497 apply(simp) |
|
2498 apply (metis ders_snoc lexer_correct_None lexer_flex) |
|
2499 apply(subst bder_retrieve) |
|
2500 apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) |
|
2501 apply(subst bder_retrieve) |
|
2502 apply (metis ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable) |
|
2503 using bmkeps_retrieve |
|
2504 find_theorems "retrieve (bders _ _) = _" |
|
2505 find_theorems "retrieve _ _ = _" |
|
2506 oops |
|
2507 |
|
2508 lemma |
|
2509 assumes "s \<in> r \<rightarrow> v" |
|
2510 shows "decode (bmkeps (bders_simp (intern r) s)) = Some v" |
|
2511 using assms |
|
2512 apply(induct s arbitrary: r v taking: length rule: measure_induct) |
|
2513 apply(subgoal_tac "x = [] \<or> (\<exists>a xs. x = xs @ [a])") |
|
2514 prefer 2 |
|
2515 apply (meson rev_exhaust) |
|
2516 apply(erule disjE) |
|
2517 apply(simp add: blexer_simp_def) |
|
2518 apply (metis Posix1(1) Posix_Prf Posix_determ Posix_mkeps bmkeps_retrieve erase_intern lexer.simps(1) lexer_correct_None retrieve_code) |
|
2519 apply(clarify) |
|
2520 apply(simp add: bders_simp_append) |
|
2521 apply(subst bmkeps_simp[symmetric]) |
|
2522 apply (metis b3 b4 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def lexer_correctness(1) option.distinct(1)) |
|
2523 apply(subst bmkeps_retrieve) |
|
2524 apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness) |
|
2525 apply(simp) |
|
2526 apply(subst bder_retrieve) |
|
2527 apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness) |
|
2528 |
|
2529 |
|
2530 find_theorems "bmkeps _ = _" |
|
2531 |
|
2532 apply(subgoal_tac "lexer r (xs @ [a]) = Some v") |
|
2533 prefer 2 |
|
2534 using lexer_correctness(1) apply blast |
|
2535 apply(simp (no_asm_simp) add: bders_simp_append) |
|
2536 apply(subst bmkeps_simp[symmetric]) |
|
2537 apply (m etis b4 bders.simps(1) bders.simps(2) bders_simp_append bnullable_correctness erase_bders erase_intern lexer_flex option.distinct(1)) |
|
2538 apply(subgoal_tac "nullable (ders (xs @ [a]) r)") |
|
2539 prefer 2 |
|
2540 apply (metis lexer_flex option.distinct(1)) |
|
2541 apply(simp add: lexer_flex) |
|
2542 apply(simp add: flex_append ders_append) |
|
2543 apply(drule_tac sym) |
|
2544 apply(simp) |
|
2545 using Posix_flex flex.simps Posix_flex2 |
|
2546 apply(drule_tac Posix_flex2) |
|
2547 apply (simp add: Prf_injval mkeps_nullable) |
|
2548 apply(drule_tac x="[a]" in spec) |
|
2549 apply(drule mp) |
|
2550 defer |
|
2551 apply(drule_tac x="ders xs r" in spec) |
|
2552 apply(drule_tac x="injval (ders xs r) a (mkeps (der a (ders xs r)))" in spec) |
|
2553 apply(simp) |
|
2554 apply(subst (asm) bmkeps_simp[symmetric]) |
|
2555 using bnullable_correctness apply fastforce |
|
2556 |
|
2557 |
|
2558 find_theorems "good (bsimp _)" |
|
2559 oops |
|
2560 |
|
2561 lemma |
|
2562 assumes "s \<in> L (erase a)" |
|
2563 shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)" |
|
2564 using assms |
|
2565 apply(induct s arbitrary: a taking : length rule: measure_induct) |
|
2566 apply(case_tac x) |
|
2567 apply(simp) |
|
2568 using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1] |
|
2569 using bsimp_idem apply auto[1] |
|
2570 apply(simp add: bders_append bders_simp_append) |
|
2571 apply(drule_tac x="bder a (bsimp aa)" in meta_spec) |
|
2572 apply(drule meta_mp) |
|
2573 defer |
|
2574 apply(simp) |
|
2575 oops |
|
2576 |
|
2577 |
|
2578 lemma |
|
2579 assumes "s \<in> L (erase r)" |
|
2580 shows "bmkeps (bders_simp r s) = bmkeps (bders r s)" |
|
2581 using assms |
|
2582 apply(induct s arbitrary: r) |
|
2583 apply(simp) |
|
2584 apply(simp add: bders_simp_append bders_append) |
|
2585 apply(drule_tac x="bsimp (bder a r)" in meta_spec) |
|
2586 apply(drule meta_mp) |
|
2587 defer |
|
2588 apply(simp) |
|
2589 |
|
2590 find_theorems "good (bsimp _)" |
|
2591 oops |
|
2592 |
|
2593 lemma |
|
2594 assumes "s \<in> L r" |
|
2595 shows "decode (bmkeps (bders_simp (intern r) s)) r = Some (flex r id s (mkeps (ders s r)))" |
|
2596 using assms |
|
2597 apply(induct s arbitrary: r) |
|
2598 apply(simp) |
|
2599 using bmkeps_retrieve decode_code mkeps_nullable nullable_correctness retrieve_code apply auto[1] |
|
2600 apply(simp add: bders_simp_append) |
|
2601 apply(subst bmkeps_simp[symmetric]) |
|
2602 apply(subgoal_tac "[] \<in> L (ders (xs @ [x]) r)") |
|
2603 prefer 2 |
|
2604 apply (meson Posix1(1) lexer_correct_None lexer_flex nullable_correctness) |
|
2605 apply(simp add: ders_append) |
|
2606 using L_bders_simp bnullable_correctness der_correctness nullable_correctness apply f orce |
|
2607 apply(simp add: flex_append ders_append) |
|
2608 apply(drule_tac x="der x r" in meta_spec) |
|
2609 apply(simp add: ders_append) |
|
2610 find_theorems "intern _" |
|
2611 find_theorems "bmkeps (bsimp _)" |
|
2612 |
|
2613 find_theorems "(_ # _) \<in> _ \<rightarrow> _" |
|
2614 oops |
|
2615 |
1869 |
2616 |
1870 lemma ZZZ: |
2617 lemma ZZZ: |
1871 assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)" |
2618 assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)" |
1872 shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))" |
2619 shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))" |
1873 using assms |
2620 using assms |
2209 apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9)) |
2902 apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9)) |
2210 apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1") |
2903 apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1") |
2211 prefer 2 |
2904 prefer 2 |
2212 apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq) |
2905 apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq) |
2213 apply(auto) |
2906 apply(auto) |
2214 sledgehammer [timeout=6000] |
2907 oops |
2215 |
2908 |
2216 |
2909 |
2217 |
2910 lemma |
2218 |
2911 assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]" |
2219 defer |
2912 shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))" |
2220 apply(case_tac list) |
2913 using assms |
2221 apply(simp) |
2914 apply(simp) |
2222 prefer 2 |
2915 oops |
2223 apply(simp) |
2916 |
2224 apply (simp add: bsimp_fuse bsimp_idem) |
2917 lemma |
2225 apply(case_tac a) |
2918 assumes "rs = [AALTs bs0 [AALTs bsa [AONE bsb, AONE bsb]]]" |
2226 apply(simp_all) |
2919 shows "flts [bsimp_AALTs bs (flts rs)] = flts (map (fuse bs) rs)" |
2227 |
2920 using assms |
2228 |
2921 apply(simp only:) |
2229 apply(subst k0b) |
2922 apply(simp only: flts.simps append_Nil2 List.list.map fuse.simps) |
2230 apply(simp) |
2923 apply(simp only: bsimp_AALTs.simps) |
2231 apply(subst (asm) k0) |
2924 apply(simp only: fuse.simps) |
2232 apply(subst (asm) (2) k0) |
2925 apply(simp only: flts.simps append_Nil2) |
2233 |
2926 find_theorems "nonnested (bsimp_AALTs _ _)" |
2234 |
2927 find_theorems "map _ (_ # _) = _" |
2235 find_theorems "asize _ < asize _" |
2928 apply(induct rs arbitrary: bs rule: flts.induct) |
2236 using bsimp_AALTs_size3 |
2929 apply(auto) |
2237 apply - |
2930 apply(case_tac rs) |
2238 apply(drule_tac x="a # list" in meta_spec) |
2931 apply(simp) |
2239 apply(drule_tac x="bs" in meta_spec) |
2932 |
2240 apply(drule meta_mp) |
2933 oops |
2241 apply(simp) |
2934 |
2242 apply(simp) |
2935 find_theorems "asize (bsimp _)" |
2243 apply(drule_tac x="(bsimp a) # list" in spec) |
2936 |
2244 apply(drule mp) |
2937 lemma CT1: |
2245 apply(simp) |
2938 shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map bsimp as))" |
2246 apply(case_tac list) |
2939 apply(induct as arbitrary: bs) |
2247 apply(simp) |
2940 apply(simp) |
2248 prefer 2 |
2941 apply(simp) |
2249 apply(simp) |
2942 by (simp add: bsimp_idem comp_def) |
2250 apply(subst (asm) k0) |
2943 |
2251 apply(subst (asm) (2) k0) |
2944 lemma CT1a: |
2252 thm k0 |
2945 shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))" |
2253 apply(subst (asm) k0b) |
2946 by (metis CT1 list.simps(8) list.simps(9)) |
2254 apply(simp) |
2947 |
2255 apply(simp) |
2948 (* CT *) |
2256 |
2949 |
2257 defer |
2950 lemma CTU: |
2258 apply(simp) |
2951 shows "bsimp_AALTs bs as = li bs as" |
2259 apply(case_tac list) |
2952 apply(induct bs as rule: li.induct) |
2260 apply(simp) |
2953 apply(auto) |
2261 defer |
2954 done |
2262 apply(simp) |
2955 |
2263 find_theorems "asize _ < asize _" |
2956 thm flts.simps |
2264 find_theorems "asize _ < asize _" |
2957 |
2265 apply(subst k0b) |
2958 |
2266 apply(simp) |
2959 lemma CTa: |
2267 apply(simp) |
2960 assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO" |
2268 |
2961 shows "flts as = as" |
2269 |
2962 using assms |
2270 apply(rule nn11a) |
2963 apply(induct as) |
2271 apply(simp) |
2964 apply(simp) |
2272 apply (metis good.simps(1) good1 good_fuse) |
2965 apply(case_tac as) |
2273 apply(simp) |
2966 apply(simp) |
2274 using fuse_append apply blast |
2967 apply (simp add: k0b) |
2275 apply(subgoal_tac "\<exists>bs rs. bsimp x43 = AALTs bs rs") |
2968 using flts_nothing by auto |
2276 prefer 2 |
2969 |
2277 using nonalt.elims(3) apply blast |
2970 lemma CT0: |
2278 apply(clarify) |
2971 assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" |
2279 apply(simp) |
2972 shows "flts [bsimp_AALTs bs1 as1] = flts (map (fuse bs1) as1)" |
2280 apply(case_tac rs) |
2973 using assms CTa |
2281 apply(simp) |
2974 apply(induct as1 arbitrary: bs1) |
2282 apply (metis arexp.distinct(7) good.simps(4) good1) |
2975 apply(simp) |
2283 apply(simp) |
2976 apply(simp) |
2284 apply(case_tac list) |
2977 apply(case_tac as1) |
2285 apply(simp) |
2978 apply(simp) |
2286 apply (metis arexp.distinct(7) good.simps(5) good1) |
2979 apply(simp) |
2287 apply(simp) |
2980 proof - |
2288 |
2981 fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list" |
2289 |
2982 assume a1: "nonalt a \<and> a \<noteq> AZERO \<and> nonalt aa \<and> aa \<noteq> AZERO \<and> (\<forall>r\<in>set list. nonalt r \<and> r \<noteq> AZERO)" |
2290 |
2983 assume a2: "\<And>as. \<forall>r\<in>set as. nonalt r \<and> r \<noteq> AZERO \<Longrightarrow> flts as = as" |
2291 |
2984 assume a3: "as1a = aa # list" |
2292 |
2985 have "flts [a] = [a]" |
2293 |
2986 using a1 k0b by blast |
2294 find_theorems "flts [_] = [_]" |
2987 then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)" |
2295 apply(case_tac x52) |
2988 using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9)) |
2296 apply(simp) |
2989 qed |
2297 apply(simp) |
2990 |
2298 apply(case_tac list) |
2991 |
2299 apply(simp) |
2992 lemma CT01: |
2300 apply(case_tac a) |
2993 assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" "\<forall>r \<in> set as2. nonalt r \<and> r \<noteq> AZERO" |
2301 apply(simp_all) |
2994 shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] = flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))" |
|
2995 using assms CT0 |
|
2996 by (metis k0 k00) |
|
2997 |
|
2998 |
|
2999 lemma CTT: |
|
3000 assumes "\<forall>r\<in>set (flts (map (bsimp \<circ> bder c) as1)). nonalt r \<and> r \<noteq> AZERO" |
|
3001 "\<forall>r\<in>set (flts (map (bsimp \<circ> bder c) as2)). nonalt r \<and> r \<noteq> AZERO" |
|
3002 shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) |
|
3003 = XXX" |
|
3004 apply(subst bsimp_idem[symmetric]) |
|
3005 apply(simp) |
|
3006 apply(subst CT01) |
|
3007 apply(rule assms) |
|
3008 apply(rule assms) |
|
3009 (* CT *) |
|
3010 |
|
3011 lemma |
|
3012 shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) |
|
3013 = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @ |
|
3014 (map (fuse bs2) (map (bder c) as2))))" |
|
3015 apply(subst bsimp_idem[symmetric]) |
|
3016 apply(simp) |
|
3017 oops |
|
3018 |
|
3019 lemma CT_exp: |
|
3020 assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
3021 shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))" |
|
3022 using assms |
|
3023 apply(induct as) |
|
3024 apply(auto) |
|
3025 done |
|
3026 |
|
3027 lemma asize_set: |
|
3028 assumes "a \<in> set as" |
|
3029 shows "asize a < Suc (sum_list (map asize as))" |
|
3030 using assms |
|
3031 apply(induct as arbitrary: a) |
|
3032 apply(auto) |
|
3033 using le_add2 le_less_trans not_less_eq by blast |
2302 |
3034 |
2303 |
3035 |
2304 lemma XXX2a_long_without_good: |
3036 lemma XXX2a_long_without_good: |
2305 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
3037 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2306 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
3038 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2309 apply(simp) |
3041 apply(simp) |
2310 apply(simp) |
3042 apply(simp) |
2311 prefer 3 |
3043 prefer 3 |
2312 apply(simp) |
3044 apply(simp) |
2313 (* AALT case *) |
3045 (* AALT case *) |
|
3046 prefer 2 |
|
3047 apply(simp del: bsimp.simps) |
|
3048 apply(subst (2) CT1) |
|
3049 apply(subst CT_exp) |
|
3050 apply(auto)[1] |
|
3051 using asize_set apply blast |
|
3052 apply(subst CT1[symmetric]) |
|
3053 apply(simp) |
|
3054 oops |
|
3055 |
|
3056 lemma big: |
|
3057 shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) = |
|
3058 bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))" |
|
3059 apply(simp add: comp_def bder_fuse) |
|
3060 apply(simp add: flts_append) |
|
3061 |
|
3062 sorry |
|
3063 |
|
3064 lemma XXX2a_long_without_good: |
|
3065 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
3066 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
|
3067 apply(case_tac x) |
|
3068 apply(simp) |
|
3069 apply(simp) |
|
3070 apply(simp) |
|
3071 prefer 3 |
|
3072 apply(simp) |
|
3073 (* AALT case *) |
2314 prefer 2 |
3074 prefer 2 |
|
3075 apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]") |
|
3076 apply(clarify) |
|
3077 apply(simp del: bsimp.simps) |
|
3078 apply(subst (2) CT1) |
|
3079 apply(simp del: bsimp.simps) |
|
3080 apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst) |
|
3081 apply(simp del: bsimp.simps) |
|
3082 apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst) |
|
3083 apply(simp del: bsimp.simps) |
|
3084 apply(subst CT1a[symmetric]) |
|
3085 apply(subst bsimp.simps) |
|
3086 apply(simp del: bsimp.simps) |
|
3087 apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1") |
|
3088 apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2") |
|
3089 apply(clarify) |
|
3090 apply(simp only:) |
|
3091 apply(simp del: bsimp.simps bder.simps) |
|
3092 apply(subst bsimp_AALTs_qq) |
|
3093 prefer 2 |
|
3094 apply(simp del: bsimp.simps) |
|
3095 apply(subst big) |
|
3096 prefer 2 |
|
3097 apply (metis (no_types, lifting) Nil_is_append_conv Nil_is_map_conv One_nat_def Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_0_conv length_append length_greater_0_conv less_Suc0 less_add_same_cancel1) |
|
3098 apply(simp add: comp_def bder_fuse) |
|
3099 |
|
3100 thm bder_fuse |
|
3101 |
|
3102 find_theorems "1 < length _" |
|
3103 |
|
3104 (* CT *) |
|
3105 (* |
|
3106 under assumption that bsimp a1 = AALT; bsimp a = AALT |
|
3107 |
|
3108 bsimp (AALT x51 (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) = |
|
3109 bsimp (AALTs x51 (map (fuse bs1) (map (bder c) as1)) @ ( map (fuse bs2) (map (bder c) as2))) |
|
3110 |
|
3111 bsimp_AALTs x51 (flts (map bsimp [a1, a2]))) |
|
3112 = bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]) |
|
3113 |
|
3114 *) |
|
3115 |
|
3116 apply(case_tac "bsimp a1") |
|
3117 prefer 5 |
|
3118 apply(simp only:) |
|
3119 apply(case_tac "bsimp a2") |
|
3120 apply(simp) |
|
3121 |
|
3122 prefer 5 |
|
3123 apply(simp only:) |
|
3124 apply(simp only: bder.simps) |
|
3125 apply(simp) |
|
3126 |
|
3127 |
|
3128 |
|
3129 |
|
3130 prefer 2 |
|
3131 using nn1b apply blast |
2315 apply(simp only:) |
3132 apply(simp only:) |
2316 apply(simp) |
3133 apply(case_tac x52) |
|
3134 apply(simp) |
|
3135 apply(simp only:) |
|
3136 apply(case_tac "\<exists>bsa rsa. a = AALTs bsa rsa") |
|
3137 apply(clarify) |
|
3138 apply(simp) |
|
3139 apply(frule_tac x="AALTs x51 ((map (fuse bsa) rsa) @ list)" in spec) |
|
3140 apply(drule mp) |
|
3141 apply(simp) |
|
3142 apply (simp add: qq) |
|
3143 apply(drule_tac x="c" in spec) |
|
3144 apply(simp only: bder.simps) |
|
3145 apply(simp) |
|
3146 apply(subst k0) |
|
3147 apply(subst (2) k0) |
|
3148 apply(subst (asm) (2) flts_append) |
|
3149 apply(rotate_tac 2) |
|
3150 |
|
3151 |
|
3152 lemma XXX2a_long_without_good: |
|
3153 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
3154 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
|
3155 apply(case_tac x) |
|
3156 apply(simp) |
|
3157 apply(simp) |
|
3158 apply(simp) |
|
3159 prefer 3 |
|
3160 apply(simp) |
|
3161 (* AALT case *) |
|
3162 prefer 2 |
|
3163 apply(subgoal_tac "nonnested (bsimp x)") |
|
3164 prefer 2 |
|
3165 using nn1b apply blast |
|
3166 apply(simp only:) |
|
3167 apply(drule_tac x="AALTs x51 (flts x52)" in spec) |
|
3168 apply(drule mp) |
|
3169 defer |
|
3170 apply(drule_tac x="c" in spec) |
|
3171 apply(simp) |
|
3172 apply(rotate_tac 2) |
|
3173 |
|
3174 apply(drule sym) |
|
3175 apply(simp) |
|
3176 |
|
3177 apply(simp only: bder.simps) |
|
3178 apply(simp only: bsimp.simps) |
2317 apply(subst bder_bsimp_AALTs) |
3179 apply(subst bder_bsimp_AALTs) |
2318 apply(case_tac x52) |
3180 apply(case_tac x52) |
2319 apply(simp) |
3181 apply(simp) |
2320 apply(simp) |
3182 apply(simp) |
|
3183 apply(case_tac list) |
|
3184 apply(simp) |
|
3185 apply(case_tac a) |
|
3186 apply(simp) |
|
3187 apply(simp) |
|
3188 apply(simp) |
|
3189 defer |
|
3190 apply(simp) |
|
3191 |
|
3192 |
|
3193 (* case AALTs list is not empty *) |
|
3194 apply(simp) |
|
3195 apply(subst k0) |
|
3196 apply(subst (2) k0) |
|
3197 apply(simp) |
|
3198 apply(case_tac "bsimp a = AZERO") |
|
3199 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
3200 prefer 2 |
|
3201 using less_iff_Suc_add apply auto[1] |
|
3202 apply(simp) |
|
3203 apply(drule_tac x="AALTs x51 list" in spec) |
|
3204 apply(drule mp) |
|
3205 apply(simp add: asize0) |
|
3206 apply(drule_tac x="c" in spec) |
|
3207 apply(simp add: bder_bsimp_AALTs) |
|
3208 apply(case_tac "nonalt (bsimp a)") |
|
3209 prefer 2 |
|
3210 apply(drule_tac x="bsimp (AALTs x51 (a#list))" in spec) |
|
3211 apply(drule mp) |
|
3212 apply(rule order_class.order.strict_trans2) |
|
3213 apply(rule bsimp_AALTs_size3) |
|
3214 apply(auto)[1] |
|
3215 apply(simp) |
|
3216 apply(subst (asm) bsimp_idem) |
|
3217 apply(drule_tac x="c" in spec) |
|
3218 apply(simp) |
|
3219 find_theorems "_ < _ \<Longrightarrow> _ \<le> _ \<Longrightarrow>_ < _" |
|
3220 apply(rule le_trans) |
|
3221 apply(subgoal_tac "flts [bsimp a] = [bsimp a]") |
|
3222 prefer 2 |
|
3223 using k0b apply blast |
|
3224 apply(simp) |
|
3225 find_theorems "asize _ < asize _" |
|
3226 |
|
3227 using bder_bsimp_AALTs |
2321 apply(case_tac list) |
3228 apply(case_tac list) |
2322 apply(simp) |
3229 apply(simp) |
|
3230 sledgeha mmer [timeout=6000] |
2323 |
3231 |
2324 apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r") |
3232 apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r") |
2325 apply(drule_tac x="bsimp (AALTs x51 x52)" in spec) |
3233 apply(drule_tac x="bsimp (AALTs x51 x52)" in spec) |
2326 apply(drule mp) |
3234 apply(drule mp) |
2327 using bsimp_AALTs_size3 apply blast |
3235 using bsimp_AALTs_size3 apply blast |