diff -r cc8e231529fb -r e1b74d618f1b thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Tue Jan 25 13:12:50 2022 +0000
+++ b/thys2/SizeBound4.thy	Thu Jan 27 23:25:26 2022 +0000
@@ -132,15 +132,6 @@
   apply(auto)
   done
 
-lemma fuse_Nil:
-  shows "fuse [] r = r"
-  by (induct r)(simp_all)
-
-(*
-lemma map_fuse_Nil:
-  shows "map (fuse []) rs = rs"
-  by (induct rs)(simp_all add: fuse_Nil)
-*)
 
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
@@ -280,23 +271,23 @@
   shows "retrieve (fuse bs r) v = bs @ retrieve r v"
   using assms
   apply(induct r arbitrary: v bs)
-         apply(auto elim: Prf_elims)[4]
-   defer
-  using retrieve_encode_STARS
-   apply(auto elim!: Prf_elims)[1]
-   apply(case_tac vs)
-    apply(simp)
-   apply(simp)
-  (* AALTs  case *)
+  apply(auto elim: Prf_elims)[4]
+  apply(case_tac x2a)
+  apply(simp)
+  using Prf_elims(1) apply blast
+  apply(case_tac x2a)
+  apply(simp)
+  apply(simp)
+  apply(case_tac list)
   apply(simp)
-  apply(case_tac x2a)
-   apply(simp)
-   apply(auto elim!: Prf_elims)[1]
+  apply(simp)
+  apply (smt (verit, best) Prf_elims(3) append_assoc retrieve.simps(4) retrieve.simps(5))
   apply(simp)
-   apply(case_tac list)
-   apply(simp)
-  apply(auto)
+  using retrieve_encode_STARS
   apply(auto elim!: Prf_elims)[1]
+  apply(case_tac vs)
+  apply(simp)
+  apply(simp)
   done
 
 lemma retrieve_fuse:
@@ -314,139 +305,92 @@
   apply(simp_all add: retrieve_fuse retrieve_encode_STARS)
   done
 
-(*
-lemma bnullable_Hdbmkeps_Hd:
-  assumes "bnullable a" 
-  shows  "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)"
-  using assms by simp
-*)
 
-
-lemma r2:
-  assumes "x \<in> set rs" "bnullable x"
-  shows "bnullable (AALTs bs rs)"
+lemma retrieve_AALTs_bnullable1:
+  assumes "bnullable r"
+  shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+         = bs @ retrieve r (mkeps (erase r))"
   using assms
-  apply(induct rs)
-   apply(auto)
+  apply(case_tac rs)
+  apply(auto simp add: bnullable_correctness)
   done
 
-lemma  r3:
-  assumes "\<not> bnullable r" 
-          "bnullables rs"
-  shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) =
-         retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))"
+lemma retrieve_AALTs_bnullable2:
+  assumes "\<not>bnullable r" "bnullables rs"
+  shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))
+         = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
   using assms
   apply(induct rs arbitrary: r bs)
-   apply(auto)[1]
   apply(auto)
   using bnullable_correctness apply blast
-    apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2)
-   apply(subst retrieve_fuse2[symmetric])
-  apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable)
-   apply(simp)
-  apply(case_tac "bnullable a")
-  apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2)
-  apply(drule_tac x="a" in meta_spec)
-  apply(drule_tac x="bs" in meta_spec)
-  apply(drule meta_mp)
-   apply(simp)
-  apply(drule meta_mp)
-   apply(auto)
-  apply(subst retrieve_fuse2[symmetric])
   apply(case_tac rs)
-    apply(simp)
-   apply(auto)[1]
-      apply (simp add: bnullable_correctness)
-  
-  apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2)
-    apply (simp add: bnullable_correctness)
-  apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2)
-  apply(simp)
+  apply(auto)
+  using bnullable_correctness apply blast
+  apply(case_tac rs)
+  apply(auto)
   done
 
-lemma t: 
+lemma bmkeps_retrieve_AALTs: 
   assumes "\<forall>r \<in> set rs. bnullable r \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" 
           "bnullables rs"
   shows "bs @ bmkepss rs = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))"
  using assms
   apply(induct rs arbitrary: bs)
   apply(auto)
