diff -r a730a5a0bab9 -r 89e6605c4ca4 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Tue Jul 23 21:21:49 2019 +0100
+++ b/thys/BitCoded.thy	Mon Jul 29 09:37:20 2019 +0100
@@ -1,9 +1,9 @@
-   
+
 theory BitCoded
   imports "Lexer" 
 begin
 
-section {* Bit-Encodings *}
+section \<open>Bit-Encodings\<close>
 
 datatype bit = Z | S
 
@@ -118,6 +118,13 @@
 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 | "erase (ASTAR _ r) = STAR (erase r)"
 
+lemma decode_code_erase:
+  assumes "\<Turnstile> v : (erase  a)"
+  shows "decode (code v) (erase a) = Some v"
+  using assms
+  by (simp add: decode_code) 
+
+
 fun nonalt :: "arexp \<Rightarrow> bool"
   where
   "nonalt (AALTs bs2 rs) = False"
@@ -560,6 +567,13 @@
 | "flts ((AALTs bs  rs1) # rs) = (map (fuse bs) rs1) @ flts rs"
 | "flts (r1 # rs) = r1 # flts rs"
 
+fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
+  where
+  "li _ [] = AZERO"
+| "li bs [a] = fuse bs a"
+| "li bs as = AALTs bs as"
+
+
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -582,6 +596,8 @@
 | "bsimp r = r"
 
 
+
+
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -1285,26 +1301,34 @@
   shows "good (bsimp a) \<or> bsimp a = AZERO"
   apply(induct a taking: asize rule: measure_induct)
   apply(case_tac x)
-       apply(simp)
-      apply(simp)
+  apply(simp)
+  apply(simp)
   apply(simp)
   prefer 3
     apply(simp)
    prefer 2
+  (*  AALTs case  *)
   apply(simp only:)
    apply(case_tac "x52")
     apply(simp)
-   apply(simp only: good0a)
+  thm good0a
+   (*  AALTs list at least one - case *)
+   apply(simp only: )
   apply(frule_tac x="a" in spec)
    apply(drule mp)
-  apply(simp)
+    apply(simp)
+   (* either first element is good, or AZERO *)
     apply(erule disjE)
      prefer 2
-     apply(simp)
+    apply(simp)
+   (* in  the AZERO case, the size  is smaller *)
    apply(drule_tac x="AALTs x51 list" in spec)
    apply(drule mp)
-  apply(simp add: asize0)
-    apply(auto)[1]
+     apply(simp add: asize0)
+    apply(subst (asm) bsimp.simps)
+  apply(subst (asm) bsimp.simps)
+    apply(assumption)
+   (* in the good case *)
   apply(frule_tac x="AALTs x51 list" in spec)
    apply(drule mp)
     apply(simp add: asize0)
@@ -1324,6 +1348,7 @@
       apply(auto)[1]
      apply auto[1]
     apply (metis ex_map_conv nn1b nn1c)
+  (* in  the AZERO case *)
    apply(simp)
    apply(frule_tac x="a" in spec)
    apply(drule mp)
@@ -1866,6 +1891,728 @@
      apply(auto)
   done
 
