# HG changeset patch
# User Chengsong
# Date 1655999998 -3600
# Node ID 6e97f4aa7cd0ffb9600f709afd0e7e871305c80b
# Parent  333013923c5a500f8d87f569b1c2ec839be85d1d
beforeBig changes

diff -r 333013923c5a -r 6e97f4aa7cd0 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jun 23 16:47:48 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 16:59:58 2022 +0100
@@ -650,41 +650,6 @@
                                  | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0)))  )"
 
 
-
-(*
-def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
-  if (ABIncludedByC(a = r, b = ctx, c = acc, 
-                    f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
-  {
-    AZERO
-  }
-  else{
-    r match {
-      case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
-        case AZERO => 
-          AZERO
-        case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
-          prune6(acc, fuse(bs1, r2), ctx)
-        case r1p => 
-          ASEQ(bs, r1p, r2)
-      }
-      case AALTS(bs, rs0) => 
-        rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
-          case Nil => 
-            AZERO
-          case r :: Nil => 
-            fuse(bs, r) 
-          case rs0p => 
-            AALTS(bs, rs0p)
-        }
-      case r => r
-    }
-  }
-}
-
-
-*)
-
 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) 
@@ -712,18 +677,99 @@
                     decode (bmkeps (bdersStrong6 (intern r) s)) r else None"
 
 
+(*
+lemma rewrite_preserves_bder: 
+  shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)"
+  and   "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2"
+proof(induction rule: rrewrite_srewrite.inducts)
+  case (bs1 bs r2)
+  then show ?case
+    by (simp add: continuous_rewrite) 
+next
+  case (bs2 bs r1)
+  then show ?case 
+    apply(auto)
+    apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2)
+    by (simp add: r_in_rstar rrewrite_srewrite.bs2)
+next
+  case (bs3 bs1 bs2 r)
+  then show ?case 
+    apply(simp)
+    
+    by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt)
+next
+  case (bs4 r1 r2 bs r3)
+  have as: "r1 \<leadsto> r2" by fact
+  have IH: "bder c r1 \<leadsto>* bder c r2" by fact
+  from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)"
+    by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq)
+next
+  case (bs5 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)
+    apply(auto)
+    using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger
+    using star_seq2 by blast
+next
+  case (bs6 bs)
+  then show ?case
+    using rrewrite_srewrite.bs6 by force 
+next
+  case (bs7 bs r)
+  then show ?case
+    by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) 
+next
+  case (bs10 rs1 rs2 bs)
+  then show ?case
+    using contextrewrites0 by force    
+next
+  case ss1
+  then show ?case by simp
+next
+  case (ss2 rs1 rs2 r)
+  then show ?case
+    by (simp add: srewrites7) 
+next
+  case (ss3 r1 r2 rs)
+  then show ?case
+    by (simp add: srewrites7) 
+next
+  case (ss4 rs)
+  then show ?case
+    using rrewrite_srewrite.ss4 by fastforce 
+next
+  case (ss5 bs1 rs1 rsb)
+  then show ?case 
+    apply(simp)
+    using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast
+next
+  case (ss6 a1 a2 bs rsa rsb)
+  then show ?case
+    apply(simp only: map_append map1)
+    apply(rule srewrites_trans)
+    apply(rule rs_in_rstar)
+    apply(rule_tac rrewrite_srewrite.ss6)
+    using Der_def der_correctness apply auto[1]
+    by blast
+qed
+*)
+
+
+
 lemma centralStrong:  
-  shows "bders_simp r s \<leadsto>* bdersStrong6 r s"
+  shows "bders r s \<leadsto>* bdersStrong6 r s"
 proof(induct s arbitrary: r rule: rev_induct)
   case Nil
-  then show "bders_simp r [] \<leadsto>* bdersStrong6 r []" by simp
+  then show "bders r [] \<leadsto>* bdersStrong6 r []" by simp
 next
   case (snoc x xs)
-  have IH: "\<And>r. bders_simp r xs \<leadsto>* bdersStrong6 r xs" by fact
-  have "bders_simp r (xs @ [x]) = bders_simp (bders_simp r xs) [x]" by (simp add: bders_simp_append)
-  also have "... \<leadsto>* bders_simp (bdersStrong6 r xs) [x]" using IH
+  have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact
+  have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append)
+  also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH
     by (simp add: rewrites_preserves_bder)
-  also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH
+  also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH
     by (simp add: rewrites_to_bsimp)
   finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
     by (simp add: bders_simp_append)
@@ -731,11 +777,11 @@
 
 lemma mainStrong: 
   assumes "bnullable (bders r s)"
-  shows "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)"
+  shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)"
 proof -
   have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry
   then 
-  show "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)" 
+  show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" 
 
   sorry
 qed