2199 apply(subst bder_retrieve[symmetric]) |
2188 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)) |
2189 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]) |
2190 apply(simp only: erase_bder[symmetric] erase_bders[symmetric]) |
2202 apply(subst LB_sym[symmetric]) |
2191 apply(subst LB_sym[symmetric]) |
2203 apply(simp) |
2192 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 |
2193 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 |
2194 |
2427 lemma L1: |
2195 lemma L1: |
2428 assumes "s \<in> r \<rightarrow> v" |
2196 assumes "s \<in> r \<rightarrow> v" |
2429 shows "decode (bmkeps (bders (intern r) s)) r = Some v" |
2197 shows "decode (bmkeps (bders (intern r) s)) r = Some v" |
2430 using assms |
2198 using assms |
2464 apply(drule meta_mp) |
2232 apply(drule meta_mp) |
2465 defer |
2233 defer |
2466 apply(simp) |
2234 apply(simp) |
2467 apply(simp add: flex_append) |
2235 apply(simp add: flex_append) |
2468 by (simp add: Posix_injval) |
2236 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 |
|
2616 |
|
2617 lemma ZZZ: |
|
2618 assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)" |
|
2619 shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))" |
|
2620 using assms |
|
2621 apply(induct x52) |
|
2622 apply(simp) |
|
2623 apply(simp) |
|
2624 apply(case_tac "bsimp a = AZERO") |
|
2625 apply(simp) |
|
2626 apply(subgoal_tac "bsimp (bder c a) = AZERO") |
|
2627 prefer 2 |
|
2628 using less_add_Suc1 apply fastforce |
|
2629 apply(simp) |
|
2630 apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs") |
|
2631 apply(clarify) |
|
2632 apply(simp) |
|
2633 apply(subst k0) |
|
2634 apply(case_tac "rs = []") |
|
2635 apply(simp) |
|
2636 apply(subgoal_tac "bsimp (bder c a) = AALTs bs []") |
|
2637 apply(simp) |
|
2638 apply (metis arexp.distinct(7) good.simps(4) good1) |
|
2639 oops |
|
2640 |
|
2641 |
2237 |
2642 |
2238 |
2643 |
2239 |
2644 lemma bders_snoc: |
2240 lemma bders_snoc: |
2645 "bder c (bders a s) = bders a (s @ [c])" |
2241 "bder c (bders a s) = bders a (s @ [c])" |
3095 apply(subst big) |
2662 apply(subst big) |
3096 prefer 2 |
2663 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) |
2664 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) |
2665 apply(simp add: comp_def bder_fuse) |
3099 |
2666 |
3100 thm bder_fuse |
2667 oops |
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 |
|
3132 apply(simp only:) |
|
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 |
2668 |
3152 lemma XXX2a_long_without_good: |
2669 lemma XXX2a_long_without_good: |
3153 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
2670 shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" |
3154 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
2671 apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct) |
3155 apply(case_tac x) |
2672 apply(case_tac x) |