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