654 (*

   638 

   655 def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {

   656   case Nil => acc

   657   case r :: rs1 => 

   658     // if(acc == ONE) 

   659     //   regConcat(r, rs1) 

   660     // else

   661       regConcat(SEQ(acc, r), rs1)

   662 }

   663 

   664 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {

   665   turnIntoTerms((regConcat(erase(r), ctx)))

   666     .toSet

   667 }

   668 

   669 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =

   670   turnIntoTerms(regConcat(r, ctx)).toSet

   671 

   672 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, 

   673 subseteqPred: (C, C) => Boolean) : Boolean = {

   674   subseteqPred(f(a, b), c)

   675 }

   676 def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 

   677   //rs1 \subseteq rs2

   678   rs1.forall(rs2.contains)

   679 

   680 

   681 }

   682 *)

   690                                  | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (map (\<lambda>r. filter notZero (prune6 acc r ctx)) rs0))  )"

   650                                  | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0)))  )"

   691 

   651 

   652 

   653 

   654 (*

   655 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {

   656   if (ABIncludedByC(a = r, b = ctx, c = acc, 

   657                     f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 

   658   {

   659     AZERO

   660   }

   661   else{

   662     r match {

   663       case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{

   664         case AZERO => 

   665           AZERO

   666         case AONE(bs1) => //when r1 becomes 1, chances to further prune r2

   667           prune6(acc, fuse(bs1, r2), ctx)

   668         case r1p => 

   669           ASEQ(bs, r1p, r2)

   670       }

   671       case AALTS(bs, rs0) => 

   672         rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {

   673           case Nil => 

   674             AZERO

   675           case r :: Nil => 

   676             fuse(bs, r) 

   677           case rs0p => 

   678             AALTS(bs, rs0p)

   679         }

   680       case r => r

   681     }

   682   }

   683 }

   684 

   685 

   686 *)

   696                        else (let pruned = prune6 acc x in 

   691                        else (let pruned = prune6 acc a [] in 

   699                                |xPrime \<Rightarrow> xPrime # (dB6 xs ((turnIntoTerms (erase pruned)) \<union> acc)  ) ) ))   "

   694                                |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc)  ) ) ))   "

   695 

   696 

   697 fun bsimpStrong6 :: "arexp \<Rightarrow> arexp" 

   698   where

   699   "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)"

   700 | "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) "

   701 | "bsimpStrong6 r = r"

   702 

   703 

   704 fun 

   705   bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp"

   706 where

   707   "bdersStrong6 r [] = r"

   708 | "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s"

   709 

   710 definition blexerStrong where

   711  "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then 

   712                     decode (bmkeps (bdersStrong6 (intern r) s)) r else None"

   713 

   714 

   715 lemma centralStrong:  

   716   shows "bders_simp r s \<leadsto>* bdersStrong6 r s"

   717 proof(induct s arbitrary: r rule: rev_induct)

   718   case Nil

   719   then show "bders_simp r [] \<leadsto>* bdersStrong6 r []" by simp

   720 next

   721   case (snoc x xs)

   722   have IH: "\<And>r. bders_simp r xs \<leadsto>* bdersStrong6 r xs" by fact

   723   have "bders_simp r (xs @ [x]) = bders_simp (bders_simp r xs) [x]" by (simp add: bders_simp_append)

   724   also have "... \<leadsto>* bders_simp (bdersStrong6 r xs) [x]" using IH

   725     by (simp add: rewrites_preserves_bder)

   726   also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH

   727     by (simp add: rewrites_to_bsimp)

   728   finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 

   729     by (simp add: bders_simp_append)

   730 qed

   731 

   732 lemma mainStrong: 

   733   assumes "bnullable (bders r s)"

   734   shows "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)"

   735 proof -

   736   have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry

   737   then 

   738   show "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)" 

   739 

   740   sorry

   741 qed

   742 

   743 

   744 

   745 

   746 theorem blexerStrong_correct :

   747   shows "blexerStrong r s = blexer_simp r s"

   748   

   749   sorry

   750