
diff -r 89e6605c4ca4 -r c470f792022b thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Jul 29 09:37:20 2019 +0100
+++ b/thys/BitCoded.thy	Mon Jul 29 12:32:28 2019 +0100
@@ -2057,7 +2057,7 @@
   apply(simp only: flex_fun_apply)
   apply(simp)
   using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
-  
+  oops
 
 lemma L08:
   assumes "s \<in> L (erase r)"
@@ -2109,8 +2109,7 @@
    prefer 2
    apply(simp)
   
-  defer
-  apply(simp only: bnullable.simps)
+   defer
   oops
 
 lemma L06_2:
@@ -2135,19 +2134,9 @@
   using L_bsimp_erase L_flat_Prf apply(auto)[1]
   done  
     
-  
-
-lemma LXX_bders:
-  assumes ""
-  shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)"
-  using assms
-  apply(induct s arbitrary: a rule: rev_induct)
-   apply(simp add: bmkeps_simp)
-  apply(simp add: bders_append) 
 
 
-
-lemma L07:
+lemma L07XX:
   assumes "s \<in> L (erase a)"
   shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))"
   using assms
@@ -2169,7 +2158,7 @@
   apply(induct s arbitrary: a)
    apply(simp)
   using L0 apply auto[1]
-  apply(simp)
+  oops
 
 thm bmkeps_retrieve bmkeps_simp Posix_mkeps
 
@@ -2177,7 +2166,7 @@
   assumes "s \<in> L (der c r)"
   shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
   using assms
-  sorry
+  oops
 
 lemma L02_bsimp:
   assumes "bnullable (bders a s)"
@@ -2201,229 +2190,8 @@
   apply(simp only: erase_bder[symmetric] erase_bders[symmetric])  
   apply(subst LB_sym[symmetric])
    apply(simp)
-  apply(rule WQ1)
-  apply(simp only: erase_bder[symmetric])
-   apply(rule L07)
-  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder erase_bders lexer_correct_None lexer_flex option.simps(3))
-  
-  apply(simp)
-  (*sledgehammer [timeout = 6000]*)
-  
-
-  using bder_retrieve
-
-
-
-lemma LX0MAIN:
-  assumes "s \<in> r \<rightarrow> v"
-  shows "decode (bmkeps (bders_simp (intern r) s)) r = Some(flex r id s v)"
-  using assms
-  apply(induct s arbitrary: r v)
-   apply(simp)
-  apply (metis LX0 Posix1(1) bders.simps(1) lexer_correctness(1) lexer_flex option.simps(3))
-  apply(simp add: bders_simp_append ders_append flex_append)
-  apply(subst bmkeps_simp[symmetric])
-  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)
-  (*apply(subgoal_tac "v = flex r id xs (injval (ders xs r) x (mkeps (ders (xs @ [x]) r)))")
-  prefer 2
-  apply (metis Posix1(1) flex.simps(1) flex.simps(2) flex_append lexer_correct_None lexer_correctness(1) lexer_flex option.inject)
-*)  apply(drule_tac x="r" in meta_spec)
-  apply(drule_tac x="(mkeps (ders xs r))" in meta_spec)
-  apply(drule meta_mp)
-    
-  defer
-  apply(simp)
-  apply(drule sym)
-  apply(simp)
-  using bder_retrieve MAIN_decode
   oops
 
-lemma LXaa:
-  assumes "s \<in> L (erase a)"
-  shows "decode (bmkeps (bsimp (bders (bsimp a) s))) (erase a) = decode (bmkeps (bders a s)) (erase a)"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1]
-  apply(simp)
-  apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec)
-  apply(drule meta_mp)
-  apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
-  apply(subst (asm) bsimp_idem)
-  apply(subst bmkeps_simp[symmetric])
-  apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness)
-  apply(subst (asm)  bmkeps_simp[symmetric])
-  apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness)
-  apply(subst bmkeps_retrieve)
-   apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) nullable_correctness)
-  apply(subst LA)
-   apply(simp)
-  apply (metis L_bsimp_erase ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable)
-    
-
-
-lemma LXaa:
-  assumes "s \<in> L (erase a)"
-  shows "bmkeps (bsimp (bders (bsimp a) s)) = bmkeps (bders a s)"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  using bmkeps_simp bnullable_correctness bsimp_idem nullable_correctness apply auto[1]
-  apply(simp)
-  apply(drule_tac x="bsimp (bder a (bsimp aa))" in meta_spec)
-  apply(drule meta_mp)
-  apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
-  apply(subst (asm) bsimp_idem)
-  apply(subst bmkeps_simp[symmetric])
-  apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) bnullable_correctness nullable_correctness)
-  apply(subst (asm)  bmkeps_simp[symmetric])
-  apply (metis L0aa L_bsimp_erase Posix1(1) bnullable_correctness ders.simps(2) ders_correctness erase_bder erase_bders nullable_correctness)
-  
-
-lemma LXaa:
-  assumes "s \<in> L (erase a)"
-  shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1]
-  apply(simp)
-  apply(drule_tac x="bder a aa" in meta_spec)
-  apply(drule meta_mp)
-  apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
-  apply(drule sym)
-  apply(simp)
-  (* transformation  to retrieve *)
-  apply(subst bmkeps_retrieve)
-  apply (metis L0aa L_bsimp_erase Posix1(1) bders.simps(2) ders_correctness erase_bders nullable_correctness)  
-  apply(subst bmkeps_retrieve)
-   apply (metis b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer_correct_None lexer_flex)
-  apply(subst (2) LC[symmetric])
-  prefer 2
-  apply(subst L0)
-  apply(subst  LA)
-   apply(simp)
-  apply (m etis L_bsimp_erase bders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable)
-     apply(subst  LA)
-   apply(simp)
-  apply (m etis L0aa b3 b4 bders_simp.simps(2) bnullable_correctness erase_bders lexer.simps(1) lexer_correctness(2) mkeps_nullable)
-  apply(subst (2) LB_sym[symmetric])
-   prefer 2
-  apply(subst L0)
-   apply(simp)
-  using lexer_correct_None lexer_flex apply fastforce
-  apply(subst (asm) bmkeps_retrieve)
-  apply (metis L_bsimp_erase bders.simps(2) erase_bders lexer_correct_None lexer_flex)
-  apply(subst (asm) bmkeps_retrieve)
-  apply (metis L0aa L_bsimp_erase b3 b4 bders_simp.simps(2) bnullable_correctness lexer.simps(1) lexer_correctness(2))
-  apply(subst LA)
-  apply (met is L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness)
-  apply(subst LA)
-  using lexer_correct_None lexer_flex mkeps_nullable apply force
-  
-  using L0aaaa LB[OF L0aaaa]
-  apply(subst LB[OF L0aaaa])
-  using L0aaaa
-  apply(rule L0aaaa)
-  
-  
-  
-  
-  
-  
-
-
-lemma L00:
-  assumes "s \<in> L (erase a)"
-  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = 
-         retrieve a (flex (erase a) id s (mkeps (ders s (erase  a))))"
-  using assms
-  apply(induct s  arbitrary: a taking: length rule: measure_induct)
-  apply(case_tac x)
-   apply(simp)
-  using L0 b3 bnullable_correctness nullable_correctness apply blast
-  apply(simp)
-  apply(drule_tac  x="[]" in  spec)
-  apply(simp)
-  apply(drule_tac  x="bders (bsimp a) (aa#list)" in  spec)
-  apply(simp)
-  apply(drule mp)
-  apply (metis L_bsimp_erase ders.simps(2) erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness)
-  using bder_retrieve bmkeps_simp bmkeps_retrieve L0  LA LB LC L02 L03 L04 L05
-  
-  oops
-
-lemma L00:
-  assumes "s \<in> L (erase (bsimp a))"
-  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (ders s (erase (bsimp a))))) = 
-         retrieve a (flex (erase a) id s (mkeps (ders s (erase  a))))"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  using L0 b3 bnullable_correctness nullable_correctness apply blast
-  apply(simp add: flex_append)
-  apply(drule_tac x="bder a aa" in meta_spec)
-  apply(drule meta_mp)
-  apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
-  apply(simp)
-  
-  (*using bmkeps_retrieve bder_retrieve*)
-  apply(subst (asm) bder_retrieve)
-  apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex)
-  apply(simp add: flex_fun_apply)
-  apply(drule sym)
-  apply(simp) 
-  using bmkeps_retrieve bder_retrieve
-  oops
-
-lemma L0a:
-  assumes "s \<in> L (erase a)"
-  shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = 
-         retrieve (bders a s) (mkeps (erase (bders a s)))"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  apply(simp)
-  apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
-  apply(drule meta_mp)
-  using L_bsimp_erase lexer_correct_None apply fastforce 
-  apply(simp)
-  apply(subst LA)
-  apply (metis L_bsimp_erase ders.simps(2) ders_correctness erase_bder lexer_correct_None lexer_flex mkeps_nullable nullable_correctness)
-  apply(subst LA)
-   apply(simp)
-   apply (metis ders.simps(2) lexer_correct_None lexer_flex mkeps_nullable)
-  
-  apply(simp)
-  (* MAIN *)
-  
-  apply(subst L00)
-  apply (met is L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
-  apply(simp)
-  done
-
-lemma L0a:
-  assumes "s \<in> L (erase a)"
-  shows "retrieve (bders_simp a s) (mkeps (erase (bders_simp a s))) = 
-         retrieve (bders a s) (mkeps (erase (bders a s)))"
-  using assms
-  apply(induct s arbitrary: a rule: rev_induct)
-   apply(simp)
-  apply(simp add: bders_simp_append)
-  apply(subst L0)
-  apply (metis L_bders_simp bnullable_correctness der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex nullable_correctness)
-  apply(subst bder_retrieve)
-  apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders lexer_correct_None lexer_flex mkeps_nullable nullable_correctness)
-  apply(simp add: bders_append)
-  apply(subst bder_retrieve)
-   apply (metis ders_snoc erase_bders lexer_correct_None lexer_flex mkeps_nullable)
-  apply(simp  add: ders_append)
-  using bder_retrieve
-  
-  find_theorems "retrieve _ (injval _ _ _)"
-find_theorems "mkeps (erase _)"
-
-
 lemma L1:
   assumes "s \<in> r \<rightarrow> v" 
   shows "decode (bmkeps (bders (intern r) s)) r = Some v"
