diff -r 50bb2c83eeb1 -r c40348a77318 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Sat Aug 10 14:18:15 2019 +0100
+++ b/thys/BitCoded2.thy	Sun Aug 11 00:28:14 2019 +0100
@@ -833,6 +833,16 @@
   by (metis assms contains6 erase_bder)
 
 
+lemma contains7a:
+  assumes "\<Turnstile> v : der c (erase r)"
+  shows "r >> retrieve r (injval (erase r) c v)"
+  using assms
+  apply -
+  apply(drule Prf_injval)
+  apply(drule contains6)
+  apply(simp)
+  done
+
 fun 
   bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
@@ -2021,7 +2031,9 @@
    apply (metis bnullable_correctness erase_fuse)+
   done
 
-lemma qq4:
+
+
+lemma qq4a:
   assumes "\<exists>x\<in>set list. bnullable x"
   shows "\<exists>x\<in>set (flts list). bnullable x"
   using assms
@@ -2079,7 +2091,7 @@
   apply(case_tac "list")
      apply(simp)
     apply(simp)
-   apply (simp add: qq4)
+   apply (simp add: qq4a)
   apply(simp)
   apply(auto)
    apply(case_tac list)
@@ -2092,7 +2104,7 @@
    apply(simp)
    apply (simp add: r0)
   apply(simp)
-  using qq4 r1 r2 by auto
+  using qq4a r1 r2 by auto
 
 
 
@@ -2145,7 +2157,7 @@
   thm q3
   apply(subst q3[symmetric])
    apply simp
-  using b3 qq4 apply auto[1]
+  using b3 qq4a apply auto[1]
   apply(subst qs3)
    apply simp
   using k1 by blast
@@ -2190,59 +2202,6 @@
   apply(simp add: blexer_correctness)
   done
 
-
-
-
-
-fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
-  where 
-  "flts2 _ [] = []"
-| "flts2 c (AZERO # rs) = flts2 c rs"
-| "flts2 c (AONE _ # rs) = flts2 c rs"
-| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
-| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
-| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then 
-    flts2 c rs
-    else ASEQ bs r1 r2 # flts2 c rs)"
-| "flts2 c (r1 # rs) = r1 # flts2 c rs"
-
-lemma  flts2_k0:
-  shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
-  apply(induct r arbitrary: c rs1)
-   apply(auto)
-  done
-
-lemma  flts2_k00:
-  shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
-  apply(induct rs1 arbitrary: rs2 c)
-   apply(auto)
-  by (metis append.assoc flts2_k0)
-
-
-lemma
-  shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
-  apply(induct c rs rule: flts2.induct)
-        apply(simp)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-  apply(simp)
-    apply(auto simp add: bder_fuse)[1]
-  defer
-   apply(simp)
-  apply(simp del: flts2.simps)
-  apply(rule conjI)
-   prefer 2
-   apply(auto)[1]
-  apply(rule impI)
-  apply(subst flts2_k0)
-  apply(subst map_append)
-  apply(subst flts2.simps)
-  apply(simp only: flts2.simps)
-  apply(auto)
-
-
-
 lemma XXX2_helper:
   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
           "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2481,97 +2440,6 @@
   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]
-  oops
-
-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
-  oops
-
 lemma L06_2:
   assumes "bnullable (bders a [c,d])"
   shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
@@ -2607,51 +2475,6 @@
   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]
-  oops
-
-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
-  oops
-
-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)
-  oops
-
 lemma L1:
   assumes "s \<in> r \<rightarrow> v" 
   shows "decode (bmkeps (bders (intern r) s)) r = Some v"
@@ -2760,19 +2583,6 @@
   apply(simp)
   using test2 by fastforce
 
-lemma XXX2a_long_without_good:
-  assumes "a = AALTs bs0  [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]" 
-  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
-        "bsimp (bder c (bsimp a)) = XXX"
-        "bsimp (bder c a) = YYY"
-  using  assms
-    apply(simp)
-  using  assms
-   apply(simp)
-   prefer 2
-  using  assms
-   apply(simp)
-  oops
 
 lemma bder_bsimp_AALTs:
   shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