+lemma LA:
+  assumes "\<Turnstile> v : ders s (erase r)"
+  shows "retrieve (bders r s) v = retrieve r (flex (erase r) id s v)"
+  using assms
+  apply(induct s arbitrary: r v rule: rev_induct)
+   apply(simp)
+  apply(simp add: bders_append ders_append)
+  apply(subst bder_retrieve)
+   apply(simp)
+  apply(drule Prf_injval)
+  by (simp add: flex_append)
+
+
+lemma LB:
+  assumes "s \<in> (erase r) \<rightarrow> v" 
+  shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+  using assms
+  apply(induct s arbitrary: r v rule: rev_induct)
+   apply(simp)
+   apply(subgoal_tac "v = mkeps (erase r)")
+    prefer 2
+  apply (simp add: Posix1(1) Posix_determ Posix_mkeps nullable_correctness)
+   apply(simp)
+  apply(simp add: flex_append ders_append)
+  by (metis Posix_determ Posix_flex Posix_injval Posix_mkeps ders_snoc lexer_correctness(2) lexer_flex)
+
+lemma LB_sym:
+  assumes "s \<in> (erase r) \<rightarrow> v" 
+  shows "retrieve r v = retrieve r (flex (erase r) id s (mkeps (erase (bders r s))))"
+  using assms
+  by (simp add: LB)
+
+
+lemma LC:
+  assumes "s \<in> (erase r) \<rightarrow> v" 
+  shows "retrieve r v = retrieve (bders r s) (mkeps (erase (bders r s)))"
+  apply(simp)
+  by (metis LA LB Posix1(1) assms lexer_correct_None lexer_flex mkeps_nullable)
+
+
+lemma L0:
+  assumes "bnullable a"
+  shows "retrieve (bsimp a) (mkeps (erase (bsimp a))) = retrieve a (mkeps (erase a))"
+  using assms
+  by (metis b3 bmkeps_retrieve bmkeps_simp bnullable_correctness)
+
+thm bmkeps_retrieve
+
+lemma L0a:
+  assumes "s \<in> L(erase a)"
+  shows "retrieve (bsimp (bders a s)) (mkeps (erase (bsimp (bders a s)))) = 
+         retrieve (bders a s) (mkeps (erase (bders a s)))"
+  using assms
+  by (metis L0 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
+  
+lemma L0aa:
+  assumes "s \<in> L (erase a)"
+  shows "[] \<in> erase (bsimp (bders a s)) \<rightarrow> mkeps (erase (bsimp (bders a s)))"
+  using assms
+  by (metis Posix_mkeps b3 bnullable_correctness erase_bders lexer_correct_None lexer_flex)
+
+lemma L0aaa:
+  assumes "[c] \<in> L (erase a)"
+  shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bder c a)))"
+  using assms
+  by (metis bders.simps(1) bders.simps(2) erase_bders lexer_correct_None lexer_correct_Some lexer_flex option.inject)
+
+lemma L0aaaa:
+  assumes "[c] \<in> L (erase a)"
+  shows "[c] \<in> (erase a) \<rightarrow> flex (erase a) id [c] (mkeps (erase (bders a [c])))"
+  using assms
+  using L0aaa by auto
+    
+
+lemma L02:
+  assumes "bnullable (bder c a)"
+  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id [c] (mkeps (erase (bder c (bsimp a))))) = 
+         retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a))))"
+  using assms
+  apply(simp)
+  using bder_retrieve L0 bmkeps_simp bmkeps_retrieve L0  LA LB
+  apply(subst bder_retrieve[symmetric])
+  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder mkeps_nullable nullable_correctness)
+  apply(simp)
+  done
+
+lemma L02_bders:
+  assumes "bnullable (bders a s)"
+  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) = 
+         retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))"
+  using assms
+  by (metis LA L_bsimp_erase bnullable_correctness ders_correctness erase_bders mkeps_nullable nullable_correctness)
+
+
+  
+
+lemma L03:
+  assumes "bnullable (bder c a)"
+  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+         bmkeps (bsimp (bder c (bsimp a)))"
+  using assms
+  by (metis L0 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness)
+
+lemma L04:
+  assumes "bnullable (bder c a)"
+  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+         retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))"     
+  using assms
+  by (metis L0 L_bsimp_erase bnullable_correctness der_correctness erase_bder nullable_correctness)
+    
+lemma L05:
+  assumes "bnullable (bder c a)"
+  shows "retrieve (bder c (bsimp a)) (mkeps (erase (bder c (bsimp a)))) =
+         retrieve (bsimp (bder c (bsimp a))) (mkeps (erase (bsimp (bder c (bsimp a)))))" 
+  using assms
+  using L04 by auto 
+
+lemma L06:
+  assumes "bnullable (bder c a)"
+  shows "bmkeps (bder c (bsimp a)) = bmkeps (bsimp (bder c (bsimp a)))"
+  using assms
+  by (metis L03 L_bsimp_erase bmkeps_retrieve bnullable_correctness der_correctness erase_bder nullable_correctness) 
+
+lemma L07:
+  assumes "s \<in> L (erase r)"
+  shows "retrieve r (flex (erase r) id s (mkeps (ders s (erase r)))) 
+            = retrieve (bders r s) (mkeps (erase (bders r s)))"
+  using assms
+  using LB LC lexer_correct_Some by auto
+
+lemma LXXX:
+  assumes "s \<in> (erase r) \<rightarrow> v" "s \<in> (erase (bsimp r)) \<rightarrow> v'"
+  shows "retrieve r v = retrieve (bsimp r) v'"
+  using  assms
+  apply -
+  thm LC
+  apply(subst LC)
+   apply(assumption)
+  apply(subst  L0[symmetric])
+  using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
+  apply(subst (2) LC)
+   apply(assumption)
+  apply(subst (2)  L0[symmetric])
+  using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
+   
+  oops  
+
+
+lemma L07a:
+  assumes "s \<in> L (erase r)"
+  shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r))))) 
+         = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
+  using assms
+  apply(induct s arbitrary: r)
+   apply(simp)
+  using L0a apply force
+  apply(drule_tac x="(bder a r)" 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)
+  apply(subst (asm) bder_retrieve)
+   apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex)
+  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]
+  
+
+lemma L08:
+  assumes "s \<in> L (erase r)"
+  shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s)))
+         = retrieve (bders r s) (mkeps (erase (bders r s)))"
+  using assms
+  apply(induct s arbitrary: r)
+   apply(simp)
+  using L0 bnullable_correctness nullable_correctness apply blast
+  apply(simp add: bders_append)
+  apply(drule_tac x="(bder a (bsimp r))" 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)
+  apply(subst LA)
+  apply (metis 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 L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
+
+thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
+  oops
+
+lemma test:
+  assumes "s = [c]"
+  shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)"
+  using assms
+   apply(simp only: bders.simps)
+   defer
+  using assms
+   apply(simp only: flex.simps id_simps)
+  using  L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] 
+  find_theorems "retrieve (bders _ _) _"
+  find_theorems "retrieve _ (mkeps _)"
+  oops
+
+lemma L06X:
+  assumes "bnullable (bder c a)"
+  shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)"
+  using assms
+  apply(induct a arbitrary: c)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    prefer 3
+    apply(simp)
+   prefer 2
+   apply(simp)
+  
+  defer
+  apply(simp only: bnullable.simps)
+  oops
+
+lemma L06_2:
+  assumes "bnullable (bders a [c,d])"
+  shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
+  using assms
+  apply(simp)
+  by (metis L_bsimp_erase bmkeps_simp bnullable_correctness der_correctness erase_bder nullable_correctness)
+  
+lemma L06_bders:
+  assumes "bnullable (bders a s)"
+  shows "bmkeps (bders (bsimp a) s) = bmkeps (bsimp (bders (bsimp a) s))"
+  using assms
+  by (metis L_bsimp_erase bmkeps_simp bnullable_correctness ders_correctness erase_bders nullable_correctness)
+
+lemma LLLL:
+  shows "L (erase a) =  L (erase (bsimp a))"
+  and "L (erase a) = {flat v | v. \<Turnstile> v: (erase a)}"
+  and "L (erase a) = {flat v | v. \<Turnstile> v: (erase (bsimp a))}"
+  using L_bsimp_erase apply(blast)
+  apply (simp add: L_flat_Prf)
+  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:
+  assumes "s \<in> L (erase a)"
+  shows "s \<in> erase a \<rightarrow> flex (erase a) id s (mkeps (ders s (erase a)))"
+  using assms
+  by (meson lexer_correct_None lexer_correctness(1) lexer_flex)
+
+lemma LX0:
+  assumes "s \<in> L r"
+  shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))"
+  by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex)
+
+
+lemma L02_bders2:
+  assumes "bnullable (bders a s)" "s = [c]"
+  shows "retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s)))  =
+         retrieve (bders a s) (mkeps (erase (bders a s)))"
+  using assms
+  apply(simp)
+  
+  apply(induct s arbitrary: a)
+   apply(simp)
+  using L0 apply auto[1]
+  apply(simp)
+
+thm bmkeps_retrieve bmkeps_simp Posix_mkeps
+
+lemma WQ1:
+  assumes "s \<in> L (der c r)"
+  shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
+  using assms
+  sorry
+
+lemma L02_bsimp:
+  assumes "bnullable (bders a s)"
+  shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) =
+         retrieve a (flex (erase a) id s (mkeps (erase (bders a s))))"
+  using assms
+  apply(induct s arbitrary: a)
+   apply(simp)
+   apply (simp add: L0)
+  apply(simp)
+  apply(drule_tac x="bder a aa" in meta_spec)
+  apply(simp)
+  apply(subst (asm) bder_retrieve)
+  using Posix_Prf Posix_flex Posix_mkeps bnullable_correctness apply fastforce
+  apply(simp add: flex_fun_apply)
+  apply(drule sym)
+  apply(simp)
+  apply(subst flex_injval)
+  apply(subst bder_retrieve[symmetric])
+  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))
+  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"
+  using assms
+  by (metis blexer_correctness blexer_def lexer_correctness(1) option.distinct(1))
+
+lemma L2:
+  assumes "s \<in> (der c r) \<rightarrow> v" 
+  shows "decode (bmkeps (bders (intern r) (c # s))) r = Some (injval r c v)"
+  using assms
+  apply(subst bmkeps_retrieve)
+  using Posix1(1) lexer_correct_None lexer_flex apply fastforce
+  using MAIN_decode
+  apply(subst MAIN_decode[symmetric])
+   apply(simp)
+   apply (meson Posix1(1) lexer_correct_None lexer_flex mkeps_nullable)
+  apply(simp)
+  apply(subgoal_tac "v = flex (der c r) id s (mkeps (ders s (der c r)))")
+   prefer 2
+   apply (metis Posix_determ lexer_correctness(1) lexer_flex option.distinct(1))
+  apply(simp)
+  apply(subgoal_tac "injval r c (flex (der c r) id s (mkeps (ders s (der c r)))) =
+    (flex (der c r) ((\<lambda>v. injval r c v) o id) s (mkeps (ders s (der c r))))")
+   apply(simp)
+  using flex_fun_apply by blast
+  
+lemma L3:
+  assumes "s2 \<in> (ders s1 r) \<rightarrow> v" 
+  shows "decode (bmkeps (bders (intern r) (s1 @ s2))) r = Some (flex r id s1 v)"
+  using assms
+  apply(induct s1 arbitrary: r s2 v rule: rev_induct)
+   apply(simp)
+  using L1 apply blast
+  apply(simp add: ders_append)
+  apply(drule_tac x="r" in meta_spec)
+  apply(drule_tac x="x # s2" in meta_spec)
+  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+  apply(drule meta_mp)
+   defer
+   apply(simp)
+   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)"
@@ -1899,39 +2646,6 @@
   apply(simp add: bders_append)
   done
 
