# HG changeset patch # User Christian Urban # Date 1557485797 -3600 # Node ID 43e070803c1c57bbb984a1d13e3b20560044bb16 # Parent db0ff630bbb73885b913f7bf17ec7a0c6d6fa953 updated diff -r db0ff630bbb7 -r 43e070803c1c exps/bit-test.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/exps/bit-test.scala Fri May 10 11:56:37 2019 +0100 @@ -0,0 +1,758 @@ + +import scala.language.implicitConversions +import scala.language.reflectiveCalls +import scala.annotation.tailrec +import scala.util.Try + +// for escaping strings +def escape(raw: String) : String = { + import scala.reflect.runtime.universe._ + Literal(Constant(raw)).toString +} + +def esc2(r: (String, String)) = (escape(r._1), escape(r._2)) + +def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match { + case Nil => Nil + case (x::xs) => { + val res = f(x) + if (acc.contains(res)) distinctBy(xs, f, acc) + else x::distinctBy(xs, f, res::acc) + } +} + +abstract class Bit +case object Z extends Bit +case object S extends Bit +case class C(c: Char) extends Bit + +type Bits = List[Bit] + +// usual regular expressions with predicates +abstract class Rexp +case object ZERO extends Rexp +case object ONE extends Rexp +case class PRED(f: Char => Boolean, s: String = "_") extends Rexp { + override def toString = s"PRED(${s})" +} +case class ALTS(rs: List[Rexp]) extends Rexp +case class SEQ(r1: Rexp, r2: Rexp) extends Rexp +case class STAR(r: Rexp) extends Rexp +case class RECD(x: String, r: Rexp) extends Rexp + + +// abbreviations +def CHAR(c: Char) = PRED(_ == c, c.toString) +def ALT(r1: Rexp, r2: Rexp) = ALTS(List(r1, r2)) +def PLUS(r: Rexp) = SEQ(r, STAR(r)) +val ANYCHAR = PRED(_ => true, ".") + +// annotated regular expressions +abstract class ARexp +case object AZERO extends ARexp +case class AONE(bs: Bits) extends ARexp +case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp { + override def toString = s"APRED(${bs}, ${s})" +} +case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp +case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp +case class ASTAR(bs: Bits, r: ARexp) extends ARexp + +// abbreviations +def AALT(bs: Bits, r1: ARexp, r2: ARexp) = AALTS(bs, List(r1, r2)) + +// values +abstract class Val +case object Empty extends Val +case class Chr(c: Char) extends Val +case class Sequ(v1: Val, v2: Val) extends Val +case class Left(v: Val) extends Val +case class Right(v: Val) extends Val +case class Stars(vs: List[Val]) extends Val +case class Rec(x: String, v: Val) extends Val + +def flatten(v: Val) : String = v match { + case Empty => "" + case Chr(c) => c.toString + case Left(v) => flatten(v) + case Right(v) => flatten(v) + case Sequ(v1, v2) => flatten(v1) + flatten(v2) + case Stars(vs) => vs.map(flatten).mkString + case Rec(_, v) => flatten(v) +} + +// extracts an environment from a value +def env(v: Val) : List[(String, String)] = v match { + case Empty => Nil + case Chr(c) => Nil + case Left(v) => env(v) + case Right(v) => env(v) + case Sequ(v1, v2) => env(v1) ::: env(v2) + case Stars(vs) => vs.flatMap(env) + case Rec(x, v) => (x, flatten(v))::env(v) +} + + +// some convenience for typing in regular expressions +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 $ (r: Rexp) = RECD(s, r) +} + + +// string of a regular expression - for testing purposes +def string(r: Rexp): String = r match { + case ZERO => "0" + case ONE => "1" + case PRED(_, s) => s + case ALTS(rs) => rs.map(string).mkString("[", "|", "]") + case SEQ(r1, r2) => s"(${string(r1)} ~ ${string(r2)})" + case STAR(r) => s"{${string(r)}}*" + case RECD(x, r) => s"(${x}! ${string(r)})" +} + +// string of an annotated regular expression - for testing purposes +def astring(a: ARexp): String = a match { + case AZERO => "0" + case AONE(_) => "1" + case APRED(_, _, s) => s + case AALTS(_, rs) => rs.map(astring).mkString("[", "|", "]") + case ASEQ(_, r1, r2) => s"(${astring(r1)} ~ ${astring(r2)})" + case ASTAR(_, r) => s"{${astring(r)}}*" +} + +//-------------------------------------------------------------------- +// BITCODED PART + +def retrieve(r: ARexp, v: Val) : Bits = (r, v) match { + case (AONE(bs), Empty) => bs + case (APRED(bs, _, _), Chr(d)) => bs + case (AALTS(bs, r::Nil), v) => bs ++ retrieve(r, v) + case (AALTS(bs, r::rs), Left(v)) => bs ++ retrieve(r, v) + case (AALTS(bs, r::rs), Right(v)) => bs ++ retrieve(AALTS(Nil, rs), v) + case (ASEQ(bs, r1, r2), Sequ(v1, v2)) => + bs ++ retrieve(r1, v1) ++ retrieve(r2, v2) + case (ASTAR(bs, r), Stars(Nil)) => bs ++ List(S) + case (ASTAR(bs, r), Stars(v::vs)) => + bs ++ List(Z) ++ retrieve(r, v) ++ retrieve(ASTAR(Nil, r), Stars(vs)) +} + +def fuse(bs: Bits, r: ARexp) : ARexp = r match { + case AZERO => AZERO + case AONE(cs) => AONE(bs ++ cs) + case APRED(cs, f, s) => APRED(bs ++ cs, f, s) + case AALTS(cs, rs) => AALTS(bs ++ cs, rs) + case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2) + case ASTAR(cs, r) => ASTAR(bs ++ cs, r) +} + +// translation into ARexps +def internalise(r: Rexp) : ARexp = r match { + case ZERO => AZERO + case ONE => AONE(Nil) + case PRED(f, s) => APRED(Nil, f, s) + case ALTS(List(r1, r2)) => + AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2)))) + case ALTS(r1::rs) => { + val AALTS(Nil, rs2) = internalise(ALTS(rs)) + AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _))) + } + case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2)) + case STAR(r) => ASTAR(Nil, internalise(r)) + case RECD(x, r) => internalise(r) +} + +internalise(("a" | "ab") ~ ("b" | "")) + +// decoding of values from bit sequences +def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match { + case (ONE, bs) => (Empty, bs) + case (PRED(f, _), C(c)::bs) => (Chr(c), bs) + case (ALTS(r::Nil), bs) => decode_aux(r, bs) + case (ALTS(rs), Z::bs1) => { + val (v, bs2) = decode_aux(rs.head, bs1) + (Left(v), bs2) + } + case (ALTS(rs), S::bs1) => { + val (v, bs2) = decode_aux(ALTS(rs.tail), bs1) + (Right(v), bs2) + } + case (SEQ(r1, r2), bs) => { + val (v1, bs1) = decode_aux(r1, bs) + val (v2, bs2) = decode_aux(r2, bs1) + (Sequ(v1, v2), bs2) + } + case (STAR(r1), S::bs) => { + val (v, bs1) = decode_aux(r1, bs) + val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1) + (Stars(v::vs), bs2) + } + case (STAR(_), Z::bs) => (Stars(Nil), bs) + case (RECD(x, r1), bs) => { + val (v, bs1) = decode_aux(r1, bs) + (Rec(x, v), bs1) + } +} + +def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match { + case (v, Nil) => v + case _ => throw new Exception("Not decodable") +} + +def encode(v: Val) : Bits = v match { + case Empty => Nil + case Chr(c) => Nil + case Left(v) => Z :: encode(v) + case Right(v) => S :: encode(v) + case Sequ(v1, v2) => encode(v1) ::: encode(v2) + case Stars(Nil) => List(S) + case Stars(v::vs) => Z :: encode(v) ::: encode(Stars(vs)) +} + + +//erase function: extracts a Rexp from Arexp +def erase(r: ARexp) : Rexp = r match{ + case AZERO => ZERO + case AONE(_) => ONE + case APRED(bs, f, s) => PRED(f, s) + case AALTS(bs, rs) => ALTS(rs.map(erase(_))) + case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2)) + case ASTAR(cs, r)=> STAR(erase(r)) +} + + +// bnullable function: tests whether the aregular +// expression can recognise the empty string +def bnullable (r: ARexp) : Boolean = r match { + case AZERO => false + case AONE(_) => true + case APRED(_,_,_) => false + case AALTS(_, rs) => rs.exists(bnullable) + case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2) + case ASTAR(_, _) => true +} + +def bmkeps(r: ARexp) : Bits = r match { + case AONE(bs) => bs + case AALTS(bs, rs) => { + val n = rs.indexWhere(bnullable) + bs ++ bmkeps(rs(n)) + } + case ASEQ(bs, r1, r2) => bs ++ bmkeps(r1) ++ bmkeps(r2) + case ASTAR(bs, r) => bs ++ List(Z) +} + +// derivative of a regular expression w.r.t. a character +def bder(c: Char, r: ARexp) : ARexp = r match { + case AZERO => AZERO + case AONE(_) => AZERO + case APRED(bs, f, _) => if (f(c)) AONE(bs:::List(C(c))) else AZERO + case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _))) + case ASEQ(bs, r1, r2) => + if (bnullable(r1)) + AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(bmkeps(r1), bder(c, r2))) + else ASEQ(bs, bder(c, r1), r2) + case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r)) +} + +def blex(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(bder(c, r), cs) +} + +def preblexing(r: ARexp, s: String) : Val = + decode(erase(r), blex(r, s.toList)) + +def blexing(r: Rexp, s: String) : Val = + decode(r, blex(internalise(r), s.toList)) + + +// derivative w.r.t. a string (iterates bder) +@tailrec +def bders (s: List[Char], r: ARexp) : ARexp = s match { + case Nil => r + case c::s => bders(s, bder(c, r)) +} + +def flats(rs: List[ARexp]): List[ARexp] = rs match { + case Nil => Nil + case AZERO :: rs1 => flats(rs1) + case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2) + case r1 :: rs2 => r1 :: flats(rs2) +} + +/* +def vsimp(r: ARexp, v: Val): Val = (r, v) match { + case (ASEQ(bs1, r1, r2), Sequ(v1, v2)) => + (bsimp(r1), bsimp(r2), vsimp(r1, v1), vsimp(r2, v2)) match { + case (AZERO, _, _, _) => throw new Exception("error") + case (_, AZERO, _, _) => throw new Exception("error") + case (AONE(_), _, _, vp2) => vp2 + case (r1s, r2s, vp1, vp2) => Sequ(vp1, vp2) + } + case (AALTS(bs1, rs), _) => distinctBy(flats(rs.map(bsimp)), erase) match { + case Nil => throw new Exception("error") + case r :: Nil => throw new Exception("error") + case rs => throw new Exception("error") + } + case _ => v +} +*/ +def vsimp(v: Val, a: ARexp): Val = (v, bsimp(a)) match { + case (Sequ(v1, v2), ASEQ(_, a1, a2)) => + (vsimp(v1, a1), vsimp(v2, a2)) match { + case (Empty, vp2) => vp2 + case (vp1, vp2) => Sequ(vp1, vp2) + } + case (Left(Left(v1)), AALTS(_, r::rs)) => Left(vsimp(v1, r)) + case (Left(v1), AALTS(_, rs)) => + if (rs.length == 1) vsimp(v1, rs.head) else Left(vsimp(v1, rs.head)) + case (Right(v1), AALTS(bs, rs)) => + if (rs.length == 1) vsimp(v1, rs.head) else Right(vsimp(v1, AALTS(bs, rs.tail))) + case _ => v +} + + +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 (r1s, r2s) => ASEQ(bs1, r1s, r2s) + } + case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp)), erase) match { + case Nil => AZERO + case r :: Nil => fuse(bs1, r) + case rs => AALTS(bs1, rs) + } + case r => r +} + +def bders_simp (s: List[Char], r: ARexp) : ARexp = s match { + case Nil => r + case c::s => bders_simp(s, bsimp(bder(c, r))) +} + +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_simp(bsimp(bder(c, r)), cs) +} + + +def blexing_simp(r: Rexp, s: String) : Val = + decode(r, blex_simp(internalise(r), s.toList)) + + +def btokenise_simp(r: Rexp, s: String) = + env(blexing_simp(r, s)).map(esc2) + +// Quick example + +val r : Rexp = ZERO | "a" + +lexing(r, "a") + +val a0 = internalise(r) +val a1 = bder('a', a0) +val a1s = bsimp(bder('a', a0)) + +val a2 = bmkeps(a1) +val a2s = bmkeps(a1s) + +val v = decode(r, a2) +val vs = decode(r, a2s) + + + +val Rr : Rexp = ONE ~ "a" + +lexing(Rr, "a") + +val Ra0 = internalise(Rr) +astring(Ra0) +val Ra1 = bder('a', Ra0) +astring(Ra1) +val Ra1s = bsimp(bder('a', Ra0)) +astring(Ra1s) + +val Ra2 = bmkeps(Ra1) +val Ra2s = bmkeps(Ra1s) + +val Rv = decode(Rr, Ra2) +val Rvs = decode(Rr, Ra2s) + + +// Testing +//============ + +def time[T](code: => T) = { + val start = System.nanoTime() + val result = code + val end = System.nanoTime() + ((end - start)/1.0e9).toString +} + +def timeR[T](code: => T) = { + val start = System.nanoTime() + for (i <- 1 to 10) code + val result = code + val end = System.nanoTime() + (result, (end - start)) +} + +//size: of a Aregx for testing purposes +def size(r: Rexp) : Int = r match { + case ZERO => 1 + case ONE => 1 + case PRED(_,_) => 1 + case SEQ(r1, r2) => 1 + size(r1) + size(r2) + case ALTS(rs) => 1 + rs.map(size).sum + case STAR(r) => 1 + size(r) + case RECD(_, r) => size(r) +} + +def asize(a: ARexp) = size(erase(a)) + + +// Lexing Rules for a Small While Language + +//symbols +val SYM = PRED("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".contains(_), "SYM") +//digits +val DIGIT = PRED("0123456789".contains(_), "NUM") +//identifiers +val ID = SYM ~ (SYM | DIGIT).% +//numbers +val NUM = STAR(DIGIT) +//keywords +val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false" +//semicolons +val SEMI: Rexp = ";" +//operators +val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/" +//whitespaces +val WHITESPACE = PLUS(" " | "\n" | "\t") +//parentheses +val RPAREN: Rexp = ")" +val LPAREN: Rexp = "(" +val BEGIN: Rexp = "{" +val END: Rexp = "}" +//strings...but probably needs not +val STRING: Rexp = "\"" ~ SYM.% ~ "\"" + + + +val WHILE_REGS = (("k" $ KEYWORD) | + ("i" $ ID) | + ("o" $ OP) | + ("n" $ NUM) | + ("s" $ SEMI) | + ("str" $ STRING) | + ("p" $ (LPAREN | RPAREN)) | + ("b" $ (BEGIN | END)) | + ("w" $ WHITESPACE)).% + + +// Some Small Tests +//================== + +println("Small tests") + +val re1 = STAR("a" | "aa") +println(astring(bders_simp("".toList, internalise(re1)))) +println(astring(bders_simp("a".toList, internalise(re1)))) +println(astring(bders_simp("aa".toList, internalise(re1)))) +println(astring(bders_simp("aaa".toList, internalise(re1)))) +println(astring(bders_simp("aaaaaa".toList, internalise(re1)))) +println(astring(bders_simp("aaaaaaaaa".toList, internalise(re1)))) +println(astring(bders_simp("aaaaaaaaaaaa".toList, internalise(re1)))) +println(astring(bders_simp("aaaaaaaaaaaaaaaaaaaaaaaaa".toList, internalise(re1)))) +println(astring(bders_simp("aaaaaabaaaabbbbbaaaaaaaaaaaaaaa".toList, internalise(re1)))) + + +for (i <- 0 to 100 by 5) { + //print("Old: " + time(tokenise_simp(re1, "a" * i))) + print(" Bit: " + time(btokenise_simp(re1, "a" * i))) + print(" Bit full simp: " + time(btokenise_simp_full(re1, "a" * i))) + println(" Bit2: " + time(btokenise2_simp(re1, "a" * i))) +} + +Console.readLine + + +// Bigger Tests +//============== + + +println("Big tests") + +val fib_prog = """ +write "Fib"; +read n; +minus1 := 0; +minus2 := 1; +while n > 0 do { + temp := minus2; + minus2 := minus1 + minus2; + minus1 := temp; + n := n - 1 +}; +write "Result"; +write minus2 +""" + + +println("fib prog tests :") +println(tokenise_simp(WHILE_REGS, fib_prog)) +println(btokenise_simp(WHILE_REGS, fib_prog)) +println("equal? " + (tokenise_simp(WHILE_REGS, fib_prog) == btokenise_simp(WHILE_REGS, fib_prog))) + +for (i <- 1 to 20) { + print("Old: " + time(tokenise_simp(WHILE_REGS, fib_prog * i))) + print(" Bit: " + time(btokenise_simp(WHILE_REGS, fib_prog * i))) + println(" Bit full simp: " + time(btokenise_simp_full(WHILE_REGS, fib_prog * i))) + //println(" Bit2: " + time(btokenise2_simp(WHILE_REGS, fib_prog * i))) +} + + +println("Original " + size(WHILE_REGS)) +println("Size Bit " + asize(bders_simp((fib_prog * 1).toList, internalise(WHILE_REGS)))) +println("Size Bitf " + asize(bders_simp_full((fib_prog * 1).toList, internalise(WHILE_REGS)))) +println("Size Bit2 " + asize(bders2_simp((fib_prog * 1).toList, internalise(WHILE_REGS)))) +println("Size Old " + size(ders_simp((fib_prog * 1).toList, WHILE_REGS))) +println("Size Pder " + psize(pders_simp((fib_prog * 1).toList, WHILE_REGS))) + +System.exit(0) + +println("Internal sizes test OK or strange") + +def perc(p1: Double, p2: Double) : String = + f"${(((p1 - p2) / p2) * 100.0) }%5.0f" + "%" + +def ders_test(n: Int, s: List[Char], r: Rexp, a: ARexp) : (Rexp, ARexp) = s match { + case Nil => (r, a) + case c::s => { + // derivative + val (rd1, tr1) = timeR(der(c, r)) + val (ad1, ta1) = timeR(bder(c, a)) + val trs1 = f"${tr1}%.5f" + val tas1 = f"${ta1}%.5f" + if (tr1 < ta1) println(s"Time strange der (step) ${n} ${perc(ta1, tr1)} sizes der ${size(rd1)} ${asize(ad1)}") + //simplification + val (rd, tr) = timeR(simp(rd1)._1) + val (ad, ta) = timeR(bsimp(ad1)) + val trs = f"${tr}%.5f" + val tas = f"${ta}%.5f" + //full simplification + val (adf, taf) = timeR(bsimp_full(ad1)) + if (tr < ta) println(s"Time strange simp (step) ${n} ${perc(ta, tr)} sizes simp ${size(rd)} ${asize(ad)}") + if (n == 1749 || n == 1734) { + println{s"Aregex before bder (size: ${asize(a)})\n ${string(erase(a))}"} + println{s"Aregex after bder (size: ${asize(ad1)})\n ${string(erase(ad1))}"} + println{s"Aregex after bsimp (size: ${asize(ad)})\n ${string(erase(ad))}"} + println{s"Aregex after bsimp_full (size: ${asize(adf)})\n ${string(erase(adf))}"} + } + ders_test(n + 1, s, rd, ad) + } +} + +val prg = (fib_prog * 10).toList +ders_test(0, prg, WHILE_REGS, internalise(WHILE_REGS)) + + +//testing the two lexings produce the same value +//enumerates strings of length n over alphabet cs +def strs(n: Int, cs: String) : Set[String] = { + if (n == 0) Set("") + else { + val ss = strs(n - 1, cs) + ss ++ + (for (s <- ss; c <- cs.toList) yield c + s) + } +} + +def enum(n: Int, s: String) : Stream[Rexp] = n match { + case 0 => ZERO #:: ONE #:: s.toStream.map(CHAR) + case n => { + val rs = enum(n - 1, s) + rs #::: + (for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) #::: + (for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) #::: + (for (r1 <- rs) yield STAR(r1)) + } +} + +def benum(n: Int, s: String) = enum(n, s).map(internalise) + +def values(r: Rexp) : Set[Val] = r match { + case ZERO => Set() + case ONE => Set(Empty) + case PRED(_, s) => Set(Chr(s.head)) + case ALTS(List(r1, r2)) => (for (v1 <- values(r1)) yield Left(v1)) ++ + (for (v2 <- values(r2)) yield Right(v2)) + case SEQ(r1, r2) => for (v1 <- values(r1); v2 <- values(r2)) yield Sequ(v1, v2) + case STAR(r) => (Set(Stars(Nil)) ++ + (for (v <- values(r)) yield Stars(List(v)))) + // to do more would cause the set to be infinite +} + + +// tests about retrieve + +def tests_retrieve(r: Rexp) = { + val vs = values(r) + val a = internalise(r) + val as = bsimp(a) + for (v <- vs) { + println(s"Testing ${string(r)} and ${v}") + val bs1 = retrieve(a, v) + val bs2 = Try(Some(retrieve(as, decode(erase(as), bs1)))).getOrElse(None) + if (Some(bs1) != bs2) println(s"Disagree on ${string(r)}, ${v}") + if (Some(bs1) != bs2) Some((r, v)) else None + } +} + +println("Testing retrieve 1") +println(enum(1, "ab").map(tests_retrieve).toList) + +// an example where the property fails +val r = (ZERO ~ "b") | "a" +val a = internalise(r) +val as = bsimp(a) +val v = Right(Chr('a')) + +println("arexp " ++ astring(a)) +println("simplified " ++ astring(as)) + +val bs1 = retrieve(a, v) +encode(v) +retrieve(as, decode(erase(as), bs1)) + +//tests retrieve and vsimp + +def tests_retrieve_vsimp(ss: Set[String])(r: Rexp) = { + val a = internalise(r) + val as = bsimp(a) + for (s <- ss.par) yield { + val v = Try(Some(preblexing(a, s))).getOrElse(None) + if (v.isDefined) { + val bs1 = retrieve(a, v.get) + val bs2 = Try(retrieve(as, vsimp(v.get, as))).getOrElse(Nil) + if (bs1 != bs2) { + println(s"Disagree on ${astring(a)}, ${astring(as)}, ${s}") + println(s" ${v.get} and ${vsimp(v.get)}") + println(s" ${bs1} and ${bs2}") + Some(a, as, s, v.get, vsimp(v.get, as), bs1, bs2) + } else None + } else None + } +} + +println("Partial searching: ") +enum(2, "abc").map(tests_retrieve_vsimp(strs(3, "abc"))). + flatten.toSet.flatten.minBy(a => asize(a._1)) + +//tests derivatives and bsimp + +def tests_ders_bsimp(ss: Set[String])(r: Rexp) = { + val a = internalise(r) + for (s <- ss.par) yield { + val d1 = bsimp(bders(s.toList, bsimp(a))) + val d2 = bsimp(bders(s.toList, a)) + if (d1 != d2) { + println(s"Disagree on ${astring(a)}") + println(s" ${astring(d1)} and ${astring(d2)}") + Some(a, d1, d2) + } else None + } +} + +println("Partial searching: ") +enum(2, "abc").map(tests_ders_bsimp(strs(1, "abc"))). + flatten.toSet.flatten.minBy(a => asize(a._1)) + + + +//tests retrieve and lexing + +def tests_retrieve_lex(ss: Set[String])(r: Rexp) = { + val a = internalise(r) + val as = bsimp(a) + for (s <- ss.par) yield { + val bs1 = Try(Some(blex(a, s.toList))).getOrElse(None) + val bs2 = Try(Some(blex(as, s.toList))).getOrElse(None) + if (bs1 != bs2) { + println(s"Disagree on ${astring(a)}, ${astring(as)}, ${s}") + println(s" ${bs1} and ${bs2}") + Some(a, as, s) + } else None + } +} + +println("Partial searching: ") +enum(2, "abc").map(tests_retrieve_lex(strs(3, "abc"))).flatten.toSet + +//Disagree on [[c|b]|[a|c]], [c|b|a], a +//Right(Left(Chr(a))) and Right(Left(Chr(a))) +//List(S, Z) and List(Z, S) + +val s = "c" +val ar : Rexp = "a" +val br : Rexp = "b" +val cr : Rexp = "c" +val r1 : Rexp = ALT(ALT(cr, br), ALT(ar,cr)) +val a1 = internalise(r1) +val a2 = bsimp(a1) +val a2a = internalise(erase(a2)) + +astring(a1) +astring(a2) +astring(a2a) + +blexing(r1 ,s) +blexing_simp(r1 ,s) +val v1 = preblexing(a1, s) +val v2 = preblexing(a2a, s) +retrieve(a1, v1) +retrieve(a2, v2) + + +//tests blexing and lexing +def tests(ss: Set[String])(r: Rexp) = { + //println(s"Testing ${r}") + for (s <- ss.par) yield { + val res1 = Try(Some(lexing_simp(r, s))).getOrElse(None) + val res2 = Try(Some(blexing_simp(r, s))).getOrElse(None) + if (res1 != res2) + { println(s"Disagree on ${r} and ${s}") + println(s" ${res1} != ${res2}") + Some((r, s)) } else None + } +} + + +println("Partial searching: ") +enum(2, "abc").map(tests(strs(3, "abc"))).toSet + + + + diff -r db0ff630bbb7 -r 43e070803c1c thys/BitCoded.thy --- a/thys/BitCoded.thy Thu Apr 11 17:37:00 2019 +0100 +++ b/thys/BitCoded.thy Fri May 10 11:56:37 2019 +0100 @@ -400,13 +400,65 @@ shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" using assms apply(induct r arbitrary: v rule: erase.induct) - apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) - apply(case_tac va) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(case_tac "c = ca") + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(rename_tac "r\<^sub>1" "r\<^sub>2" rs v) + apply(erule Prf_elims) + apply(simp) + apply(simp) + apply(case_tac rs) + apply(simp) + apply(simp) + apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) apply(simp) - apply(auto) - by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) + apply(case_tac "nullable (erase r1)") + apply(simp) + apply(erule Prf_elims) + apply(subgoal_tac "bnullable r1") + prefer 2 + using bnullable_correctness apply blast + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(subgoal_tac "bnullable r1") + prefer 2 + using bnullable_correctness apply blast + apply(simp) + apply(simp add: retrieve_fuse2) + apply(simp add: bmkeps_retrieve) + apply(simp) + apply(erule Prf_elims) + apply(simp) + using bnullable_correctness apply blast + apply(rename_tac bs r v) + apply(simp) + apply(erule Prf_elims) + apply(clarify) + apply(erule Prf_elims) + apply(clarify) + apply(subst injval.simps) + apply(simp del: retrieve.simps) + apply(subst retrieve.simps) + apply(subst retrieve.simps) + apply(simp) + apply(simp add: retrieve_fuse2) + done + lemma MAIN_decode: assumes "\ v : ders s r" shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" @@ -425,18 +477,23 @@ Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact have asm: "\ v : ders (s @ [c]) r" by fact then have asm2: "\ injval (ders s r) c v : ders s r" - by(simp add: Prf_injval ders_append) + by (simp add: Prf_injval ders_append) have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" by (simp add: flex_append) also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" using asm2 IH by simp also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" - using asm by(simp_all add: bder_retrieve ders_append) + using asm by (simp_all add: bder_retrieve ders_append) finally show "Some (flex r id (s @ [c]) v) = decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) qed +definition blex where + "blex a s \ if bnullable (bders a s) then Some (bmkeps (bders a s)) else None" + + + definition blexer where "blexer r s \ if bnullable (bders (intern r) s) then decode (bmkeps (bders (intern r) s)) r else None" @@ -513,6 +570,9 @@ decode (bmkeps (bders_simp (intern r) s)) r else None" + + + lemma asize0: shows "0 < asize r" apply(induct r) @@ -964,6 +1024,20 @@ apply(auto) by (metis (mono_tags, hide_lams) imageE nn1c set_map) +lemma nn1d: + assumes "bsimp r = AALTs bs rs" + shows "\r1 \ set rs. \ bs. r1 \ AALTs bs rs2" + using nn1b assms + by (metis nn1qq) + +lemma nn_flts: + assumes "nonnested (AALTs bs rs)" + shows "\r \ set (flts rs). nonalt r" + using assms + apply(induct rs arbitrary: bs rule: flts.induct) + apply(auto) + done + lemma rt: shows "sum_list (map asize (flts (map bsimp rs))) \ sum_list (map asize rs)" apply(induct rs) @@ -973,6 +1047,16 @@ apply(simp) by (smt add_le_cancel_right add_mono bsimp_size flts.simps(1) flts_size k0 le_iff_add list.simps(9) map_append sum_list.Cons sum_list.append trans_le_add1) +lemma bsimp_AALTs_qq: + assumes "1 < length rs" + shows "bsimp_AALTs bs rs = AALTs bs rs" + using assms + apply(case_tac rs) + apply(simp) + apply(case_tac list) + apply(simp_all) + done + lemma flts_idem: assumes "\r \ set rs. bsimp (bsimp r) = bsimp r" shows "flts (map bsimp (flts (map bsimp rs))) = flts (map bsimp rs)" @@ -1007,7 +1091,7 @@ apply(simp) apply(case_tac a) apply(simp_all) - sorry + oops lemma bsimp_AALTs_idem: (*assumes "\r \ set rs. bsimp (bsimp r) = bsimp r \ nonalt (bsimp r)" *) @@ -1091,6 +1175,149 @@ prefer 3 oops +lemma ww: + shows "bsimp_AALTs bs [r] = fuse bs r" + by simp + +lemma flts_0: + assumes "nonnested (AALTs bs rs)" + shows "\r \ set (flts rs). r \ AZERO" + using assms + apply(induct rs arbitrary: bs rule: flts.induct) + apply(simp) + apply(simp) + defer + apply(simp) + apply(simp) + apply(simp) +apply(simp) + apply(rule ballI) + apply(simp) + done + +lemma q1: + shows "AZERO \ set (flts (map bsimp rs))" + apply(induct rs) + apply(simp) + apply(simp) + apply(case_tac rs) + apply(simp) + +lemma cc: + assumes "bsimp (fuse bs' r) = (AALTs bs rs)" + shows "\r \ set rs. r \ AZERO" + using assms + apply(induct r arbitrary: rs bs bs' rule: bsimp.induct) + apply(simp) + apply(case_tac "bsimp r1 = AZERO") + apply simp + apply(case_tac "bsimp r2 = AZERO") + apply(simp) + apply(case_tac "\bs'. bsimp r1 = AONE bs'") + apply(auto)[1] + apply (simp add: bsimp_ASEQ0) + apply(case_tac "\bs'. bsimp r1 = AONE bs'") + apply(auto)[2] + apply (simp add: bsimp_ASEQ2) + using bsimp_fuse apply fastforce + apply (simp add: bsimp_ASEQ1) + prefer 2 + apply(simp) + defer + apply(simp) + apply(simp) + apply(simp) + (* AALT case *) + apply(simp only: fuse.simps) + apply(simp) + apply(case_tac "flts (map bsimp rs)") + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + apply(case_tac a) + apply(simp_all) + apply(auto) + apply (metis ex_map_conv list.set_intros(1) nn1b nn1c nonalt.simps(1)) + apply(case_tac rs) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp) + + + apply(subgoal_tac "\r \ set (flts (map bsimp rs)). r \ AZERO") + prefer 2 + apply(rule_tac bs="bs' @ bs1" in flts_0) + + + thm bsimp_AALTs_qq + apply(case_tac "1 < length rs") + apply(drule_tac bsimp_AALTs_qq) + apply(subgoal_tac "nonnested (AALTs bs rsa)") + prefer 2 + apply (metis nn1b) + apply(rule ballI) + apply(simp) + apply(drule_tac x="r" in meta_spec) + apply(simp) + (* HERE *) + apply(drule flts_0) + + + + apply(simp) + + + + + apply(subst + + apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) + + prefer 2 + + + apply(induct r arbitrary: rs bs bs' rule: bsimp.induct) + apply(auto) + apply(case_tac "bsimp r1 = AZERO") + apply simp + apply(case_tac "bsimp r2 = AZERO") + apply(simp) + apply(case_tac "\bs'. bsimp r1 = AONE bs'") + apply(auto) + apply (simp add: bsimp_ASEQ0) + apply(case_tac "\bs'. bsimp r1 = AONE bs'") + apply(auto) + apply (simp add: bsimp_ASEQ2) + using bsimp_fuse apply fastforce + apply (simp add: bsimp_ASEQ1) + + + + apply(subst + + apply (sm t arexp.distinct(15) arexp.distinct(21) arexp.distinct(25) arexp.distinct(29) arexp.inject(4) b1 fuse.elims) + + prefer 2 + + + +lemma ww1: + assumes "flts [r1] = [r2]" "r1 \ AZERO" + shows "r1 = r2" + using assms + apply(case_tac r1) + apply(simp) + apply(simp) + apply(simp) + apply(simp) + prefer 2 + apply(simp) + apply(simp) + apply(auto) + oops + lemma bsimp_idem: shows "bsimp (bsimp r) = bsimp r" apply(induct r taking: "asize" rule: measure_induct) @@ -1104,8 +1331,87 @@ apply (simp add: bsimp_ASEQ_idem) apply(clarify) apply(case_tac x52) + apply(simp) + (* AALT case where rs is of the form _ # _ *) + apply(clarify) apply(simp) - apply(simp) + apply(case_tac "length (flts (bsimp a # map bsimp list)) \ 1") + prefer 2 + apply(subst bsimp_AALTs_qq) + apply(auto)[1] + apply(simp) + prefer 2 + apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \ + length (flts (bsimp a # map bsimp list)) = 1") + prefer 2 + apply(auto)[1] + using le_SucE apply blast + apply(erule disjE) + apply(simp) + apply(simp) + apply(subst k0) + apply(subst (2) k0) + apply(subst (asm) k0) + apply(simp) + apply(subgoal_tac "length (flts [bsimp a]) = 1 \ + length (flts (map bsimp list)) = 1") + prefer 2 + apply linarith + apply(erule disjE) + apply(simp) + prefer 2 + apply(simp) + apply(drule_tac x="AALTs x51 list" in spec) + apply(drule mp) + apply(simp) + using asize0 apply blast + apply(simp) + apply(frule_tac x="a" in spec) + apply(drule mp) + apply(simp) + apply(subgoal_tac "\r. flts [bsimp a] = [r]") + prefer 2 + apply (simp add: length_Suc_conv) + apply(clarify) + apply(simp only: ) + apply(case_tac "bsimp a = AZERO") + apply simp + apply(case_tac "\bs rs. bsimp a = AALTs bs rs") + apply(clarify) + apply(simp) + apply(drule_tac x="AALTs bs rs" in spec) + apply(drule mp) + apply(simp) + apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1) + apply(simp) + + apply(subst ww) + apply(subst ww) + apply(frule_tac x="fuse x51 r" in spec) + apply(drule mp) + apply(simp) + apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons) + apply(case_tac "bsimp a = AZERO") + apply simp + apply(case_tac "\bs rs. bsimp a = AALTs bs rs") + apply(clarify) + + defer + + apply( + apply(case_tac a) + apply(simp_all) + apply(subgoal_tac "\r. flts [bsimp a] = [r]") + prefer 2 + apply (simp add: length_Suc_conv) + apply auto[1] + apply(case_tac + apply(clarify) + + defer + apply(auto)[1] + + apply(subst k0) apply(subst (2) k0) apply(case_tac "bsimp a = AZERO") @@ -1480,7 +1786,7 @@ defer apply(subst bsimp_ASEQ1) - using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce + using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force using L_bsimp_erase L_ lemma retrieve_XXX: @@ -1744,7 +2050,7 @@ apply(auto elim!: Prf_elims)[1] apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO") apply(simp) - apply (metis L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse) + apply (met is L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse) apply(case_tac "\bs. bsimp (fuse [Z] (bder c r)) = AONE bs") apply(clarify) apply(subgoal_tac "L (der c (erase r)) = {[]}") @@ -1960,7 +2266,7 @@ apply(subst blexer_def) apply(subgoal_tac "bnullable (bders (intern r) (a # s))") prefer 2 - apply (metis Posix_injval blexer_correctness blexer_def lexer_correctness(2)) + apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2)) apply(simp) @@ -1992,6 +2298,198 @@ apply(simp) apply(subst bnullable_correctness[symmetric]) apply(simp) + oops + +lemma flts_append: + "flts (xs1 @ xs2) = flts xs1 @ flts xs2" + apply(induct xs1 arbitrary: xs2 rule: rev_induct) + apply(auto) + apply(case_tac xs) + apply(auto) + apply(case_tac x) + apply(auto) + apply(case_tac x) + apply(auto) + done + +lemma flts_bsimp: + "flts (map bsimp rs) = map bsimp (flts rs)" +apply(induct rs taking: size rule: measure_induct) + apply(case_tac x) + apply(simp) + apply(simp) + apply(induct rs rule: flts.induct) + apply(simp) + apply(simp) + defer + apply(simp) + apply(simp) + defer + apply(simp) + apply(subst List.list.map(2)) + apply(simp only: flts.simps) + apply(subst k0) + apply(subst map_append) + apply(simp only:) + apply(simp del: bsimp.simps) + apply(case_tac rs1) + apply(simp) + apply(simp) + apply(case_tac list) + apply(simp_all) + thm map + apply(subst map.simps) + apply(auto) + defer + apply(case_tac "(bsimp va) = AZERO") + apply(simp) + + using b3 apply for ce + apply(case_tac "(bsimp a2) = AZERO") + apply(simp) + apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) + apply(case_tac "\bs. (bsimp a1) = AONE bs") + apply(clarify) + apply(simp) + + +lemma XXX: + shows "bsimp (bsimp a) = bsimp a" + sorry + +lemma bder_fuse: + shows "bder c (fuse bs a) = fuse bs (bder c a)" + apply(induct a arbitrary: bs c) + apply(simp_all) + done + +lemma XXX2: + shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)" + apply(induct a arbitrary: c) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply(auto)[1] + apply(case_tac "(bsimp a1) = AZERO") + apply(simp) + using b3 apply force + apply(case_tac "(bsimp a2) = AZERO") + apply(simp) + apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1)) + apply(case_tac "\bs. (bsimp a1) = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ2) + apply(subgoal_tac "bmkeps a1 = bs") + prefer 2 + apply (simp add: bmkeps_simp) + apply(simp) + apply(subst (1) bsimp_fuse[symmetric]) + defer + apply(subst bsimp_ASEQ1) + apply(simp) + apply(simp) + apply(simp) + apply(auto)[1] + apply (metis XXX bmkeps_simp bsimp_fuse) + using b3 apply blast + apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1) + apply(simp) + prefer 2 + apply(subst bder_fuse) + apply(subst bsimp_fuse[symmetric]) + apply(simp) + sorry + + +thm bsimp_AALTs.simps +thm bsimp.simps +thm flts.simps + +lemma XXX3: + "bsimp (bders (bsimp r) s) = bsimp (bders r s)" + apply(induct s arbitrary: r rule: rev_induct) + apply(simp) + apply (simp add: XXX) + apply(simp add: bders_append) + apply(subst (2) XXX2[symmetric]) + apply(subst XXX2[symmetric]) + apply(drule_tac x="r" in meta_spec) + apply(simp) + done + +lemma XXX4: + "bders_simp (bsimp r) s = bsimp (bders r s)" + apply(induct s arbitrary: r) + apply(simp) + apply(simp) + by (metis XXX2) + + +lemma + assumes "bnullable (bder c r)" "bnullable (bder c (bsimp r))" + shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))" + using assms + apply(induct r arbitrary: c) + apply(simp) + apply(simp) + apply(simp) + prefer 3 + apply(simp) + apply(auto)[1] + apply(case_tac "(bsimp r1) = AZERO") + apply(simp) + apply(case_tac "(bsimp r2) = AZERO") + apply(simp) + apply (simp add: bsimp_ASEQ0) + apply(case_tac "\bs. (bsimp r1) = AONE bs") + apply(clarify) + apply(simp) + apply(subgoal_tac "bnullable r1") + prefer 2 + using b3 apply force + apply(simp) + apply(simp add: bsimp_ASEQ2) + prefer 2 + + + + apply(subst bsimp_ASEQ2) + + + + + + +lemma + assumes "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)" + shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)" + using assms + apply(induct s2 arbitrary: a s1) + apply(simp) + using bmkeps_simp apply blast + apply(simp add: bders_append) + apply(drule_tac x="aa" in meta_spec) + apply(drule_tac x="s1 @ [a]" in meta_spec) + apply(drule meta_mp) + apply(simp add: bders_append) + apply(simp add: bders_append) + apply(drule meta_mp) + apply (metis b4 bders.simps(2) bders_simp.simps(2)) + apply(simp) + + apply (met is b4 bders.simps(2) bders_simp.simps(2)) + + + + using b3 apply blast + using b3 apply auto[1] + apply(auto simp add: blex_def) + prefer 3 + + diff -r db0ff630bbb7 -r 43e070803c1c thys/Exercises.thy --- a/thys/Exercises.thy Thu Apr 11 17:37:00 2019 +0100 +++ b/thys/Exercises.thy Fri May 10 11:56:37 2019 +0100 @@ -50,9 +50,8 @@ apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) using Nil_is_append_conv apply blast apply blast -apply(auto) -using Star_cstring - by (metis concat_eq_Nil_conv) + apply(auto) + by (metis Star_decomp hd_Cons_tl list.distinct(1)) lemma atmostempty_correctness_aux: shows "atmostempty r \ \ somechars r" @@ -110,8 +109,22 @@ lemma Star_atmostempty: assumes "A \ {[]}" shows "A\ \ {[]}" -using assms -using Star_cstring concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce + using assms + using Star_decomp concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD + apply(auto) +proof - + fix x :: "char list" + assume a1: "x \ A\" + assume "\c x A. c # x \ A\ \ \s1 s2. x = s1 @ s2 \ c # s1 \ A \ s2 \ A\" + then have f2: "\cs C c. \csa. c # csa \ C \ c # cs \ C\" + by auto + obtain cc :: "char list \ char" and ccs :: "char list \ char list" where + "\cs. cs = [] \ cc cs # ccs cs = cs" + by (metis (no_types) list.exhaust) + then show "x = []" + using f2 a1 by (metis assms empty_iff insert_iff list.distinct(1) subset_singletonD) +qed + lemma Star_empty_string_finite: shows "finite ({[]}\)" diff -r db0ff630bbb7 -r 43e070803c1c thys/Journal/Paper.thy --- a/thys/Journal/Paper.thy Thu Apr 11 17:37:00 2019 +0100 +++ b/thys/Journal/Paper.thy Fri May 10 11:56:37 2019 +0100 @@ -1686,6 +1686,73 @@ *} +section {* HERE *} + +text {* + \begin{center} + \begin{tabular}{llcl} + 1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ + 2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ + 3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ + 4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\ + 4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\ + 4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ & + @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\ + 5) & @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + 6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ + \end{tabular} + \end{center} + + \begin{lemma} + @{thm [mode=IfThen] bder_retrieve} + \end{lemma} + + \begin{proof} + By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are + straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to + @{term ZERO}. This means @{term "\ v : ZERO"} cannot hold. Similarly in case of rule 3) + where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption + we know @{term "\ v : ONE"}, which implies @{term "v = Void"}. The equation follows by + simplification of left- and right-hand side. In case @{term "c \ d"} we have again + @{term "\ v : ZERO"}, which cannot hold. + + For rule 4a) we have again @{term "\ v : ZERO"}. The property holds by IH for rule 4b). + The induction hypothesis is + \[ + @{term "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"} + \] + which is what left- and right-hand side simplify to. The slightly more interesting case + is for 4c). By assumption we have + @{term "\ v : ALT (der c (erase r\<^sub>1)) (der c (erase (AALTs bs (r\<^sub>2 # rs))))"}. This means we + have either (*) @{term "\ v1 : der c (erase r\<^sub>1)"} with @{term "v = Left v1"} or + (**) @{term "\ v2 : der c (erase (AALTs bs (r\<^sub>2 # rs)))"} with @{term "v = Right v2"}. + The former case is straightforward by simplification. The second case is \ldots TBD. + + Rule 5) TBD. + + Finally for rule 6) the reasoning is as follows: By assumption we have + @{term "\ v : SEQ (der c (erase r)) (STAR (erase r))"}. This means we also have + @{term "v = Seq v1 v2"}, @{term "\ v1 : der c (erase r)"} and @{term "v2 = Stars vs"}. + We want to prove + \begin{align} + & @{term "retrieve (ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)) v"}\\ + &= @{term "retrieve (ASTAR bs r) (injval (STAR (erase r)) c v)"} + \end{align} + The right-hand side @{term inj}-expression is equal to + @{term "Stars (injval (erase r) c v1 # vs)"}, which means the @{term retrieve}-expression + simplifies to + \[ + @{term "bs @ [Z] @ retrieve r (injval (erase r) c v1) @ retrieve (ASTAR [] r) (Stars vs)"} + \] + The left-hand side (3) above simplifies to + \[ + @{term "bs @ retrieve (fuse [Z] (bder c r)) v1 @ retrieve (ASTAR [] r) (Stars vs)"} + \] + We can move out the @{term "fuse [Z]"} and then use the IH to show that left-hand side + and right-hand side are equal. This completes the proof. + \end{proof} +*} + (*<*) diff -r db0ff630bbb7 -r 43e070803c1c thys/journal.pdf Binary file thys/journal.pdf has changed