--- a/thys3/BlexerSimp.thy	Thu Jun 23 16:10:04 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 16:47:48 2022 +0100
@@ -614,22 +614,6 @@
 
 
 
-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 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {}) "
-| "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"
 
 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"
@@ -651,52 +635,119 @@
 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where
   "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))"
 
-(*
-def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
-  case Nil => acc
-  case r :: rs1 => 
-    // if(acc == ONE) 
-    //   regConcat(r, rs1) 
-    // else
-      regConcat(SEQ(acc, r), rs1)
-}
 
-def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
-  turnIntoTerms((regConcat(erase(r), ctx)))
-    .toSet
-}
-
-def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
-  turnIntoTerms(regConcat(r, ctx)).toSet
-
-def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 
-subseteqPred: (C, C) => Boolean) : Boolean = {
-  subseteqPred(f(a, b), c)
-}
-def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
-  //rs1 \subseteq rs2
-  rs1.forall(rs2.contains)
-
-
-}
-*)
 
 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 (map (\<lambda>r. filter notZero (prune6 acc r ctx)) rs0))  )"
+                                 | 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) 
-                       else (let pruned = prune6 acc x in 
+                       else (let pruned = prune6 acc a [] in 
                               (case pruned of
                                  AZERO \<Rightarrow> dB6 as acc
-                               |xPrime \<Rightarrow> xPrime # (dB6 xs ((turnIntoTerms (erase pruned)) \<union> 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 centralStrong:  
+  shows "bders_simp 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
+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
+    by (simp add: rewrites_preserves_bder)
+  also have "... \<leadsto>* bders_simp (bders_simp 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)
+qed
+
+lemma mainStrong: 
+  assumes "bnullable (bders r s)"
+  shows "bmkeps (bders_simp 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)" 
+
+  sorry
+qed
+
+
+
+
+theorem blexerStrong_correct :
+  shows "blexerStrong r s = blexer_simp r s"
+  
+  sorry
+
 
 
 end