--- 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