-lemma
-  assumes "bnullable (bders a s)" "good a"
-  shows "bmkeps (bders_simp a s) = bmkeps (bders a s)"
-  using assms
-  apply(induct s arbitrary: a)
-   apply(simp)
-  apply(simp add: bders_append bders_simp_append)
-  apply(drule_tac x="bsimp (bsimp (bder a aa))" in meta_spec)
-  apply(drule meta_mp)
-  apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
-  apply(subgoal_tac "good (bsimp (bder a aa)) \<or> bsimp (bder a aa) = AZERO")
-   apply(auto simp add: bders_AZERO)
-    prefer 2
-    apply (metis b4 bders.simps(2) bders_AZERO(2) bders_simp.simps(2) bnullable.simps(1))
-   prefer 2
-  using good1 apply auto[1]
-  apply(drule meta_mp)
-   apply (simp add: bsimp_idem)
-  apply (subst (asm) (1) bsimp_idem)
-  apply(simp)
-  apply(subst (asm) (2) bmkeps_simp)
-   apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
-  apply (subst (asm) (1) bsimp_idem)
-  oops
-
-
-lemma
-  shows "bmkeps (bders (bders_simp a s2) s1) = bmkeps (bders_simp a (s2 @ s1))"
-  apply(induct s2 arbitrary: a s1)
-   apply(simp)
-  defer
-  apply(simp add: bders_append bders_simp_append)
-  oops
 
 lemma QQ1:
   shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
