--- a/thys2/SizeBound.thy Fri Jan 07 22:29:14 2022 +0000
+++ b/thys2/SizeBound.thy Tue Jan 11 23:55:13 2022 +0000
@@ -138,6 +138,14 @@
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"
@@ -737,18 +745,6 @@
done
-lemma bsimp_AALTs_qq:
- assumes "1 < length rs"
- shows "bsimp_AALTs bs rs = AALTs bs rs"
- using assms
- apply(case_tac rs)
- apply(simp)
- apply(case_tac list)
- apply(simp_all)
- done
-
-
-
lemma bbbbs1:
shows "nonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
using nonalt.elims(3) by auto
@@ -868,23 +864,21 @@
apply(simp_all)
done
+
+
+
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"
+| "ASEQ bs1 (AONE bs2) r \<leadsto> fuse (bs1@bs2) r"
| "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3"
| "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4"
| "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
| "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)"
| "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)"
-(*the below rule for extracting common prefixes between a list of rexp's bitcodes*)
-(***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******)
-(*opposite direction also allowed, which means bits are free to be moved around
-as long as they are on the right path*)
-| "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)"
| "AALTs bs [] \<leadsto> AZERO"
| "AALTs bs [r] \<leadsto> fuse bs r"
| "erase a1 = erase a2 \<Longrightarrow> AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> AALTs bs (rsa@[a1]@rsb@rsc)"
@@ -896,17 +890,22 @@
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']
-*)
+(* 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')"
lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
@@ -952,7 +951,6 @@
apply auto
done
-
corollary srewrites_alt1:
assumes "rs1 s\<leadsto>* rs2"
shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
@@ -992,7 +990,8 @@
and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
by (simp_all)
-lemma trivialbsimpsrewrites:
+
+lemma trivialbsimp_srewrites:
"\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)"
apply(induction rs)
@@ -1001,29 +1000,13 @@
by (metis insert_iff list.simps(15) list.simps(9) srewrites.simps)
-lemma bsimp_AALTsrewrites:
+lemma bsimp_AALTs_rewrites:
"AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs"
apply(induction rs)
apply simp
apply(rule r_in_rstar)
- apply (simp add: rrewrite.intros(10))
- apply(case_tac "rs = Nil")
- apply(simp)
- using rrewrite.intros(12) apply auto[1]
- using r_in_rstar rrewrite.intros(11) apply presburger
- apply(subgoal_tac "length (a#rs) > 1")
- apply(simp add: bsimp_AALTs_qq)
- apply(simp)
- done
-
-(* 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')"
+ using rrewrite.intros(9) apply blast
+ by (metis bsimp_AALTs.elims list.discI rrewrite.intros(10) rrewrites.simps)
@@ -1082,7 +1065,7 @@
apply auto
done
-lemma fltsrewrites: " AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
+lemma flts_rewrites: " AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)"
apply(induction rs)
apply simp
apply(case_tac "a = AZERO")
@@ -1103,13 +1086,40 @@
apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3))
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)"
- apply(subgoal_tac " rs s\<leadsto>* (map bsimp rs)")
- prefer 2
- using trivialbsimpsrewrites apply auto[1]
- using srewrites_alt1 by auto
+(* TEST *)
+lemma r:
+ assumes "AALTs bs rs1 \<leadsto> AALTs bs rs2"
+ shows "AALTs bs (x # rs1) \<leadsto>* AALTs bs (x # rs2)"
+ using assms
+ apply(erule_tac rrewrite.cases)
+ apply(auto)
+ apply (metis append_Cons append_Nil rrewrite.intros(6) r_in_rstar)
+ apply (metis append_Cons append_self_conv2 rrewrite.intros(7) r_in_rstar)
+ apply (metis Cons_eq_appendI append_eq_append_conv2 rrewrite.intros(8) self_append_conv r_in_rstar)
+ apply(case_tac rs2)
+ apply(auto)
+ apply(case_tac r)
+ apply(auto)
+ apply (metis append_Nil2 append_butlast_last_id butlast.simps(2) last.simps list.distinct(1) list.map_disc_iff r_in_rstar rrewrite.intros(8))
+ apply(case_tac r)
+ apply(auto)
+ defer
+ apply(rule r_in_rstar)
+ apply (metis append_Cons append_Nil rrewrite.intros(11))
+ apply(rule real_trans)
+ apply(rule r_in_rstar)
+ using rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified]
+ apply(rule_tac rrewrite.intros(8)[where ?rsb = "[]", of "bs" "[x]" "[]" , simplified])
+ apply(simp add: map_fuse_Nil fuse_Nil)
+ done
+lemma alts_simpalts:
+ "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow>
+ AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)"
+ apply(induct rs)
+ apply(auto)[1]
+ using trivialbsimp_srewrites apply auto[1]
+ by (simp add: srewrites_alt1 ss2)
lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb"
apply auto
@@ -1149,7 +1159,7 @@
(erase `
(set rs1 \<union> set rs2)))) ")
prefer 2
- using rrewrite.intros(12) apply force
+ using rrewrite.intros(11) apply force
using r_in_rstar apply force
apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)")
prefer 2
@@ -1161,7 +1171,7 @@
apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto>
AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))")
apply force
- apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(12) same_append_eq somewhereMapInside)
+ apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(11) same_append_eq somewhereMapInside)
by force
@@ -1192,7 +1202,7 @@
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)
+ by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites real_trans)
next
case "3_1"
then show "AZERO \<leadsto>* bsimp AZERO"
@@ -1262,7 +1272,7 @@
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)
+ by (metis bnullable.simps(1) bnullable.simps(4) bsimp_AALTs.simps(1) bsimp_AALTs_rewrites qq2 rewritesnullable self_append_conv third_segment_bnullable)
lemma rewrite_bmkepsalt:
"\<lbrakk>bnullable (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)); bnullable (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))\<rbrakk>
@@ -1302,25 +1312,21 @@
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)
+ by (metis bnullable.simps(1) bnullable.simps(4) bnullable_segment qq1 qq2 rewrite_nullable rrewrite.intros(9) 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)
+ case (9 bs)
then show ?case
by fastforce
next
- case (11 bs r)
+ case (10 bs r)
then show ?case
by (simp add: b2)
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 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
@@ -1393,21 +1399,17 @@
then show ?case
using rrewrite.intros(8) by force
next
- case (9 bs bs1 rs)
+ case (9 bs)
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))
+ by (simp add: r_in_rstar rrewrite.intros(9))
next
- case (11 bs r)
+ case (10 bs r)
then show ?case
- by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(11))
+ by (metis fuse.simps(4) fuse_append r_in_rstar rrewrite.intros(10))
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 a1 a2 bs rsa rsb rsc)
then show ?case
- using fuse.simps(4) r_in_rstar rrewrite.intros(12) by auto
+ using fuse.simps(4) r_in_rstar rrewrite.intros(11) by auto
qed
lemma rewrites_fuse:
@@ -1437,7 +1439,7 @@
bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))"
apply(simp)
- using rrewrite.intros(12) by auto
+ using rrewrite.intros(11) by auto
lemma rewrite_after_der:
assumes "r1 \<leadsto> r2"
@@ -1451,12 +1453,12 @@
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)
+ by (meson contextrewrites1 r_in_rstar real_trans rrewrite.intros(9) 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)
+ by (metis bder_fuse fuse_append rrewrite.intros(10) rrewrite0away rrewrites.simps to_zero_in_alt)
next
case (4 r1 r2 bs r3)
have as: "r1 \<leadsto> r2" by fact
@@ -1467,9 +1469,8 @@
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
+ from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)"
+ using bder.simps(5) 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
@@ -1488,19 +1489,15 @@
"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)
+ case (9 bs)
then show "bder c (AALTs bs []) \<leadsto>* bder c AZERO"
- by (simp add: r_in_rstar rrewrite.intros(10))
+ by (simp add: r_in_rstar rrewrite.intros(9))
next
- case (11 bs r)
+ case (10 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))
+ by (simp add: bder_fuse r_in_rstar rrewrite.intros(10))
next
- case (12 a1 a2 bs rsa rsb rsc)
+ case (11 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
@@ -1533,10 +1530,13 @@
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
proof -
have "bders r s \<leadsto>* bders_simp r s" by (rule central)
then
@@ -1545,6 +1545,8 @@
qed
+
+
theorem main_main:
shows "blexer r s = blexer_simp r s"
unfolding blexer_def blexer_simp_def