@@ -2810,38 +2620,6 @@
   by (metis flts_fuse flts_nothing)
 
 
-lemma PP:
-  assumes "bnullable (bders r s)" 
-  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 add: bders_append bders_simp_append)
-  oops
-
-lemma PP:
-  assumes "bnullable (bders r s)"
-  shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)"
-  using assms
-  apply(induct s arbitrary: r rule: rev_induct)
-   apply(simp)
-  using bmkeps_simp apply auto[1]
-  apply(simp add: bders_append bders_simp_append)
-  apply(drule_tac x="bder a (bsimp r)" in meta_spec)
-  apply(drule_tac meta_mp)
-   defer
-  oops
-
-
-lemma
-  assumes "asize (bsimp a) = asize a"  "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
-  shows "bsimp a = a"
-  using assms
-  apply(simp)
-  oops
-
-
 lemma iii:
   assumes "bsimp_AALTs bs rs \<noteq> AZERO"
   shows "rs \<noteq> []"
@@ -2883,14 +2661,6 @@
 
 (* CT *)
 
-lemma CTU:
-  shows "bsimp_AALTs bs as = li bs as"
-  apply(induct bs as rule: li.induct)
-    apply(auto)
-  done
-
-find_theorems "bder _ (bsimp_AALTs _ _)"
-
 lemma CTa:
   assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
   shows  "flts as = as"
@@ -2947,446 +2717,44 @@
   apply(induct as arbitrary: a)
    apply(auto)
   using le_add2 le_less_trans not_less_eq by blast
-  
 
-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(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 YY:
-  assumes "flts (map bsimp as1) = xs"
-  shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs"
-  using assms
-  apply(induct as1 arbitrary: bs1 xs)
-   apply(simp)
-  apply(auto)
-  by (metis bsimp_fuse flts_fuse k0 list.simps(9))
-  
-
-lemma flts_nonalt:
-  assumes "flts (map bsimp xs) = ys"
-  shows "\<forall>y \<in> set ys. nonalt y"
-  using assms
-  apply(induct xs arbitrary: ys)
-   apply(auto)
-  apply(case_tac xs)
-   apply(auto)
-  using flts2 good1 apply fastforce
-  by (smt ex_map_conv list.simps(9) nn1b nn1c)
-
-
-lemma WWW3:
-  shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
-         flts (map bsimp (map (fuse bs1) as1))"
-  by (metis CT0 YY flts_nonalt flts_nothing qqq1)
-
-
-
-lemma WWW5:
-  shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)"
-  apply(induct as1)
-   apply(auto)
-  done
-
-lemma big0:
-  shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
-         bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
-  by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append)
-
-lemma bignA:
-  shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) =
-         bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))"
-  apply(simp)
-  apply(subst k0)
-  apply(subst WWW3)
-  apply(simp add: flts_append)
-  done
-
-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)
-  (* SEQ case *)
-   apply(simp only:)
-   apply(subst CT1_SEQ)
-  apply(simp only: bsimp.simps)
-
-  (* AALT case *)
-   prefer 2
-   apply(simp only:)
-   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])
-  (* \<rightarrow> *)
-  apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
-            and  s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
-     apply(simp)
-     apply(subst bsimp.simps)
-    apply(simp del: bsimp.simps bder.simps)
-
-    apply(subst bder_bsimp_AALTs)
-    apply(subst bsimp.simps)
-    apply(subst WWW2[symmetric])
-    apply(subst bsimp_AALTs_qq)
-  defer 
-    apply(subst bsimp.simps)
-    
-  (* <- *)
-    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 big0)
-       apply(simp add: WWW4)
-  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)
-  oops
-
-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)
+lemma PPP:
+  assumes "\<Turnstile> v : ders s r"
+  shows "bders (intern r) s >> code v"
+  using  assms
+  apply(induct s arbitrary: r v rule: rev_induct)
    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)