@@ -2039,19 +2753,6 @@
    apply (metis n0 nn1b test2)
   by (metis flts_fuse flts_nothing)
 
-lemma "good (bsimp a) \<or> bsimp a = AZERO"
-  by (simp add: good1)
-
-
-lemma 
-  assumes "bnullable (bders r s)" "good r"
-  shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
-  using assms
-  apply(induct s arbitrary: r)
-   apply(simp)
-  using bmkeps_simp apply auto[1]
-  apply(simp)
-  by (simp add: test2)
 
 lemma PP:
   assumes "bnullable (bders r s)" 
@@ -2101,7 +2802,7 @@
   using assms
   apply(induct x52 arbitrary: x51)
    apply(simp)
-  
+  oops
   
 
 lemma
@@ -2160,15 +2861,7 @@
    apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
   apply(auto)
    apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
-   
-  apply(drule_tac x="AALTs x51 list" in spec)
-  apply(drule mp)
-   apply(auto simp add: asize0)[1]
- 
-
-
-(* HERE*)
-
+  oops
 
 
 
@@ -2211,94 +2904,133 @@
    prefer 2
   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)
   apply(auto)
-  sledgehammer [timeout=6000]  
-
-
-
-
-  defer
-  apply(case_tac  list)
-    apply(simp)
-    prefer 2
-    apply(simp)
-   apply (simp add: bsimp_fuse bsimp_idem)
-  apply(case_tac a)
-       apply(simp_all)
+  oops
+
+
+lemma  
+  assumes "rs = [AALTs bsa [AONE bsb, AONE bsb]]"
+  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
+  using assms
+  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)
   