-  apply (metis (no_types, opaque_lifting) bmkepss.cases bnullable_correctness erase.simps(5) erase.simps(6) mkeps.simps(3) retrieve.simps(3) retrieve.simps(4))
-  apply (metis r3)
-  apply (metis (no_types, lifting) bmkepss.cases bnullable_correctness empty_iff erase.simps(6) list.set(1) mkeps.simps(3) retrieve.simps(4))
-  apply (metis r3)
-  done
-      
+  using retrieve_AALTs_bnullable1 apply presburger
+  apply (metis retrieve_AALTs_bnullable2)
+  apply (simp add: retrieve_AALTs_bnullable1)
+  by (metis retrieve_AALTs_bnullable2)
+
+    
 lemma bmkeps_retrieve:
   assumes "bnullable r"
   shows "bmkeps r = retrieve r (mkeps (erase r))"
   using assms
   apply(induct r)
-  apply(auto)
-  using t by auto
+  apply(auto)  
+  using bmkeps_retrieve_AALTs by auto
 
 lemma bder_retrieve:
   assumes "\<Turnstile> v : der c (erase r)"
   shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"
   using assms  
   apply(induct r arbitrary: v rule: erase.induct)
-         apply(simp)
-         apply(erule Prf_elims)
-        apply(simp)
-        apply(erule Prf_elims) 
-        apply(simp)
-      apply(case_tac "c = ca")
-       apply(simp)
-       apply(erule Prf_elims)
-       apply(simp)
-      apply(simp)
-       apply(erule Prf_elims)
-  apply(simp)
-      apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
-    apply(erule Prf_elims)
-     apply(simp)
-    apply(simp)
-    apply(case_tac rs)
-     apply(simp)
-    apply(simp)
-  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq)
-   apply(simp)
-   apply(case_tac "nullable (erase r1)")
-    apply(simp)
-  apply(erule Prf_elims)
-     apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-     apply(erule Prf_elims)
-     apply(simp)
-   apply(subgoal_tac "bnullable r1")
-  prefer 2
-  using bnullable_correctness apply blast
-    apply(simp)
-    apply(simp add: retrieve_fuse2)
-    apply(simp add: bmkeps_retrieve)
-   apply(simp)
-   apply(erule Prf_elims)
-   apply(simp)
-  using bnullable_correctness apply blast
-  apply(rename_tac bs r v)
+  using Prf_elims(1) apply auto[1]
+  using Prf_elims(1) apply auto[1]
+  apply(auto)[1]
+  apply (metis Prf_elims(4) injval.simps(1) retrieve.simps(1) retrieve.simps(2))
+  using Prf_elims(1) apply blast
+  (* AALTs case *)
   apply(simp)
   apply(erule Prf_elims)
-     apply(clarify)
+  apply(simp)
+  apply(simp)
+  apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v)
+  apply(erule Prf_elims)
+  apply(simp)
+  apply(simp)
+  apply(case_tac rs)
+  apply(simp)
+  apply(simp)
+  using Prf_elims(3) apply fastforce
+  (* ASEQ case *) 
+  apply(simp)
+  apply(case_tac "nullable (erase r1)")
+  apply(simp)
+  apply(erule Prf_elims)
+  using Prf_elims(2) bnullable_correctness apply force
+  apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+  apply (simp add: bmkeps_retrieve bnullable_correctness retrieve_fuse2)
+  using Prf_elims(2) apply force
+  (* ASTAR case *)  
+  apply(rename_tac bs r v)
+  apply(simp)  
   apply(erule Prf_elims)
   apply(clarify)