-   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)
-    apply(drule mp)
-  using bsimp_AALTs_size3 apply blast
-    apply(drule_tac x="c" in spec)
-  apply(subst (asm) (2) test)
+   apply (simp add: Posix_Prf contains2)
+  apply(simp add: bders_append ders_append flex_append)
+  apply(frule Prf_injval)
+  apply(drule meta_spec)
+  apply(drule meta_spec)
+  apply(drule meta_mp)
+   apply(assumption)
+  apply(subst retrieve_code)
+   apply(assumption)
+  apply(subst (asm) retrieve_code)
+   apply(assumption)
+  using contains7 contains7a contains6 retrieve_code
+  apply(rule contains7)
   
-   apply(case_tac x52)
-    apply(simp)
-   apply(simp)
-  apply(case_tac "bsimp a = AZERO")
-     apply(simp)
-     apply(subgoal_tac "bsimp (bder c a) = AZERO")
-      prefer 2
-     apply auto[1]
-  apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2)
-    apply(simp)
-    apply(drule_tac x="AALTs x51 list" in spec)
-    apply(drule mp)
-     apply(simp add: asize0)
-  apply(simp)
-   apply(case_tac list)
-    prefer 2
-    apply(simp)
-  apply(case_tac "bsimp aa = AZERO")
-     apply(simp)
-     apply(subgoal_tac "bsimp (bder c aa) = AZERO")
-      prefer 2
-      apply auto[1]
-      apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1)
-     apply(simp)
-  apply(drule_tac x="AALTs x51 (a#lista)" in spec)
-    apply(drule mp)
-     apply(simp  add: asize0)
-     apply(simp)
-     apply (metis flts.simps(2) k0)
-    apply(subst k0)
-  apply(subst (2) k0)
-  
-  
-  using less_add_Suc1 apply fastforce
-    apply(subst k0)
-  
-
-    apply(simp)
-    apply(case_tac "bsimp a = AZERO")
-     apply(simp)
-     apply(subgoal_tac "bsimp (bder c a) = AZERO")
-      prefer 2
-  apply auto[1]
-     apply(simp)
-  apply(case_tac "nonalt (bsimp a)")
-     apply(subst bsimp_AALTs1)
-      apply(simp)
-  using less_add_Suc1 apply fastforce
-  
-     apply(subst bsimp_AALTs1)
-  
-  using nn11a apply b last
-
-  (* SEQ case *)
-   apply(clarify)
-  apply(subst  bsimp.simps)
-   apply(simp del: bsimp.simps)
-   apply(auto simp del: bsimp.simps)[1]
-    apply(subgoal_tac "bsimp x42 \<noteq> AZERO")
-  prefer 2
-  using b3 apply force
-  apply(case_tac "bsimp x43 = AZERO")
-     apply(simp)
-     apply (simp add: bsimp_ASEQ0)
-  apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2)
-    apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
-     apply(clarify)
-     apply(simp)
-     apply(subst bsimp_ASEQ2)
-     apply(subgoal_tac "bsimp (bder c x42) = AZERO")
-      prefer 2
-  using less_add_Suc1 apply fastforce
-     apply(simp)
-     apply(frule_tac x="x43" in spec)
-  apply(drule mp)
-     apply(simp)
-  apply(drule_tac x="c" in spec)
-     apply(subst bder_fuse)
-  apply(subst bsimp_fuse[symmetric])
-     apply(simp)
-  apply(subgoal_tac "bmkeps x42 = bs")
-      prefer 2
-      apply (simp add: bmkeps_simp)
-     apply(simp)
-     apply(subst bsimp_fuse[symmetric])
-  apply(case_tac "nonalt (bsimp (bder c x43))")
-      apply(subst bsimp_AALTs1)
-  using nn11a apply blast
-  using fuse_append apply blast
-     apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs")
-      prefer 2
-  using bbbbs1 apply blast
-  apply(clarify)
-     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 del: bsimp_AALTs.simps)
-  apply(simp only: bsimp_AALTs.simps)
-     apply(simp)
+  find_theorems "bder _ _ >> _"
+  find_theorems "code _ = _"
+  find_theorems "\<Turnstile> _ : der _ _"
   
   
 