-  
-  apply(subst k0b)
-      apply(simp)
-    apply(subst (asm) k0)
-  apply(subst (asm) (2) k0)
-
-
-  find_theorems "asize _ < asize _"
-  using bsimp_AALTs_size3
-  apply -
-  apply(drule_tac x="a # list" in meta_spec)
-  apply(drule_tac x="bs" in meta_spec)
-  apply(drule meta_mp)
+  oops  
+
+  find_theorems "asize (bsimp _)"
+
+lemma CT1:
+  shows "bsimp (AALTs bs as) = bsimp(AALTs bs (map  bsimp as))"
+  apply(induct as arbitrary: bs)
    apply(simp)
   apply(simp)
-  apply(drule_tac x="(bsimp a) # list" in spec)
-  apply(drule mp)
+  by (simp add: bsimp_idem comp_def)
+  
+lemma CT1a:
+  shows "bsimp (AALT bs a1 a2) = bsimp(AALT bs (bsimp a1) (bsimp a2))"
+  by (metis CT1 list.simps(8) list.simps(9))
+
+(* CT *)
+
+lemma CTU:
+  shows "bsimp_AALTs bs as = li bs as"
+  apply(induct bs as rule: li.induct)
+    apply(auto)
+  done
+
+thm flts.simps
+
+
+lemma CTa:
+  assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
+  shows  "flts as = as"
+  using assms
+  apply(induct as)
    apply(simp)
-  apply(case_tac  list)
-    apply(simp)
-    prefer 2
-    apply(simp)
-    apply(subst (asm) k0)
-  apply(subst (asm) (2) k0)
-  thm k0
-  apply(subst (asm) k0b)
-      apply(simp)
-     apply(simp)
-  
-   defer
+  apply(case_tac as)
    apply(simp)
-   apply(case_tac  list)
-    apply(simp)
-    defer
+  apply (simp add: k0b)
+  using flts_nothing by auto
+
+lemma CT0:
+  assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" 
+  shows "flts [bsimp_AALTs bs1 as1] =  flts (map (fuse bs1) as1)"
+  using assms CTa
+  apply(induct as1 arbitrary: bs1)
     apply(simp)
