diff -r a7344c9afbaf -r b2bea5968b89 thys2/SizeBound3.thy
--- a/thys2/SizeBound3.thy	Tue Jun 14 18:06:33 2022 +0100
+++ b/thys2/SizeBound3.thy	Thu Jun 23 16:09:40 2022 +0100
@@ -703,28 +703,6 @@
   shows "(\<Union> (RL ` rerase ` (set (distinctBy rs rerase {})))) = \<Union> (RL ` rerase ` (set rs))"
   by (metis RL_rerase_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 RL_bsimp_rerase:
   shows "RL (rerase r) = RL (rerase (bsimp r))"
@@ -964,6 +942,8 @@
   apply(simp)
   done
 
+
+
 lemma ss6_stronger:
   shows "rs1 s\<leadsto>* distinctBy rs1 rerase {}"
   by (metis append_Nil list.set(1) list.simps(8) ss6_stronger_aux)
@@ -1523,7 +1503,6 @@
   prefer 2
    apply(subgoal_tac "distinct (map rerase (v # vb # vc)) = True")
     prefer 2
-  sledgehammer
     apply blast
   prefer 2
    apply force
@@ -1876,7 +1855,7 @@
        prefer 2
   apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
   using dB_keeps_property apply presburger
-  sledgehammer
+  
 
   using dB_does_more_job apply presburger
   apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood")
@@ -2036,203 +2015,6 @@
   apply(auto)[1]  
   done
   
-lemma test:
-  assumes "agood r"
-  shows "bsimp r = r"
-  using assms
-  apply(induct r taking: "asize" rule: measure_induct)
-  apply(erule agood.elims)
-                      apply(simp_all)
-  apply(subst k0)
-  apply(subst (2) k0)
-                apply(subst flts_qq)
-                  apply(auto)[1]
-                 apply(auto)[1]
-  oops
-
-
-
-lemma bsimp_idem:
-  shows "bsimp (bsimp r) = bsimp r"
-  using test good1
-  oops
-
-(*
-lemma erase_preimage1:
-  assumes "anonalt r"
-  shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs"
-  apply(case_tac r)
-  apply simp+
-  using anonalt.simps(1) assms apply presburger
-  by fastforce
-
-lemma erase_preimage_char:
-  assumes "anonalt r"
-  shows "erase r = CH c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
-  apply(case_tac r)
-  apply simp+
-  using assms apply fastforce
-  by simp
-
-lemma erase_preimage_seq:
-  assumes "anonalt r"
-  shows "erase r = SEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> erase a1 = r1 \<and> erase a2 = r2"
-  apply(case_tac r)
-  apply simp+
-  using assms apply fastforce
-  by simp
-
-lemma rerase_preimage_seq:
-  assumes "anonalt r"
-  shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2 "
-  using rerase_preimage4 by presburger
-
-lemma seq_recursive_equality:
-  shows "\<lbrakk>r1 = a1; r2 = a2\<rbrakk> \<Longrightarrow> SEQ r1 r2 = SEQ a1 a2"
-  by meson
-
-lemma almost_identical_image:
-  assumes "agood r" "\<forall>r \<in> rset. agood r"
-  shows "erase r \<in> erase ` rset \<Longrightarrow> \<exists>r' \<in> rset. erase r' = erase r"
-  by auto
-
-lemma goodalts_never_change:
-  assumes "r = AALTs bs rs" "agood r"
-  shows "\<exists>r1 r2. erase r = ALT r1 r2"
-  by (metis agood.simps(4) agood.simps(5) assms(1) assms(2) bmkepss.cases erase.simps(6))
-
-
-fun shape_preserving :: "arexp \<Rightarrow> bool" where
-  "shape_preserving AZERO = True"
-| "shape_preserving (AONE bs) = True"
-| "shape_preserving (ACHAR bs c) = True"
-| "shape_preserving (AALTs bs []) = False"
-| "shape_preserving (AALTs bs [a]) = False"
-| "shape_preserving (AALTs bs (a1 # a2 # rs)) = (\<forall>r \<in> set (a1 # a2 # rs). shape_preserving r)"
-| "shape_preserving (ASEQ bs r1 r2) = (shape_preserving r1 \<and> shape_preserving r2)"
-| "shape_preserving (ASTAR bs r) = shape_preserving r"
-
-
-lemma good_shape_preserving:
-  assumes "\<nexists>bs r0. r = ASTAR bs r0"
-  shows "agood r \<Longrightarrow> shape_preserving r"
-  using assms
-
-  apply(induct r)
-  prefer 6
-  
-  apply blast
-      apply simp
- 
-  oops
-
-
-
-
-
-lemma shadow_arexp_rerase_erase:
-  shows "\<lbrakk>agood r; agood r';  erase r = erase r'\<rbrakk> \<Longrightarrow> rerase r = rerase r'"
-  apply(induct r )
-       apply simp
-      apply(induct r')
-           apply simp+
-       apply (metis goodalts_never_change rexp.distinct(15))
-  apply simp+
-     apply (metis anonalt.elims(3) erase_preimage_char goodalts_never_change rerase.simps(3) rexp.distinct(21))
-    apply(induct r')
-         apply simp
-  apply simp
-  apply simp
-      apply(subgoal_tac "agood r1")
-  prefer 2
-  apply (metis SizeBound3.good_SEQ agood.simps(10) agood.simps(11) agood.simps(2) agood.simps(3) agood.simps(33) agood.simps(7) bsimp.cases)
-      apply(subgoal_tac "agood r2")
-       apply(subgoal_tac "agood r'1")
-        apply(subgoal_tac "agood r'2")
-         apply(subgoal_tac "rerase r'1 = rerase r1")
-  apply(subgoal_tac "rerase r'2 = rerase r2")
-  
-  using rerase.simps(5) apply presburger
-  oops
-
-
-
-lemma rerase_erase_good:
-  assumes "agood r" "\<forall>r \<in> rset. agood r"
-  shows "erase r \<in> erase ` rset \<Longrightarrow> rerase r \<in> rerase ` rset"
-  using assms
-  apply(case_tac r)
-       apply simp+
-  oops
-
-lemma rerase_erase_both:
-  assumes "\<forall>r \<in> rset. agood r" "agood r"
-  shows "(rerase r \<in> (rerase ` rset)) \<longleftrightarrow> (erase r \<in> (erase ` rset))"
-  using assms
-  apply(induct r )
-       apply force
-  apply simp
-      apply(case_tac "RONE \<in> rerase ` rset")
-       apply(subgoal_tac "\<exists>bs. (AONE bs) \<in> rset")
-        apply (metis erase.simps(2) rev_image_eqI)
-       apply (metis image_iff rerase_preimage2)
-      apply(subgoal_tac "\<nexists>bs. (AONE bs) \<in> rset")
-  apply(subgoal_tac "ONE \<notin> erase ` rset")
-  
-        apply blast
-  sledgehammer
-       apply (metis erase_preimage1 image_iff)
-      apply (metis rerase.simps(2) rev_image_eqI)
-     apply (smt (verit, best) erase.simps(3) erase_preimage_char image_iff rerase.simps(3) rerase_preimage3)
-(*    apply simp
-    apply(subgoal_tac "(RSEQ (rerase r1) (rerase r2) \<in> rerase ` rset) \<Longrightarrow>  (SEQ (erase r1) (erase r2) \<in> erase ` rset)")
-  prefer 2
-     apply(subgoal_tac "\<exists>bs a1 a2. (ASEQ bs a1 a2) \<in> rset \<and> rerase a1 = rerase r1 \<and> rerase a2 = rerase r2")
-      prefer 2
-  apply (metis (full_types) image_iff rerase_preimage4)
-     apply(erule exE)+
-     apply(subgoal_tac "erase (ASEQ bs a1 a2) \<in> (erase ` rset) ")
-      apply(subgoal_tac "SEQ (erase a1) (erase a2) \<in> (erase ` rset)")
-  apply(subgoal_tac "SEQ (erase a1) (erase a2) = SEQ (erase r1) (erase r2)")
-        apply metis
-       apply(erule conjE)+*)
-  apply(drule_tac x = "rset" in meta_spec)+
-  
-
-
-
-  oops
-
-
-lemma rerase_pushin1_general:
-  assumes "\<forall>r \<in> set rs. agood r"
-  shows "map rerase (distinctBy rs erase (erase ` rset)) = rdistinct (map rerase rs) (rerase ` rset)"
-  apply(induct rs arbitrary: rset)
-   apply simp+
-  apply(case_tac "erase a \<in> erase ` rset")
-   apply simp
-  
-
-
-  oops
-
-lemma rerase_erase:
-  assumes "\<forall>r \<in> set as. agood r \<and> anonalt r"
-  shows "rdistinct (map rerase as) (rerase ` rset) = map rerase (distinctBy as erase (erase ` rset))"
-  using assms
-  apply(induct as)
-   apply simp+
-
-  sorry
-
-
-lemma rerase_pushin1:
-  assumes "\<forall>r \<in> set rs. anonalt r \<and> agood r"
-  shows "map rerase (distinctBy rs erase {}) = rdistinct (map rerase rs) {}"
-  apply(insert rerase_erase)
-  by (metis assms image_empty)
-  
-*)
 
 
 
@@ -2337,4 +2119,7 @@
   apply(insert aders_simp_finiteness)
   by (simp add: rders_simp_bounded)
 
+unused_thms
+
+
 end