# HG changeset patch # User Christian Urban # Date 1490022797 0 # Node ID e59cec211f4fb339b192678779ee82e14e8b2802 # Parent 2dc1647eab9eceb3ce966d79ddbeaeb00e043b36 added automata implementation diff -r 2dc1647eab9e -r e59cec211f4f progs/scala/autos.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/progs/scala/autos.scala Mon Mar 20 15:13:17 2017 +0000 @@ -0,0 +1,533 @@ +// DFAs and NFAs based on Scala's partial functions +import scala.util.Try + + +// type abbreviation for partial functions +type :=>[A, B] = PartialFunction[A, B] + + +// some states for test cases +abstract class State +case object Q0 extends State +case object Q1 extends State +case object Q2 extends State +case object Q3 extends State +case object Q4 extends State +case object Q5 extends State +case object Q6 extends State + + +// class for DFAs +case class DFA[A, C](start: A, // starting state + delta: (A, C) :=> A, // transition + fins: A => Boolean) { // final states + + // given a state and a "string", what is the next + // state, if there is any? + def deltas(q: A, s: List[C]) : A = s match { + case Nil => q + case c::cs => deltas(delta(q, c), cs) + } + + // is a "string" accepted by an DFA? + def accepts(s: List[C]) : Boolean = + Try(fins(deltas(start, s))) getOrElse false + +} + +// DFA 1 +val dtrans1 : (State, Char) :=> State = + { case (Q0, 'a') => Q0 + case (Q0, 'b') => Q1 + } + +val dfa1 = DFA(Q0, dtrans1, Set[State](Q1)) + +dfa1.accepts("aaab".toList) // true +dfa1.accepts("aacb".toList) // false + +// another DFA test +abstract class S +case object S0 extends S +case object S1 extends S +case object S2 extends S +case object Sink extends S + +// transition function with a sink state +// S0 --a--> S1 --a--> S2 +val sigma : (S, Char) :=> S = + { case (S0, 'a') => S1 + case (S1, 'a') => S2 + case _ => Sink + } + +val dfa1a = DFA(S0, sigma, Set[S](S2)) + +dfa1a.accepts("aa".toList) //true +dfa1a.accepts("".toList) //false +dfa1a.accepts("ab".toList) //false + + +// class for NFAs +case class NFA[A, C](starts: Set[A], // starting states + delta: Set[(A, C) :=> A], // transitions + fins: A => Boolean) { // final states + + // given a state and a character, what is the set of next states? + // if there is none => empty set + def next(q: A, c: C) : Set[A] = + delta.flatMap((d) => Try(d(q, c)).toOption) + + def nexts(qs: Set[A], c: C) : Set[A] = + qs.flatMap(next(_, c)) + + // given some states and a string, what is the set of next states? + def deltas(qs: Set[A], s: List[C]) : Set[A] = s match { + case Nil => qs + case c::cs => deltas(nexts(qs, c), cs) + } + + // is a string accepted by an NFA? + def accepts(s: List[C]) : Boolean = + deltas(starts, s).exists(fins) +} + + + + +// NFA test cases + +// 1 +val trans1 = Set[(State, Char) :=> State]( + { case (Q0, 'a') => Q1 }, + { case (Q0, _) => Q0 }, + { case (Q1, _) => Q2 }, + { case (Q2, _) => Q3 }, + { case (Q3, _) => Q4 }, + { case (Q4, 'b') => Q5 }, + { case (Q5, 'c') => Q6 } +) + +val nfa1 = NFA(Set[State](Q0), trans1, Set[State](Q6)) + +nfa1.accepts("axaybzbc".toList) // true +nfa1.accepts("aaaaxaybzbc".toList) // true +nfa1.accepts("axaybzbd".toList) // false + + +// 2 +val trans2 = Set[(State, Char) :=> State]( + { case (Q0, 'a') => Q0 }, + { case (Q0, 'a') => Q1 }, + { case (Q0, 'b') => Q2 }, + { case (Q1, 'a') => Q1 }, + { case (Q2, 'b') => Q2 } +) + +val nfa2 = NFA(Set[State](Q0), trans2, Set[State](Q2)) + +nfa2.accepts("aa".toList) // false +nfa2.accepts("aaaaa".toList) // false +nfa2.accepts("aaaaab".toList) // true +nfa2.accepts("aaaaabbb".toList) // true +nfa2.accepts("aaaaabbbaaa".toList) // false +nfa2.accepts("ac".toList) // false + +// 3 +val trans3 = Set[(State, Char) :=> State]( + { case (Q0, _) => Q0 }, + { case (Q0, 'a') => Q1 }, + { case (Q0, 'b') => Q3 }, + { case (Q1, 'b') => Q2 }, + { case (Q2, 'c') => Q5 }, + { case (Q3, 'c') => Q4 }, + { case (Q4, 'd') => Q5 } +) + +val nfa3 = NFA(Set[State](Q0), trans3, Set[State](Q5)) + +nfa3.accepts("aaaaabc".toList) // true +nfa3.accepts("aaaabcd".toList) // true +nfa3.accepts("aaaaab".toList) // false +nfa3.accepts("aaaabc".toList) // true +nfa3.accepts("aaaaabbbaaa".toList) // false + + + +// subset, or powerset, construction +def powerset[A, C](nfa: NFA[A, C]) : DFA[Set[A], C] = { + DFA(nfa.starts, + { case (qs, c) => nfa.nexts(qs, c) }, + _.exists(nfa.fins)) +} + +val dfa2 = powerset(nfa1) + +dfa2.accepts("axaybzbc".toList) // true +dfa2.accepts("aaaaxaybzbc".toList) // true +dfa2.accepts("axaybzbd".toList) // false + +val dfa3 = powerset(nfa2) + +dfa3.accepts("aa".toList) // false +dfa3.accepts("aaaaa".toList) // false +dfa3.accepts("aaaaab".toList) // true +dfa3.accepts("aaaaabbb".toList) // true +dfa3.accepts("aaaaabbbaaa".toList) // false +dfa3.accepts("ac".toList) // false + + + + +// epsilon NFA + + +// fixpoint construction +import scala.annotation.tailrec +@tailrec +def fixpT[A](f: A => A, x: A): A = { + val fx = f(x) + if (fx == x) x else fixpT(f, fx) +} + + +case class eNFA[A, C](starts: Set[A], // starting state + delta: Set[(A, Option[C]) :=> A], // transition edges + fins: A => Boolean) { // final states + + // epsilon transitions + def enext(q: A) : Set[A] = + delta.flatMap((d) => Try(d(q, None)).toOption) + + def enexts(qs: Set[A]) : Set[A] = + qs ++ qs.flatMap(enext(_)) + + // epsilon closure + def ecl(qs: Set[A]) : Set[A] = + fixpT(enexts, qs) + + // "normal" transition + def next(q: A, c: C) : Set[A] = + delta.flatMap((d) => Try(d(q, Some(c))).toOption) + + def nexts(qs: Set[A], c: C) : Set[A] = + qs.flatMap(next(_, c)) + + def deltas(qs: Set[A], s: List[C]) : Set[A] = s match { + case Nil => ecl(qs) + case c::cs => deltas(ecl(nexts(ecl(qs), c)), cs) + } + + def accepts(s: List[C]) : Boolean = + deltas(starts, s.toList).exists(fins) +} + + +val etrans1 = Set[(State, Option[Char]) :=> State]( + { case (Q0, Some('a')) => Q1 }, + { case (Q1, None) => Q0 } +) + +val enfa = eNFA(Set[State](Q0), etrans1, Set[State](Q1)) + +enfa.accepts("a".toList) // true +enfa.accepts("".toList) // false +enfa.accepts("aaaaa".toList) // true +enfa.accepts("aaaaab".toList) // flase +enfa.accepts("aaaaabbb".toList) // false +enfa.accepts("aaaaabbbaaa".toList) // false +enfa.accepts("ac".toList) // false + + + +// Regular expressions fro derivative automata + +abstract class Rexp +case object ZERO extends Rexp +case object ONE extends Rexp +case class CHAR(c: Char) extends Rexp { + override def toString = c.toString +} +case object ALL extends Rexp { + override def toString = "." +} +case class ALT(r1: Rexp, r2: Rexp) extends Rexp +case class SEQ(r1: Rexp, r2: Rexp) extends Rexp { + override def toString = r1.toString + " ~ " + r2.toString +} +case class STAR(r: Rexp) extends Rexp { + override def toString = r.toString + "*" +} +case class NTIMES(r: Rexp, n: Int) extends Rexp { + override def toString = r.toString + "{" + n.toString + "}" +} +case class UPNTIMES(r: Rexp, n: Int) extends Rexp + + +def get_chars(r: Rexp) : Set[Char] = r match { + case ZERO => Set() + case ONE => Set() + case CHAR(c) => Set(c) + case ALT(r1, r2) => get_chars(r1) ++ get_chars(r2) + case SEQ(r1, r2) => get_chars(r1) ++ get_chars(r2) + case STAR(r) => get_chars(r) + case NTIMES(r, _) => get_chars(r) + case UPNTIMES(r, _) => get_chars(r) + case ALL => ('a' to 'z').toSet +} + + + +import scala.language.implicitConversions +import scala.language.reflectiveCalls + +def charlist2rexp(s: List[Char]): Rexp = s match { + case Nil => ONE + case c::Nil => CHAR(c) + case c::s => SEQ(CHAR(c), charlist2rexp(s)) +} +implicit def string2rexp(s: String): Rexp = charlist2rexp(s.toList) + +implicit def RexpOps (r: Rexp) = new { + def | (s: Rexp) = ALT(r, s) + def % = STAR(r) + def ~ (s: Rexp) = SEQ(r, s) +} + +implicit def stringOps (s: String) = new { + def | (r: Rexp) = ALT(s, r) + def | (r: String) = ALT(s, r) + def % = STAR(s) + def ~ (r: Rexp) = SEQ(s, r) + def ~ (r: String) = SEQ(s, r) +} + +def simp(r: Rexp) : Rexp = r match { + case ALT(r1, r2) => (simp(r1), simp(r2)) match { + case (ZERO, r2s) => r2s + case (r1s, ZERO) => r1s + case (r1s, r2s) => if (r1s == r2s) r1s else ALT (r1s, r2s) + } + case SEQ(r1, r2) => (simp(r1), simp(r2)) match { + case (ZERO, _) => ZERO + case (_, ZERO) => ZERO + case (ONE, r2s) => r2s + case (r1s, ONE) => r1s + case (r1s, r2s) => SEQ(r1s, r2s) + } + case NTIMES(r, n) => if (n == 0) ONE else NTIMES(simp(r), n) + case UPNTIMES(r, n) => if (n == 0) ONE else UPNTIMES(simp(r), n) + case r => r +} + + +// nullable function: tests whether the regular +// expression can recognise the empty string +def nullable(r: Rexp) : Boolean = r match { + case ZERO => false + case ONE => true + case CHAR(_) => false + case ALL => false + case ALT(r1, r2) => nullable(r1) || nullable(r2) + case SEQ(r1, r2) => nullable(r1) && nullable(r2) + case STAR(_) => true + case NTIMES(r, i) => if (i == 0) true else nullable(r) + case UPNTIMES(r: Rexp, n: Int) => true +} + +// derivative of a regular expression w.r.t. a character +def der(c: Char, r: Rexp) : Rexp = r match { + case ZERO => ZERO + case ONE => ZERO + case CHAR(d) => if (c == d) ONE else ZERO + case ALL => ONE + case ALT(r1, r2) => ALT(der(c, r1), der(c, r2)) + case SEQ(r1, r2) => + if (nullable(r1)) ALT(SEQ(der(c, r1), r2), der(c, r2)) + else SEQ(der(c, r1), r2) + case STAR(r1) => SEQ(der(c, r1), STAR(r1)) + case NTIMES(r1, i) => + if (i == 0) ZERO else + if (nullable(r1)) SEQ(der(c, r1), UPNTIMES(r1, i - 1)) + else SEQ(der(c, r1), NTIMES(r1, i - 1)) + case UPNTIMES(r1, i) => + if (i == 0) ZERO + else SEQ(der(c, r1), UPNTIMES(r1, i - 1)) +} + + +// partial derivative of a regular expression w.r.t. a character +def pder(c: Char, r: Rexp) : Set[Rexp] = r match { + case ZERO => Set() + case ONE => Set() + case CHAR(d) => if (c == d) Set(ONE) else Set() + case ALL => Set(ONE) + case ALT(r1, r2) => pder(c, r1) ++ pder(c, r2) + case SEQ(r1, r2) => + (for (pr1 <- pder(c, r1)) yield SEQ(pr1, r2)) ++ + (if (nullable(r1)) pder(c, r2) else Set()) + case STAR(r1) => + for (pr1 <- pder(c, r1)) yield SEQ(pr1, STAR(r1)) + case NTIMES(r1, i) => + if (i == 0) Set() else + if (nullable(r1)) + for (pr1 <- pder(c, r1)) yield SEQ(pr1, UPNTIMES(r1, i - 1)) + else + for (pr1 <- pder(c, r1)) yield SEQ(pr1, NTIMES(r1, i - 1)) + case UPNTIMES(r1, i) => + if (i == 0) Set() + else + for (pr1 <- pder(c, r1)) yield SEQ(pr1, UPNTIMES(r1, i - 1)) +} + +def ppder(c: Char, rs: Set[Rexp]) : Set[Rexp] = + rs.flatMap(pder(c, _)) + + + +// quick-and-dirty translation of a pder automaton + +val r = STAR(ALL) ~ "a" ~ NTIMES(ALL, 3) ~ "bc" +val pder_nfa = NFA[Set[Rexp], Char](Set(Set(r)), + Set( { case (rs, c) => rs.flatMap(pder(c, _))} ), + _.exists(nullable)) + + + +pder_nfa.accepts("axaybzbc".toList) // true +pder_nfa.accepts("aaaaxaybzbc".toList) // true +pder_nfa.accepts("axaybzbd".toList) // false + + + +// Derivative and Partial Derivative Automaton construction + + +type DState = Rexp // state type of the derivative automaton +type DStates = Set[Rexp] +type Trans = (DState, Char) :=> DState // transition functions of the der/pder auto +type MTrans = Map[(DState, Char), DState] // transition Maps +type STrans = Set[MTrans] // set of transition Maps + + + +// Brzozoswki Derivative automaton construction ... simple +// version, might not terminate + +def goto(sigma: Set[Char], delta: MTrans, qs: DStates, q: DState, c: Char) : (DStates, MTrans) = { + val qder = simp(der(c, q)) + qs.find(_ == qder) match { + case Some(qexists) => (qs, delta + ((q, c) -> qexists)) + case None => explore(sigma, delta + ((q, c) -> qder), qs + qder, qder) + } +} + +def explore(sigma: Set[Char], delta: MTrans, qs: DStates, q: DState) : (DStates, MTrans) = + sigma.foldLeft((qs, delta)) { case ((qs, delta), c) => goto(sigma, delta, qs, q, c) } + + +def mkDFA(r: Rexp) = { + val sigma = get_chars(r) + val (qs, delta) = explore(sigma, Map(), Set[Rexp](r), r) + val fins = qs.filter(nullable(_)) + val deltaf : (Rexp, Char) :=> Rexp = { case (q, c) => delta(q, c) } + println(s"Automata size: ${qs.size}") + DFA(r, deltaf, fins) +} + +val re = "ab" | "ac" +val d1 = mkDFA(re) + +d1.accepts("ab".toList) // true +d1.accepts("ac".toList) // true +d1.accepts("aa".toList) // false + +val d2 = mkDFA(r) + +d2.accepts("axaybzbc".toList) // true +d2.accepts("aaaaxaybzbc".toList) // true +d2.accepts("axaybzbd".toList) // false + +for (n <- (1 to 10).toList) + mkDFA(STAR(ALL) ~ "a" ~ NTIMES(ALL, n) ~ "bc") + + +// this is an example where mkDFA does not terminate +val big_aux = STAR("a" | "b") +val big = SEQ(big_aux, SEQ("a",SEQ("b", big_aux))) + +//mkDFA(big) // does not terminate + + + +// Antimirov Partial derivative automata construction ... definitely terminates + + +// to transform (concrete) Maps into functions +def toFun(m: MTrans) : Trans = + { case (q, c) => m(q, c) } + +def pgoto(sigma: Set[Char], delta: STrans, qs: DStates, q: DState, c: Char) : (DStates, STrans) = { + val qders = pder(c, q).map(simp(_)) // set of simplified partial derivatives + qders.foldLeft((qs, delta)) { case ((qs, delta), qnew) => padd(sigma, delta, qs, q, qnew, c) } +} + +def padd(sigma: Set[Char], delta: STrans, qs: DStates, + q: DState, qnew: DState, c: Char) : (DStates, STrans) = { + qs.find(_ == qnew) match { + case Some(qexists) => (qs, delta + Map((q, c) -> qexists)) + case None => pexplore(sigma, delta + Map((q, c) -> qnew), qs + qnew, qnew) + } +} + +def pexplore(sigma: Set[Char], delta: STrans, qs: DStates, q: DState) : (DStates, STrans) = + sigma.foldLeft((qs, delta)) { case ((qs, delta), c) => pgoto(sigma, delta, qs, q, c) } + +def mkNFA(r: Rexp) : NFA[Rexp, Char]= { + val sigma = get_chars(r) + val (qs, delta) = pexplore(sigma, Set(), Set(r), r) + val fins = qs.filter(nullable(_)) + val deltaf = delta.map(toFun(_)) + println(s"NFA size: ${qs.size}") + NFA(Set(r), deltaf, fins) +} + + +// simple example from Scott's paper + +val n1 = mkNFA(re) // size = 4 + +n1.accepts("ab".toList) // true +n1.accepts("ac".toList) // true +n1.accepts("aa".toList) // false + +// example from: Partial Derivative and Position Bisimilarity +// Automata, Eva Maia, Nelma Moreira, Rogerio Reis + +val r_test = STAR(("a" ~ STAR("b")) | "b") ~ "a" +val t1 = pder('a', r_test).map(simp(_)) +val t2 = pder('b', r_test).map(simp(_)) + +mkNFA(r_test) // size = 3 + + +// simple example involving double star +// with depth-first search causes catastrophic backtracing + +val n2 = mkNFA(STAR(STAR("a")) ~ "b") // size 3 + +n2.accepts("aaaaaab".toList) // true +n2.accepts("aaaaaa".toList) // false +n2.accepts(("a" * 100).toList) // false + +val r1 = STAR(ALL) ~ "a" ~ NTIMES(ALL, 1) ~ "bc" +mkNFA(r1) // size = 5 + +val n3 = mkNFA(r) // size = 7 + +n3.accepts("axaybzbc".toList) // true +n3.accepts("aaaaxaybzbc".toList) // true +n3.accepts("axaybzbd".toList) // false + +for (n <- (1 to 100).toList) + mkNFA(STAR(ALL) ~ "a" ~ NTIMES(ALL, n) ~ "bc") diff -r 2dc1647eab9e -r e59cec211f4f thys/LexerExt.thy --- a/thys/LexerExt.thy Fri Mar 17 19:47:42 2017 +0000 +++ b/thys/LexerExt.thy Mon Mar 20 15:13:17 2017 +0000 @@ -223,6 +223,9 @@ | NMTIMES rexp nat nat | PLUS rexp | AND rexp rexp +| NOT rexp +| ALLL +| ALLBUT section {* Semantics of Regular Expressions *} @@ -241,6 +244,9 @@ | "L (NMTIMES r n m) = (\i\{n..m} . (L r) \ i)" | "L (PLUS r) = (\i\ {1..} . (L r) \ i)" | "L (AND r1 r2) = (L r1) \ (L r2)" +| "L (NOT r) = UNIV - (L r)" +| "L (ALLL) = UNIV" +| "L (ALLBUT) = UNIV - {[]}" section {* Nullable, Derivatives *} @@ -259,6 +265,10 @@ | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" | "nullable (PLUS r) = (nullable r)" | "nullable (AND r1 r2) = (nullable r1 \ nullable r2)" +| "nullable (NOT r) = (\nullable r)" +| "nullable (ALLL) = True" +| "nullable (ALLBUT) = False" + fun der :: "char \ rexp \ rexp" @@ -285,6 +295,10 @@ SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" | "der c (PLUS r) = SEQ (der c r) (STAR r)" | "der c (AND r1 r2) = AND (der c r1) (der c r2)" +| "der c (NOT r) = NOT (der c r)" +| "der c (ALLL) = ALLL" +| "der c (ALLBUT) = ALLL" + fun ders :: "string \ rexp \ rexp" @@ -339,7 +353,7 @@ apply(simp only: der.simps if_True) apply(simp only: L.simps) apply(simp) -apply(auto) +apply(auto)[3] apply(subst (asm) Sequ_UNION[symmetric]) apply(subst (asm) test[symmetric]) apply(auto simp add: Der_UNION)[1] @@ -364,12 +378,20 @@ apply(case_tac xa) apply(simp) apply(simp) -apply(auto) +apply(auto)[1] apply(auto simp add: Sequ_def Der_def)[1] using Star_def apply auto[1] apply(case_tac "[] \ L r") -apply(auto) -using Der_UNION Der_star Star_def by fastforce +apply(auto)[1] +using Der_UNION Der_star Star_def apply fastforce +apply(simp) +apply(simp) +apply(simp add: Der_def) +apply(blast) +(* ALLL*) +apply(simp add: Der_def) +apply(simp add: Der_def) +done lemma ders_correctness: shows "L (ders s r) = Ders s (L r)" @@ -412,6 +434,9 @@ | Left val | Stars "val list" | And val val +| Not val +| Alll +| Allbut section {* The string behind a value *} @@ -426,78 +451,14 @@ | "flat (Stars []) = []" | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" | "flat (And v1 v2) = flat v1" +| "flat (Not v) = flat v" +| "flat Allbut = []" + lemma flat_Stars [simp]: "flat (Stars vs) = concat (map flat vs)" by (induct vs) (auto) - -section {* Relation between values and regular expressions *} - -inductive - Prf :: "val \ rexp \ bool" ("\ _ : _" [100, 100] 100) -where - "\\ v1 : r1; \ v2 : r2\ \ \ Seq v1 v2 : SEQ r1 r2" -| "\ v1 : r1 \ \ Left v1 : ALT r1 r2" -| "\ v2 : r2 \ \ Right v2 : ALT r1 r2" -| "\ Void : ONE" -| "\ Char c : CHAR c" -| "\\v \ set vs. \ v : r\ \ \ Stars vs : STAR r" -| "\\v \ set vs. \ v : r; length vs \ n\ \ \ Stars vs : UPNTIMES r n" -| "\\v \ set vs. \ v : r; length vs = n\ \ \ Stars vs : NTIMES r n" -| "\\v \ set vs. \ v : r; length vs \ n\ \ \ Stars vs : FROMNTIMES r n" -| "\\v \ set vs. \ v : r; length vs \ n; length vs \ m\ \ \ Stars vs : NMTIMES r n m" -| "\\v \ set vs. \ v : r; length vs \ 1\ \ \ Stars vs : PLUS r" -| "\\ v1 : r1; \ v2 : r2; flat v1 = flat v2\ \ \ And v1 v2: AND r1 r2" - - -inductive_cases Prf_elims: - "\ v : ZERO" - "\ v : SEQ r1 r2" - "\ v : ALT r1 r2" - "\ v : ONE" - "\ v : CHAR c" -(* "\ vs : STAR r"*) - -lemma Prf_STAR: - assumes "\v\set vs. \ v : r \ flat v \ L r" - shows "concat (map flat vs) \ L r\" -using assms -apply(induct vs) -apply(auto) -done - -lemma Prf_Pow: - assumes "\v\set vs. \ v : r \ flat v \ L r" - shows "concat (map flat vs) \ L r \ length vs" -using assms -apply(induct vs) -apply(auto simp add: Sequ_def) -done - -lemma Prf_flat_L: - assumes "\ v : r" shows "flat v \ L r" -using assms -apply(induct v r rule: Prf.induct) -apply(auto simp add: Sequ_def) -apply(rule Prf_STAR) -apply(simp) -apply(rule_tac x="length vs" in bexI) -apply(rule Prf_Pow) -apply(simp) -apply(simp) -apply(rule Prf_Pow) -apply(simp) -apply(rule_tac x="length vs" in bexI) -apply(rule Prf_Pow) -apply(simp) -apply(simp) -apply(rule_tac x="length vs" in bexI) -apply(rule Prf_Pow) -apply(simp) -apply(simp) -using Prf_Pow by blast - lemma Star_Pow: assumes "s \ A \ n" shows "\ss. concat ss = s \ (\s \ set ss. s \ A) \ (length ss = n)" @@ -518,91 +479,6 @@ using Star_Pow by blast -lemma Star_val: - assumes "\s\set ss. \v. s = flat v \ \ v : r" - shows "\vs. concat (map flat vs) = concat ss \ (\v\set vs. \ v : r)" -using assms -apply(induct ss) -apply(auto) -apply (metis empty_iff list.set(1)) -by (metis concat.simps(2) list.simps(9) set_ConsD) - -lemma Star_val_length: - assumes "\s\set ss. \v. s = flat v \ \ v : r" - shows "\vs. concat (map flat vs) = concat ss \ (\v\set vs. \ v : r) \ (length vs) = (length ss)" -using assms -apply(induct ss) -apply(auto) -by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD) - - - - - -lemma L_flat_Prf2: - assumes "s \ L r" shows "\v. \ v : r \ flat v = s" -using assms -apply(induct r arbitrary: s) -apply(auto simp add: Sequ_def intro: Prf.intros) -using Prf.intros(1) flat.simps(5) apply blast -using Prf.intros(2) flat.simps(3) apply blast -using Prf.intros(3) flat.simps(4) apply blast -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -using Star_string Star_val apply force -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r) \ (length vs = x)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -using Star_Pow Star_val_length apply blast -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r) \ (length vs = x2)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -using Star_Pow Star_val_length apply blast -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r) \ (length vs = x)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -using Star_Pow Star_val_length apply blast -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r) \ (length vs = x)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -apply(simp) -using Star_Pow Star_val_length apply blast -apply(subgoal_tac "\vs::val list. concat (map flat vs) = s \ (\v \ set vs. \ v : r) \ (length vs = x)") -apply(auto)[1] -apply(rule_tac x="Stars vs" in exI) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -using Star_Pow Star_val_length apply blast -(* AND *) -using Prf.intros(12) by fastforce - -lemma L_flat_Prf: - "L(r) = {flat v | v. \ v : r}" -using Prf_flat_L L_flat_Prf2 by blast - - section {* Sulzmann and Lu functions *} fun @@ -618,6 +494,8 @@ | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" | "mkeps(PLUS r) = Stars ([mkeps r])" | "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)" +| "mkeps(NOT r) = Not (Allbut)" +| "mkeps(ALLL) = Void" fun injval :: "rexp \ char \ val \ val" @@ -636,32 +514,29 @@ | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" | "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)" + section {* Mkeps, injval *} lemma mkeps_flat: assumes "nullable(r)" shows "flat (mkeps r) = []" using assms -apply (induct rule: nullable.induct) -apply(auto) -by meson - -lemma mkeps_nullable: - assumes "nullable(r)" - shows "\ mkeps r : r" -using assms -apply(induct r rule: mkeps.induct) -apply(auto intro: Prf.intros) -apply(metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl) -apply(rule Prf.intros) -apply(simp_all add: mkeps_flat) +apply (induct r) +apply(auto)[15] +apply(case_tac "x3a < x2") +apply(auto)[2] done lemma Prf_injval_flat: - assumes "\ v : der c r" + assumes "flat v \ L (der c r)" shows "flat (injval r c v) = c # (flat v)" using assms apply(induct arbitrary: v rule: der.induct) +apply(simp_all) +apply(case_tac "c = d") +prefer 2 +apply(simp) +apply(simp) apply(auto elim!: Prf_elims split: if_splits) apply(metis mkeps_flat) apply(rotate_tac 2)