-  find_theorems "asize _ < asize _"
-  find_theorems "asize _ < asize _"
-apply(subst k0b)
-      apply(simp)
-     apply(simp)
-
-
-      apply(rule nn11a)
-      apply(simp)
-     apply (metis good.simps(1) good1 good_fuse)
-    apply(simp)
-  using fuse_append apply blast
-   apply(subgoal_tac "\<exists>bs rs. bsimp x43 = AALTs bs rs")
-    prefer 2
-  using nonalt.elims(3) apply blast
-   apply(clarify)
+   apply(simp)
+  apply(case_tac as1)
    apply(simp)
-   apply(case_tac rs)
-    apply(simp)
-    apply (metis arexp.distinct(7) good.simps(4) good1)
-   apply(simp)
-  apply(case_tac list)
-    apply(simp)
-    apply (metis arexp.distinct(7) good.simps(5) good1)
   apply(simp)
+proof -
+fix a :: arexp and as1a :: "arexp list" and bs1a :: "bit list" and aa :: arexp and list :: "arexp list"
+  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)"
+  assume a2: "\<And>as. \<forall>r\<in>set as. nonalt r \<and> r \<noteq> AZERO \<Longrightarrow> flts as = as"
+  assume a3: "as1a = aa # list"
+  have "flts [a] = [a]"
+using a1 k0b by blast
+then show "fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list = flts (fuse bs1a a # fuse bs1a aa # map (fuse bs1a) list)"
+  using a3 a2 a1 by (metis (no_types) append.left_neutral append_Cons flts_fuse k00 k0b list.simps(9))
+qed
   
   
-  
-  
-  
+lemma CT01:
+  assumes "\<forall>r \<in> set as1. nonalt r \<and> r \<noteq> AZERO" "\<forall>r \<in> set as2. nonalt r \<and> r \<noteq> AZERO" 
+  shows "flts [bsimp_AALTs bs1 as1, bsimp_AALTs bs2 as2] =  flts ((map (fuse bs1) as1) @ (map (fuse bs2) as2))"
+  using assms CT0
+  by (metis k0 k00)
   
-  find_theorems "flts [_] = [_]"
-   apply(case_tac x52)
+
+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(simp)
-  apply(case_tac list)
-    apply(simp)
-    apply(case_tac a)
-  apply(simp_all)
+  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)))
+          = bsimp (AALTs bs ((map (fuse bs1) (map (bder c) as1)) @
+                             (map (fuse bs2) (map (bder c) as2))))"
+  apply(subst  bsimp_idem[symmetric])
+  apply(simp)
+  oops
+
+lemma CT_exp:
+  assumes "\<forall>a \<in> set as. bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  shows "map bsimp (map (bder c) as) = map bsimp (map (bder c) (map bsimp as))"
+  using assms
+  apply(induct as)
+   apply(auto)
+  done
+
+lemma asize_set:
+  assumes "a \<in> set as"
+  shows "asize a < Suc (sum_list (map asize as))"
+  using assms
+  apply(induct as arbitrary: a)
+   apply(auto)
+  using le_add2 le_less_trans not_less_eq by blast
   
 
 lemma XXX2a_long_without_good:
@@ -2311,15 +3043,191 @@
   prefer 3
     apply(simp)
   (* AALT case *)
+   prefer 2
+   apply(simp del: bsimp.simps)
+   apply(subst (2) CT1)
+   apply(subst CT_exp)
+    apply(auto)[1]
+  using asize_set apply blast
+   apply(subst CT1[symmetric])
+  apply(simp)
+  oops
+
+lemma big:
+  shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
+         bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
+  apply(simp add: comp_def bder_fuse)
+  apply(simp add: flts_append)
+   
+  sorry    
+
+lemma XXX2a_long_without_good:
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
+  apply(case_tac x)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  prefer 3
+    apply(simp)
+  (* AALT case *)
   prefer 2