@@ -2467,178 +2235,6 @@
    apply(simp add:  flex_append)
   by (simp add: Posix_injval)
 
-lemma L4:
-  assumes "[c] \<in> r \<rightarrow> v" 
-  shows "bmkeps (bder c (bsimp (intern r))) = code (flex r id [c] v)"
-  using assms
-  apply(subst bmkeps_retrieve)
-  apply (metis L_bsimp_erase Posix1(1) bders.simps(1) bders.simps(2) erase_bders erase_intern lexer_correct_None lexer_flex)
-  apply(subst bder_retrieve)
-  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)
-  apply(simp)
-  
-  
-
-
-
-lemma
-  assumes "s \<in>  L r" 
-  shows "bmkeps (bders_simp (intern r) s) = bmkeps (bders (intern r) s)"
-  using assms
-  apply(induct s  arbitrary: r rule: rev_induct)
-   apply(simp)
-  apply(simp add: bders_simp_append bders_append)
-  apply(subst bmkeps_simp[symmetric])
-  apply (metis b4 bders.simps(1) bders.simps(2) bders_simp_append blexer_correctness blexer_def lexer_correct_None)
-  apply(subst bmkeps_retrieve)
-   apply(simp)
-  apply (metis L_bders_simp der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness)
-     apply(subst bmkeps_retrieve)
-   apply(simp)
-   apply (metis ders_snoc lexer_correct_None lexer_flex)
-  apply(subst bder_retrieve)
-  apply (metis L_bders_simp der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness)
-  apply(subst bder_retrieve)
-  apply (metis ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable)
-  using bmkeps_retrieve
-  find_theorems "retrieve (bders _ _) = _"
-  find_theorems "retrieve _ _ = _"
-  oops
-
-lemma
-  assumes "s \<in> r \<rightarrow> v" 
-  shows "decode (bmkeps (bders_simp (intern r) s)) = Some v"
-  using  assms
-  apply(induct s  arbitrary: r v taking: length rule: measure_induct)
-  apply(subgoal_tac "x = [] \<or> (\<exists>a xs. x = xs @ [a])")
-   prefer 2
-   apply (meson rev_exhaust)
-  apply(erule disjE)
-   apply(simp add: blexer_simp_def)
-  apply (metis Posix1(1) Posix_Prf Posix_determ Posix_mkeps bmkeps_retrieve erase_intern lexer.simps(1) lexer_correct_None retrieve_code)
-  apply(clarify)
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  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))
-  apply(subst bmkeps_retrieve)
-  apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bder erase_bders erase_intern lexer_correct_None lexer_flex nullable_correctness)
-  apply(simp)
-  apply(subst bder_retrieve)
-  apply (metis L_bders_simp Posix1(1) der_correctness ders_snoc erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable nullable_correctness)
-  
-  
-  find_theorems "bmkeps _ = _"
-
-  apply(subgoal_tac "lexer r (xs @ [a]) = Some v")
-   prefer 2
-  using lexer_correctness(1) apply blast
-  apply(simp (no_asm_simp) add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  apply (m etis b4 bders.simps(1) bders.simps(2) bders_simp_append bnullable_correctness erase_bders erase_intern lexer_flex option.distinct(1))
-  apply(subgoal_tac "nullable (ders (xs @ [a]) r)")
-   prefer 2
-   apply (metis lexer_flex option.distinct(1)) 
-  apply(simp add: lexer_flex)
-  apply(simp add: flex_append ders_append)
-  apply(drule_tac sym)
-  apply(simp)
-  using Posix_flex flex.simps Posix_flex2
-  apply(drule_tac Posix_flex2)
-  apply (simp add: Prf_injval mkeps_nullable)
-  apply(drule_tac x="[a]" in spec)
-  apply(drule mp)
-   defer
-   apply(drule_tac x="ders xs r" in spec)
-   apply(drule_tac x="injval (ders xs r) a (mkeps (der a (ders xs r)))" in spec)
-   apply(simp)
-   apply(subst (asm) bmkeps_simp[symmetric])
-  using bnullable_correctness apply fastforce
-    
-  
-  find_theorems "good (bsimp _)"
-  oops
-
-lemma 
-  assumes "s \<in> L (erase a)"
-  shows "bmkeps (bders (bsimp a) s) = bmkeps (bders a s)"
-  using assms
-  apply(induct s arbitrary: a taking : length rule: measure_induct)
-  apply(case_tac x)
-  apply(simp)
-  using bmkeps_simp bnullable_correctness nullable_correctness apply auto[1]
-  using bsimp_idem apply auto[1]
-  apply(simp add: bders_append bders_simp_append)
-  apply(drule_tac x="bder a (bsimp aa)" in meta_spec)    
-  apply(drule meta_mp)
-   defer
-  apply(simp)
-  oops
-
-
-lemma
-  assumes "s \<in> L (erase r)"
-  shows "bmkeps (bders_simp r s) = bmkeps (bders r s)"
-  using assms
-    apply(induct s arbitrary: r)
-   apply(simp)
-  apply(simp add: bders_simp_append bders_append)
-  apply(drule_tac x="bsimp (bder a r)" in meta_spec)    
-  apply(drule meta_mp)
-   defer
-  apply(simp)
-  
-  find_theorems "good (bsimp _)"
-  oops
-
-lemma
-  assumes "s \<in> L r"
-  shows "decode (bmkeps (bders_simp (intern r) s)) r = Some (flex r id s (mkeps (ders s r)))"
-  using assms
-  apply(induct s arbitrary: r)
-   apply(simp)
-  using bmkeps_retrieve decode_code mkeps_nullable nullable_correctness retrieve_code apply auto[1]
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-   apply(subgoal_tac "[] \<in> L (ders (xs @ [x]) r)")
-    prefer 2
-    apply (meson Posix1(1) lexer_correct_None lexer_flex nullable_correctness)
-  apply(simp add: ders_append)
-  using L_bders_simp bnullable_correctness der_correctness nullable_correctness apply f orce
-  apply(simp add: flex_append ders_append)
-  apply(drule_tac x="der x r" in meta_spec)    
-  apply(simp add: ders_append)
-  find_theorems "intern _"
-  find_theorems "bmkeps (bsimp _)"
-
-  find_theorems "(_ # _) \<in> _ \<rightarrow> _"
-  oops
-
-
-lemma ZZZ:
-  assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)"
-  shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))"
-  using assms
-  apply(induct x52)
-   apply(simp)
-  apply(simp)
-  apply(case_tac "bsimp a = AZERO")
-   apply(simp)
-   apply(subgoal_tac "bsimp (bder c a) = AZERO")
-    prefer 2
-  using less_add_Suc1 apply fastforce
-   apply(simp)
-  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
-   apply(clarify)
-   apply(simp)
-   apply(subst k0)
-   apply(case_tac "rs = []")
-  apply(simp)
-   apply(subgoal_tac "bsimp (bder c a) = AALTs bs []")
-     apply(simp)
-  apply (metis arexp.distinct(7) good.simps(4) good1)
-  oops
-  
-
 
 
 lemma bders_snoc:
