Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/BitCoded.thy
changeset 343 f139bdc0dcd5
parent 341 abf178a5db58
child 382 aef235b965bb
equal deleted inserted replaced
342:f0e876ed43fa 343:f139bdc0dcd5 
   565   "flts [] = []"
 
   565   "flts [] = []"
 
   566 | "flts (AZERO # rs) = flts rs"
 
   566 | "flts (AZERO # rs) = flts rs"
 
   567 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 
   567 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 
   568 | "flts (r1 # rs) = r1 # flts rs"
 
   568 | "flts (r1 # rs) = r1 # flts rs"
 
   569 
   569 
       
   570 
       
   571 
       
   572 
   570 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
 
   573 fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
 
   571   where
 
   574   where
 
   572   "li _ [] = AZERO"
 
   575   "li _ [] = AZERO"
 
   573 | "li bs [a] = fuse bs a"
 
   576 | "li bs [a] = fuse bs a"
 
   574 | "li bs as = AALTs bs as"
 
   577 | "li bs as = AALTs bs as"
 
       
   578 
       
   579 
   575 
   580 
   576 
   581 
   577 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
 
   582 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
 
   578   where
 
   583   where
 
   579   "bsimp_ASEQ _ AZERO _ = AZERO"
 
   584   "bsimp_ASEQ _ AZERO _ = AZERO"
 
  1080   shows "\<forall>r \<in>  set (flts rs). nonalt r"
 
  1085   shows "\<forall>r \<in>  set (flts rs). nonalt r"
 
  1081   using assms
 
  1086   using assms
 
  1082   apply(induct rs arbitrary: bs rule: flts.induct)
 
  1087   apply(induct rs arbitrary: bs rule: flts.induct)
 
  1083         apply(auto)
 
  1088         apply(auto)
 
  1084   done
 
  1089   done
 
       
  1090 
       
  1091 
  1085 
  1092 
  1086 lemma rt:
 
  1093 lemma rt:
 
  1087   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
 
  1094   shows "sum_list (map asize (flts (map bsimp rs))) \<le> sum_list (map asize rs)"
 
  1088   apply(induct rs)
 
  1095   apply(induct rs)
 
  1089    apply(simp)
 
  1096    apply(simp)
 
  1781   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
  1788   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
 
  1782   apply(induct a arbitrary: bs c)
 
  1789   apply(induct a arbitrary: bs c)
 
  1783        apply(simp_all)
 
  1790        apply(simp_all)
 
  1784   done
 
  1791   done
 
  1785 
  1792 
       
  1793 
       
  1794 fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
 
       
  1795   where 
       
  1796   "flts2 _ [] = []"
 
       
  1797 | "flts2 c (AZERO # rs) = flts2 c rs"
 
       
  1798 | "flts2 c (AONE _ # rs) = flts2 c rs"
 
       
  1799 | "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
 
       
  1800 | "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
 
       
  1801 | "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 
       
  1802     flts2 c rs
 
       
  1803     else ASEQ bs r1 r2 # flts2 c rs)"
 
       
  1804 | "flts2 c (r1 # rs) = r1 # flts2 c rs"
 
       
  1805 
       
  1806 lemma  flts2_k0:
 
       
  1807   shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
 
       
  1808   apply(induct r arbitrary: c rs1)
 
       
  1809    apply(auto)
 
       
  1810   done
 
       
  1811 
       
  1812 lemma  flts2_k00:
 
       
  1813   shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
 
       
  1814   apply(induct rs1 arbitrary: rs2 c)
 
       
  1815    apply(auto)
 
       
  1816   by (metis append.assoc flts2_k0)
 
       
  1817 
       
  1818 
       
  1819 lemma
 
       
  1820   shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
 
       
  1821   apply(induct c rs rule: flts2.induct)
 
       
  1822         apply(simp)
 
       
  1823        apply(simp)
 
       
  1824       apply(simp)
 
       
  1825      apply(simp)
 
       
  1826   apply(simp)
 
       
  1827     apply(auto simp add: bder_fuse)[1]
 
       
  1828   defer
 
       
  1829    apply(simp)
 
       
  1830   apply(simp del: flts2.simps)
 
       
  1831   apply(rule conjI)
 
       
  1832    prefer 2
 
       
  1833    apply(auto)[1]
 
       
  1834   apply(rule impI)
 
       
  1835   apply(subst flts2_k0)
 
       
  1836   apply(subst map_append)
 
       
  1837   apply(subst flts2.simps)
 
       
  1838   apply(simp only: flts2.simps)
 
       
  1839   apply(auto)
 
       
  1840 
       
  1841 
       
  1842 
  1786 lemma XXX2_helper:
 
  1843 lemma XXX2_helper:
 
  1787   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
  1844   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
  1788           "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
 
  1845           "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
 
  1789   shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
 
  1846   shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
 
  1790   using assms
 
  1847   using assms
 
  2388   using assms
 
  2445   using assms
 
  2389   apply(induct bs  rs rule: bsimp_AALTs.induct)
 
  2446   apply(induct bs  rs rule: bsimp_AALTs.induct)
 
  2390     apply(auto)
 
  2447     apply(auto)
 
  2391   done
 
  2448   done
 
  2392 
  2449 
  2393 lemma
 
  2450 lemma CT1_SEQ:
 
  2394   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"
 
  2451   shows "bsimp (ASEQ bs a1 a2) = bsimp (ASEQ bs (bsimp a1) (bsimp a2))"
 
  2395    "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))" 
  2452   apply(simp add: bsimp_idem)
 
  2396           "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
 
  2453   done
 
  2397    shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
 
       
  2398   using assms
 
       
  2399   apply(induct x52 arbitrary: x51)
 
       
  2400    apply(simp)
 
       
  2401   oops
 
       
  2402   
       
  2403 
       
  2404 lemma
 
       
  2405   assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
 
       
  2406   shows "bsimp a = a"
 
       
  2407   using assms
 
       
  2408   apply(induct a taking: asize rule: measure_induct)
 
       
  2409   apply(case_tac x)
 
       
  2410        apply(simp_all)
 
       
  2411    apply(case_tac "(bsimp x42) = AZERO")
 
       
  2412     apply(simp add: asize0)
 
       
  2413   apply(case_tac "(bsimp x43) = AZERO")
 
       
  2414     apply(simp add: asize0)
 
       
  2415     apply (metis bsimp_ASEQ0)
 
       
  2416    apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
 
       
  2417     apply(auto)[1]
 
       
  2418     apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
 
       
  2419   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)
 
       
  2420   (* ALT case *)
 
       
  2421   apply(frule iii)
 
       
  2422   apply(case_tac x52)
 
       
  2423    apply(simp)
 
       
  2424   apply(simp)
 
       
  2425   apply(subst k0)
 
       
  2426   apply(subst (asm) k0)
 
       
  2427   apply(subst (asm) (2) k0)
 
       
  2428   apply(subst (asm) (3) k0)
 
       
  2429   apply(case_tac "(bsimp a) = AZERO")
 
       
  2430    apply(simp)
 
       
  2431   apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
 
       
  2432   apply(simp)
 
       
  2433   apply(case_tac "nonalt  (bsimp a)")
 
       
  2434    prefer 2
 
       
  2435   apply(drule_tac  x="AALTs x51 (bsimp a # list)" in  spec)
 
       
  2436    apply(drule mp)
 
       
  2437   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)
 
       
  2438    apply(drule mp)  
       
  2439     apply(simp)
 
       
  2440   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)
 
       
  2441    apply(drule mp)
 
       
  2442   apply(simp)
 
       
  2443   using bsimp_idem apply auto[1]
 
       
  2444     apply(simp add: bsimp_idem)
 
       
  2445   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)
 
       
  2446   apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
 
       
  2447   apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
 
       
  2448   prefer 2
 
       
  2449   using k0b apply blast
 
       
  2450   apply(clarify)
 
       
  2451   apply(simp only:)
 
       
  2452   apply(simp)
 
       
  2453   apply(case_tac "flts (map bsimp list) = Nil")
 
       
  2454    apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less) 
       
  2455   apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) =  AALTs x51 (bsimp a # flts (map bsimp list))")
 
       
  2456    prefer 2
 
       
  2457    apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
 
       
  2458   apply(auto)
 
       
  2459    apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
 
       
  2460   oops
 
       
  2461 
       
  2462 
       
  2463 
       
  2464 
       
  2465 lemma OOO:
 
       
  2466   shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
 
       
  2467   apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
 
       
  2468   apply(case_tac x)
 
       
  2469    apply(simp)
 
       
  2470   apply(simp)
 
       
  2471   apply(case_tac "a = AZERO")
 
       
  2472    apply(simp)
 
       
  2473   apply(case_tac "list")
 
       
  2474     apply(simp)
 
       
  2475   apply(simp)
 
       
  2476   apply(case_tac "bsimp a = AZERO")
 
       
  2477    apply(simp)
 
       
  2478   apply(case_tac "list")
 
       
  2479     apply(simp)
 
       
  2480     apply(simp add: bsimp_fuse[symmetric])
 
       
  2481   apply(simp)
 
       
  2482   apply(case_tac "nonalt (bsimp a)")
 
       
  2483   apply(case_tac list)
 
       
  2484   apply(simp)
 
       
  2485     apply(subst k0b)
 
       
  2486       apply(simp)
 
       
  2487      apply(simp)
 
       
  2488     apply(simp add: bsimp_fuse)
 
       
  2489    apply(simp)
 
       
  2490   apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
 
       
  2491    prefer 2
 
       
  2492   using bsimp_size le_neq_implies_less apply blast
 
       
  2493    apply(erule disjE)
 
       
  2494   apply(drule_tac x="(bsimp a) # list" in spec)
 
       
  2495   apply(drule mp)
 
       
  2496     apply(simp)
 
       
  2497    apply(simp)
 
       
  2498   apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
 
       
  2499     apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs  \<and> rs \<noteq> Nil \<and> length rs > 1")
 
       
  2500    prefer 2
 
       
  2501   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)
 
       
  2502   apply(auto)
 
       
  2503   oops
 
       
  2504 
       
  2505 
       
  2506 lemma  
       
  2507   assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
 
       
  2508   shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
 
       
  2509   using assms
 
       
  2510   apply(simp)
 
       
  2511   oops
 
       
  2512 
       
  2513 
       
  2514 
  2454 
  2515 lemma CT1:
 
  2455 lemma CT1:
 
  2516   shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map  bsimp as))"
 
  2456   shows "bsimp (AALTs bs as) = bsimp (AALTs bs (map  bsimp as))"
 
  2517   apply(induct as arbitrary: bs)
 
  2457   apply(induct as arbitrary: bs)
 
  2518    apply(simp)
 
  2458    apply(simp)
 
  2519   apply(simp)
 
  2459   apply(simp)
 
  2520   by (simp add: bsimp_idem comp_def)
 
  2460   by (simp add: bsimp_idem comp_def)
 
  2521   
  2461   
  2522 lemma CT1a:
 
  2462 lemma CT1a:
 
  2523   shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
 
  2463   shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
 
  2524   by (metis CT1 list.simps(8) list.simps(9))
 
  2464   by (metis CT1 list.simps(8) list.simps(9))
 
       
  2465 
       
  2466 lemma WWW2:
 
       
  2467   shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
 
       
  2468          bsimp_AALTs bs1 (flts (map bsimp as1))"
 
       
  2469   by (metis bsimp.simps(2) bsimp_idem)
 
       
  2470 
       
  2471 lemma CT1b:
 
       
  2472   shows "bsimp (bsimp_AALTs bs as) = bsimp (bsimp_AALTs bs (map bsimp as))"
 
       
  2473   apply(induct bs as rule: bsimp_AALTs.induct)
 
       
  2474     apply(auto simp add: bsimp_idem)
 
       
  2475   apply (simp add: bsimp_fuse bsimp_idem)
 
       
  2476   by (metis bsimp_idem comp_apply)
 
       
  2477   
       
  2478   
       
  2479 
  2525 
  2480 
  2526 (* CT *)
 
  2481 (* CT *)
 
  2527 
  2482 
  2528 lemma CTU:
 
  2483 lemma CTU:
 
  2529   shows "bsimp_AALTs bs as = li bs as"
 
  2484   shows "bsimp_AALTs bs as = li bs as"
 
  2530   apply(induct bs as rule: li.induct)
 
  2485   apply(induct bs as rule: li.induct)
 
  2531     apply(auto)
 
  2486     apply(auto)
 
  2532   done
 
  2487   done
 
  2533 
  2488 
  2534 
  2489 find_theorems "bder _ (bsimp_AALTs _ _)"
 
  2535 
  2490 
  2536 lemma CTa:
 
  2491 lemma CTa:
 
  2537   assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
 
  2492   assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
 
  2538   shows  "flts as = as"
 
  2493   shows  "flts as = as"
 
  2539   using assms
 
  2494   using assms
 
  2572   using assms CT0
 
  2527   using assms CT0
 
  2573   by (metis k0 k00)
 
  2528   by (metis k0 k00)
 
  2574   
  2529   
  2575 
  2530 
  2576 
  2531 
  2577 
       
  2578 lemma 
       
  2579   shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
 
       
  2580           = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
 
       
  2581                              (map (fuse bs2) (map (bder c) as2))))"
 
       
  2582   apply(subst  bsimp_idem[symmetric])
 
       
  2583   apply(simp)
 
       
  2584   oops
 
       
  2585 
       
  2586 lemma CT_exp:
 
  2532 lemma CT_exp:
 
  2587   assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
 
  2533   assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
 
  2588   shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
 
  2534   shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
 
  2589   using assms
 
  2535   using assms
 
  2590   apply(induct as)
 
  2536   apply(induct as)
 
  2639   apply(case_tac xs)
 
  2585   apply(case_tac xs)
 
  2640    apply(auto)
 
  2586    apply(auto)
 
  2641   using flts2 good1 apply fastforce
 
  2587   using flts2 good1 apply fastforce
 
  2642   by (smt ex_map_conv list.simps(9) nn1b nn1c)
 
  2588   by (smt ex_map_conv list.simps(9) nn1b nn1c)
 
  2643 
  2589 
  2644 lemma WWW2:
 
       
  2645   shows "bsimp (bsimp_AALTs bs1 (flts (map bsimp as1))) =
 
       
  2646          bsimp_AALTs bs1 (flts (map bsimp as1))"
 
       
  2647   by (metis bsimp.simps(2) bsimp_idem)
 
       
  2648 
  2590 
  2649 lemma WWW3:
 
  2591 lemma WWW3:
 
  2650   shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
 
  2592   shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
 
  2651          flts (map bsimp (map (fuse bs1) as1))"
 
  2593          flts (map bsimp (map (fuse bs1) as1))"
 
  2652   by (metis CT0 YY flts_nonalt flts_nothing qqq1)
 
  2594   by (metis CT0 YY flts_nonalt flts_nothing qqq1)
 
  3017        apply(simp)
 
  2959        apply(simp)
 
  3018       apply(simp)
 
  2960       apply(simp)
 
  3019      apply(simp)
 
  2961      apply(simp)
 
  3020     prefer 3
 
  2962     prefer 3
 
  3021     apply(simp)
 
  2963     apply(simp)
 
       
  2964   (* SEQ case *)
 
       
  2965    apply(simp only:)
 
       
  2966    apply(subst CT1_SEQ)
 
       
  2967   apply(simp only: bsimp.simps)
 
       
  2968 
  3022   (* AALT case *)
 
  2969   (* AALT case *)
 
  3023    prefer 2
 
  2970    prefer 2
 
  3024    apply(simp only:)
 
  2971    apply(simp only:)
 
  3025    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
 
  2972    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
 
  3026     apply(clarify)
 
  2973     apply(clarify)
 
  3027   apply(simp del: bsimp.simps)
 
  2974     apply(simp del: bsimp.simps)
 
  3028   apply(subst (2) CT1) 
  2975   apply(subst (2) CT1) 
  3029     apply(simp del: bsimp.simps)
 
  2976     apply(simp del: bsimp.simps)
 
  3030   apply(rule_tac t="bsimp (bder c a1)" and  s="bsimp (bder c (bsimp a1))" in subst)
 
  2977   apply(rule_tac t="bsimp (bder c a1)" and  s="bsimp (bder c (bsimp a1))" in subst)
 
  3031   apply(simp del: bsimp.simps)
 
  2978   apply(simp del: bsimp.simps)
 
  3032   apply(rule_tac t="bsimp (bder c a2)" and  s="bsimp (bder c (bsimp a2))" in subst)
 
  2979   apply(rule_tac t="bsimp (bder c a2)" and  s="bsimp (bder c (bsimp a2))" in subst)
 
  3033      apply(simp del: bsimp.simps)
 
  2980      apply(simp del: bsimp.simps)
 
  3034     apply(subst  CT1a[symmetric])
 
  2981     apply(subst  CT1a[symmetric])
 
       
  2982   (* \<rightarrow> *)
 
       
  2983   apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
 
       
  2984             and  s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
 
       
  2985      apply(simp)
 
       
  2986      apply(subst bsimp.simps)
 
       
  2987     apply(simp del: bsimp.simps bder.simps)
 
       
  2988 
       
  2989     apply(subst bder_bsimp_AALTs)
 
       
  2990     apply(subst bsimp.simps)
 
       
  2991     apply(subst WWW2[symmetric])
 
       
  2992     apply(subst bsimp_AALTs_qq)
 
       
  2993   defer 
       
  2994     apply(subst bsimp.simps)
 
       
  2995     
       
  2996   (* <- *)
 
  3035     apply(subst bsimp.simps)
 
  2997     apply(subst bsimp.simps)
 
  3036     apply(simp del: bsimp.simps)
 
  2998     apply(simp del: bsimp.simps)
 
  3037 (*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
 
  2999 (*bsimp_AALTs x51 (map (bder c) (flts [a1, a2])) =
 
  3038     bsimp_AALTs x51 (flts (map (bder c) [a1, a2]))*)
 
  3000     bsimp_AALTs x51 (flts (map (bder c) [a1, a2]))*)
 
  3039   apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
 
  3001   apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
 
  3044       apply(subst bsimp_AALTs_qq)
 
  3006       apply(subst bsimp_AALTs_qq)
 
  3045        prefer 2
 
  3007        prefer 2
 
  3046        apply(simp del: bsimp.simps)
 
  3008        apply(simp del: bsimp.simps)
 
  3047        apply(subst big0)
 
  3009        apply(subst big0)
 
  3048        apply(simp add: WWW4)
 
  3010        apply(simp add: WWW4)
 
  3049   apply (metis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
 
  3011   apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
 
  3050   oops
 
  3012   oops
 
  3051 
  3013 
  3052 lemma XXX2a_long_without_good:
 
  3014 lemma XXX2a_long_without_good:
 
  3053   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
 
  3015   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
 
  3054   apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
 
  3016   apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
lexing