--- a/thys3/BlexerSimp.thy Thu Jun 23 18:57:19 2022 +0100
+++ b/thys3/BlexerSimp.thy Thu Jun 23 19:11:02 2022 +0100
@@ -65,6 +65,70 @@
+fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where
+ "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c"
+
+fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and
+ turnIntoTerms :: "rexp \<Rightarrow> rexp list "
+ where
+ "furtherSEQ ONE r2 = turnIntoTerms r2 "
+| "furtherSEQ r11 r2 = [SEQ r11 r2]"
+| "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2"
+| "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))"
+| "turnIntoTerms r = [r]"
+
+fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
+ "regConcat acc [] = acc"
+| "regConcat ONE (r # rs1) = regConcat r rs1"
+| "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1"
+
+fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
+ "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))"
+
+
+
+fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where
+ "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"
+
+fun notZero :: "arexp \<Rightarrow> bool" where
+ "notZero AZERO = True"
+| "notZero _ = False"
+
+fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
+ "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else
+ (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
+ | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )"
+
+
+
+fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
+ "dB6 [] acc = []"
+| "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc)
+ else (let pruned = prune6 acc a [] in
+ (case pruned of
+ AZERO \<Rightarrow> dB6 as acc
+ |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) "
+
+
+fun bsimpStrong6 :: "arexp \<Rightarrow> arexp"
+ where
+ "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
+| "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) "
+| "bsimpStrong6 r = r"
+
+
+fun
+ bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+where
+ "bdersStrong6 r [] = r"
+| "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s"
+
+definition blexerStrong where
+ "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then
+ decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
+
+
+
inductive
rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
and
@@ -371,50 +435,6 @@
qed
-lemma rewrites_to_bsimp:
- shows "r \<leadsto>* bsimp r"
-proof (induction r rule: bsimp.induct)
- case (1 bs1 r1 r2)
- have IH1: "r1 \<leadsto>* bsimp r1" by fact
- have IH2: "r2 \<leadsto>* bsimp r2" by fact
- { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO"
- with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
- then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
- by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)
- then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto
- }
- moreover
- { assume "\<exists>bs. bsimp r1 = AONE bs"
- then obtain bs where as: "bsimp r1 = AONE bs" by blast
- with IH1 have "r1 \<leadsto>* AONE bs" by simp
- then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
- with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)"
- using rewrites_fuse by (meson rrewrites_trans)
- then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp
- then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as)
- }
- moreover
- { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)"
- then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)"
- by (simp add: bsimp_ASEQ1)
- then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2
- by (metis rrewrites_trans star_seq star_seq2)
- then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp
- }
- ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast
-next
- case (2 bs1 rs)
- have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact
- then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites)
- also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites)
- also have "... s\<leadsto>* distinctWith (flts (map bsimp rs)) eq1 {}" by (simp add: ss6_stronger)
- finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})"
- using contextrewrites0 by auto
- also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})"
- by (simp add: bsimp_AALTs_rewrites)
- finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp
-qed (simp_all)
-
lemma to_zero_in_alt:
shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2"
@@ -519,69 +539,6 @@
-
-fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where
- "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c"
-
-fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and
- turnIntoTerms :: "rexp \<Rightarrow> rexp list "
- where
- "furtherSEQ ONE r2 = turnIntoTerms r2 "
-| "furtherSEQ r11 r2 = [SEQ r11 r2]"
-| "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2"
-| "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))"
-| "turnIntoTerms r = [r]"
-
-fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where
- "regConcat acc [] = acc"
-| "regConcat ONE (r # rs1) = regConcat r rs1"
-| "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1"
-
-fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
- "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))"
-
-
-
-fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where
- "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)"
-
-fun notZero :: "arexp \<Rightarrow> bool" where
- "notZero AZERO = True"
-| "notZero _ = False"
-
-fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where
- "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else
- (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2
- | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )"
-
-
-fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where
- "dB6 [] acc = []"
-| "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc)
- else (let pruned = prune6 acc a [] in
- (case pruned of
- AZERO \<Rightarrow> dB6 as acc
- |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) "
-
-
-fun bsimpStrong6 :: "arexp \<Rightarrow> arexp"
- where
- "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"
-| "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) "
-| "bsimpStrong6 r = r"
-
-
-fun
- bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
-where
- "bdersStrong6 r [] = r"
-| "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s"
-
-definition blexerStrong where
- "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then
- decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
-
-
lemma bders_simp_appendStrong :
shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
apply(induct s1 arbitrary: s2 rule: rev_induct)