+   apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
+    apply(clarify)
+  apply(simp del: bsimp.simps)
+  apply(subst (2) CT1) 
+    apply(simp del: bsimp.simps)
+  apply(rule_tac t="bsimp (bder c a1)" and  s="bsimp (bder c (bsimp a1))" in subst)
+  apply(simp del: bsimp.simps)
+  apply(rule_tac t="bsimp (bder c a2)" and  s="bsimp (bder c (bsimp a2))" in subst)
+     apply(simp del: bsimp.simps)
+    apply(subst  CT1a[symmetric])
+    apply(subst bsimp.simps)
+    apply(simp del: bsimp.simps)
+  apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
+  apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2")
+      apply(clarify)
+  apply(simp only:)
+      apply(simp del: bsimp.simps bder.simps)
+      apply(subst bsimp_AALTs_qq)
+       prefer 2
+       apply(simp del: bsimp.simps)
+       apply(subst big)
+       prefer 2
+  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(simp)
+   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)
+
+
+lemma XXX2a_long_without_good:
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
+  apply(case_tac x)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  prefer 3
+    apply(simp)
+  (* AALT case *)
+   prefer 2
+   apply(subgoal_tac "nonnested (bsimp x)")
+    prefer 2
+  using nn1b apply blast
+   apply(simp only:)
+  apply(drule_tac x="AALTs x51 (flts x52)" in spec)
+   apply(drule mp)
+    defer
+    apply(drule_tac x="c" in spec)
+    apply(simp)
+    apply(rotate_tac 2)
+  
+    apply(drule sym)
+  apply(simp)
+
+   apply(simp only: bder.simps)
+   apply(simp only: bsimp.simps)
    apply(subst bder_bsimp_AALTs)
    apply(case_tac x52)
     apply(simp)
    apply(simp)
+  apply(case_tac list)
+    apply(simp)
+    apply(case_tac a)
+         apply(simp)
+        apply(simp)
+       apply(simp)
+      defer
+      apply(simp)
+  
+
+   (* case AALTs list is not empty *)
+   apply(simp)
+   apply(subst k0)
+   apply(subst (2) k0)
+   apply(simp)
+   apply(case_tac "bsimp a = AZERO")
+    apply(subgoal_tac "bsimp (bder c a) = AZERO")
+     prefer 2
+  using less_iff_Suc_add apply auto[1]
+    apply(simp)
+  apply(drule_tac x="AALTs x51 list" in  spec)
+   apply(drule mp)
+    apply(simp add: asize0)
+   apply(drule_tac x="c" in spec)
+    apply(simp add: bder_bsimp_AALTs)
+   apply(case_tac  "nonalt (bsimp a)")
+    prefer 2
+  apply(drule_tac x="bsimp (AALTs x51 (a#list))" in  spec)
+    apply(drule mp)
+     apply(rule order_class.order.strict_trans2)
+      apply(rule bsimp_AALTs_size3)
+      apply(auto)[1]
+     apply(simp)
+    apply(subst (asm) bsimp_idem)
+  apply(drule_tac x="c" in spec)
+  apply(simp)  
+  find_theorems "_ < _ \<Longrightarrow> _ \<le> _ \<Longrightarrow>_ < _"
+  apply(rule le_trans)
+  apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
+     prefer 2
+  using k0b apply blast
+    apply(simp)
+  find_theorems "asize _ < asize _"
+  
+  using bder_bsimp_AALTs
    apply(case_tac list)
-  apply(simp)
+    apply(simp)
+   sledgeha mmer [timeout=6000]  
 
    apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r")
     apply(drule_tac x="bsimp (AALTs x51 x52)" in spec)
@@ -2581,6 +3489,19 @@
    apply(simp only: bders.simps)
    apply(subst bders_simp.simps)
   apply(simp)
-    
+  oops   
+
+
+lemma
+  fixes n :: nat
+  shows "(\<Sum>i \<in> {0..n}. i) = n * (n + 1) div 2"
+  apply(induct n)
+  apply(simp)
+  apply(simp)
+  done
+
+
+
+
 
 end
\ No newline at end of file