-  apply(subst injval.simps)
-  apply(simp del: retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(subst retrieve.simps)
-  apply(simp)
-  apply(simp add: retrieve_fuse2)
-  done
-  
+  apply(erule Prf_elims)
+  apply(clarify)
+  by (simp add: retrieve_fuse2)
 
 
 lemma MAIN_decode:
@@ -581,79 +525,6 @@
   apply(simp_all)
   done
 
-lemma L_bsimp_ASEQ:
-  "L (erase (ASEQ bs r1 r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
-  apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
-  apply(simp_all)
-  by (metis erase_fuse fuse.simps(4))
-
-lemma L_bsimp_AALTs:
-  "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))"
-  apply(induct bs rs rule: bsimp_AALTs.induct)
-  apply(simp_all add: erase_fuse)
-  done
-
-lemma L_erase_AALTs:
-  shows "L (erase (AALTs bs rs)) = \<Union> (L ` erase ` (set rs))"
-  apply(induct rs)
-   apply(simp)
-  apply(simp)
-  apply(case_tac rs)
-   apply(simp)
-  apply(simp)
-  done
-
-lemma L_erase_flts:
-  shows "\<Union> (L ` erase ` (set (flts rs))) = \<Union> (L ` erase ` (set rs))"
-  apply(induct rs rule: flts.induct)
-  apply(simp_all)
-  apply(auto)
-  using L_erase_AALTs erase_fuse apply auto[1]
-  by (simp add: L_erase_AALTs erase_fuse)
-
-lemma L_erase_dB_acc:
-  shows "(\<Union> (L ` acc) \<union> (\<Union> (L ` erase ` (set (distinctBy rs erase acc))))) 
-            = \<Union> (L ` acc) \<union>  \<Union> (L ` erase ` (set rs))"
-  apply(induction rs arbitrary: acc)
-  apply simp_all
-  by (smt (z3) SUP_absorb UN_insert sup_assoc sup_commute)
-
-
-lemma L_erase_dB:
-  shows "(\<Union> (L ` erase ` (set (distinctBy rs erase {})))) = \<Union> (L ` erase ` (set rs))"
-  by (metis L_erase_dB_acc Un_commute Union_image_empty)
-
-lemma L_bsimp_erase:
-  shows "L (erase r) = L (erase (bsimp r))"
-  apply(induct r)
-  apply(simp)
-  apply(simp)
-  apply(simp)
-  apply(auto simp add: Sequ_def)[1]
-  apply(subst L_bsimp_ASEQ[symmetric])
-  apply(auto simp add: Sequ_def)[1]
-  apply(subst (asm)  L_bsimp_ASEQ[symmetric])
-  apply(auto simp add: Sequ_def)[1]
-  apply(simp)
-  apply(subst L_bsimp_AALTs[symmetric])
-  defer
-  apply(simp)
-  apply(subst (2)L_erase_AALTs)  
-  apply(subst L_erase_dB)
-  apply(subst L_erase_flts)
-  apply (simp add: L_erase_AALTs)
-  done
-
-lemma L_bders_simp:
-  shows "L (erase (bders_simp r s)) = L (erase (bders r s))"
-  apply(induct s arbitrary: r rule: rev_induct)
-  apply(simp)
-  apply(simp)
-  apply(simp add: ders_append)
-  apply(simp add: bders_simp_append)
-  apply(simp add: L_bsimp_erase[symmetric])
-  by (simp add: der_correctness)
-
 
 lemma bmkeps_fuse:
   assumes "bnullable r"
@@ -668,17 +539,6 @@
   apply(auto simp add: bmkeps_fuse bnullable_fuse)
   done
 
-
-lemma b4:
-  shows "bnullable (bders_simp r s) = bnullable (bders r s)"
-proof -
-  have "L (erase (bders_simp r s)) = L (erase (bders r s))"
-    using L_bders_simp by force
-  then show "bnullable (bders_simp r s) = bnullable (bders r s)"
-    using bnullable_correctness nullable_correctness by blast
-qed
-
-
 lemma bder_fuse:
   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
   apply(induct a arbitrary: bs c)
@@ -860,7 +720,7 @@
     apply(rule rrewrite_srewrite.ss6[simplified])
     apply(simp add: erase_fuse)
     done
- qed (auto intro: rrewrite_srewrite.intros)
+qed (auto intro: rrewrite_srewrite.intros)
 
 
 lemma rewrites_fuse:  
@@ -1173,7 +1033,7 @@
 theorem main_blexer_simp: 
   shows "blexer r s = blexer_simp r s"
   unfolding blexer_def blexer_simp_def
-  using b4 main_aux by simp
+  by (metis central main_aux rewrites_bnullable_eq)
 
 
 theorem blexersimp_correctness: