--- a/thys2/SizeBound.thy Thu Nov 04 01:07:34 2021 +0000
+++ b/thys2/SizeBound.thy Thu Nov 04 09:45:41 2021 +0000
@@ -118,30 +118,12 @@
| "erase (ASTAR _ r) = STAR (erase r)"
-
-
fun nonalt :: "arexp \<Rightarrow> bool"
where
"nonalt (AALTs bs2 rs) = False"
| "nonalt r = True"
-fun good :: "arexp \<Rightarrow> bool" where
- "good AZERO = False"
-| "good (AONE cs) = True"
-| "good (ACHAR cs c) = True"
-| "good (AALTs cs []) = False"
-| "good (AALTs cs [r]) = False"
-| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
-| "good (ASEQ _ AZERO _) = False"
-| "good (ASEQ _ (AONE _) _) = False"
-| "good (ASEQ _ _ AZERO) = False"
-| "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
-| "good (ASTAR cs r) = True"
-
-
-
-
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
"fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)"
@@ -238,8 +220,6 @@
apply(simp_all)
done
-thm Posix.induct
-
lemma erase_intern [simp]:
shows "erase (intern r) = r"
apply(induct r)
@@ -551,8 +531,9 @@
(if (f x) \<in> acc then distinctBy xs f acc
else x # (distinctBy xs f ({f x} \<union> acc)))"
-
-
+lemma dB_single_step:
+ shows "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
+ by simp
fun flts :: "arexp list \<Rightarrow> arexp list"
where
@@ -563,16 +544,6 @@
-
-fun li :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp"
- where
- "li _ [] = AZERO"
-| "li bs [a] = fuse bs a"
-| "li bs as = AALTs bs as"
-
-
-
-
fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
where
"bsimp_ASEQ _ AZERO _ = AZERO"
@@ -591,12 +562,10 @@
fun bsimp :: "arexp \<Rightarrow> arexp"
where
"bsimp (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)"
-| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {} ) "
+| "bsimp (AALTs bs1 rs) = bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {}) "
| "bsimp r = r"
-
-
fun
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
@@ -605,23 +574,16 @@
definition blexer_simp where
"blexer_simp r s \<equiv> if bnullable (bders_simp (intern r) s) then
- decode (bmkeps (bders_simp (intern r) s)) r else None"
+ decode (bmkeps (bders_simp (intern r) s)) r else None"
export_code bders_simp in Scala module_name Example
lemma bders_simp_append:
shows "bders_simp r (s1 @ s2) = bders_simp (bders_simp r s1) s2"
apply(induct s1 arbitrary: r s2)
- apply(simp)
- apply(simp)
+ apply(simp_all)
done
-
-
-
-
-
-
lemma L_bsimp_ASEQ:
"L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -674,25 +636,25 @@
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(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(auto)
- apply (simp add: L_erase_AALTs)
+ apply (simp add: L_erase_AALTs)
using L_erase_AALTs by blast
+
+
lemma bsimp_ASEQ0:
shows "bsimp_ASEQ bs r1 AZERO = AZERO"
apply(induct r1)
apply(auto)
done
-
-
lemma bsimp_ASEQ1:
assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2"
@@ -711,7 +673,7 @@
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)
apply(simp add: ders_append)
apply(simp add: bders_simp_append)
@@ -748,23 +710,6 @@
apply(simp)
by (metis append_assoc in_set_conv_decomp r1 r2)
-lemma qq3:
- shows "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)"
- apply(induct rs arbitrary: bs)
- apply(simp)
- apply(simp)
- done
-
-
-
-
-
-fun nonnested :: "arexp \<Rightarrow> bool"
- where
- "nonnested (AALTs bs2 []) = True"
-| "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
-| "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)"
-| "nonnested r = True"
lemma flts_append:
shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -1006,41 +951,44 @@
done
-corollary srewrites_alt1: "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+corollary srewrites_alt1:
+ assumes "rs1 s\<leadsto>* rs2"
+ shows "AALTs bs rs1 \<leadsto>* AALTs bs rs2"
+using assms
by (metis append.left_neutral srewrites_alt)
-lemma star_seq: "r1 \<leadsto>* r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
- apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
- apply(rule rs1)
- apply(erule rrewrites.cases)
- apply(simp)
- apply(rule r_in_rstar)
- apply(rule rrewrite.intros(4))
- apply simp
- apply(rule rs2)
- apply(assumption)
- apply(rule rrewrite.intros(4))
- by assumption
+lemma star_seq:
+ assumes "r1 \<leadsto>* r2"
+ shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3"
+using assms
+apply(induct r1 r2 arbitrary: r3 rule: rrewrites.induct)
+apply(auto intro: rrewrite.intros)
+done
-lemma star_seq2: "r3 \<leadsto>* r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
- apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
- apply auto
- using rrewrite.intros(5) by blast
-
+lemma star_seq2:
+ assumes "r3 \<leadsto>* r4"
+ shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r1 r4"
+using assms
+apply(induct r3 r4 arbitrary: r1 rule: rrewrites.induct)
+apply(auto intro: rrewrite.intros)
+done
-lemma continuous_rewrite: "\<lbrakk>r1 \<leadsto>* AZERO\<rbrakk> \<Longrightarrow> ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+lemma continuous_rewrite:
+ assumes "r1 \<leadsto>* AZERO"
+ shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+using assms
apply(induction ra\<equiv>"r1" rb\<equiv>"AZERO" arbitrary: bs1 r1 r2 rule: rrewrites.induct)
- apply (simp add: r_in_rstar rrewrite.intros(1))
-
- by (meson rrewrite.intros(1) rrewrites.intros(2) star_seq)
+ apply(auto intro: rrewrite.intros r_in_rstar star_seq)
+ by (meson rrewrite.intros(1) rs2 star_seq)
-lemma bsimp_aalts_simpcases: "AONE bs \<leadsto>* (bsimp (AONE bs))" "AZERO \<leadsto>* bsimp AZERO" "ACHAR bs c \<leadsto>* (bsimp (ACHAR bs c))"
- apply (simp add: rrewrites.intros(1))
- apply (simp add: rrewrites.intros(1))
- by (simp add: rrewrites.intros(1))
+lemma bsimp_aalts_simpcases:
+ shows "AONE bs \<leadsto>* bsimp (AONE bs)"
+ and "AZERO \<leadsto>* bsimp AZERO"
+ 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)"
@@ -1072,8 +1020,6 @@
-
-
lemma flts_prepend: "\<lbrakk>nonalt a; nonazero a\<rbrakk> \<Longrightarrow> flts (a#rs) = a # (flts rs)"
by (metis append_Cons append_Nil flts_single1 flts_append)
@@ -1098,14 +1044,14 @@
apply blast
using bbbbs1 apply blast
- apply(simp add: nonalt.simps)+
+ apply(simp)+
apply (meson nonazero.elims(3))
by (meson fs4 nonalt.elims(3) nonazero.elims(3))
-lemma rrewrite0away: "AALTs bs ( AZERO # rsb) \<leadsto> AALTs bs rsb"
+lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb"
by (metis append_Nil rrewrite.intros(7))
@@ -1139,7 +1085,7 @@
apply(case_tac "\<exists>bs2 rs2. a = AALTs bs2 rs2")
apply(erule exE)+
- apply(simp add: flts.simps)
+ apply(simp)
prefer 2
apply(subst flts_prepend)
@@ -1164,16 +1110,6 @@
apply auto
done
-fun distinctByAcc :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'b set"
- where
- "distinctByAcc [] f acc = acc"
-| "distinctByAcc (x#xs) f acc =
- (if (f x) \<in> acc then distinctByAcc xs f acc
- else (distinctByAcc xs f ({f x} \<union> acc)))"
-
-lemma dB_single_step: "distinctBy (a#rs) f {} = a # distinctBy rs f {f a}"
- apply simp
- done
lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2"
using split_list by fastforce
@@ -1236,7 +1172,8 @@
-lemma bsimp_rewrite: " (rrewrites r ( bsimp r))"
+lemma bsimp_rewrite:
+ shows "r \<leadsto>* bsimp r"
apply(induction r rule: bsimp.induct)
apply simp
apply(case_tac "bsimp r1 = AZERO")
@@ -1315,12 +1252,11 @@
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 nonbnullable_lists_concat qq3 by presburger
+ 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 qq3 apply blast
+ using r2 apply blast
apply(case_tac "bnullable r")
apply blast
@@ -1359,7 +1295,7 @@
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 qq2 qq3)
+ apply (metis bnullable.simps(4) qq2)
apply (metis append.assoc)
@@ -1380,7 +1316,7 @@
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 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
+ apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr)
thm qq1
@@ -1427,7 +1363,7 @@
apply (simp add: b2)
- by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append)
+ by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append)
lemma rewrites_bmkeps:
assumes "r1 \<leadsto>* r2" "bnullable r1"
@@ -1496,16 +1432,19 @@
-lemma rewrites_fuse: "r2 \<leadsto>* r2' \<Longrightarrow> (fuse bs1 r2) \<leadsto>* (fuse bs1 r2')"
- apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
- apply simp
- by (meson real_trans rewrite_fuse)
+lemma rewrites_fuse:
+ assumes "r2 \<leadsto>* r2'"
+ shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'"
+using assms
+apply(induction r2 r2' arbitrary: bs1 rule: rrewrites.induct)
+apply(auto intro: rewrite_fuse real_trans)
+done
-lemma bder_fuse_list: " map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
- apply(induction rs1)
- apply simp
- by (simp add: bder_fuse)
-
+lemma bder_fuse_list:
+ shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1"
+apply(induction rs1)
+apply(simp_all add: bder_fuse)
+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))"