1998 (* AALTs case *) |
1989 (* AALTs case *) |
1999 apply(simp) |
1990 apply(simp) |
2000 using test2 by fastforce |
1991 using test2 by fastforce |
2001 |
1992 |
2002 lemma XXX2a_long_without_good: |
1993 lemma XXX2a_long_without_good: |
|
1994 assumes "a = AALTs bs0 [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]" |
2003 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
1995 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2004 apply(induct a arbitrary: c taking: asize rule: measure_induct) |
1996 "bsimp (bder c (bsimp a)) = XXX" |
|
1997 "bsimp (bder c a) = YYY" |
|
1998 using assms |
|
1999 apply(simp) |
|
2000 using assms |
|
2001 apply(simp) |
|
2002 prefer 2 |
|
2003 using assms |
|
2004 apply(simp) |
|
2005 oops |
|
2006 |
|
2007 lemma bder_bsimp_AALTs: |
|
2008 shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)" |
|
2009 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
2010 apply(simp) |
|
2011 apply(simp) |
|
2012 apply (simp add: bder_fuse) |
|
2013 apply(simp) |
|
2014 done |
|
2015 |
|
2016 lemma flts_nothing: |
|
2017 assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r" |
|
2018 shows "flts rs = rs" |
|
2019 using assms |
|
2020 apply(induct rs rule: flts.induct) |
|
2021 apply(auto) |
|
2022 done |
|
2023 |
|
2024 lemma flts_flts: |
|
2025 assumes "\<forall>r \<in> set rs. good r" |
|
2026 shows "flts (flts rs) = flts rs" |
|
2027 using assms |
|
2028 apply(induct rs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct) |
|
2029 apply(case_tac x) |
|
2030 apply(simp) |
|
2031 apply(simp) |
|
2032 apply(case_tac a) |
|
2033 apply(simp_all add: bder_fuse flts_append) |
|
2034 apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO") |
|
2035 prefer 2 |
|
2036 apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2) |
|
2037 apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r") |
|
2038 prefer 2 |
|
2039 apply (metis n0 nn1b test2) |
|
2040 by (metis flts_fuse flts_nothing) |
|
2041 |
|
2042 lemma "good (bsimp a) \<or> bsimp a = AZERO" |
|
2043 by (simp add: good1) |
|
2044 |
|
2045 |
|
2046 lemma |
|
2047 assumes "bnullable (bders r s)" "good r" |
|
2048 shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)" |
|
2049 using assms |
|
2050 apply(induct s arbitrary: r) |
|
2051 apply(simp) |
|
2052 using bmkeps_simp apply auto[1] |
|
2053 apply(simp) |
|
2054 by (simp add: test2) |
|
2055 |
|
2056 lemma PP: |
|
2057 assumes "bnullable (bders r s)" |
|
2058 shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)" |
|
2059 using assms |
|
2060 apply(induct s arbitrary: r) |
|
2061 apply(simp) |
|
2062 using bmkeps_simp apply auto[1] |
|
2063 apply(simp add: bders_append bders_simp_append) |
|
2064 oops |
|
2065 |
|
2066 lemma PP: |
|
2067 assumes "bnullable (bders r s)" |
|
2068 shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)" |
|
2069 using assms |
|
2070 apply(induct s arbitrary: r rule: rev_induct) |
|
2071 apply(simp) |
|
2072 using bmkeps_simp apply auto[1] |
|
2073 apply(simp add: bders_append bders_simp_append) |
|
2074 apply(drule_tac x="bder a (bsimp r)" in meta_spec) |
|
2075 apply(drule_tac meta_mp) |
|
2076 defer |
|
2077 oops |
|
2078 |
|
2079 |
|
2080 lemma |
|
2081 assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]" |
|
2082 shows "bsimp a = a" |
|
2083 using assms |
|
2084 apply(simp) |
|
2085 oops |
|
2086 |
|
2087 |
|
2088 lemma iii: |
|
2089 assumes "bsimp_AALTs bs rs \<noteq> AZERO" |
|
2090 shows "rs \<noteq> []" |
|
2091 using assms |
|
2092 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
2093 apply(auto) |
|
2094 done |
|
2095 |
|
2096 lemma |
|
2097 assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y" |
|
2098 "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))" |
|
2099 "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO" |
|
2100 shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52" |
|
2101 using assms |
|
2102 apply(induct x52 arbitrary: x51) |
|
2103 apply(simp) |
|
2104 |
|
2105 |
|
2106 |
|
2107 lemma |
|
2108 assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO" |
|
2109 shows "bsimp a = a" |
|
2110 using assms |
|
2111 apply(induct a taking: asize rule: measure_induct) |
|
2112 apply(case_tac x) |
|
2113 apply(simp_all) |
|
2114 apply(case_tac "(bsimp x42) = AZERO") |
|
2115 apply(simp add: asize0) |
|
2116 apply(case_tac "(bsimp x43) = AZERO") |
|
2117 apply(simp add: asize0) |
|
2118 apply (metis bsimp_ASEQ0) |
|
2119 apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs") |
|
2120 apply(auto)[1] |
|
2121 apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less) |
|
2122 apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less) |
|
2123 (* ALT case *) |
|
2124 apply(frule iii) |
|
2125 apply(case_tac x52) |
|
2126 apply(simp) |
|
2127 apply(simp) |
|
2128 apply(subst k0) |
|
2129 apply(subst (asm) k0) |
|
2130 apply(subst (asm) (2) k0) |
|
2131 apply(subst (asm) (3) k0) |
|
2132 apply(case_tac "(bsimp a) = AZERO") |
|
2133 apply(simp) |
|
2134 apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt) |
|
2135 apply(simp) |
|
2136 apply(case_tac "nonalt (bsimp a)") |
|
2137 prefer 2 |
|
2138 apply(drule_tac x="AALTs x51 (bsimp a # list)" in spec) |
|
2139 apply(drule mp) |
|
2140 apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons) |
|
2141 apply(drule mp) |
|
2142 apply(simp) |
|
2143 apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons) |
|
2144 apply(drule mp) |
|
2145 apply(simp) |
|
2146 using bsimp_idem apply auto[1] |
|
2147 apply(simp add: bsimp_idem) |
|
2148 apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons) |
|
2149 apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2)) |
|
2150 apply(subgoal_tac "flts [bsimp a] = [bsimp a]") |
|
2151 prefer 2 |
|
2152 using k0b apply blast |
|
2153 apply(clarify) |
|
2154 apply(simp only:) |
|
2155 apply(simp) |
|
2156 apply(case_tac "flts (map bsimp list) = Nil") |
|
2157 apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less) |
|
2158 apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) = AALTs x51 (bsimp a # flts (map bsimp list))") |
|
2159 prefer 2 |
|
2160 apply (metis bsimp_AALTs.simps(3) neq_Nil_conv) |
|
2161 apply(auto) |
|
2162 apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt) |
|
2163 |
|
2164 apply(drule_tac x="AALTs x51 list" in spec) |
|
2165 apply(drule mp) |
|
2166 apply(auto simp add: asize0)[1] |
|
2167 |
|
2168 |
|
2169 |
|
2170 (* HERE*) |
|
2171 |
|
2172 |
|
2173 |
|
2174 |
|
2175 |
|
2176 lemma OOO: |
|
2177 shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))" |
|
2178 apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct) |
|
2179 apply(case_tac x) |
|
2180 apply(simp) |
|
2181 apply(simp) |
|
2182 apply(case_tac "a = AZERO") |
|
2183 apply(simp) |
|
2184 apply(case_tac "list") |
|
2185 apply(simp) |
|
2186 apply(simp) |
|
2187 apply(case_tac "bsimp a = AZERO") |
|
2188 apply(simp) |
|
2189 apply(case_tac "list") |
|
2190 apply(simp) |
|
2191 apply(simp add: bsimp_fuse[symmetric]) |
|
2192 apply(simp) |
|
2193 apply(case_tac "nonalt (bsimp a)") |
|
2194 apply(case_tac list) |
|
2195 apply(simp) |
|
2196 apply(subst k0b) |
|
2197 apply(simp) |
|
2198 apply(simp) |
|
2199 apply(simp add: bsimp_fuse) |
|
2200 apply(simp) |
|
2201 apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a") |
|
2202 prefer 2 |
|
2203 using bsimp_size le_neq_implies_less apply blast |
|
2204 apply(erule disjE) |
|
2205 apply(drule_tac x="(bsimp a) # list" in spec) |
|
2206 apply(drule mp) |
|
2207 apply(simp) |
|
2208 apply(simp) |
|
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)) |
|
2210 apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs \<and> rs \<noteq> Nil \<and> length rs > 1") |
|
2211 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) |
|
2213 apply(auto) |
|
2214 sledgehammer [timeout=6000] |
|
2215 |
|
2216 |
|
2217 |
|
2218 |
|
2219 defer |
|
2220 apply(case_tac list) |
|
2221 apply(simp) |
|
2222 prefer 2 |
|
2223 apply(simp) |
|
2224 apply (simp add: bsimp_fuse bsimp_idem) |
|
2225 apply(case_tac a) |
|
2226 apply(simp_all) |
|
2227 |
|
2228 |
|
2229 apply(subst k0b) |
|
2230 apply(simp) |
|
2231 apply(subst (asm) k0) |
|
2232 apply(subst (asm) (2) k0) |
|
2233 |
|
2234 |
|
2235 find_theorems "asize _ < asize _" |
|
2236 using bsimp_AALTs_size3 |
|
2237 apply - |
|
2238 apply(drule_tac x="a # list" in meta_spec) |
|
2239 apply(drule_tac x="bs" in meta_spec) |
|
2240 apply(drule meta_mp) |
|
2241 apply(simp) |
|
2242 apply(simp) |
|
2243 apply(drule_tac x="(bsimp a) # list" in spec) |
|
2244 apply(drule mp) |
|
2245 apply(simp) |
|
2246 apply(case_tac list) |
|
2247 apply(simp) |
|
2248 prefer 2 |
|
2249 apply(simp) |
|
2250 apply(subst (asm) k0) |
|
2251 apply(subst (asm) (2) k0) |
|
2252 thm k0 |
|
2253 apply(subst (asm) k0b) |
|
2254 apply(simp) |
|
2255 apply(simp) |
|
2256 |
|
2257 defer |
|
2258 apply(simp) |
|
2259 apply(case_tac list) |
|
2260 apply(simp) |
|
2261 defer |
|
2262 apply(simp) |
|
2263 find_theorems "asize _ < asize _" |
|
2264 find_theorems "asize _ < asize _" |
|
2265 apply(subst k0b) |
|
2266 apply(simp) |
|
2267 apply(simp) |
|
2268 |
|
2269 |
|
2270 apply(rule nn11a) |
|
2271 apply(simp) |
|
2272 apply (metis good.simps(1) good1 good_fuse) |
|
2273 apply(simp) |
|
2274 using fuse_append apply blast |
|
2275 apply(subgoal_tac "\<exists>bs rs. bsimp x43 = AALTs bs rs") |
|
2276 prefer 2 |
|
2277 using nonalt.elims(3) apply blast |
|
2278 apply(clarify) |
|
2279 apply(simp) |
|
2280 apply(case_tac rs) |
|
2281 apply(simp) |
|
2282 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
2283 apply(simp) |
|
2284 apply(case_tac list) |
|
2285 apply(simp) |
|
2286 apply (metis arexp.distinct(7) good.simps(5) good1) |
|
2287 apply(simp) |
|
2288 |
|
2289 |
|
2290 |
|
2291 |
|
2292 |
|
2293 |
|
2294 find_theorems "flts [_] = [_]" |
|
2295 apply(case_tac x52) |
|
2296 apply(simp) |
|
2297 apply(simp) |
|
2298 apply(case_tac list) |
|
2299 apply(simp) |
|
2300 apply(case_tac a) |
|
2301 apply(simp_all) |
|
2302 |
|
2303 |
|
2304 lemma XXX2a_long_without_good: |
|
2305 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
|
2306 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2005 apply(case_tac x) |
2307 apply(case_tac x) |
2006 apply(simp) |
2308 apply(simp) |
2007 apply(simp) |
2309 apply(simp) |
2008 apply(simp) |
2310 apply(simp) |
2009 prefer 3 |
2311 prefer 3 |
2010 apply(simp) |
2312 apply(simp) |
2011 apply(simp) |
2313 (* AALT case *) |
2012 apply(auto)[1] |
2314 prefer 2 |
|
2315 apply(simp only:) |
|
2316 apply(simp) |
|
2317 apply(subst bder_bsimp_AALTs) |
|
2318 apply(case_tac x52) |
|
2319 apply(simp) |
|
2320 apply(simp) |
|
2321 apply(case_tac list) |
|
2322 apply(simp) |
|
2323 |
|
2324 apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r") |
|
2325 apply(drule_tac x="bsimp (AALTs x51 x52)" in spec) |
|
2326 apply(drule mp) |
|
2327 using bsimp_AALTs_size3 apply blast |
|
2328 apply(drule_tac x="c" in spec) |
|
2329 apply(subst (asm) (2) test) |
|
2330 |
|
2331 apply(case_tac x52) |
|
2332 apply(simp) |
|
2333 apply(simp) |
|
2334 apply(case_tac "bsimp a = AZERO") |
|
2335 apply(simp) |
|
2336 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
2337 prefer 2 |
|
2338 apply auto[1] |
|
2339 apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2) |
|
2340 apply(simp) |
|
2341 apply(drule_tac x="AALTs x51 list" in spec) |
|
2342 apply(drule mp) |
|
2343 apply(simp add: asize0) |
|
2344 apply(simp) |
|
2345 apply(case_tac list) |
|
2346 prefer 2 |
|
2347 apply(simp) |
|
2348 apply(case_tac "bsimp aa = AZERO") |
|
2349 apply(simp) |
|
2350 apply(subgoal_tac "bsimp (bder c aa) = AZERO") |
|
2351 prefer 2 |
|
2352 apply auto[1] |
|
2353 apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1) |
|
2354 apply(simp) |
|
2355 apply(drule_tac x="AALTs x51 (a#lista)" in spec) |
|
2356 apply(drule mp) |
|
2357 apply(simp add: asize0) |
|
2358 apply(simp) |
|
2359 apply (metis flts.simps(2) k0) |
|
2360 apply(subst k0) |
|
2361 apply(subst (2) k0) |
|
2362 |
|
2363 |
|
2364 using less_add_Suc1 apply fastforce |
|
2365 apply(subst k0) |
|
2366 |
|
2367 |
|
2368 apply(simp) |
|
2369 apply(case_tac "bsimp a = AZERO") |
|
2370 apply(simp) |
|
2371 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
2372 prefer 2 |
|
2373 apply auto[1] |
|
2374 apply(simp) |
|
2375 apply(case_tac "nonalt (bsimp a)") |
|
2376 apply(subst bsimp_AALTs1) |
|
2377 apply(simp) |
|
2378 using less_add_Suc1 apply fastforce |
|
2379 |
|
2380 apply(subst bsimp_AALTs1) |
|
2381 |
|
2382 using nn11a apply b last |
|
2383 |
|
2384 (* SEQ case *) |
|
2385 apply(clarify) |
|
2386 apply(subst bsimp.simps) |
|
2387 apply(simp del: bsimp.simps) |
|
2388 apply(auto simp del: bsimp.simps)[1] |
|
2389 apply(subgoal_tac "bsimp x42 \<noteq> AZERO") |
|
2390 prefer 2 |
|
2391 using b3 apply force |
|
2392 apply(case_tac "bsimp x43 = AZERO") |
|
2393 apply(simp) |
|
2394 apply (simp add: bsimp_ASEQ0) |
|
2395 apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2) |
|
2396 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
|
2397 apply(clarify) |
|
2398 apply(simp) |
|
2399 apply(subst bsimp_ASEQ2) |
|
2400 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |
|
2401 prefer 2 |
|
2402 using less_add_Suc1 apply fastforce |
|
2403 apply(simp) |
|
2404 apply(frule_tac x="x43" in spec) |
|
2405 apply(drule mp) |
|
2406 apply(simp) |
|
2407 apply(drule_tac x="c" in spec) |
|
2408 apply(subst bder_fuse) |
|
2409 apply(subst bsimp_fuse[symmetric]) |
|
2410 apply(simp) |
|
2411 apply(subgoal_tac "bmkeps x42 = bs") |
|
2412 prefer 2 |
|
2413 apply (simp add: bmkeps_simp) |
|
2414 apply(simp) |
|
2415 apply(subst bsimp_fuse[symmetric]) |
|
2416 apply(case_tac "nonalt (bsimp (bder c x43))") |
|
2417 apply(subst bsimp_AALTs1) |
|
2418 using nn11a apply blast |
|
2419 using fuse_append apply blast |
|
2420 apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs") |
|
2421 prefer 2 |
|
2422 using bbbbs1 apply blast |
|
2423 apply(clarify) |
|
2424 apply(simp) |
|
2425 apply(case_tac rs) |
|
2426 apply(simp) |
|
2427 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
2428 apply(simp) |
|
2429 apply(case_tac list) |
|
2430 apply(simp) |
|
2431 apply (metis arexp.distinct(7) good.simps(5) good1) |
|
2432 apply(simp del: bsimp_AALTs.simps) |
|
2433 apply(simp only: bsimp_AALTs.simps) |
|
2434 apply(simp) |
|
2435 |
|
2436 |
|
2437 |
|
2438 |
|
2439 (* HERE *) |
2013 apply(case_tac "x42 = AZERO") |
2440 apply(case_tac "x42 = AZERO") |
2014 apply(simp) |
2441 apply(simp) |
2015 apply(case_tac "bsimp x43 = AZERO") |
2442 apply(case_tac "bsimp x43 = AZERO") |
2016 apply(simp) |
2443 apply(simp) |
2017 apply (simp add: bsimp_ASEQ0) |
2444 apply (simp add: bsimp_ASEQ0) |
2018 apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO") |
2445 apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO") |
2019 apply(simp) |
2446 apply(simp) |
2020 apply (metis bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2) |
2447 apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2) |
2021 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
2448 apply(case_tac "\<exists>bs. bsimp x42 = AONE bs") |
2022 apply(clarify) |
2449 apply(clarify) |
2023 apply(simp) |
2450 apply(simp) |
2024 apply(subst bsimp_ASEQ2) |
2451 apply(subst bsimp_ASEQ2) |
2025 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |
2452 apply(subgoal_tac "bsimp (bder c x42) = AZERO") |