--- a/thys2/SizeBound.thy Tue Dec 14 16:32:33 2021 +0000
+++ b/thys2/SizeBound.thy Fri Jan 07 22:25:26 2022 +0000
@@ -238,6 +238,12 @@
apply(simp_all)
done
+lemma bnullable_fuse:
+ shows "bnullable (fuse bs r) = bnullable r"
+ apply(induct r arbitrary: bs)
+ apply(auto)
+ done
+
lemma retrieve_encode_STARS:
assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
@@ -691,7 +697,6 @@
shows "bnullable (bders_simp r s) = bnullable (bders r s)"
by (metis L_bders_simp bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
-
lemma qq1:
assumes "\<exists>r \<in> set rs. bnullable r"
shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs rs)"
@@ -710,6 +715,17 @@
apply(simp)
by (metis append_assoc in_set_conv_decomp r1 r2)
+lemma qq3:
+ assumes "bnullable (AALTs bs (rs @ rs1))"
+ "bnullable (AALTs bs (rs @ rs2))"
+ "\<lbrakk>bnullable (AALTs bs rs1); bnullable (AALTs bs rs2); \<forall>r\<in>set rs. \<not>bnullable r\<rbrakk> \<Longrightarrow>
+ bmkeps (AALTs bs rs1) = bmkeps (AALTs bs rs2)"
+ shows "bmkeps (AALTs bs (rs @ rs1)) = bmkeps (AALTs bs (rs @ rs2))"
+ using assms
+ apply(case_tac "\<exists>r \<in> set rs. bnullable r")
+ using qq1 apply auto[1]
+ by (metis UnE bnullable.simps(4) qq2 set_append)
+
lemma flts_append:
shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -739,10 +755,6 @@
-
-
-
-
fun nonazero :: "arexp \<Rightarrow> bool"
where
"nonazero AZERO = False"
@@ -850,17 +862,15 @@
apply(simp)
using qq4 r1 r2 by auto
-
-
-
lemma bder_fuse:
shows "bder c (fuse bs a) = fuse bs (bder c a)"
apply(induct a arbitrary: bs c)
apply(simp_all)
done
-inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
- where
+inductive
+ rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+where
"ASEQ bs AZERO r2 \<leadsto> AZERO"
| "ASEQ bs r1 AZERO \<leadsto> AZERO"
| "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r"
@@ -880,17 +890,21 @@
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
-inductive rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
- where
-rs1[intro, simp]:"r \<leadsto>* r"
+inductive
+ rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+where
+ rs1[intro, simp]:"r \<leadsto>* r"
| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
-inductive srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
- where
-ss1: "[] s\<leadsto>* []"
-|ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
-(*rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
-[r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
+inductive
+ srewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ s\<leadsto>* _" [100, 100] 100)
+where
+ ss1: "[] s\<leadsto>* []"
+| ss2: "\<lbrakk>r \<leadsto>* r'; rs s\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) s\<leadsto>* (r'#rs')"
+
+(*
+rs1 = [r1, r2, ..., rn] rs2 = [r1', r2', ..., rn']
+ [r1, r2, ..., rn] \<leadsto>* [r1', r2, ..., rn] \<leadsto>* [...r2',...] \<leadsto>* [r1', r2',... rn']
*)
@@ -898,12 +912,12 @@
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
using rrewrites.intros(1) rrewrites.intros(2) by blast
-lemma real_trans [trans]:
+lemma real_trans[trans]:
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
shows "r1 \<leadsto>* r3"
using a2 a1
apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct)
- apply(auto)
+ apply(auto)
done
@@ -978,7 +992,8 @@
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
by (simp_all)
-lemma trivialbsimpsrewrites: "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
+lemma trivialbsimpsrewrites:
+ "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
apply(induction rs)
apply simp
@@ -986,7 +1001,8 @@
by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
-lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
+lemma bsimp_AALTsrewrites:
+ "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
apply(induction rs)
apply simp
apply(rule r_in_rstar)
@@ -1000,12 +1016,14 @@
apply(simp)
done
-inductive frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
- where
-fs1: "[] f\<leadsto>* []"
-|fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
-|fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
-|fs4: "\<lbrakk>rs f\<leadsto>* rs';nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
+(* rewrites for lists *)
+inductive
+ frewrites:: "arexp list \<Rightarrow> arexp list \<Rightarrow> bool" (" _ f\<leadsto>* _" [100, 100] 100)
+where
+ fs1: "[] f\<leadsto>* []"
+| fs2: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (AZERO#rs) f\<leadsto>* rs'"
+| fs3: "\<lbrakk>rs f\<leadsto>* rs'\<rbrakk> \<Longrightarrow> ((AALTs bs rs1) # rs) f\<leadsto>* ((map (fuse bs) rs1) @ rs')"
+| fs4: "\<lbrakk>rs f\<leadsto>* rs'; nonalt r; nonazero r\<rbrakk> \<Longrightarrow> (r#rs) f\<leadsto>* (r#rs')"
@@ -1105,7 +1123,8 @@
apply auto
by (metis split_list)
-lemma alts_dBrewrites_withFront: " AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
+lemma alts_dBrewrites_withFront:
+ "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))"
apply(induction rs arbitrary: rsa)
apply simp
apply(drule_tac x = "rsa@[a]" in meta_spec)
@@ -1154,16 +1173,13 @@
using alts_dBrewrites_withFront
by (metis append_Nil dB_single_step empty_set image_empty)
-
-
-
-
-
lemma bsimp_rewrite:
shows "r \<leadsto>* bsimp r"
- apply(induction r rule: bsimp.induct)
- apply simp
- apply(case_tac "bsimp r1 = AZERO")
+proof (induction r rule: bsimp.induct)
+ case (1 bs1 r1 r2)
+ then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)"
+ apply(simp)
+ apply(case_tac "bsimp r1 = AZERO")
apply simp
using continuous_rewrite apply blast
apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
@@ -1172,37 +1188,28 @@
apply(subst bsimp_ASEQ2)
apply (meson real_trans rrewrite.intros(3) rrewrites.intros(2) star_seq star_seq2)
apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 real_trans rrewrite.intros(2) rs2 star_seq star_seq2)
- defer
- using bsimp_aalts_simpcases(2) apply blast
- apply simp
- apply simp
- apply simp
-
- apply auto
-
-
- apply(subgoal_tac "AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)")
- apply(subgoal_tac "AALTs bs1 (map bsimp rs) \<leadsto>* AALTs bs1 (flts (map bsimp rs))")
- apply(subgoal_tac "AALTs bs1 (flts (map bsimp rs)) \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})")
- apply(subgoal_tac "AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {} )")
-
-
- apply (meson real_trans)
-
- apply (meson bsimp_AALTsrewrites)
-
- apply (meson alts_dBrewrites)
-
- using fltsrewrites apply auto[1]
-
- using alts_simpalts by force
-
-
-lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
- apply(induction r1 r2 rule: rrewrite.induct)
- apply auto
- apply (metis bnullable_correctness erase_fuse)+
done
+next
+ case (2 bs1 rs)
+ then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)"
+ by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTsrewrites fltsrewrites real_trans)
+next
+ case "3_1"
+ then show "AZERO \<leadsto>* bsimp AZERO"
+ by simp
+next
+ case ("3_2" v)
+ then show "AONE v \<leadsto>* bsimp (AONE v)"
+ by simp
+next
+ case ("3_3" v va)
+ then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)"
+ by simp
+next
+ case ("3_4" v va)
+ then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)"
+ by simp
+qed
lemma rewrite_non_nullable_strong:
assumes "r1 \<leadsto> r2"
@@ -1229,41 +1236,16 @@
apply simp
using rewrite_non_nullable_strong by blast
-lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow>
-\<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) "
- apply simp
- apply blast
- done
-
-
-lemma nomember_bnullable: "\<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk>
- \<Longrightarrow> \<not>bnullable (AALTs bs (rs1 @ [r] @ rs2))"
- using bnullable.simps(4) nonbnullable_lists_concat by presburger
-
-lemma bnullable_segment: " bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
- apply(case_tac "\<exists>r0\<in>set rs1. bnullable r0")
- using r2 apply blast
- apply(case_tac "bnullable r")
-
- apply blast
- apply(case_tac "\<exists>r0\<in>set rs2. bnullable r0")
-
- using bnullable.simps(4) apply presburger
- apply(subgoal_tac "False")
-
- apply blast
-
- using nomember_bnullable by blast
-
-
+lemma bnullable_segment:
+ "bnullable (AALTs bs (rs1@[r]@rs2)) \<Longrightarrow> bnullable (AALTs bs rs1) \<or> bnullable (AALTs bs rs2) \<or> bnullable r"
+ by auto
lemma bnullablewhichbmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk>
\<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
+
using qq2 bnullable_Hdbmkeps_Hd by force
-
-
lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
\<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))"
apply(subst bnullable_Hdbmkeps_Hd)
@@ -1271,102 +1253,84 @@
apply simp
by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3)
-lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
-bnullable (AALTs bs rs3)"
-
- by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable)
+lemma third_segment_bnullable:
+ "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
+ bnullable (AALTs bs rs3)"
+ apply(auto)
+ done
+lemma third_segment_bmkeps:
+ "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
+ bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
+ by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTsrewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
-lemma third_segment_bmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
-bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)"
- apply(subgoal_tac "bnullable (AALTs bs rs3)")
- apply(subgoal_tac "\<forall>r \<in> set (rs1@rs2). \<not>bnullable r")
- apply(subgoal_tac "bmkeps (AALTs bs (rs1@rs2@rs3)) = bmkeps (AALTs bs ((rs1@rs2)@rs3) )")
- apply (metis bnullable.simps(4) qq2)
-
- apply (metis append.assoc)
-
- apply (metis append.assoc in_set_conv_decomp r2 third_segment_bnullable)
-
- using third_segment_bnullable by blast
-
+lemma rewrite_bmkepsalt:
+ "\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
+ \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+ apply(rule qq3)
+ apply(simp)
+ apply(simp)
+ apply(case_tac "bnullable (AALTs bs1 rs1)")
+ using spillbmkepslistr apply blast
+ apply(subst qq2)
+ apply(auto simp add: bnullable_fuse r1)
+ done
-lemma rewrite_bmkepsalt: " \<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
- \<Longrightarrow> bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
- apply(case_tac "bnullable (AALTs bs rsa)")
-
- using qq1 apply force
- apply(case_tac "bnullable (AALTs bs1 rs1)")
- apply(subst qq2)
-
-
- using r2 apply blast
-
- apply (metis list.set_intros(1))
- apply (metis append_Nil bnullable.simps(1) rewrite_non_nullable_strong rrewrite.intros(10) spillbmkepslistr third_segment_bmkeps)
- apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ")
- prefer 2
-
- apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps)
- by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps)
-
+lemma rewrite_bmkeps_aux:
+ assumes "r1 \<leadsto> r2" "bnullable r1" "bnullable r2"
+ shows "bmkeps r1 = bmkeps r2"
+ using assms
+proof (induction r1 r2 rule: rrewrite.induct)
+ case (1 bs r2)
+ then show ?case by simp
+next
+ case (2 bs r1)
+ then show ?case by simp
+next
+ case (3 bs bs1 r)
+ then show ?case by (simp add: b2)
+next
+ case (4 r1 r2 bs r3)
+ then show ?case by simp
+next
+ case (5 r3 r4 bs r1)
+ then show ?case by simp
+next
+ case (6 r r' bs rs1 rs2)
+ then show ?case
+ by (metis append_Cons append_Nil bnullable.simps(4) bnullable_segment bnullablewhichbmkeps qq3 r1 rewrite_non_nullable_strong)
+next
+ case (7 bs rsa rsb)
+ then show ?case
+ by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(10) rrewrite0away third_segment_bmkeps)
+next
+ case (8 bs rsa bs1 rs1 rsb)
+ then show ?case
+ by (simp add: rewrite_bmkepsalt)
+next
+ case (9 bs bs1 rs)
+ then show ?case
+ by (simp add: q3a)
+next
+ case (10 bs)
+ then show ?case
+ by fastforce
+next
+ case (11 bs r)
+ then show ?case
+ by (simp add: b2)
+next
+ case (12 a1 a2 bs rsa rsb rsc)
+ then show ?case
+ by (smt (verit, ccfv_threshold) append_Cons append_eq_appendI append_self_conv2 bnullable_correctness list.set_intros(1) qq3 r1)
+qed
-lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; bnullable r1\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
-
- apply(frule rewrite_nullable)
- apply simp
- apply(induction r1 r2 rule: rrewrite.induct)
- apply simp
- using bnullable.simps(1) bnullable.simps(5) apply blast
- apply (simp add: b2)
- apply simp
- apply simp
- apply(frule bnullable_segment)
- apply(case_tac "bnullable (AALTs bs rs1)")
- using qq1 apply force
- apply(case_tac "bnullable r")
- using bnullablewhichbmkeps rewrite_nullable apply presburger
- apply(subgoal_tac "bnullable (AALTs bs rs2)")
- apply(subgoal_tac "\<not> bnullable r'")
- apply (simp add: qq2 r1)
+lemma rewrite_bmkeps:
+ assumes "r1 \<leadsto> r2" "bnullable r1"
+ shows "bmkeps r1 = bmkeps r2"
+ using assms(1) assms(2) rewrite_bmkeps_aux rewrite_nullable by blast
- using rewrite_non_nullable apply blast
-
- apply blast
- apply (simp add: flts_append qs3)
- apply (simp add: rewrite_bmkepsalt)
- using q3a apply force
-
- apply (simp add: q3a)
- apply (simp add: b2)
- apply(simp del: append.simps)
- apply(case_tac "bnullable a1")
- apply (metis append.assoc in_set_conv_decomp qq1)
- apply(case_tac "\<exists>r \<in> set rsa. bnullable r")
- using qq1 apply presburger
- apply(case_tac "\<exists>r \<in> set rsb. bnullable r")
- apply (metis UnCI append.assoc qq1 set_append)
- apply(case_tac "bnullable a2")
- apply (metis bnullable_correctness)
- apply(subst qq2)
- apply blast
- apply(auto)[1]
- apply(subst qq2)
- apply (metis empty_iff list.set(1) set_ConsD)
- apply(auto)[1]
- apply(subst qq2)
- apply(auto)[2]
- apply(subst qq2)
- apply(auto)[2]
- apply(subst qq2)
- apply(auto)[2]
- apply(subst qq2)
- apply(auto)[2]
- apply(subst qq2)
- apply(auto)[2]
- apply(simp)
- done
lemma rewrites_bmkeps:
assumes "r1 \<leadsto>* r2" "bnullable r1"
@@ -1389,50 +1353,68 @@
lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)"
by (metis append_Cons append_Nil rrewrite.intros(6))
-lemma alt_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALT bs r r2 \<leadsto> AALT bs r' r2"
- using alts_rewrite_front by blast
-
lemma to_zero_in_alt: " AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
by (simp add: alts_rewrite_front rrewrite.intros(1))
-lemma alt_remove0_front: " AALT bs AZERO r \<leadsto> AALTs bs [r]"
- by (simp add: rrewrite0away)
-
-lemma alt_rewrites_back: "r2 \<leadsto>* r2' \<Longrightarrow>AALT bs r1 r2 \<leadsto>* AALT bs r1 r2'"
- apply(induction r2 r2' arbitrary: bs rule: rrewrites.induct)
- apply simp
- by (meson rs1 rs2 srewrites_alt1 ss1 ss2)
-
-lemma rewrite_fuse: " r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto>* fuse bs r3"
- apply(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
- apply auto
-
- apply (simp add: continuous_rewrite)
-
- apply (simp add: r_in_rstar rrewrite.intros(2))
-
- apply (metis fuse_append r_in_rstar rrewrite.intros(3))
-
- using r_in_rstar star_seq apply blast
-
- using r_in_rstar star_seq2 apply blast
-
- using contextrewrites2 r_in_rstar apply auto[1]
-
- using rrewrite.intros(8) apply auto[1]
- using rrewrite.intros(7) apply auto[1]
- using rrewrite.intros(8) apply force
- apply (metis append_assoc r_in_rstar rrewrite.intros(9))
- apply (simp add: r_in_rstar rrewrite.intros(10))
- apply (metis fuse_append r_in_rstar rrewrite.intros(11))
- using rrewrite.intros(12) by auto
-
+lemma rewrite_fuse:
+ assumes "r2 \<leadsto> r3"
+ shows "fuse bs r2 \<leadsto>* fuse bs r3"
+ using assms
+proof(induction r2 r3 arbitrary: bs rule: rrewrite.induct)
+ case (1 bs r2)
+ then show ?case
+ by (simp add: continuous_rewrite)
+next
+ case (2 bs r1)
+ then show ?case
+ using rrewrite.intros(2) by force
+next
+ case (3 bs bs1 r)
+ then show ?case
+ by (metis fuse.simps(5) fuse_append r_in_rstar rrewrite.intros(3))
+next
+ case (4 r1 r2 bs r3)
+ then show ?case
+ by (simp add: r_in_rstar star_seq)
+next
+ case (5 r3 r4 bs r1)
+ then show ?case
+ using fuse.simps(5) r_in_rstar star_seq2 by auto
+next
+ case (6 r r' bs rs1 rs2)
+ then show ?case
+ using contextrewrites2 r_in_rstar by force
+next
+ case (7 bs rsa rsb)
+ then show ?case
+ using rrewrite.intros(7) by force
+next
+ case (8 bs rsa bs1 rs1 rsb)
+ then show ?case
+ using rrewrite.intros(8) by force
+next
+ case (9 bs bs1 rs)
+ then show ?case
+ by (metis append.assoc fuse.simps(4) r_in_rstar rrewrite.intros(9))
+next
+ case (10 bs)
+ then show ?case
+ by (simp add: r_in_rstar rrewrite.intros(10))
+next
+ case (11 bs r)
+ then show ?case
+ by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11))
+next
+ case (12 a1 a2 bs rsa rsb rsc)
+ then show ?case
+ using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto
+qed
lemma rewrites_fuse:
- assumes "r2 \<leadsto>* r2'"
- shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
+ assumes "r1 \<leadsto>* r2"
+ shows "fuse bs r1 \<leadsto>* fuse bs r2"
using assms
-apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
+apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct)
apply(auto intro: rewrite_fuse real_trans)
done
@@ -1443,7 +1425,8 @@
done
-lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+lemma rewrite_der_altmiddle:
+ "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
apply simp
apply(simp add: bder_fuse_list del: append.simps)
by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend)
@@ -1456,63 +1439,72 @@
using rrewrite.intros(12) by auto
-lemma rewrite_after_der: "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
- apply(induction r1 r2 arbitrary: c rule: rrewrite.induct)
-
- apply (simp add: r_in_rstar rrewrite.intros(1))
- apply simp
-
- apply (meson contextrewrites1 r_in_rstar rrewrite.intros(10) rrewrite.intros(2) rrewrite0away rs2)
- apply(simp)
- apply(rule many_steps_later)
- apply(rule to_zero_in_alt)
- apply(rule many_steps_later)
- apply(rule alt_remove0_front)
- apply(rule many_steps_later)
- apply(rule rrewrite.intros(11))
- using bder_fuse fuse_append rs1 apply presburger
- apply(case_tac "bnullable r1")
- prefer 2
- apply(subgoal_tac "\<not>bnullable r2")
- prefer 2
- using rewrite_non_nullable apply presburger
- apply simp+
-
- using star_seq apply auto[1]
- apply(subgoal_tac "bnullable r2")
- apply simp+
- apply(subgoal_tac "bmkeps r1 = bmkeps r2")
- prefer 2
- using rewrite_bmkeps apply auto[1]
- using contextrewrites1 star_seq apply auto[1]
- using rewrite_nullable apply auto[1]
- apply(case_tac "bnullable r1")
- apply simp
- apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4")
- prefer 2
- using rrewrite.intros(5) apply blast
- apply(rule many_steps_later)
- apply(rule alt_rewrite_front)
- apply assumption
- apply (meson alt_rewrites_back rewrites_fuse)
-
- apply (simp add: r_in_rstar rrewrite.intros(5))
-
- using contextrewrites2 apply force
-
- using rrewrite.intros(7) apply force
-
- using rewrite_der_altmiddle apply auto[1]
-
- apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9))
- apply (simp add: r_in_rstar rrewrite.intros(10))
-
- apply (simp add: r_in_rstar rrewrite.intros(10))
- using bder_fuse r_in_rstar rrewrite.intros(11) apply presburger
-
-
- using lock_step_der_removal by auto
-
+lemma rewrite_after_der:
+ assumes "r1 \<leadsto> r2"
+ shows "(bder c r1) \<leadsto>* (bder c r2)"
+ using assms
+proof(induction r1 r2 rule: rrewrite.induct)
+ case (1 bs r2)
+ then show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO"
+ by (simp add: continuous_rewrite)
+next
+ case (2 bs r1)
+ then show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO"
+ apply(simp)
+ by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(10) rrewrite.intros(2) rrewrite0away)
+next
+ case (3 bs bs1 r)
+ then show "bder c (ASEQ bs (AONE bs1) r) \<leadsto>* bder c (fuse (bs @ bs1) r)"
+ apply(simp)
+ by (metis bder_fuse fuse_append rrewrite.intros(11) rrewrite0away rrewrites.simps to_zero_in_alt)
+next
+ case (4 r1 r2 bs r3)
+ have as: "r1 \<leadsto> r2" by fact
+ have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+ from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
+ by (simp add: contextrewrites1 rewrite_bmkeps rewrite_non_nullable_strong star_seq)
+next
+ case (5 r3 r4 bs r1)
+ have as: "r3 \<leadsto> r4" by fact
+ have IH: "bder c r3 \<leadsto>* bder c r4" by fact
+ from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
+ apply(simp)
+ using r_in_rstar rewrites_fuse srewrites_alt1 ss1 ss2 star_seq2 by presburger
+next
+ case (6 r r' bs rs1 rs2)
+ have as: "r \<leadsto> r'" by fact
+ have IH: "bder c r \<leadsto>* bder c r'" by fact
+ from as IH show "bder c (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto>* bder c (AALTs bs (rs1 @ [r'] @ rs2))"
+ apply(simp)
+ using contextrewrites2 by force
+next
+ case (7 bs rsa rsb)
+ then show "bder c (AALTs bs (rsa @ [AZERO] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ rsb))"
+ apply(simp)
+ using rrewrite.intros(7) by auto
+next
+ case (8 bs rsa bs1 rs1 rsb)
+ then show
+ "bder c (AALTs bs (rsa @ [AALTs bs1 rs1] @ rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))"
+ using rewrite_der_altmiddle by auto
+next
+ case (9 bs bs1 rs)
+ then show "bder c (AALTs (bs @ bs1) rs) \<leadsto>* bder c (AALTs bs (map (fuse bs1) rs))"
+ by (metis bder.simps(4) bder_fuse_list list.map_comp r_in_rstar rrewrite.intros(9))
+next
+ case (10 bs)
+ then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
+ by (simp add: r_in_rstar rrewrite.intros(10))
+next
+ case (11 bs r)
+ then show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)"
+ by (simp add: bder_fuse r_in_rstar rrewrite.intros(11))
+next
+ case (12 a1 a2 bs rsa rsb rsc)
+ have as: "erase a1 = erase a2" by fact
+ then show "bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
+ using lock_step_der_removal by force
+qed
lemma rewrites_after_der:
@@ -1523,6 +1515,7 @@
apply(simp_all add: rewrite_after_der real_trans)
done
+
lemma central:
shows "bders r s \<leadsto>* bders_simp r s"
proof(induct s arbitrary: r rule: rev_induct)
@@ -1540,20 +1533,27 @@
by (simp add: bders_simp_append)
qed
-
lemma quasi_main:
assumes "bnullable (bders r s)"
shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
- using assms central rewrites_bmkeps by blast
+ using assms central rewrites_bmkeps
+proof -
+ have "bders r s \<leadsto>* bders_simp r s" by (rule central)
+ then
+ show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms
+ by (rule rewrites_bmkeps)
+qed
+
theorem main_main:
shows "blexer r s = blexer_simp r s"
- by (simp add: b4 blexer_def blexer_simp_def quasi_main)
+ unfolding blexer_def blexer_simp_def
+ using b4 quasi_main by simp
theorem blexersimp_correctness:
shows "lexer r s = blexer_simp r s"
- using blexer_correctness main_main by auto
+ using blexer_correctness main_main by simp