@@ -2914,25 +2510,7 @@
   apply(simp)
   oops
 
-lemma
-  assumes "rs = [AALTs bs0 [AALTs bsa [AONE bsb, AONE bsb]]]"
-  shows "flts [bsimp_AALTs bs (flts rs)] = flts (map (fuse bs) rs)"
-  using assms
-  apply(simp only:)
-  apply(simp only: flts.simps append_Nil2 List.list.map fuse.simps)
-  apply(simp only: bsimp_AALTs.simps)
-  apply(simp only: fuse.simps)
-  apply(simp only: flts.simps append_Nil2)
-  find_theorems "nonnested (bsimp_AALTs _ _)"
-  find_theorems "map _ (_ # _) = _"
-  apply(induct rs arbitrary: bs rule: flts.induct)
-        apply(auto)
-  apply(case_tac rs)
-       apply(simp)
-  
-  oops  
 
-  find_theorems "asize (bsimp _)"
 
 lemma CT1:
   shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map  bsimp as))"
@@ -2953,7 +2531,6 @@
     apply(auto)
   done
 
-thm flts.simps
 
 
 lemma CTa:
@@ -2996,17 +2573,7 @@
   by (metis k0 k00)
   
 
-lemma CTT:
-  assumes "\<forall>r\<in>set (flts (map (bsimp \<circ> bder c) as1)). nonalt r \<and> r \<noteq> AZERO"
-          "\<forall>r\<in>set (flts (map (bsimp \<circ> bder c) as2)). nonalt r \<and> r \<noteq> AZERO"
-  shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
-          = XXX"
-  apply(subst bsimp_idem[symmetric])
-  apply(simp)
-  apply(subst CT01)
-    apply(rule assms)
-   apply(rule assms)
-  (* CT *)
+
 
 lemma 
   shows "bsimp (AALT bs (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2)))
@@ -3097,57 +2664,7 @@
   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)
       apply(simp add: comp_def bder_fuse)
   
-  thm bder_fuse
-  
-  find_theorems "1 < length _"
-
-(* CT *)
-(*
-  under assumption that bsimp a1 = AALT; bsimp a = AALT
-
-  bsimp (AALT x51 (AALTs bs1 (map (bder c) as1)) (AALTs bs2 (map (bder c) as2))) =
-  bsimp (AALTs x51 (map (fuse bs1) (map (bder c) as1)) @ ( map (fuse bs2) (map (bder c) as2)))
-
-  bsimp_AALTs x51 (flts (map bsimp [a1, a2])))
-  = bsimp_AALTs x51 (flts [bsimp a1, bsimp a2])
-  
-*)
-
-    apply(case_tac "bsimp a1")
-         prefer 5
-         apply(simp only:)
-         apply(case_tac "bsimp a2")
-              apply(simp)
-  
-         prefer 5
-              apply(simp only:)
-  apply(simp only: bder.simps)
-  apply(simp)
-  
-
-
-
-    prefer 2
-  using nn1b apply blast
-   apply(simp only:)
-   apply(case_tac x52)
-    apply(simp)
-   apply(simp only:)
-   apply(case_tac "\<exists>bsa rsa. a = AALTs  bsa rsa")
-    apply(clarify)  
-  apply(simp)
-  apply(frule_tac x="AALTs x51 ((map (fuse bsa)  rsa) @ list)" in spec)
-    apply(drule mp)
-     apply(simp)
-     apply (simp add: qq)
-    apply(drule_tac x="c" in spec)
-    apply(simp only: bder.simps)
-    apply(simp)
-    apply(subst   k0)
-    apply(subst (2)  k0)
-   apply(subst (asm) (2) flts_append)
-    apply(rotate_tac 2)
-
+  oops
 
 lemma XXX2a_long_without_good:
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"




