--- a/thys2/SizeBound4.thy Sun Jan 30 23:36:31 2022 +0000
+++ b/thys2/SizeBound4.thy Sun Jan 30 23:37:29 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"
@@ -155,7 +146,7 @@
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
"retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
-| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
+| "retrieve (AALTs bs [r]) v = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
| "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -225,8 +216,8 @@
| "bders r (c#s) = bders (bder c r) s"
lemma bders_append:
- "bders r (s1 @ s2) = bders (bders r s1) s2"
- apply(induct s1 arbitrary: r s2)
+ "bders c (s1 @ s2) = bders (bders c s1) s2"
+ apply(induct s1 arbitrary: c s2)
apply(simp_all)
done
@@ -274,29 +265,28 @@
apply(simp_all)
done
-
lemma retrieve_fuse2:
assumes "\<Turnstile> v : (erase r)"
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 +304,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:
@@ -514,7 +457,7 @@
(if (f x) \<in> acc then distinctBy xs f acc
else x # (distinctBy xs f ({f x} \<union> acc)))"
-
+
fun flts :: "arexp list \<Rightarrow> arexp list"
where
@@ -581,84 +524,12 @@
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"
shows "bmkeps (fuse bs r) = bs @ bmkeps r"
- by (metis assms bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
+ using assms
+ by (metis bmkeps_retrieve bnullable_correctness erase_fuse mkeps_nullable retrieve_fuse2)
lemma bmkepss_fuse:
assumes "bnullables rs"
@@ -668,21 +539,10 @@
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)
- apply(simp_all)
+ apply(simp_all)
done
@@ -700,7 +560,7 @@
| bs5: "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| bs6: "AALTs bs [] \<leadsto> AZERO"
| bs7: "AALTs bs [r] \<leadsto> fuse bs r"
-| bs10: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
+| bs8: "rs1 s\<leadsto> rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto> AALTs bs rs2"
| ss1: "[] s\<leadsto> []"
| ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)"
| ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)"
@@ -726,11 +586,6 @@
shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
using rrewrites.intros(1) rrewrites.intros(2) by blast
-lemma srewrites_single :
- shows "rs1 s\<leadsto> rs2 \<Longrightarrow> rs1 s\<leadsto>* rs2"
- using rrewrites.intros(1) rrewrites.intros(2) by blast
-
-
lemma rrewrites_trans[trans]:
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
shows "r1 \<leadsto>* r3"
@@ -753,13 +608,13 @@
"rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
apply(induct rs1 rs2 rule: srewrites.inducts)
apply simp
- using bs10 r_in_rstar rrewrites_trans by blast
+ using bs8 r_in_rstar rrewrites_trans by blast
lemma contextrewrites1:
"r \<leadsto>* r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto>* AALTs bs (r' # rs)"
apply(induct r r' rule: rrewrites.induct)
apply simp
- using bs10 ss3 by blast
+ using bs8 ss3 by blast
lemma srewrite1:
shows "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs @ rs1) s\<leadsto> (rs @ rs2)"
@@ -777,9 +632,9 @@
shows "r1 \<leadsto> r2 \<Longrightarrow> True"
and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
apply(induct rule: rrewrite_srewrite.inducts)
- apply(auto)
- apply (metis append_Cons append_Nil srewrites1)
- apply(meson srewrites.simps ss3)
+ apply(auto)
+ apply (metis append_Cons append_Nil srewrites1)
+ apply(meson srewrites.simps ss3)
apply (meson srewrites.simps ss4)
apply (meson srewrites.simps ss5)
by (metis append_Cons append_Nil srewrites.simps ss6)
@@ -806,15 +661,15 @@
shows "[r1] s\<leadsto>* [r2]"
using assms
apply(induct r1 r2 rule: rrewrites.induct)
- apply(auto)
+ apply(auto)
by (meson srewrites.simps srewrites_trans ss3)
lemma srewrites7:
assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2"
shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)"
using assms
- by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
-
+ by (smt (verit, del_insts) append.simps srewrites1 srewrites3 srewrites6 srewrites_trans)
+
lemma ss6_stronger_aux:
shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))"
apply(induct rs2 arbitrary: rs1)
@@ -828,47 +683,47 @@
shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
using ss6_stronger_aux[of "[]" _] by auto
-
lemma rewrite_preserves_fuse:
shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3"
- and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3"
+ and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto> map (fuse bs) rs3"
proof(induct rule: rrewrite_srewrite.inducts)
case (bs3 bs1 bs2 r)
- then show ?case
+ then show "fuse bs (ASEQ bs1 (AONE bs2) r) \<leadsto> fuse bs (fuse (bs1 @ bs2) r)"
by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3)
next
- case (bs7 bs r)
- then show ?case
+ case (bs7 bs1 r)
+ then show "fuse bs (AALTs bs1 [r]) \<leadsto> fuse bs (fuse bs1 r)"
by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7)
next
case (ss2 rs1 rs2 r)
- then show ?case
- using srewrites7 by force
+ then show "map (fuse bs) (r # rs1) s\<leadsto> map (fuse bs) (r # rs2)"
+ by (simp add: rrewrite_srewrite.ss2)
next
case (ss3 r1 r2 rs)
- then show ?case by (simp add: r_in_rstar srewrites7)
+ then show "map (fuse bs) (r1 # rs) s\<leadsto> map (fuse bs) (r2 # rs)"
+ by (simp add: rrewrite_srewrite.ss3)
next
case (ss5 bs1 rs1 rsb)
- then show ?case
- apply(simp)
- by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps)
+ have "map (fuse bs) (AALTs bs1 rs1 # rsb) = AALTs (bs @ bs1) rs1 # (map (fuse bs) rsb)" by simp
+ also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))"
+ by (simp add: rrewrite_srewrite.ss5)
+ finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)"
+ by (simp add: comp_def fuse_append)
next
case (ss6 a1 a2 rsa rsb rsc)
- then show ?case
+ then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)"
apply(simp)
- apply(rule srewrites_single)
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:
assumes "r1 \<leadsto>* r2"
shows "fuse bs r1 \<leadsto>* fuse bs r2"
using assms
apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
-apply(auto intro: rewrite_preserves_fuse rrewrites_trans)
+apply(auto intro: rewrite_preserves_fuse)
done
@@ -911,13 +766,12 @@
by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps)
lemma trivialbsimp_srewrites:
- "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
+ assumes "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x"
+ shows "rs s\<leadsto>* (map f rs)"
+using assms
apply(induction rs)
- apply simp
- apply(simp)
- using srewrites7 by auto
-
-
+ apply(simp_all add: srewrites7)
+ done
lemma fltsfrewrites: "rs s\<leadsto>* flts rs"
apply(induction rs rule: flts.induct)
@@ -1044,7 +898,7 @@
lemma to_zero_in_alt:
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
- by (simp add: bs1 bs10 ss3)
+ by (simp add: bs1 bs8 ss3)
@@ -1054,7 +908,6 @@
apply(simp_all add: bder_fuse)
done
-
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"
@@ -1072,7 +925,7 @@
case (bs3 bs1 bs2 r)
show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)"
apply(simp)
- by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
+ by (metis (no_types, lifting) bder_fuse bs8 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
next
case (bs4 r1 r2 bs r3)
have as: "r1 \<leadsto> r2" by fact
@@ -1097,7 +950,7 @@
show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7)
next
- case (bs10 rs1 rs2 bs)
+ case (bs8 rs1 rs2 bs)
have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact
then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)"
using contextrewrites0 by force
@@ -1168,12 +1021,10 @@
qed
-
-
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:
@@ -1181,6 +1032,79 @@
using blexer_correctness main_blexer_simp by simp
+(* below is the idempotency of bsimp *)
+
+lemma bsimp_ASEQ_fuse:
+ shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2"
+ apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct)
+ apply(auto)
+ done
+
+lemma bsimp_AALTs_fuse:
+ assumes "\<forall>r \<in> set rs. fuse bs1 (fuse bs2 r) = fuse (bs1 @ bs2) r"
+ shows "fuse bs1 (bsimp_AALTs bs2 rs) = bsimp_AALTs (bs1 @ bs2) rs"
+ using assms
+ apply(induct bs2 rs arbitrary: bs1 rule: bsimp_AALTs.induct)
+ apply(auto)
+ done
+
+lemma bsimp_fuse:
+ shows "fuse bs (bsimp r) = bsimp (fuse bs r)"
+ apply(induct r arbitrary: bs)
+ apply(simp_all add: bsimp_ASEQ_fuse bsimp_AALTs_fuse fuse_append)
+ done
+
+lemma bsimp_ASEQ_idem:
+ assumes "bsimp (bsimp r1) = bsimp r1" "bsimp (bsimp r2) = bsimp r2"
+ shows "bsimp (bsimp_ASEQ x1 (bsimp r1) (bsimp r2)) = bsimp_ASEQ x1 (bsimp r1) (bsimp r2)"
+ using assms
+ apply(case_tac "bsimp r1 = AZERO")
+ apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+ apply(simp)
+ apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ apply(auto)[1]
+ apply (metis bsimp_fuse)
+ apply(simp add: bsimp_ASEQ1)
+ done
+
+lemma bsimp_AALTs_idem:
+ assumes "\<forall>r \<in> set rs. bsimp (bsimp r) = bsimp r"
+ shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (map bsimp rs)"
+ using assms
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(simp)
+ apply(simp)
+ using bsimp_fuse apply presburger
+ oops
+
+lemma bsimp_idem_rev:
+ shows "\<nexists>r2. bsimp r1 \<leadsto> r2"
+ apply(induct r1 rule: bsimp.induct)
+ apply(auto)
+ defer
+ defer
+ using rrewrite.simps apply blast
+ using rrewrite.cases apply blast
+ using rrewrite.simps apply blast
+ using rrewrite.cases apply blast
+ apply(case_tac "bsimp r1 = AZERO")
+ apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+ apply(simp)
+ apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ apply(auto)[1]
+ prefer 2
+ apply (smt (verit, best) arexp.distinct(25) arexp.inject(3) bsimp_ASEQ1 rrewrite.simps)
+ defer
+ oops
+
+lemma bsimp_idem:
+ shows "bsimp (bsimp r) = bsimp r"
+ apply(induct r rule: bsimp.induct)
+ apply(auto)
+ using bsimp_ASEQ_idem apply presburger
+ oops
export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers