diff -r 692911c0b981 -r 3178f0e948ac thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jul 21 20:22:35 2022 +0100
+++ b/thys3/BlexerSimp.thy	Tue Aug 02 22:11:22 2022 +0100
@@ -303,27 +303,7 @@
   apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") 
   sorry
 
-(*
-lemma ss6_stronger_aux:
-  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
-  apply(induct rs2 arbitrary: rs1)
-   apply simp
-  apply(case_tac "erase a \<in> erase ` set rs1")
-   apply(simp)
-   apply(drule_tac x = "rs1" in meta_spec)
-  apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
-  using srewrites_trans apply blast
-  using deletes_dB apply presburger
-  apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1")
-  
-  apply simp
 
-  apply(auto)
-  prefer 2
-  apply(drule_tac x="rs1 @ [a]" in meta_spec)
-  apply(simp)
-  sorry
-*)
 
 
 lemma ss6_stronger:
@@ -348,6 +328,7 @@
 harmless sorry
 *)
 
+
   sorry
 
 thm seqFold.simps
@@ -359,7 +340,8 @@
 done
 
 
-lemma tint_seqFold_eq: shows"set (tint (seqFold (erase x42) [erase x43])) = 
+lemma tint_seqFold_eq: shows
+"set (tint (seqFold (erase x42) [erase x43])) = 
            set (tint (SEQ (erase x42) (erase x43)))"
   apply(case_tac "erase x42 = ONE")
    apply simp
@@ -377,18 +359,31 @@
 
 
 
-lemma top_bitcodes_preserved_p6:
-  shows "\<lbrakk> r = ASEQ bs a1 a2 \<rbrakk> \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)"
-  apply(induct r arbitrary: as)
-       apply simp
-  apply simp
-     apply simp
 
-  apply(case_tac "a1")
-         apply simp
+lemma p6fa_aux:
+  shows " fuse bs
+            (bsimp_AALTs bs\<^sub>0 as) = 
+           
+            (bsimp_AALTs (bs @ bs\<^sub>0) as)"
+  by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv)
 
 
-  sorry
+lemma p6pfuse_alts:
+  shows 
+" \<And>bs\<^sub>0 as\<^sub>0.     
+       \<lbrakk>\<And>a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\<rbrakk>
+       \<Longrightarrow> \<not> set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<longrightarrow>
+           fuse bs
+            (case a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
+             | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
+             | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa) 
+              =
+           (case fuse bs a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa
+            | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2
+            | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)"
+  apply simp
+  using p6fa_aux by presburger
+
 
 
 
@@ -406,9 +401,27 @@
     apply simp
   using tint_seqFold_eq
   apply simp
+    apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append)
+  using p6pfuse_alts apply presburger
+  by simp
 
+
+(*
+The top-level bitlist stays the same:
+\<^sub>b\<^sub>sa ------pruning----->  \<^sub>b\<^sub>s\<^sub>' b  \<Longrightarrow>        \<exists>bs3. bs' = bs @ bs3 
+*)
+lemma top_bitcodes_preserved_p6:
+  shows "top r = bs \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)"
+  
+
+  apply(induct r arbitrary: as)
+
+(*this sorry requires more care *)
+  
   sorry
 
+
+
 corollary prune6_preserves_fuse_srewrite:
   shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)"
   apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]")
@@ -567,7 +580,14 @@
   case (ss6 a1 a2 rsa rsb rsc)
   then show ?case
     by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD)
-qed (auto)
+next
+           prefer 10
+  case (ss7 as a as1)
+  then show ?case
+    
+(*this sorry requires more effort*)
+  sorry
+qed(auto)
 
 lemma rewrites_bmkeps: 
   assumes "r1 \<leadsto>* r2" "bnullable r1" 
@@ -606,6 +626,12 @@
   shows "(map f [a]) = [f a]"
   by (simp)
 
+lemma "set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<Longrightarrow>
+       set (tint (erase (bder c a))) \<subseteq> (\<Union>x\<in>set (map (bder c) as). set (tint (erase x)))"
+  
+  sorry
+
+
 lemma rewrite_preserves_bder: 
   shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
   and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
@@ -681,6 +707,11 @@
     apply(rule_tac rrewrite_srewrite.ss6)
     using Der_def der_correctness apply auto[1]
     by blast
+next
+  case (ss7 as a as1)
+  then show ?case
+    apply simp
+    sorry
 qed
 
 lemma rewrites_preserves_bder: 
@@ -733,18 +764,20 @@
       by (metis rrewrites_trans star_seq star_seq2) 
     then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp
   } 
-  ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry
+  ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" 
+    by blast
 next
   case (2 bs1 rs)
   have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact
   then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites)
   also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) 
-  also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger)
-  finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+  also have "... s\<leadsto>* dB6 (flts (map bsimpStrong6 rs))  {}" by (simp add: ss6_stronger)
+  finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs))  {})"
     using contextrewrites0 by auto
-  also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+  also have "... \<leadsto>* bsimp_AALTs  bs1 (dB6 (flts (map bsimpStrong6 rs))  {})"
     by (simp add: bsimp_AALTs_rewrites)     
-  finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
+  finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" 
+    using bsimpStrong6.simps(2) by presburger
 qed (simp_all)