--- a/thys2/SizeBound.thy Tue Nov 02 19:42:52 2021 +0000
+++ b/thys2/SizeBound.thy Thu Nov 04 01:07:34 2021 +0000
@@ -766,18 +766,9 @@
| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
| "nonnested r = True"
-
-lemma k0:
- shows "flts (r # rs1) = flts [r] @ flts rs1"
- apply(induct r arbitrary: rs1)
- apply(auto)
- done
-
-lemma k00:
- shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
- apply(induct rs1 arbitrary: rs2)
- apply(auto)
- by (metis append.assoc k0)
+lemma flts_append:
+ shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+by (induct xs1 arbitrary: xs2 rule: flts.induct)(auto)
lemma k0a:
shows "flts [AALTs bs rs] = map (fuse bs) rs"
@@ -785,12 +776,6 @@
done
-
-
-
-
-
-
lemma bsimp_AALTs_qq:
assumes "1 < length rs"
shows "bsimp_AALTs bs rs = AALTs bs rs"
@@ -811,17 +796,7 @@
-lemma flts_append:
- "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
- apply(induct xs1 arbitrary: xs2 rule: rev_induct)
- apply(auto)
- apply(case_tac xs)
- apply(auto)
- apply(case_tac x)
- apply(auto)
- apply(case_tac x)
- apply(auto)
- done
+
fun nonazero :: "arexp \<Rightarrow> bool"
where
@@ -940,38 +915,6 @@
done
-fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
- where
- "flts2 _ [] = []"
-| "flts2 c (AZERO # rs) = flts2 c rs"
-| "flts2 c (AONE _ # rs) = flts2 c rs"
-| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
-| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
-| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then
- flts2 c rs
- else ASEQ bs r1 r2 # flts2 c rs)"
-| "flts2 c (r1 # rs) = r1 # flts2 c rs"
-
-
-
-
-
-
-
-
-
-
-
-
-
-lemma WQ1:
- assumes "s \<in> L (der c r)"
- shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
- using assms
- oops
-
-
-
lemma bder_bsimp_AALTs:
shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
apply(induct bs rs rule: bsimp_AALTs.induct)
@@ -983,20 +926,6 @@
-lemma
- assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
- shows "bsimp a = a"
- using assms
- apply(simp)
- oops
-
-
-
-
-
-
-
-
inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
where
"ASEQ bs AZERO r2 \<leadsto> AZERO"
@@ -1036,7 +965,7 @@
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
using rrewrites.intros(1) rrewrites.intros(2) by blast
-lemma real_trans:
+lemma real_trans [trans]:
assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
shows "r1 \<leadsto>* r3"
using a2 a1
@@ -1146,7 +1075,7 @@
lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
- by (metis append_Cons append_Nil flts_single1 k00)
+ by (metis append_Cons append_Nil flts_single1 flts_append)
lemma fltsfrewrites: "rs f\<leadsto>* (flts rs)"
apply(induction rs)
@@ -1221,7 +1150,7 @@
apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)")
apply (metis append_Nil frewritesaalts)
apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
- by (metis append_Cons append_Nil fltsfrewrites frewritesaalts k00 k0a)
+ by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a)
lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow>
AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
@@ -1345,38 +1274,36 @@
using alts_simpalts by force
-lemma rewritenullable: "\<lbrakk>r1 \<leadsto> r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2"
- apply(induction r1 r2 rule: rrewrite.induct)
- apply(simp)+
- apply (metis bnullable_correctness erase_fuse)
- apply simp
- apply simp
- apply auto[1]
- apply auto[1]
- apply auto[4]
- apply (metis UnCI bnullable_correctness erase_fuse imageI)
- apply (metis bnullable_correctness erase_fuse)
- apply (metis bnullable_correctness erase_fuse)
-
- apply (metis bnullable_correctness erase.simps(5) erase_fuse)
-
-
- by (smt (z3) Un_iff bnullable_correctness insert_iff list.set(2) qq3 set_append)
-
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
+lemma rewrite_non_nullable_strong:
+ assumes "r1 \<leadsto> r2"
+ shows "bnullable r1 = bnullable r2"
+using assms
+apply(induction r1 r2 rule: rrewrite.induct)
+apply(auto)
+apply(metis bnullable_correctness erase_fuse)+
+apply(metis UnCI bnullable_correctness erase_fuse imageI)
+apply(metis bnullable_correctness erase_fuse)+
+done
-lemma rewritesnullable: "\<lbrakk> r1 \<leadsto>* r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2"
+lemma rewrite_nullable:
+ assumes "r1 \<leadsto> r2" "bnullable r1"
+ shows "bnullable r2"
+using assms rewrite_non_nullable_strong
+by auto
+
+lemma rewritesnullable:
+ assumes "r1 \<leadsto>* r2" "bnullable r1"
+ shows "bnullable r2"
+using assms
apply(induction r1 r2 rule: rrewrites.induct)
- apply simp
- apply(rule rewritenullable)
- apply simp
apply simp
- done
+ 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 ) "
@@ -1412,30 +1339,6 @@
\<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)"
using qq2 bnullable_Hdbmkeps_Hd by force
-lemma rrewrite_nbnullable: "\<lbrakk> r1 \<leadsto> r2 ; \<not> bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2"
- apply(induction rule: rrewrite.induct)
- apply auto[1]
- apply auto[1]
- apply auto[1]
- apply (metis bnullable_correctness erase_fuse)
- apply auto[1]
- apply auto[1]
- apply auto[1]
- apply auto[1]
- apply auto[1]
- apply (metis bnullable_correctness erase_fuse)
- apply auto[1]
- apply (metis bnullable_correctness erase_fuse)
- apply auto[1]
- apply (metis bnullable_correctness erase_fuse)
- apply auto[1]
- apply auto[1]
-
- apply (metis bnullable_correctness erase_fuse)
-
- by (meson rewrite_non_nullable rrewrite.intros(13))
-
-
lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1)
@@ -1448,7 +1351,7 @@
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) rrewrite_nbnullable)
+ by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable)
lemma third_segment_bmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow>
@@ -1477,22 +1380,22 @@
using r2 apply blast
apply (metis list.set_intros(1))
- apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewritenullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
+ apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
thm qq1
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 rewritenullable rrewrite.intros(11) third_segment_bmkeps)
-
+ apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(11) third_segment_bmkeps)
+
by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps)
lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
- apply(frule rewritenullable)
+ apply(frule rewrite_nullable)
apply simp
apply(induction r1 r2 rule: rrewrite.induct)
apply simp
@@ -1504,12 +1407,12 @@
apply(case_tac "bnullable (AALTs bs rs1)")
using qq1 apply force
apply(case_tac "bnullable r")
- using bnullablewhichbmkeps rewritenullable apply presburger
+ using bnullablewhichbmkeps rewrite_nullable apply presburger
apply(subgoal_tac "bnullable (AALTs bs rs2)")
apply(subgoal_tac "\<not> bnullable r'")
apply (simp add: qq2 r1)
- using rrewrite_nbnullable apply blast
+ using rewrite_non_nullable apply blast
apply blast
apply (simp add: flts_append qs3)
@@ -1526,21 +1429,24 @@
by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append)
-
+lemma rewrites_bmkeps:
+ assumes "r1 \<leadsto>* r2" "bnullable r1"
+ shows "bmkeps r1 = bmkeps r2"
+ using assms
+proof(induction r1 r2 rule: rrewrites.induct)
+ case (rs1 r)
+ then show "bmkeps r = bmkeps r" by simp
+next
+ case (rs2 r1 r2 r3)
+ then have IH: "bmkeps r1 = bmkeps r2" by simp
+ have a1: "bnullable r1" by fact
+ have a2: "r1 \<leadsto>* r2" by fact
+ have a3: "r2 \<leadsto> r3" by fact
+ have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable)
+ then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp
+ then show "bmkeps r1 = bmkeps r3" using IH by simp
+qed
-lemma rewrites_bmkeps: "\<lbrakk> (r1 \<leadsto>* r2); (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2"
- apply(induction r1 r2 rule: rrewrites.induct)
- apply simp
- apply(subgoal_tac "bnullable r2")
- prefer 2
- apply(metis rewritesnullable)
- apply(subgoal_tac "bmkeps r1 = bmkeps r2")
- prefer 2
- apply fastforce
- using rewrite_bmkeps by presburger
-
-
-thm rrewrite.intros(12)
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))
@@ -1648,7 +1554,7 @@
prefer 2
using rewrite_bmkeps apply auto[1]
using contextrewrites1 star_seq apply auto[1]
- using rewritenullable 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")
@@ -1680,34 +1586,44 @@
-lemma rewrites_after_der: " r1 \<leadsto>* r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
- apply(induction r1 r2 rule: rrewrites.induct)
- apply(rule rs1)
- by (meson real_trans rewrite_after_der)
-
+lemma rewrites_after_der:
+ assumes "r1 \<leadsto>* r2"
+ shows "bder c r1 \<leadsto>* bder c r2"
+using assms
+apply(induction r1 r2 rule: rrewrites.induct)
+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)
+ case Nil
+ then show "bders r [] \<leadsto>* bders_simp r []" by simp
+next
+ case (snoc x xs)
+ have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact
+ have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
+ also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH
+ by (simp add: rewrites_after_der)
+ also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
+ by (simp add: bsimp_rewrite)
+ finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])"
+ by (simp add: bders_simp_append)
+qed
-lemma central: " (bders r s) \<leadsto>* (bders_simp r s)"
- apply(induct s arbitrary: r rule: rev_induct)
-
- apply simp
- apply(subst bders_append)
- apply(subst bders_simp_append)
- by (metis bders.simps(1) bders.simps(2) bders_simp.simps(1) bders_simp.simps(2) bsimp_rewrite real_trans rewrites_after_der)
+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
-
-
-thm arexp.induct
-
-lemma quasi_main: "bnullable (bders r s) \<Longrightarrow> bmkeps (bders r s) = bmkeps (bders_simp r s)"
- using central rewrites_bmkeps by blast
-
-theorem main_main: "blexer r s = blexer_simp r s"
+theorem main_main:
+ shows "blexer r s = blexer_simp r s"
by (simp add: b4 blexer_def blexer_simp_def quasi_main)
-theorem blexersimp_correctness: "blexer_simp r s= lexer r s"
+theorem blexersimp_correctness:
+ shows "lexer r s = blexer_simp r s"
using blexer_correctness main_main by auto