# HG changeset patch # User Christian Urban # Date 1646221421 0 # Node ID 222333d2bdc27ab4132981e0576b8561f6b84668 # Parent 0cce1aee0fb26ffc6f49d6cc4fefda9e2807125e updated diff -r 0cce1aee0fb2 -r 222333d2bdc2 progs/scala/re-bit2.scala --- a/progs/scala/re-bit2.scala Mon Feb 21 23:38:26 2022 +0000 +++ b/progs/scala/re-bit2.scala Wed Mar 02 11:43:41 2022 +0000 @@ -1,3 +1,7 @@ + + + + import scala.language.implicitConversions import scala.language.reflectiveCalls import scala.annotation.tailrec @@ -225,71 +229,11 @@ case r1 :: rs2 => r1 :: flats(rs2) } -def projectFirstChild(rs: List[ARexp]) : List[ARexp] = rs match { - case (ASEQ(bs, r1, r2p)::rs1) => r1::projectFirstChild(rs1) - case Nil => Nil - } - - - -def distinctBy2(xs: List[ARexp], acc: List[Rexp] = Nil): List[ARexp] = xs match { - case Nil => Nil - case (x::xs) => { - val res = erase(x) - if(acc.contains(res)) - distinctBy2(xs, acc) - else - x match { - case ASEQ(bs0, AALTS(bs1, rs), r2) => - val newTerms = distinctBy2(rs.map(r1 => ASEQ(Nil, r1, r2)), acc) - val rsPrime = projectFirstChild(newTerms) - newTerms match { - case Nil => distinctBy2(xs, acc) - case t::Nil => ASEQ(bs0, fuse(bs1, rsPrime.head), r2)::distinctBy2(xs, erase(t)::acc) - case ts => ASEQ(bs0, AALTS(bs1, rsPrime), r2)::distinctBy2(xs, newTerms.map(erase(_)):::acc) - } - case x => x::distinctBy2(xs, res::acc) - } - } - } - -/* -def strongBsimp(r: ARexp): ARexp = - { - r match { - case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(r2)) match { - case (AZERO, _) => AZERO - case (_, AZERO) => AZERO - case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) - case (r1s, r2s) => ASEQ(bs1, r1s, r2s) - } - case AALTS(bs1, rs) => { - val rs_simp = rs.map(strongBsimp(_)) - val flat_res = flats(rs_simp) - val dist_res = distinctBy2(flat_res)//distinctBy(flat_res, erase) - dist_res match { - case Nil => AZERO - case s :: Nil => fuse(bs1, s) - case rs => AALTS(bs1, rs) - } - - } - case r => r - } - } -*/ - def bsimp(r: ARexp): ARexp = r match { case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match { case (AZERO, _) => AZERO case (_, AZERO) => AZERO case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) - //case (AALTS(bs, rs), r) => - // AALTS(Nil, rs.map(ASEQ(bs1 ++ bs, _, r))) - //case (ASEQ(bs2, r1, ASTAR(bs3, r2)), ASTAR(bs4, r3)) if erase(r2) == erase(r3) => - // ASEQ(bs1 ++ bs2, r1, ASTAR(bs3, r2)) - //case (ASEQ(bs2, r1, r2), r3) => - // ASEQ(bs1 ++ bs2, r1, ASEQ(Nil, r2, r3)) case (r1s, r2s) => ASEQ(bs1, r1s, r2s) } case AALTS(bs1, rs) => (flts(rs.map(bsimp))).distinctBy(erase) match { @@ -297,7 +241,6 @@ case r::Nil => fuse(bs1, r) case rs => AALTS(bs1, rs) } - //case (ASTAR(bs1, ASTAR(bs2, r))) => bsimp(ASTAR(bs1 ++ bs2, r)) case r => r } @@ -310,12 +253,101 @@ def blex_simp(r: ARexp, s: List[Char]) : Bits = s match { case Nil => if (bnullable(r)) bmkeps(r) else throw new Exception("Not matched") - case c::cs => blex(bsimp(bder(c, r)), cs) + case c::cs => blex_simp(bsimp(bder(c, r)), cs) } def blexing_simp(r: Rexp, s: String) : Val = decode(r, blex_simp(internalise(r), s.toList)) +////////////////////// +// new simplification + +// collects first components of sequences. +def coll(r: Rexp, rs: List[Rexp]) : List[Rexp] = rs match { + case Nil => Nil + case SEQ(r1, r2) :: rs => + if (r == r2) r1 :: coll(r, rs) else coll(r, rs) + case r1 :: rs => coll(r, rs) +} + +def bsimp_ASEQ1(bs: Bits, r1: ARexp, r2: ARexp) : ARexp = r1 match { + case AZERO => AZERO + case AONE(bs1) => fuse(bs ::: bs1, r2) + case _ => ASEQ(bs, r1, r2) +} + +def bsimp_AALTs(bs: Bits, rs: List[ARexp]) : ARexp = rs match { + case Nil => AZERO + case r::Nil => fuse(bs, r) + case _ => AALTS(bs, rs) +} + +def prune(r: ARexp, all: List[Rexp]) : ARexp = r match { + case ASEQ(bs, r1, r2) => { + val termsTruncated = coll(erase(r2), all) + val pruned = prune(r1, termsTruncated) + bsimp_ASEQ1(bs, pruned, r2) + } + case AALTS(bs, rs) => { + val rsp = rs.map(prune(_, all)).filter(_ != AZERO) + bsimp_AALTs(bs, rsp) + } + case r => + if (all.contains(erase(r))) r else AZERO +} + +def oneSimp(r: Rexp) : Rexp = r match { + case SEQ(ONE, r) => r + case SEQ(r1, r2) => SEQ(oneSimp(r1), r2) + case r => r +} + +def breakup(r: Rexp) : List[Rexp] = r match { + case SEQ(r1, r2) => breakup(r1).map(SEQ(_, r2)) + case ALT(r1, r2) => breakup(r1) ::: breakup(r2) + case _ => r::Nil +} + +def addToAcc(r: ARexp, acc: List[Rexp]) : List[Rexp] = + breakup(erase(r)).filterNot(r => acc.contains(oneSimp(r))) + +def dBStrong(rs: List[ARexp], acc: List[Rexp]) : List[ARexp] = rs match { + case Nil => Nil + case r::rs => if (acc.contains(erase(r))) dBStrong(rs, acc) + else prune(r, addToAcc(r, acc)) match { + case AZERO => dBStrong(rs, addToAcc(r, acc) ::: acc) + case r1 => r1 :: dBStrong(rs, addToAcc(r, acc) ::: acc) + } +} + +def bsimp_ASEQ(bs: Bits, r1: ARexp, r2: ARexp) : ARexp = (r1, r2) match { + case (AZERO, _) => AZERO + case (_, AZERO) => AZERO + case (AONE(bs1), r2) => fuse(bs ::: bs1, r2) + case _ => ASEQ(bs, r1, r2) +} + +def bsimp2(r: ARexp): ARexp = r match { + case ASEQ(bs1, r1, r2) => bsimp_ASEQ(bs1, bsimp2(r1), bsimp2(r2)) + case AALTS(bs1, rs) => bsimp_AALTs(bs1, dBStrong(flts(rs.map(bsimp2(_))), Nil)) + case r => r +} + +def bders_simp2(r: ARexp, s: List[Char]) : ARexp = s match { + case Nil => r + case c::cs => bders_simp2(bsimp2(bder(c, r)), cs) +} + + +def blex_simp2(r: ARexp, s: List[Char]) : Bits = s match { + case Nil => if (bnullable(r)) bmkeps(r) + else throw new Exception("Not matched") + case c::cs => blex_simp2(bsimp2(bder(c, r)), cs) +} + +def blexing_simp2(r: Rexp, s: String) : Val = + decode(r, blex_simp2(internalise(r), s.toList)) + //println(blexing_simp(reg, "aab")) @@ -377,6 +409,9 @@ case STAR(r1) => 1 + size(r1) } +def asize(r: ARexp) : Int = size(erase(r)) +def psize(rs: Set[Rexp]) : Int = rs.map(size(_)).sum + def pp(r: ARexp): String = r match { case ASEQ(_, ACHAR(_, a1),ASEQ(_, r1, r2)) => s"${a1}${pp(r1)}${pp(r2)}" case ASEQ(_, ACHAR(_, a1),ACHAR(_, a2)) => s"${a1}${a2}" @@ -389,6 +424,27 @@ } +val TEST = STAR("a" | "aa") +println(asize(bders(("a" * 0).toList, internalise(TEST)))) +println(asize(bders(("a" * 1).toList, internalise(TEST)))) +println(asize(bders(("a" * 2).toList, internalise(TEST)))) +println(asize(bders(("a" * 3).toList, internalise(TEST)))) +println(asize(bders(("a" * 4).toList, internalise(TEST)))) + +println(asize(bders_simp(internalise(TEST), ("a" * 0).toList))) +println(asize(bders_simp(internalise(TEST), ("a" * 1).toList))) +println(asize(bders_simp(internalise(TEST), ("a" * 2).toList))) +println(asize(bders_simp(internalise(TEST), ("a" * 3).toList))) +println(asize(bders_simp(internalise(TEST), ("a" * 4).toList))) + + +println(asize(bders_simp2(internalise(TEST), ("a" * 0).toList))) +println(asize(bders_simp2(internalise(TEST), ("a" * 1).toList))) +println(asize(bders_simp2(internalise(TEST), ("a" * 2).toList))) +println(asize(bders_simp2(internalise(TEST), ("a" * 3).toList))) +println(asize(bders_simp2(internalise(TEST), ("a" * 4).toList))) +println(asize(bders_simp2(internalise(TEST), ("a" * 5).toList))) + // Some Tests //============ @@ -419,6 +475,7 @@ println(blexing(STARREG, "a" * 3)) println(blexing_simp(STARREG, "a" * 3)) +println(pders(List(STARREG), "a" * 3)) size(STARREG) @@ -436,6 +493,9 @@ size(erase(bders_simp(internalise(STARREG), ("a" * 102).toList))) size(erase(bders_simp(internalise(STARREG), ("a" * 103).toList))) +size(erase(bders_simp2(internalise(STARREG), ("a" * 103).toList))) +psize(pders(("a" * 103).toList, Set(STARREG))) + println(bders_simp(internalise(STARREG), ("a" * 1).toList)) println(bders_simp(internalise(STARREG), ("a" * 2).toList)) println(bders_simp(internalise(STARREG), ("a" * 3).toList)) @@ -709,3 +769,25 @@ encode(inj(dr, 'a', decode(dr_der, res1))) */ + + + + + + + +/* +def star(n: Long) = if ((n & 1L) == 1L) "*" else " " +def stars(n: Long): String = if (n == 0L) "" else star(n) + " " + stars(n >> 1) +def spaces(n: Int) = " " * n + + +def sierpinski(n: Int) { + ((1 << n) - 1 to 0 by -1).foldLeft(1L) { + case (bitmap, remainingLines) => + println(spaces(remainingLines) + stars(bitmap)) + (bitmap << 1) ^ bitmap + } +} + +*/ \ No newline at end of file diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/PDerivs.thy --- a/thys2/PDerivs.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/PDerivs.thy Wed Mar 02 11:43:41 2022 +0000 @@ -400,8 +400,9 @@ apply(rule subset_trans) thm pders_STAR apply(rule pders_STAR) - apply(simp) - apply(auto simp add: pders_Set_def)[1] + apply(simp) + apply(auto simp add: pders_Set_def)[1] +(* rest of SEQ case *) apply(simp) apply(rule conjI) apply blast diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/Paper/Paper.thy --- a/thys2/Paper/Paper.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/Paper/Paper.thy Wed Mar 02 11:43:41 2022 +0000 @@ -675,7 +675,7 @@ transforms a bitcoded regular expression into a (standard) regular expression by just erasing the annotated bitsequences. We omit the straightforward definition. For defining the algorithm, we also need - the functions \textit{bnullable} and \textit{bmkeps}, which are the + the functions \textit{bnullable} and \textit{bmkeps}(\textit{s}), which are the ``lifted'' versions of \textit{nullable} and \textit{mkeps} acting on bitcoded regular expressions. % @@ -695,14 +695,16 @@ & \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\ - $\textit{bmkeps}\,(\textit{ALTs}\,bs\,r\!::\!\rs)$ & $\dn$ & - $\textit{if}\;\textit{bnullable}\,r$\\ - & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,r$\\ - & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,\rs$\\ + $\textit{bmkeps}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ & + $bs\,@\,\textit{bmkepss}\,\rs$\\ $\textit{bmkeps}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &\\ \multicolumn{3}{r}{$bs \,@\,\textit{bmkeps}\,r_1\,@\, \textit{bmkeps}\,r_2$}\\ $\textit{bmkeps}\,(\textit{STAR}\,bs\,r)$ & $\dn$ & - $bs \,@\, [\S]$ + $bs \,@\, [\S]$\\ + $\textit{bmkepss}\,(r\!::\!\rs)$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,r$\\ + & &$\textit{then}\;\textit{bmkeps}\,r$\\ + & &$\textit{else}\;\textit{bmkepss}\,\rs$ \end{tabular} \end{tabular} \end{center} @@ -1040,7 +1042,7 @@ \noindent where we scan the list from left to right (because we have to remove later copies). In @{text distinctBy}, @{text f} is a function and @{text acc} is an accumulator for regular - expressions---essentially a set of regular expression that we have already seen + expressions---essentially a set of regular expressions that we have already seen while scanning the list. Therefore we delete an element, say @{text x}, from the list provided @{text "f x"} is already in the accumulator; otherwise we keep @{text x} and scan the rest of the list but @@ -1182,12 +1184,12 @@ simplified regular expressions in small steps (unlike the @{text bsimp}-function which does the same in a big step), and show that each of the small steps preserves the bitcodes that lead to the final POSIX value. - The rewrite system is organised such that $\leadsto$ is for bitcode regular + The rewrite system is organised such that $\leadsto$ is for bitcoded regular expressions and $\stackrel{s}{\leadsto}$ for lists of bitcoded regular expressions. The former essentially implements the simplifications of @{text "bsimpSEQ"} and @{text flts}; while the latter implements the simplifications in @{text "bsimpALTs"}. We can show that any bitcoded - regular expression reduces in one or more steps to the simplified + regular expression reduces in zero or more steps to the simplified regular expression generated by @{text bsimp}: \begin{lemma}\label{lemone} @@ -1317,9 +1319,9 @@ text {* -In this section let us sketch our argument on why the size of the simplified +In this section let us sketch our argument for why the size of the simplified derivatives with the aggressive simplification function is finite. Suppose -we have a size functions for bitcoded regular expressions, written +we have a size function for bitcoded regular expressions, written @{text "|r|"}, which counts the number of nodes if we regard $r$ as a tree (we omit the precise definition). For this we show that for every $r$ there exists a bound $N$ @@ -1418,7 +1420,7 @@ \cite[Page 14]{Sulzmann2014}. Given the growth of the derivatives in some cases even after aggressive simplification, this - is a hard to believe fact. A similar claim of about a theoretical runtime + is a hard to believe fact. A similar claim about a theoretical runtime of @{text "O(n\<^sup>2)"} is made for the Verbatim lexer, which calculates POSIX matches and is based on derivatives \cite{verbatim}. In this case derivatives are not simplified. Clearly our result of having finite diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/SizeBound4.thy --- a/thys2/SizeBound4.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/SizeBound4.thy Wed Mar 02 11:43:41 2022 +0000 @@ -1019,7 +1019,7 @@ apply(simp only: map_append) apply(simp only: map_single) apply(rule rs_in_rstar) - thm rrewrite_srewrite.intros + thm rrewrite_srewrite.intros apply(rule rrewrite_srewrite.ss6) using as apply(auto simp add: der_correctness Der_def) diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/SizeBound6CT.thy --- a/thys2/SizeBound6CT.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/SizeBound6CT.thy Wed Mar 02 11:43:41 2022 +0000 @@ -47,24 +47,69 @@ shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]" by auto + +fun ordsuf :: "char list \ char list list" + where + "ordsuf [] = []" +| "ordsuf (x # xs) = (ordsuf xs) @ [(x # xs)]" + +lemma + shows "ordsuf [c] = [[c]]" + and "ordsuf [c2, c3] = [[c3], [c2,c3]]" + and "ordsuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]" + by auto + +lemma ordsuf_last: + shows "ordsuf (xs @ [x]) = [x] # (map (\s. s @ [x]) (ordsuf xs))" + apply(induct xs) + apply(auto) + done + +lemma ordsuf_append: + shows "ordsuf (s1 @ s) = (ordsuf s) @ (map (\s11. s11 @ s) (ordsuf s1))" +apply(induct s1 arbitrary: s rule: rev_induct) + apply(simp) + apply(drule_tac x="[x] @ s" in meta_spec) + apply(simp) + apply(subst ordsuf_last) + apply(simp) + done + + +lemma + "orderedSuf xs = ordsuf xs" + apply(induct xs rule: rev_induct) + apply(simp) + apply(simp) + apply(subst ordsuf_last) + apply(simp) + oops + +(* +(* lemma throwing_elem_around: shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))" and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\s11. s11 @ ([a] @ s))) (orderedSuf s1) )" + apply(auto) + prefer 2 + sorry - +*) lemma suf_cons: shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\s11. s11 @ s) (orderedSuf s1))" + apply(induct s1 arbitrary: s rule: rev_induct) + apply(simp) + apply(drule_tac x="[x] @ s" in meta_spec) + apply(simp) + + apply(induct s arbitrary: s1) apply simp - apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s") - prefer 2 - apply simp - apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)") - prefer 2 - apply presburger apply(drule_tac x="s1 @ [a]" in meta_spec) - sorry + apply(simp only: append_assoc append.simps) + + using throwing_elem_around(2) by force @@ -141,11 +186,6 @@ (if x \ acc then rdistinct xs acc else x # (rdistinct xs ({x} \ acc)))" -lemma rdistinct_idem: - shows "rdistinct (x # (rdistinct rs {x})) {} = x # (rdistinct rs {x})" - - sorry - @@ -199,7 +239,14 @@ | "rlist_size [] = 0" thm neq_Nil_conv - +lemma hand_made_def_rlist_size: + shows "rlist_size rs = sum_list (map rsize rs)" +proof (induct rs) + case Nil show ?case by simp +next + case (Cons a rs) thus ?case + by simp +qed lemma rsimp_aalts_smaller: shows "rsize (rsimp_ALTs rs) \ rsize (RALTS rs)" @@ -249,7 +296,7 @@ where "cond_list r1 r2 s = rders_cond_list r2 (nullable_bools r1 (orderedPref s) ) (orderedSuf s)" -thm rsimp_SEQ.simps + lemma rSEQ_mono: shows "rsize (rsimp_SEQ r1 r2) \rsize ( RSEQ r1 r2)" apply auto @@ -267,16 +314,83 @@ apply simp_all done +lemma ralts_cap_mono: + shows "rsize (RALTS rs) \ Suc ( sum_list (map rsize rs)) " + by simp + +lemma rflts_def_idiot: + shows "\ a \ RZERO; \rs1. a = RALTS rs1\ + \ rflts (a # rs) = a # rflts rs" + apply(case_tac a) + apply simp_all + done + + +lemma rflts_mono: + shows "sum_list (map rsize (rflts rs))\ sum_list (map rsize rs)" + apply(induct rs) + apply simp + apply(case_tac "a = RZERO") + apply simp + apply(case_tac "\rs1. a = RALTS rs1") + apply(erule exE) + apply simp + apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)") + prefer 2 + using rflts_def_idiot apply blast + apply simp + done + +lemma rdistinct_smaller: shows "sum_list (map rsize (rdistinct rs ss)) \ +sum_list (map rsize rs )" + apply (induct rs arbitrary: ss) + apply simp + by (simp add: trans_le_add2) + +lemma rdistinct_phi_smaller: "sum_list (map rsize (rdistinct rs {})) \ sum_list (map rsize rs)" + by (simp add: rdistinct_smaller) + + +lemma rsimp_alts_mono : + shows "\x. (\xa. xa \ set x \ rsize (rsimp xa) \ rsize xa) \ +rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \ Suc (sum_list (map rsize x))" + apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) + \ rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))") + prefer 2 + using rsimp_aalts_smaller apply auto[1] + apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \Suc( sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})))") + prefer 2 + using ralts_cap_mono apply blast + apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})) \ + sum_list (map rsize ( (rflts (map rsimp x))))") + prefer 2 + using rdistinct_smaller apply presburger + apply(subgoal_tac "sum_list (map rsize (rflts (map rsimp x))) \ + sum_list (map rsize (map rsimp x))") + prefer 2 + using rflts_mono apply blast + apply(subgoal_tac "sum_list (map rsize (map rsimp x)) \ sum_list (map rsize x)") + prefer 2 + + apply (simp add: sum_list_mono) + by linarith + + + + + lemma rsimp_mono: shows "rsize (rsimp r) \ rsize r" + apply(induct r) - apply simp_all + apply simp_all + apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \ rsize (RSEQ (rsimp r1) (rsimp r2))") apply force using rSEQ_mono - apply presburger - sorry + apply presburger + using rsimp_alts_mono by auto lemma idiot: shows "rsimp_SEQ RONE r = r" @@ -284,21 +398,15 @@ apply simp_all done -lemma no_dup_after_simp: - shows "RALTS rs = rsimp r \ distinct rs" +lemma no_alt_short_list_after_simp: + shows "RALTS rs = rsimp r \ rsimp_ALTs rs = RALTS rs" sorry lemma no_further_dB_after_simp: shows "RALTS rs = rsimp r \ rdistinct rs {} = rs" + sorry -lemma longlist_withstands_rsimp_alts: - shows "length rs \ 2 \ rsimp_ALTs rs = RALTS rs" - sorry - -lemma no_alt_short_list_after_simp: - shows "RALTS rs = rsimp r \ rsimp_ALTs rs = RALTS rs" - sorry lemma idiot2: shows " \r1 \ RZERO; r1 \ RONE;r2 \ RZERO\ @@ -552,6 +660,10 @@ RALTS (r # (cond_list r1 r2 (s @ [c]))) = RALTS (r # ((rder c r2) # (map (rder c) (cond_list r1 r2 s))))" using suffix_plus1charn by blast +lemma simp_flatten2: + shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" + sorry + lemma simp_flatten: shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" @@ -831,14 +943,7 @@ )" sorry -lemma hand_made_def_rlist_size: - shows "rlist_size rs = sum_list (map rsize rs)" -proof (induct rs) - case Nil show ?case by simp -next - case (Cons a rs) thus ?case - by simp -qed + (*this section deals with the property of distinctBy: creates a list without duplicates*) lemma distinct_mono: @@ -1017,7 +1122,7 @@ "star_update c r [] = []" |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) then (s@[c]) # [c] # (star_update c r Ss) - else s # (star_update c r Ss) )" + else (s@[c]) # (star_update c r Ss) )" lemma star_update_case1: shows "rnullable (rders_simp r s) \ star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" @@ -1025,16 +1130,68 @@ by force lemma star_update_case2: - shows "\rnullable (rders_simp r s) \ star_update c r (s # Ss) = s # (star_update c r Ss)" + shows "\rnullable (rders_simp r s) \ star_update c r (s # Ss) = (s @ [c]) # (star_update c r Ss)" + by simp + +lemma bubble_break: shows "rflts [r, RZERO] = rflts [r]" + apply(case_tac r) + apply simp+ + done + +lemma rsimp_alts_idem_aux1: + shows "rsimp_ALTs (rdistinct (rflts [rsimp a]) {}) = rsimp (RALTS [a])" + by force + + + +lemma rsimp_alts_idem_aux2: + shows "rsimp a = rsimp (RALTS [a])" + apply(simp) + apply(case_tac "rsimp a") + apply simp+ + apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) by simp lemma rsimp_alts_idem: shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))" - sorry + apply(induct as) + apply(subgoal_tac "rsimp (rsimp_ALTs [a, rsimp (rsimp_ALTs [])]) = rsimp (rsimp_ALTs [a, RZERO])") + prefer 2 + apply simp + using bubble_break rsimp_alts_idem_aux2 apply auto[1] + apply(case_tac as) + apply(subgoal_tac "rsimp_ALTs( aa # as) = aa") + prefer 2 + apply simp + using head_one_more_simp apply fastforce + apply(subgoal_tac "rsimp_ALTs (aa # as) = RALTS (aa # as)") + prefer 2 + + using rsimp_ALTs.simps(3) apply presburger + + apply(simp only:) + apply(subgoal_tac "rsimp_ALTs (a # aa # aaa # list) = RALTS (a # aa # aaa # list)") + prefer 2 + using rsimp_ALTs.simps(3) apply presburger + apply(simp only:) + apply(subgoal_tac "rsimp_ALTs [a, rsimp (RALTS (aa # aaa # list))] = RALTS (a # [rsimp (RALTS (aa # aaa # list))])") + prefer 2 + + using rsimp_ALTs.simps(3) apply presburger + apply(simp only:) + using simp_flatten2 + apply(subgoal_tac " rsimp (RALT a (rsimp (RALTS (aa # aaa # list)))) = rsimp (RALT a ((RALTS (aa # aaa # list)))) ") + prefer 2 + + apply (metis head_one_more_simp list.simps(9) rsimp.simps(2)) + apply (simp only:) + done + lemma rsimp_alts_idem2: shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))" - sorry + using head_one_more_simp rsimp_alts_idem by auto + lemma evolution_step1: shows "rsimp @@ -1056,6 +1213,225 @@ (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) " by (simp add: assms rsimp_alts_idem) +lemma rsimp_seq_aux1: + shows "r = RONE \ r2 = RSTAR r0 \ rsimp_SEQ r r2 = r2" + apply simp + done + +lemma multiple_alts_simp_flatten: + shows "rsimp (RALT (RALT r1 r2) (rsimp_ALTs rs)) = rsimp (RALTS (r1 # r2 # rs))" + by (metis Cons_eq_appendI append_self_conv2 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem simp_flatten) + + +lemma evo3_main_aux1: + shows "rsimp + (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = + rsimp + (RALTS + (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # + RSEQ (rders_simp r [x]) (RSTAR r) # map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" + apply(subgoal_tac "rsimp + (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = +rsimp + (RALT (RALT (RSEQ ( (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) ") + prefer 2 + apply (simp add: rsimp_idem) + apply (simp only:) + apply(subst multiple_alts_simp_flatten) + by simp + + +lemma evo3_main_nullable: + shows " +\a Ss. + \rsimp (rsimp_ALTs (map (\s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); + rders_simp r a \ RONE; rders_simp r a \ RZERO; rnullable (rders_simp r a)\ + \ rsimp + (rsimp_ALTs + [rder x (RSEQ (rders_simp r a) (RSTAR r)), + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" + apply(subgoal_tac "rder x (RSEQ (rders_simp r a) (RSTAR r)) + = RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r))") + prefer 2 + apply simp + apply(simp only:) + apply(subgoal_tac "star_update x r (a # Ss) = (a @ [x]) # [x] # (star_update x r Ss)") + prefer 2 + using star_update_case1 apply presburger + apply(simp only:) + apply(subst List.list.map(2))+ + apply(subgoal_tac "rsimp + (rsimp_ALTs + [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = +rsimp + (RALTS + [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])") + prefer 2 + using rsimp_ALTs.simps(3) apply presburger + apply(simp only:) + apply(subgoal_tac " rsimp + (rsimp_ALTs + (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # + rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) += + rsimp + (RALTS + (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # + rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") + + prefer 2 + using rsimp_ALTs.simps(3) apply presburger + apply (simp only:) + apply(subgoal_tac " rsimp + (RALT (RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ ( (rder x r)) (RSTAR r))) + (rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = + rsimp + (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) + (rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") + prefer 2 + apply (simp add: rsimp_idem) + apply(simp only:) + apply(subgoal_tac " rsimp + (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) + (rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = + rsimp + (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + (rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") + prefer 2 + using rders_simp_append rders_simp_one_char rsimp_idem apply presburger + apply(simp only:) + apply(subgoal_tac " rsimp + (RALTS + (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # + rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) = + rsimp + (RALTS + (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # + RSEQ (rders_simp r [x]) (RSTAR r) # map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") + prefer 2 + apply (smt (z3) idiot2 list.simps(9) rrexp.distinct(9) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_idem) + apply(simp only:) + apply(subgoal_tac " rsimp + (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + (rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = + rsimp + (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) + ( (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) ") + prefer 2 + using rsimp_idem apply force + apply(simp only:) + using evo3_main_aux1 by blast + + +lemma evo3_main_not1: + shows " \rnullable (rders_simp r a) \ rder x (RSEQ (rders_simp r a) (RSTAR r)) = RSEQ (rder x (rders_simp r a)) (RSTAR r)" + by fastforce + + +lemma evo3_main_not2: + shows "\rnullable (rders_simp r a) \ rsimp + (rsimp_ALTs + (rder x (RSEQ (rders_simp r a) (RSTAR r)) # rs)) = rsimp + (rsimp_ALTs + ((RSEQ (rders_simp r (a @ [x])) (RSTAR r)) # rs))" + by (simp add: rders_simp_append rsimp_alts_idem2 rsimp_idem) + +lemma evo3_main_not3: + shows "rsimp + (rsimp_ALTs + (rsimp_SEQ r1 (RSTAR r) # rs)) = + rsimp (rsimp_ALTs + (RSEQ r1 (RSTAR r) # rs))" + by (metis idiot2 rrexp.distinct(9) rsimp.simps(1) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) + + +lemma evo3_main_notnullable: + shows "\a Ss. + \rsimp (rsimp_ALTs (map (\s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); + rders_simp r a \ RONE; rders_simp r a \ RZERO; \rnullable (rders_simp r a)\ + \ rsimp + (rsimp_ALTs + [rder x (RSEQ (rders_simp r a) (RSTAR r)), + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" + apply(subst star_update_case2) + apply simp + apply(subst List.list.map(2)) + apply(subst evo3_main_not2) + apply simp + apply(subst evo3_main_not3) + using rsimp_alts_idem by presburger + + +lemma evo3_aux2: + shows "rders_simp r a = RONE \ rsimp_SEQ (rders_simp (rders_simp r a) [x]) (RSTAR r) = RZERO" + by simp +lemma evo3_aux3: + shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" + by (metis list.simps(8) list.simps(9) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem) + +lemma evo3_aux4: + shows " rsimp + (rsimp_ALTs + [RSEQ (rder x r) (RSTAR r), + rsimp (rsimp_ALTs rs)]) = + rsimp + (rsimp_ALTs + (rsimp_SEQ (rders_simp r [x]) (RSTAR r) # rs))" + by (metis rders_simp_one_char rsimp.simps(1) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) + +lemma evo3_aux5: + shows "rders_simp r a \ RONE \ rders_simp r a \ RZERO \ rsimp_SEQ (rders_simp r a) (RSTAR r) = RSEQ (rders_simp r a) (RSTAR r)" + using idiot2 by blast + + +lemma evolution_step3: + shows" \a Ss. + rsimp (rsimp_ALTs (map (\s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) \ + rsimp + (rsimp_ALTs + [rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)), + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = + rsimp (rsimp_ALTs (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" + apply(case_tac "rders_simp r a = RONE") + apply(subst rsimp_seq_aux1) + apply simp + apply(subst rder.simps(6)) + apply(subgoal_tac "rnullable (rders_simp r a)") + prefer 2 + using rnullable.simps(2) apply presburger + apply(subst star_update_case1) + apply simp + + apply(subst List.list.map)+ + apply(subst rders_simp_append) + apply(subst evo3_aux2) + apply simp + apply(subst evo3_aux3) + apply(subst evo3_aux4) + apply simp + apply(case_tac "rders_simp r a = RZERO") + + apply (simp add: rsimp_alts_idem2) + apply(subgoal_tac "rders_simp r (a @ [x]) = RZERO") + prefer 2 + using rder.simps(1) rders_simp_append rders_simp_one_char rsimp.simps(3) apply presburger + using rflts.simps(2) rsimp.simps(3) rsimp_SEQ.simps(1) apply presburger + apply(subst evo3_aux5) + apply simp + apply(case_tac "rnullable (rders_simp r a) ") + using evo3_main_nullable apply blast + using evo3_main_notnullable apply blast + done (* proof (prove) @@ -1075,11 +1451,8 @@ apply(subst List.list.map(2)) apply(subst evolution_step2) apply simp - apply(case_tac "rnullable (rders_simp r a)") - apply(subst star_update_case1) - apply simp - apply(subst List.list.map)+ - sledgehammer + + sorry @@ -1094,7 +1467,8 @@ lemma ralts_vs_rsimpalts: shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)" - sorry + by (metis evo3_aux3 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) simp_flatten2) + lemma linearity_of_list_of_star_or_starseqs: fixes r::rrexp and Ss::"char list list" and x::char @@ -1156,14 +1530,119 @@ using star_list_push_der apply presburger + by (metis ralts_vs_rsimpalts starseq_list_evolution) + + +lemma starder_is_a_list: + shows " \Ss. rders_simp (RSTAR r) s = rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) \ rders_simp (RSTAR r) s = RSTAR r" + apply(case_tac s) + prefer 2 + apply (metis neq_Nil_conv starder_is_a_list_of_stars_or_starseqs) + apply simp + done + + +(** start about bounds here**) + + +lemma list_simp_size: + shows "rlist_size (map rsimp rs) \ rlist_size rs" + apply(induct rs) + apply simp + apply simp + apply (subgoal_tac "rsize (rsimp a) \ rsize a") + prefer 2 + using rsimp_mono apply fastforce + using add_le_mono by presburger + +lemma inside_list_simp_inside_list: + shows "r \ set rs \ rsimp r \ set (map rsimp rs)" + apply (induct rs) + apply simp + apply auto + done + + +lemma rsize_star_seq_list: + shows "(\s. rsize (rders_simp r0 s) < N0 ) \ \N3.\Ss. +rlist_size (rdistinct (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3" sorry +lemma rdistinct_bound_by_no_simp: + shows " + + rlist_size (rdistinct (map rsimp rs) (set (map rsimp ss))) + \ (rlist_size (rdistinct rs (set ss))) +" + apply(induct rs arbitrary: ss) + apply simp + apply(case_tac "a \ set ss") + apply(subgoal_tac "rsimp a \ set (map rsimp ss)") + prefer 2 + using inside_list_simp_inside_list apply blast + + apply simp + apply simp + by (metis List.set_insert add_le_mono image_insert insert_absorb rsimp_mono trans_le_add2) + + +lemma starder_closed_form_bound_aux1: + shows +"\Ss. rsize (rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \ + Suc (rlist_size ( (rdistinct ( ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {}))) " + + sorry + +lemma starder_closed_form_bound: + shows "(\s. rsize (rders_simp r0 s) < N0 ) \ \N3.\Ss. +rsize(rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3" + apply(subgoal_tac " \N3.\Ss. +rlist_size (rdistinct (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss) {}) < N3") + prefer 2 + + using rsize_star_seq_list apply auto[1] + apply(erule exE) + apply(rule_tac x = "Suc N3" in exI) + apply(subgoal_tac "\Ss. rsize (rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) \ + Suc (rlist_size ( (rdistinct ( ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss))) {})))") + prefer 2 + using starder_closed_form_bound_aux1 apply blast + by (meson less_trans_Suc linorder_not_le not_less_eq) + + +thm starder_closed_form_bound_aux1 + +(* + "ralts_vs_rsimpalts", , and "starder_closed_form_bound_aux1", which could be due to a bug in Sledgehammer or to inconsistent axioms (including "sorry"s) +*) + +lemma starder_size_bound: + shows "(\s. rsize (rders_simp r0 s) < N0 ) \ \N3.\Ss. +rsize(rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \ +rsize (RSTAR r0) < N3" + apply(subgoal_tac " \N3.\Ss. +rsize(rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3") + prefer 2 + using starder_closed_form_bound apply blast + apply(erule exE) + apply(rule_tac x = "max N3 (Suc (rsize (RSTAR r0)))" in exI) + using less_max_iff_disj by blast + + + + lemma finite_star: shows "(\s. rsize (rders_simp r0 s) < N0 ) \ \N3. \s.(rsize (rders_simp (RSTAR r0) s)) < N3" - - sorry + apply(subgoal_tac " \N3. \Ss. +rsize(rsimp (RALTS ( (map (\s1. rsimp_SEQ (rders_simp r0 s1) (RSTAR r0)) Ss)))) < N3 \ +rsize (RSTAR r0) < N3") + prefer 2 + using starder_size_bound apply blast + apply(erule exE) + apply(rule_tac x = N3 in exI) + by (metis starder_is_a_list) lemma rderssimp_zero: diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/SizeBoundStrong.thy --- a/thys2/SizeBoundStrong.thy Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/SizeBoundStrong.thy Wed Mar 02 11:43:41 2022 +0000 @@ -585,17 +585,20 @@ | "bsimp_ASEQ1 bs r1 r2 = ASEQ bs r1 r2" -fun collect where +fun collect :: "rexp \ rexp list \ rexp list" where \collect _ [] = []\ -| \collect erasedR2 ((SEQ r1 r2) # rs) = (if r2 = erasedR2 then r1 # (collect erasedR2 rs) - else collect erasedR2 rs)\ +| \collect erasedR2 ((SEQ r1 r2) # rs) = + (if r2 = erasedR2 then r1 # (collect erasedR2 rs) else collect erasedR2 rs)\ | \collect erasedR2 (r # rs) = collect erasedR2 rs\ fun pruneRexp where - \pruneRexp (ASEQ bs r1 r2) allowableTerms = -( let termsTruncated = (collect (erase r2) allowableTerms) in (let pruned = pruneRexp r1 termsTruncated in (bsimp_ASEQ1 bs pruned r2)) )\ -| \pruneRexp (AALTs bs rs) allowableTerms = (let rsp = (filter (\r. r \ AZERO) (map (\r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp ) + "pruneRexp (ASEQ bs r1 r2) allowableTerms = + (let termsTruncated = (collect (erase r2) allowableTerms) in + (let pruned = pruneRexp r1 termsTruncated in + (bsimp_ASEQ1 bs pruned r2)))" +| \pruneRexp (AALTs bs rs) allowableTerms = + (let rsp = (filter (\r. r \ AZERO) (map (\r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp ) \ | \pruneRexp r allowableTerms = (if (erase r) \ (set allowableTerms) then r else AZERO)\ diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/blexer2.sc --- a/thys2/blexer2.sc Mon Feb 21 23:38:26 2022 +0000 +++ b/thys2/blexer2.sc Wed Mar 02 11:43:41 2022 +0000 @@ -622,7 +622,9 @@ def bders_simp(s: List[Char], r: ARexp) : ARexp = s match { case Nil => r - case c::s => bders_simp(s, bsimp(bder(c, r))) + case c::s => + println(erase(r)) + bders_simp(s, bsimp(bder(c, r))) } def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r)) @@ -818,59 +820,60 @@ val pderSTAR = pderUNIV(STARREG) val refSize = pderSTAR.map(size(_)).sum - println("different partial derivative terms:") - pderSTAR.foreach(r => r match { + // println("different partial derivative terms:") + // pderSTAR.foreach(r => r match { - case SEQ(head, rstar) => - println(shortRexpOutput(head) ++ "~STARREG") - case STAR(rstar) => - println("STARREG") + // case SEQ(head, rstar) => + // println(shortRexpOutput(head) ++ "~STARREG") + // case STAR(rstar) => + // println("STARREG") - } - ) - println("the total number of terms is") - //println(refSize) - println(pderSTAR.size) + // } + // ) + // println("the total number of terms is") + // //println(refSize) + // println(pderSTAR.size) val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%) val B : Rexp = ((ONE).%) val C : Rexp = ("d") ~ ((ONE).%) val PRUNE_REG : Rexp = (C | B | A) val APRUNE_REG = internalise(PRUNE_REG) - // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG)) - // println("program executes and gives: as disired!") - // println(shortRexpOutput(erase(program_solution))) - val simpedPruneReg = strongBsimp(APRUNE_REG) - println(shortRexpOutput(erase(simpedPruneReg))) - for(i <- List(100, 900 ) ){// 100, 400, 800, 840, 841, 900 - val prog0 = "a" * i - //println(s"test: $prog0") - println(s"testing with $i a's" ) - //val bd = bdersSimp(prog0, STARREG)//DB - val sbd = bdersSimpS(prog0, STARREG)//strongDB - starPrint(erase(sbd)) - val subTerms = breakIntoTerms(erase(sbd)) - //val subTermsLarge = breakIntoTerms(erase(bd)) + // // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG)) + // // println("program executes and gives: as disired!") + // // println(shortRexpOutput(erase(program_solution))) + // val simpedPruneReg = strongBsimp(APRUNE_REG) + + // println(shortRexpOutput(erase(simpedPruneReg))) + // for(i <- List(1,2 ) ){// 100, 400, 800, 840, 841, 900 + // val prog0 = "a" * i + // //println(s"test: $prog0") + // println(s"testing with $i a's" ) + // //val bd = bdersSimp(prog0, STARREG)//DB + // val sbd = bdersSimpS(prog0, STARREG)//strongDB + // starPrint(erase(sbd)) + // val subTerms = breakIntoTerms(erase(sbd)) + // //val subTermsLarge = breakIntoTerms(erase(bd)) - println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}") + // println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}") - println("the number of distinct subterms for bsimp with strongDB") - println(subTerms.distinct.size) - //println(subTermsLarge.distinct.size) - println("which coincides with the number of PDER terms") + // println("the number of distinct subterms for bsimp with strongDB") + // println(subTerms.distinct.size) + // //println(subTermsLarge.distinct.size) + // println("which coincides with the number of PDER terms") - // println(shortRexpOutput(erase(sbd))) - // println(shortRexpOutput(erase(bd))) + // // println(shortRexpOutput(erase(sbd))) + // // println(shortRexpOutput(erase(bd))) - println("pdersize, original, strongSimp") - println(refSize, size(STARREG), asize(sbd)) + // println("pdersize, original, strongSimp") + // println(refSize, size(STARREG), asize(sbd)) - val vres = strong_blexing_simp( STARREG, prog0) - println(vres) - } + // val vres = strong_blexing_simp( STARREG, prog0) + // println(vres) + // } // println(vs.length) // println(vs) @@ -878,6 +881,9 @@ // val prog1 = """read n; write n""" // println(s"test: $prog1") // println(lexing_simp(WHILE_REGS, prog1)) + val display = ("a"| "ab").% + val adisplay = internalise(display) + bders_simp( "aaaaa".toList, adisplay) } small() diff -r 0cce1aee0fb2 -r 222333d2bdc2 thys2/paper.pdf Binary file thys2/paper.pdf has changed