# HG changeset patch
# User Chengsong
# Date 1568393204 -3600
# Node ID 04391e303101a346c50abe57584336d64bf1824c
# Parent  97741a7b8b371717d35fa651bbd88b7d1785c79f
lemma proved

diff -r 97741a7b8b37 -r 04391e303101 thys/BitCoded2CT.thy
--- a/thys/BitCoded2CT.thy	Fri Sep 13 15:39:11 2019 +0100
+++ b/thys/BitCoded2CT.thy	Fri Sep 13 17:46:44 2019 +0100
@@ -3088,12 +3088,38 @@
 lemma derc_alt00:
   assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
   shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
-  oops
-
+  using assms
+  apply -
+  apply(case_tac "bsimp a")
+  prefer 6
+       apply(simp)+
+  apply(subst bder_bsimp_AALTs)
+  by (metis append_Nil contains51c map_bder_fuse map_map)
+lemma derc_alt01:
+  shows "\<And>a list1 list2.
+       \<lbrakk> bder c (bsimp a) >> bs ;
+        bder c a >> bs; as = [a] @ list2; flts (map bsimp list1) = [];
+        flts (map bsimp list2) \<noteq> []\<rbrakk>
+       \<Longrightarrow> bder c (bsimp_AALTs [] (flts [bsimp a] @ flts (map bsimp list2))) >> bs"
+  using bder_bsimp_AALTs contains51b derc_alt00 f_cont2 by fastforce
+
+lemma derc_alt10:
+  shows "\<And>a list1 list2.
+       \<lbrakk>  a \<in> set as; bder c (bsimp a) >> bs;
+        bder c a >> bs; as = list1 @ [a] @ list2; flts (map bsimp list1) \<noteq> [];
+flts(map bsimp list2) = []\<rbrakk>
+       \<Longrightarrow> bder c (bsimp_AALTs []
+              (flts (map bsimp list1) @
+               flts (map bsimp [a]) @ flts (map bsimp list2))) >> bs"
+  apply(subst bder_bsimp_AALTs)
+  apply simp
+  using bder_bsimp_AALTs contains50 derc_alt00 f_cont2 by fastforce
+
+
+(*QUESTION*)
 lemma derc_alt:
   assumes "bder c (AALTs [] as) >> bs" 
-(*QUESTION*)
-and "\<forall> a \<in> as. (bder c a >> bs) \<Rightarrow> (bder c (bsimp a) >> bs)"
+   and "\<forall>a \<in> set as. ((bder c a >> bs) \<longrightarrow> (bder c (bsimp a) >> bs))"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
   using assms
   apply -
@@ -3118,15 +3144,18 @@
   apply(case_tac "flts (map bsimp list1) = Nil")
   apply(case_tac "flts (map bsimp list2) = Nil")
   apply simp
-
+  using derc_alt00 apply blast
+  apply simp
+  using derc_alt01 apply blast
+  apply(case_tac "flts (map bsimp list2) = Nil")
+  using derc_alt10 apply blast
+  by (smt bder_bsimp_AALTs contains50 contains51b derc_alt00 f_cont2 list.simps(8) list.simps(9) map_append)
 
   (*find_theorems "flts _ = _ "*)
 (*  (*HERE*)
   apply(drule  i_know_it_must_be_a_theorem_but_dunno_its_name)
 *)
 
-  oops
-
 lemma transfer:
   assumes " (a \<Rightarrow> c) \<and> (c \<Rightarrow> b)"
   shows "a \<Rightarrow> b"
@@ -3681,6 +3710,7 @@
   apply(subgoal_tac "rsX \<noteq> []")
    prefer 2
    apply (metis arexp.distinct(7) good.simps(4) good1)
+
   by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))
 
 lemma CONTAINS1: