# HG changeset patch
# User Chengsong
# Date 1656007862 -3600
# Node ID 9feeb279afdd04c2e04c173157163dd32f4b8fb9
# Parent  9972877a3f397820d8bc3b9076a042c3319b17f0
more deletion of bsimp related

diff -r 9972877a3f39 -r 9feeb279afdd thys3/BlexerSimp.thy
--- 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)