-
-(* HERE *)
-apply(case_tac "x42 = AZERO")
-     apply(simp)
-   apply(case_tac "bsimp x43 = AZERO")
-     apply(simp)
-     apply (simp add: bsimp_ASEQ0)
-     apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
-      apply(simp)
-  apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
-  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
-     apply(clarify)
-     apply(simp)
-     apply(subst bsimp_ASEQ2)
-     apply(subgoal_tac "bsimp (bder c x42) = AZERO")
-      apply(simp)
-  prefer 2
-  using less_add_Suc1 apply fastforce
-     apply(subgoal_tac "bmkeps x42 = bs")
-      prefer 2
-      apply (simp add: bmkeps_simp)
-     apply(simp)
-     apply(case_tac "nonalt (bsimp (bder c x43))")
-  apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a)
-     apply(subgoal_tac "nonnested (bsimp (bder c x43))")
-      prefer 2
-  using nn1b apply blast
-     apply(case_tac x43)
-          apply(simp)
-         apply(simp)
-        apply(simp)
-       prefer 3
-       apply(simp)
-       apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6)) 
-      apply(simp)
-      apply(auto)[1]
-       apply(case_tac "(bsimp (bder c x42a)) = AZERO")
-        apply(simp)
-  
-       apply(simp)
-  
-  
-  
-     apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) =  AALTs bs1 rs1 ) \<or>
-                        (\<exists>bs1 r. bsimp (bder c x43) =  fuse bs1 r)")
-      prefer 2
-  apply (metis fuse_empty)
-     apply(erule disjE)
-  prefer 2
-     apply(clarify)
-     apply(simp only:)
-     apply(simp)
-     apply(simp add: fuse_append)
-     apply(subst bder_fuse)
-     apply(subst bsimp_fuse[symmetric])
-     apply(subst bder_fuse)
-     apply(subst bsimp_fuse[symmetric])
-     apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
-      prefer 2
-  using less_add_Suc2 apply bl ast
-     apply(simp only: )
-     apply(subst bsimp_fuse[symmetric])
-      apply(simp only: )
-  
-     apply(simp only: fuse.simps)
+  find_theorems "_ >> (code _)"
+  apply(induct s arbitrary: a bs rule: rev_induct)
+   apply(simp)
+  apply(simp add: bders_simp_append bders_append)
+  apply(rule contains55)
+  find_theorems "bder _ _ >> _"
+  apply(drule_tac x="bder a aa" in meta_spec)
+  apply(drule_tac x="bs" in meta_spec)
   apply(simp)
-      apply(case_tac rs1)
-      apply(simp)
-      apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse)
-  apply(simp)
-  apply(case_tac list)
-      apply(simp)
-      apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
-     apply(simp only: bsimp_AALTs.simps map_cons.simps)
-     apply(auto)[1]
-  
-  
-      
-      apply(subst bsimp_fuse[symmetric])
-  apply(subgoal_tac "bmkeps x42 = bs")
-      prefer 2
-      apply (simp add: bmkeps_simp)
-  
-  
-        apply(simp)
-  
-  using b3 apply force
-  using bsimp_ASEQ0 test2 apply fo rce
-  thm good_SEQ test2
-     apply (simp add: good_SEQ test2)
-    apply (simp add: good_SEQ test2)
-  apply(case_tac "x42 = AZERO")
-     apply(simp)
-   apply(case_tac "x43 = AZERO")
-    apply(simp)
-  apply (simp add: bsimp_ASEQ0)
-  apply(case_tac "\<exists>bs. x42 = AONE bs")
-     apply(clarify)
-     apply(simp)
-    apply(subst bsimp_ASEQ1)
-      apply(simp)
-  using bsimp_ASEQ0 test2 apply fo rce
-     apply (simp add: good_SEQ test2)
-    apply (simp add: good_SEQ test2)
-  apply (simp add: good_SEQ test2)
-  (* AALTs case *)
-  apply(simp)
-  using test2 by fa st force
-
-
-lemma XXX4ab:
-  shows "good (bders_simp (bsimp r) s)  \<or> bders_simp (bsimp r) s = AZERO"
-  apply(induct s arbitrary: r rule:  rev_induct)
-   apply(simp)
-  apply (simp add: good1)
-  apply(simp add: bders_simp_append)
-  apply (simp add: good1)
-  done
+  apply(rule contains55)
+  find_theorems "bsimp _ >> _"
 
 lemma XXX4:
   assumes "good a"