Binary file Literature/boost-semantics.pdf has changed

Binary file Literature/hein-proj-thesis.pdf has changed

--- a/progs/scala/re-bit.scala	Wed May 16 20:58:39 2018 +0100
+++ b/progs/scala/re-bit.scala	Wed Aug 15 13:48:57 2018 +0100
@@ -9,7 +9,7 @@
 case class ALT(r1: Rexp, r2: 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
+
 
 abstract class ARexp 
 case object AZERO extends ARexp
@@ -26,7 +26,7 @@
 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
+
    
 // some convenience for typing in regular expressions
 def charlist2rexp(s : List[Char]): Rexp = s match {
@@ -48,9 +48,73 @@
   def % = STAR(s)
   def ~ (r: Rexp) = SEQ(s, r)
   def ~ (r: String) = SEQ(s, r)
-  def $ (r: Rexp) = RECD(s, 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 ALT(r1, r2) => nullable(r1) || nullable(r2)
+  case SEQ(r1, r2) => nullable(r1) && nullable(r2)
+  case STAR(_) => 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 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(r) => SEQ(der(c, r), STAR(r))
+}
+
+// derivative w.r.t. a string (iterates der)
+def ders (s: List[Char], r: Rexp) : Rexp = s match {
+  case Nil => r
+  case c::s => ders(s, der(c, r))
 }
 
+// mkeps and injection part
+def mkeps(r: Rexp) : Val = r match {
+  case ONE => Empty
+  case ALT(r1, r2) => 
+    if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
+  case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
+  case STAR(r) => Stars(Nil)
+}
+
+
+def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
+  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
+  case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
+  case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
+  case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
+  case (ALT(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
+  case (ALT(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
+  case (CHAR(d), Empty) => Chr(c) 
+}
+
+// main lexing function (produces a value)
+// - no simplification
+def lex(r: Rexp, s: List[Char]) : Val = s match {
+  case Nil => if (nullable(r)) mkeps(r) 
+              else throw new Exception("Not matched")
+  case c::cs => inj(r, c, lex(der(c, r), cs))
+}
+
+def lexing(r: Rexp, s: String) : Val = lex(r, s.toList)
+
+
+
+// Bitcoded + Annotation
+//=======================
+
 // translation into ARexps
 def fuse(bs: List[Boolean], r: ARexp) : ARexp = r match {
   case AZERO => AZERO
@@ -68,11 +132,22 @@
   case ALT(r1, r2) => AALT(Nil, fuse(List(false), internalise(r1)), fuse(List(true), internalise(r2)))
   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" | ""))
 
+def retrieve(r: ARexp, v: Val) : List[Boolean] = (r, v) match {
+  case (AONE(bs), Empty) => bs
+  case (ACHAR(bs, c), Chr(d)) => bs
+  case (AALT(bs, r1, r2), Left(v)) => bs ++ retrieve(r1, v)
+  case (AALT(bs, r1, r2), Right(v)) => bs ++ retrieve(r2, v)
+  case (ASEQ(bs, r1, r2), Sequ(v1, v2)) => 
+    bs ++ retrieve(r1, v1) ++ retrieve(r2, v2)
+  case (ASTAR(bs, r), Stars(Nil)) => bs ++ List(true)
+  case (ASTAR(bs, r), Stars(v :: vs)) => 
+     bs ++ List(false) ++ retrieve(r, v) ++ retrieve(ASTAR(Nil, r), Stars(vs))
+}
+
 
 def decode_aux(r: Rexp, bs: List[Boolean]) : (Val, List[Boolean]) = (r, bs) match {
   case (ONE, bs) => (Empty, bs)
@@ -96,10 +171,6 @@
     (Stars(v::vs), bs2)
   }
   case (STAR(_), true::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: List[Boolean]) = decode_aux(r, bs) match {
@@ -107,63 +178,73 @@
   case _ => throw new Exception("Not decodable")
 }
 
+def encode(v: Val) : List[Boolean] = v match {
+  case Empty => Nil
+  case Chr(c) => Nil
+  case Left(v) => false :: encode(v)
+  case Right(v) => true :: encode(v)
+  case Sequ(v1, v2) => encode(v1) ::: encode(v2)
+  case Stars(Nil) => List(true)
+  case Stars(v::vs) => false :: encode(v) ::: encode(Stars(vs))
+}
+
+
 // nullable function: tests whether the aregular 
 // expression can recognise the empty string
-def nullable (r: ARexp) : Boolean = r match {
+def anullable (r: ARexp) : Boolean = r match {
   case AZERO => false
   case AONE(_) => true
   case ACHAR(_,_) => false
-  case AALT(_, r1, r2) => nullable(r1) || nullable(r2)
-  case ASEQ(_, r1, r2) => nullable(r1) && nullable(r2)
+  case AALT(_, r1, r2) => anullable(r1) || anullable(r2)
+  case ASEQ(_, r1, r2) => anullable(r1) && anullable(r2)
   case ASTAR(_, _) => true
 }
 
 def mkepsBC(r: ARexp) : List[Boolean] = r match {
   case AONE(bs) => bs
   case AALT(bs, r1, r2) => 
-    if (nullable(r1)) bs ++ mkepsBC(r1) else bs ++ mkepsBC(r2)
+    if (anullable(r1)) bs ++ mkepsBC(r1) else bs ++ mkepsBC(r2)
   case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)
   case ASTAR(bs, r) => bs ++ List(true)
 }
 
 // derivative of a regular expression w.r.t. a character
-def der (c: Char, r: ARexp) : ARexp = r match {
+def ader(c: Char, r: ARexp) : ARexp = r match {
   case AZERO => AZERO
   case AONE(_) => AZERO
   case ACHAR(bs, d) => if (c == d) AONE(bs) else AZERO
-  case AALT(bs, r1, r2) => AALT(bs, der(c, r1), der(c, r2))
+  case AALT(bs, r1, r2) => AALT(bs, ader(c, r1), ader(c, r2))
   case ASEQ(bs, r1, r2) => 
-    if (nullable(r1)) AALT(bs, ASEQ(Nil, der(c, r1), r2), fuse(mkepsBC(r1), der(c, r2)))
-    else ASEQ(bs, der(c, r1), r2)
-  case ASTAR(bs, r) => ASEQ(bs, fuse(List(false), der(c, r)), ASTAR(Nil, r))
+    if (anullable(r1)) AALT(bs, ASEQ(Nil, ader(c, r1), r2), fuse(mkepsBC(r1), ader(c, r2)))
+    else ASEQ(bs, ader(c, r1), r2)
+  case ASTAR(bs, r) => ASEQ(bs, fuse(List(false), ader(c, r)), ASTAR(Nil, r))
 }
 
 // derivative w.r.t. a string (iterates der)
 @tailrec
-def ders (s: List[Char], r: ARexp) : ARexp = s match {
+def aders (s: List[Char], r: ARexp) : ARexp = s match {
   case Nil => r
-  case c::s => ders(s, der(c, r))
+  case c::s => aders(s, ader(c, r))
 }
 
 // main unsimplified lexing function (produces a value)
-def lex(r: ARexp, s: List[Char]) : List[Boolean] = s match {
-  case Nil => if (nullable(r)) mkepsBC(r) else throw new Exception("Not matched")
-  case c::cs => lex(der(c, r), cs)
+def alex(r: ARexp, s: List[Char]) : List[Boolean] = s match {
+  case Nil => if (anullable(r)) mkepsBC(r) else throw new Exception("Not matched")
+  case c::cs => alex(ader(c, r), cs)
 }
 
-def pre_lexing(r: Rexp, s: String) = lex(internalise(r), s.toList)
-def lexing(r: Rexp, s: String) : Val = decode(r, lex(internalise(r), s.toList))
+def pre_alexing(r: ARexp, s: String)  : List[Boolean] = alex(r, s.toList)
+def alexing(r: Rexp, s: String) : Val = decode(r, pre_alexing(internalise(r), s))
 
 
-
-def simp(r: ARexp): ARexp = r match {
-  case ASEQ(bs1, r1, r2) => (simp(r1), simp(r2)) match {
+def asimp(r: ARexp): ARexp = r match {
+  case ASEQ(bs1, r1, r2) => (asimp(r1), asimp(r2)) match {
       case (AZERO, _) => AZERO
       case (_, AZERO) => AZERO
       case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
       case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
   }
-  case AALT(bs1, r1, r2) => (simp(r1), simp(r2)) match {
+  case AALT(bs1, r1, r2) => (asimp(r1), asimp(r2)) match {
       case (AZERO, r2s) => fuse(bs1, r2s)
       case (r1s, AZERO) => fuse(bs1, r1s)
       case (r1s, r2s) => AALT(bs1, r1s, r2s)
@@ -171,12 +252,14 @@
   case r => r
 }
 
-def lex_simp(r: ARexp, s: List[Char]) : List[Boolean] = s match {
-  case Nil => if (nullable(r)) mkepsBC(r) else throw new Exception("Not matched")
-  case c::cs => lex(simp(der(c, r)), cs)
+def alex_simp(r: ARexp, s: List[Char]) : List[Boolean] = s match {
+  case Nil => if (anullable(r)) mkepsBC(r) 
+              else throw new Exception("Not matched")
+  case c::cs => alex(asimp(ader(c, r)), cs)
 }
 
-def lexing_simp(r: Rexp, s: String) : Val = decode(r, lex_simp(internalise(r), s.toList))
+def alexing_simp(r: Rexp, s: String) : Val = 
+  decode(r, alex_simp(internalise(r), s.toList))
 
 
 
@@ -188,7 +271,6 @@
   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
@@ -199,7 +281,6 @@
   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 Tests
@@ -214,70 +295,27 @@
 
 
 val rf = ("a" | "ab") ~ ("ab" | "")
-println(pre_lexing(rf, "ab"))
-println(lexing(rf, "ab"))
-println(lexing_simp(rf, "ab"))
+println(pre_alexing(internalise(rf), "ab"))
+println(alexing(rf, "ab"))
+println(alexing_simp(rf, "ab"))
 
 val r0 = ("a" | "ab") ~ ("b" | "")
-println(pre_lexing(r0, "ab"))
-println(lexing(r0, "ab"))
-println(lexing_simp(r0, "ab"))
+println(pre_alexing(internalise(r0), "ab"))
+println(alexing(r0, "ab"))
+println(alexing_simp(r0, "ab"))
 
 val r1 = ("a" | "ab") ~ ("bcd" | "cd")
-println(lexing(r1, "abcd"))
-println(lexing_simp(r1, "abcd"))
-
-println(lexing((("" | "a") ~ ("ab" | "b")), "ab"))
-println(lexing_simp((("" | "a") ~ ("ab" | "b")), "ab"))
-
-println(lexing((("" | "a") ~ ("b" | "ab")), "ab"))
-println(lexing_simp((("" | "a") ~ ("b" | "ab")), "ab"))
+println(alexing(r1, "abcd"))
+println(alexing_simp(r1, "abcd"))
 
-println(lexing((("" | "a") ~ ("c" | "ab")), "ab"))
-println(lexing_simp((("" | "a") ~ ("c" | "ab")), "ab"))
-
-
-// Two Simple Tests for the While Language
-//========================================
-
-// Lexing Rules 
+println(alexing((("" | "a") ~ ("ab" | "b")), "ab"))
+println(alexing_simp((("" | "a") ~ ("ab" | "b")), "ab"))
 
-def PLUS(r: Rexp) = r ~ r.%
-val SYM = "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z"
-val DIGIT = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
-val ID = SYM ~ (SYM | DIGIT).% 
-val NUM = PLUS(DIGIT)
-val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false"
-val SEMI: Rexp = ";"
-val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/"
-val WHITESPACE = PLUS(" " | "\n" | "\t")
-val RPAREN: Rexp = ")"
-val LPAREN: Rexp = "("
-val BEGIN: Rexp = "{"
-val END: Rexp = "}"
-val STRING: Rexp = "\"" ~ SYM.% ~ "\""
+println(alexing((("" | "a") ~ ("b" | "ab")), "ab"))
+println(alexing_simp((("" | "a") ~ ("b" | "ab")), "ab"))
 
-val WHILE_REGS = (("k" $ KEYWORD) | 
-                  ("i" $ ID) | 
-                  ("o" $ OP) | 
-                  ("n" $ NUM) | 
-                  ("s" $ SEMI) | 
-                  ("str" $ STRING) |
-                  ("p" $ (LPAREN | RPAREN)) | 
-                  ("b" $ (BEGIN | END)) | 
-                  ("w" $ WHITESPACE)).%
-
-println("prog0 test")
-
-val prog0 = """read n"""
-println(env(lexing(WHILE_REGS, prog0)))
-println(env(lexing_simp(WHILE_REGS, prog0)))
-
-println("prog1 test")
-
-val prog1 = """read  n; write (n)"""
-println(env(lexing(WHILE_REGS, prog1)))
-println(env(lexing_simp(WHILE_REGS, prog1)))
+println(alexing((("" | "a") ~ ("c" | "ab")), "ab"))
+println(alexing_simp((("" | "a") ~ ("c" | "ab")), "ab"))
 
 
 // Sulzmann's tests
@@ -285,13 +323,158 @@
 
 val sulzmann = ("a" | "b" | "ab").%
 
-println(lexing(sulzmann, "a" * 10))
-println(lexing_simp(sulzmann, "a" * 10))
+println(alexing(sulzmann, "a" * 10))
+println(alexing_simp(sulzmann, "a" * 10))
 
-for (i <- 1 to 6501 by 500) {
-  println(i + ": " + "%.5f".format(time_needed(1, lexing_simp(sulzmann, "a" * i))))
+for (i <- 1 to 4001 by 500) {
+  println(i + ": " + "%.5f".format(time_needed(1, alexing_simp(sulzmann, "a" * i))))
 }
 
 for (i <- 1 to 16 by 5) {
-  println(i + ": " + "%.5f".format(time_needed(1, lexing_simp(sulzmann, "ab" * i))))
+  println(i + ": " + "%.5f".format(time_needed(1, alexing_simp(sulzmann, "ab" * i))))
+}
+
+
+
+
+// some automatic testing
+
+def clear() = {
+  print("")
+  //print("\33[H\33[2J")
+}
+
+// enumerates regular expressions until a certain depth
+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))
+  }
+}
+
+
+//enum(2, "ab").size
+//enum(3, "ab").size
+//enum(3, "abc").size
+//enum(4, "ab").size
+
+import scala.util.Try
+
+def test_mkeps(r: Rexp) = {
+  val res1 = Try(Some(mkeps(r))).getOrElse(None)
+  val res2 = Try(Some(decode(r, mkepsBC(internalise(r))))).getOrElse(None) 
+  if (res1 != res2) println(s"Mkeps disagrees on ${r}")
+  if (res1 != res2) Some(r) else (None)
+}
+
+println("Testing mkeps")
+enum(2, "ab").map(test_mkeps).toSet
+//enum(3, "ab").map(test_mkeps).toSet
+//enum(3, "abc").map(test_mkeps).toSet
+
+
+//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)
+  }
+}
+
+//tests lexing and lexingB
+def tests_inj(ss: Set[String])(r: Rexp) = {
+  clear()
+  println(s"Testing ${r}")
+  for (s <- ss.par) yield {
+    val res1 = Try(Some(alexing(r, s))).getOrElse(None)
+    val res2 = Try(Some(alexing_simp(r, s))).getOrElse(None)
+    if (res1 != res2) println(s"Disagree on ${r} and ${s}")
+    if (res1 != res2) println(s"   ${res1} !=  ${res2}")
+    if (res1 != res2) Some((r, s)) else None
+  }
 }
+
+//println("Testing lexing 1")
+//enum(2, "ab").map(tests_inj(strs(2, "ab"))).toSet
+//println("Testing lexing 2")
+//enum(2, "ab").map(tests_inj(strs(3, "abc"))).toSet
+//println("Testing lexing 3")
+//enum(3, "ab").map(tests_inj(strs(3, "abc"))).toSet
+
+
+def tests_alexer(ss: Set[String])(r: Rexp) = {
+  clear()
+  println(s"Testing ${r}")
+  for (s <- ss.par) yield {
+    val d = der('b', r)
+    val ad = ader('b', internalise(r))
+    val res1 = Try(Some(encode(inj(r, 'a', alexing(d, s))))).getOrElse(None)
+    val res2 = Try(Some(pre_alexing(ad, s))).getOrElse(None)
+    if (res1 != res2) println(s"Disagree on ${r} and 'a'::${s}")
+    if (res1 != res2) println(s"   ${res1} !=  ${res2}")
+    if (res1 != res2) Some((r, s)) else None
+  }
+}
+
+println("Testing alexing 1")
+println(enum(2, "ab").map(tests_alexer(strs(2, "ab"))).toSet)
+
+
+def values(r: Rexp) : Set[Val] = r match {
+  case ZERO => Set()
+  case ONE => Set(Empty)
+  case CHAR(c) => Set(Chr(c))
+  case ALT(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
+}
+
+def tests_ader(c: Char)(r: Rexp) = {
+  val d = der(c, r)
+  val vals = values(d)
+  for (v <- vals) {
+    println(s"Testing ${r} and ${v}")
+    val res1 = retrieve(ader(c, internalise(r)), v)
+    val res2 = encode(inj(r, c, decode(d, retrieve(internalise(der(c, r)), v))))
+    if (res1 != res2) println(s"Disagree on ${r}, ${v} and der = ${d}")
+    if (res1 != res2) println(s"   ${res1} !=  ${res2}")
+    if (res1 != res2) Some((r, v)) else None
+  }
+}
+
+println("Testing ader/der")
+println(enum(2, "ab").map(tests_ader('a')).toSet)
+
+val er = SEQ(ONE,CHAR('a')) 
+val ev = Right(Empty) 
+val ed = ALT(SEQ(ZERO,CHAR('a')),ONE)
+
+retrieve(internalise(ed), ev) // => [true]
+internalise(er)
+ader('a', internalise(er))
+retrieve(ader('a', internalise(er)), ev) // => []
+decode(ed, List(true)) // gives the value for derivative
+decode(er, List())     // gives the value for original value
+
+
+val dr = STAR(CHAR('a'))
+val dr_der = SEQ(ONE,STAR(CHAR('a'))) // derivative of dr
+val dr_val = Sequ(Empty,Stars(List())) // value of dr_def
+
+
+val res1 = retrieve(internalise(der('a', dr)), dr_val) // => [true]
+val res2 = retrieve(ader('a', internalise(dr)), dr_val) // => [false, true]
+decode(dr_der, res1) // gives the value for derivative
+decode(dr, res2)     // gives the value for original value
+
+encode(inj(dr, 'a', decode(dr_der, res1)))
+

--- a/thys/Lexer.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Lexer.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -53,7 +53,7 @@
   assumes "\<Turnstile> v : der c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
-apply(induct arbitrary: v rule: der.induct)
+apply(induct c r arbitrary: v rule: der.induct)
 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
@@ -238,20 +238,33 @@
 
 lemma lexer_correct_None:
   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
-apply(induct s arbitrary: r)
-apply(simp add: nullable_correctness)
-apply(drule_tac x="der a r" in meta_spec)
-apply(auto simp add: der_correctness Der_def)
+  apply(induct s arbitrary: r)
+  apply(simp)
+  apply(simp add: nullable_correctness)
+  apply(simp)
+  apply(drule_tac x="der a r" in meta_spec) 
+  apply(auto)
+  apply(auto simp add: der_correctness Der_def)
 done
 
 lemma lexer_correct_Some:
   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
-apply(induct s arbitrary: r)
-apply(auto simp add: Posix_mkeps nullable_correctness)[1]
-apply(drule_tac x="der a r" in meta_spec)
-apply(simp add: der_correctness Der_def)
-apply(rule iffI)
-apply(auto intro: Posix_injval simp add: Posix1(1))
+  apply(induct s arbitrary : r)
+  apply(simp only: lexer.simps)
+  apply(simp)
+  apply(simp add: nullable_correctness Posix_mkeps)
+  apply(drule_tac x="der a r" in meta_spec)
+  apply(simp (no_asm_use) add: der_correctness Der_def del: lexer.simps) 
+  apply(simp del: lexer.simps)
+  apply(simp only: lexer.simps)
+  apply(case_tac "lexer (der a r) s = None")
+   apply(auto)[1]
+  apply(simp)
+  apply(erule exE)
+  apply(simp)
+  apply(rule iffI)
+  apply(simp add: Posix_injval)
+  apply(simp add: Posix1(1))
 done 
 
 lemma lexer_correctness:
@@ -260,4 +273,37 @@
 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
 using Posix1(1) lexer_correct_None lexer_correct_Some by blast
 
+
+
+
+fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)"
+  where
+  "flex r f [] = f"
+| "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s"  
+
+lemma flex_fun_apply:
+  shows "g (flex r f s v) = flex r (g o f) s v"
+  apply(induct s arbitrary: g f r v)
+  apply(simp_all add: comp_def)
+  by meson
+
+lemma flex_append:
+  shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
+  apply(induct s1 arbitrary: s2 r f)
+   apply(simp)
+  apply(drule_tac x="s2" in meta_spec)
+  apply(drule_tac x="der a r" in meta_spec)
+  apply(simp)
+  done  
+
+lemma lexer_flex:
+  shows "lexer r s = (if nullable (ders s r) 
+                      then Some(flex r id s (mkeps (ders s r))) else None)"
+  apply(induct s arbitrary: r)
+  apply(simp)
+  apply(simp add: flex_fun_apply)
+  done  
+
+unused_thms
+
 end
\ No newline at end of file

--- a/thys/PositionsExt.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/PositionsExt.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -126,7 +126,7 @@
 
 
 
-section {* POSIX Ordering of Values According to Okui & Suzuki *}
+section {* POSIX Ordering of Values According to Okui \& Suzuki *}
 
 
 definition PosOrd:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _" [60, 60, 59] 60)
@@ -196,9 +196,9 @@
 using assms
 using PosOrd_irrefl PosOrd_trans by blast 
 
-text {*
+(*
   :\<sqsubseteq>val and :\<sqsubset>val are partial orders.
-*}
+*)
 
 lemma PosOrd_ordering:
   shows "ordering (\<lambda>v1 v2. v1 :\<sqsubseteq>val v2) (\<lambda> v1 v2. v1 :\<sqsubset>val v2)"

--- a/thys/ROOT	Wed May 16 20:58:39 2018 +0100
+++ b/thys/ROOT	Wed Aug 15 13:48:57 2018 +0100
@@ -1,13 +1,13 @@
 session "Lex" = HOL +
   theories [document = false]
         "Spec"
-	"SpecExt"
+	(*"SpecExt"*)
         "Lexer"
-        "LexerExt"
+        (*"LexerExt"*)
         "Simplifying"
         (*"Sulzmann"*) 
         "Positions"
-	"PositionsExt"
+	(*"PositionsExt"*)
         "Exercises"
 
 session Paper in "Paper" = Lex +

--- a/thys/Simplifying.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Simplifying.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -230,7 +230,7 @@
    qed
  qed  
 
-
+(*
 fun simp2_ALT where
   "simp2_ALT ZERO r2 seen = (r2, seen)"
 | "simp2_ALT r1 ZERO seen = (r1, seen)"
@@ -367,5 +367,5 @@
    apply(simp add: Sequ_def)
    apply(auto)[1]
   oops  
-
+*)
 end
\ No newline at end of file

--- a/thys/Spec.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Spec.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -565,4 +565,5 @@
 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)
 done
 
+
 end
\ No newline at end of file

--- a/thys/Sulzmann.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Sulzmann.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -1,346 +1,21 @@
    
 theory Sulzmann
-  imports "Positions" 
+  imports "Lexer" 
 begin
 
-
-section {* Sulzmann's "Ordering" of Values *}
-
-inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100)
-where
-  MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" 
-| C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" 
-| C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" 
-| A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)"
-| A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')"
-| A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')"
-| K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))"
-| K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))"
-| K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk>  \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))"
-
-
-(*
-inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
-where
-  C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" 
-| C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" 
-| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)"
-| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Right v2)"
-| A3: "v2 \<preceq>r2 v2' \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Right v2')"
-| A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')"
-| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))"
-| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
-| K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
-| K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
-*)
-(*| MY1: "Void \<preceq>ONE Void" 
-| MY2: "(Char c) \<preceq>(CHAR c) (Char c)" 
-| MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" 
-*)
-
-(*
-lemma ValOrd_refl: 
-  assumes "\<turnstile> v : r" 
-  shows "v \<preceq>r v"
-using assms
-apply(induct r rule: Prf.induct)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(simp)
-done
-*)
-
-lemma ValOrd_irrefl: 
-  assumes "\<turnstile> v : r"  "v \<prec> v" 
-  shows "False"
-using assms
-apply(induct v r rule: Prf.induct)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-done
-
-lemma prefix_sprefix:
-  shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)"
-apply(auto simp add: sprefix_list_def prefix_list_def)
-done
-
-
-
-lemma Posix_CPT2:
-  assumes "v1 \<prec> v2" 
-  shows "v1 :\<sqsubset>val v2" 
-using assms
-apply(induct v1 v2 arbitrary: rule: ValOrd.induct)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply(rule val_ord_SeqI1)
-apply(simp)
-apply(simp)
-apply(rule val_ord_SeqI2)
-apply(simp)
-apply(simp)
-apply(simp add: val_ord_ex_def)
-apply(rule_tac x="[0]" in exI)
-apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1]
-apply(smt inlen_bigger)
-apply(rule val_ord_RightI)
-apply(simp)
-apply(simp)
-apply(rule val_ord_LeftI)
-apply(simp)
-apply(simp)
-defer
-apply(rule val_ord_StarsI)
-apply(simp)
-apply(simp)
-apply(rule val_ord_StarsI2)
-apply(simp)
-apply(simp)
-oops
-
-lemma QQ: 
-  shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y"
-  by auto
-
-lemma Posix_CPT2:
-  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
-  shows "v1 \<prec> v2"
-using assms
-apply(induct r arbitrary: v1 v2 s)  
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(simp add: val_ord_ex_def)
-apply(auto simp add: val_ord_def)[1]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: val_ord_ex_def val_ord_def)[1]
-(* SEQ case *)
-apply(subst (asm) (5) CPTpre_def)
-apply(subst (asm) (5) CPTpre_def)
-apply(auto)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(frule val_ord_shorterE)
-apply(subst (asm) QQ)
-apply(erule disjE)
-apply(drule val_ord_SeqE)
-apply(erule disjE)
-apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 8)
-apply(drule_tac x="v1b" in meta_spec)
-apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
-apply(simp)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(rule ValOrd.intros(2))
-apply(assumption)
-apply(frule val_ord_shorterE)
-apply(subst (asm) append_eq_append_conv_if)
-apply(simp)
-apply (metis append_assoc append_eq_append_conv_if length_append)
-
-
-thm le
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-
-apply(subst (asm) (3) CPTpre_def)
-apply(subst (asm) (3) CPTpre_def)
-apply(auto)[1]
-apply(drule_tac meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule val_ord_SeqE)
-apply(erule disjE)
-apply(simp add: append_eq_append_conv2)
-apply(auto)
-prefer 2
-apply(rule  ValOrd.intros(2))
-prefer 2
-apply(simp)
-thm ValOrd.intros
-apply(case_tac "flat v1b = flat v1a")
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-
-
-
-
-lemma Posix_CPT:
-  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s"
-  shows "v1 \<preceq>r v2" 
-using assms
-apply(induct r arbitrary: v1 v2 s rule: rexp.induct)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule ValOrd.intros)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule ValOrd.intros)
-(*SEQ case *)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-thm val_ord_SEQ
-apply(drule_tac r="r1a" in  val_ord_SEQ)
-apply(simp)
-using Prf_CPrf apply blast
-using Prf_CPrf apply blast
-apply(erule disjE)
-apply(rule C2)
-prefer 2
-apply(simp)
-apply(rule C1)
-apply blast
-
-apply(simp add: append_eq_append_conv2)
-apply(clarify)
-apply(auto)[1]
-apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 8)
-apply(drule_tac x="v1b" in meta_spec)
-apply(rotate_tac 8)
-apply(simp)
-
-(* HERE *)
-apply(subst (asm) (3) val_ord_ex_def)
-apply(clarify)
-apply(subst (asm) val_ord_def)
-apply(clarify)
-apply(rule ValOrd.intros)
-
-
-apply(simp add: val_ord_ex_def)
-oops
-
-
-lemma ValOrd_trans:
-  assumes "x \<preceq>r y" "y \<preceq>r z"
-  and "x \<in> CPT r s" "y \<in> CPT r s" "z \<in> CPT r s"
-  shows "x \<preceq>r z"
-using assms
-apply(induct x r y arbitrary: s z rule: ValOrd.induct)
-apply(rotate_tac 2)
-apply(erule ValOrd.cases)
-apply(simp_all)[13]
-apply(rule ValOrd.intros)
-apply(drule_tac x="s" in meta_spec)
-apply(drule_tac x="v1'a" in meta_spec)
-apply(drule_tac meta_mp)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(simp add: CPT_def)
-oops
-
-lemma ValOrd_preorder:
-  "preorder_on (CPT r s) {(v1, v2). v1 \<preceq>r v2 \<and> v1 \<in> (CPT r s) \<and> v2 \<in> (CPT r s)}"
-apply(simp add: preorder_on_def)
-apply(rule conjI)
-apply(simp add: refl_on_def)
-apply(auto)
-apply(rule ValOrd_refl)
-apply(simp add: CPT_def)
-apply(rule Prf_CPrf)
-apply(auto)[1]
-apply(simp add: trans_def)
-apply(auto)
-
-definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
-where 
-  "v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)"
-
-(*
-
-
-inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
-where
-  "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
-| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
-| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
-| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
-| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
-| "Void \<succ>EMPTY Void"
-| "(Char c) \<succ>(CHAR c) (Char c)"
-| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
-| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
-| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
-| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
-| "(Stars []) \<succ>(STAR r) (Stars [])"
-*)
-
-
 section {* Bit-Encodings *}
 
-
 fun 
-  code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
+  code :: "val \<Rightarrow> bool list"
 where
-  "code Void ONE = []"
-| "code (Char c) (CHAR d) = []"
-| "code (Left v) (ALT r1 r2) = False # (code v r1)"
-| "code (Right v) (ALT r1 r2) = True # (code v r2)"
-| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
-| "code (Stars []) (STAR r) = [True]"
-| "code (Stars (v # vs)) (STAR r) =  False # (code v r) @ code (Stars vs) (STAR r)"
+  "code Void = []"
+| "code (Char c) = []"
+| "code (Left v) = False # (code v)"
+| "code (Right v) = True # (code v)"
+| "code (Seq v1 v2) = (code v1) @ (code v2)"
+| "code (Stars []) = [True]"
+| "code (Stars (v # vs)) =  False # (code v) @ code (Stars vs)"
+
 
 fun 
   Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
@@ -365,12 +40,6 @@
                                     in (Stars_add v vs, ds''))"
 by pat_completeness auto
 
-termination
-apply(size_change)
-oops
-
-term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"
-
 lemma decode'_smaller:
   assumes "decode'_dom (ds, r)"
   shows "length (snd (decode' ds r)) \<le> length ds"
@@ -385,24 +54,35 @@
 apply(auto dest!: decode'_smaller)
 by (metis less_Suc_eq_le snd_conv)
 
-fun 
+definition
   decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
 where
-  "decode ds r = (let (v, ds') = decode' ds r 
+  "decode ds r \<equiv> (let (v, ds') = decode' ds r 
                   in (if ds' = [] then Some v else None))"
 
+lemma decode'_code_Stars:
+  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" 
+  shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
+  using assms
+  apply(induct vs)
+  apply(auto)
+  done
+
 lemma decode'_code:
-  assumes "\<turnstile> v : r"
-  shows "decode' ((code v r) @ ds) r = (v, ds)"
+  assumes "\<Turnstile> v : r"
+  shows "decode' ((code v) @ ds) r = (v, ds)"
 using assms
-by (induct v r arbitrary: ds) (auto)
+  apply(induct v r arbitrary: ds) 
+  apply(auto)
+  using decode'_code_Stars by blast
 
 
 lemma decode_code:
-  assumes "\<turnstile> v : r"
-  shows "decode (code v r) r = Some v"
-using assms decode'_code[of _ _ "[]"]
-by auto
+  assumes "\<Turnstile> v : r"
+  shows "decode (code v) r = Some v"
+  using assms unfolding decode_def
+  by (smt append_Nil2 decode'_code old.prod.case)
+
 
 datatype arexp =
   AZERO
@@ -429,6 +109,7 @@
 | "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"
 | "internalise (STAR r) = ASTAR [] (internalise r)"
 
+
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where
   "retrieve (AONE bs) Void = bs"
 | "retrieve (ACHAR bs c) (Char d) = bs"
@@ -439,6 +120,19 @@
 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 
      bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
 
+
+fun 
+  aerase :: "arexp \<Rightarrow> rexp"
+where
+  "aerase AZERO = ZERO"
+| "aerase (AONE _) = ONE"
+| "aerase (ACHAR _ c) = CHAR c"
+| "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)"
+| "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)"
+| "aerase (ASTAR _ r) = STAR (aerase r)"
+
+
+
 fun
  anullable :: "arexp \<Rightarrow> bool"
 where
@@ -471,21 +165,194 @@
       else ASEQ bs (ader c r1) r2)"
 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"
 
-lemma
-  assumes "\<turnstile> v : der c r"
-  shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r"
-using assms
-apply(induct c r arbitrary: v rule: der.induct)
-apply(simp_all)
-apply(erule Prf_elims)
-apply(erule Prf_elims)
-apply(case_tac "c = d")
-apply(simp)
-apply(erule Prf_elims)
-apply(simp)
-apply(simp)
-apply(erule Prf_elims)
-apply(auto split: prod.splits)[1]
-oops
+
+fun 
+ aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp"
+where
+  "aders [] r = r"
+| "aders (c # s) r = aders s (ader c r)"
+
+fun 
+  alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+where
+  "alex r [] = r"
+| "alex r (c#s) = alex (ader c r) s"
+
+lemma anullable_correctness:
+  shows "nullable (aerase r) = anullable r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
+lemma aerase_fuse:
+  shows "aerase (fuse bs r) = aerase r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
+
+lemma aerase_ader:
+  shows "aerase (ader a r) = der a (aerase r)"
+  apply(induct r)
+  apply(simp_all add: aerase_fuse anullable_correctness)
+  done
+
+lemma aerase_internalise:
+  shows "aerase (internalise r) = r"
+  apply(induct r)
+  apply(simp_all add: aerase_fuse)
+  done
+
+
+lemma aerase_alex:
+  shows "aerase (alex r s) = ders s (aerase r)"
+  apply(induct s arbitrary: r )
+  apply(simp_all add: aerase_ader)
+  done
+
+lemma retrieve_encode_STARS:
+  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v"
+  shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)"
+  using assms
+  apply(induct vs)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma retrieve_afuse2:
+  assumes "\<Turnstile> v : (aerase r)"
+  shows "retrieve (fuse bs r) v = bs @ retrieve r v"
+  using assms
+  apply(induct r arbitrary: v bs)
+  apply(auto)
+  using Prf_elims(1) apply blast
+  using Prf_elims(4) apply fastforce
+  using Prf_elims(5) apply fastforce
+  apply (smt Prf_elims(2) append_assoc retrieve.simps(5))
+   apply(erule Prf_elims)
+    apply(simp)
+   apply(simp)
+  apply(erule Prf_elims)
+  apply(simp)
+  apply(case_tac vs)
+   apply(simp)
+  apply(simp)
+  done
+
+lemma retrieve_afuse:
+  assumes "\<Turnstile> v : r"
+  shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v"
+  using assms 
+  by (simp_all add: retrieve_afuse2 aerase_internalise)
+
+
+lemma retrieve_encode:
+  assumes "\<Turnstile> v : r"
+  shows "code v = retrieve (internalise r) v"
+  using assms
+  apply(induct v r)
+  apply(simp_all add: retrieve_afuse retrieve_encode_STARS)
+  done
+
+
+lemma alex_append:
+  "alex r (s1 @ s2) = alex (alex r s1) s2"
+  apply(induct s1 arbitrary: r s2)
+   apply(simp_all)
+  done
 
+lemma ders_append:
+  shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
+  apply(induct s1 arbitrary: s2 r)
+  apply(auto)
+  done
+
+
+
+
+lemma Q00:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<Turnstile> v : r"
+  using assms
+  apply(induct) 
+  apply(auto intro: Prf.intros)
+  by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))
+
+lemma Qa:
+  assumes "anullable r"
+  shows "retrieve r (mkeps (aerase r)) = amkeps r"
+  using assms
+  apply(induct r)
+       apply(auto)
+  using anullable_correctness apply auto[1]
+  apply (simp add: anullable_correctness)
+  by (simp add: anullable_correctness)
+
+  
+lemma Qb:
+  assumes "\<Turnstile> v : der c (aerase r)"
+  shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)"
+  using assms
+  apply(induct r arbitrary: v c)
+       apply(simp_all)
+  using Prf_elims(1) apply blast
+  using Prf_elims(1) apply blast
+     apply(auto)[1]
+  using Prf_elims(4) apply fastforce
+  using Prf_elims(1) apply blast
+    apply(auto split: if_splits)[1]
+  apply(auto elim!: Prf_elims)[1]
+       apply(rotate_tac 1)
+       apply(drule_tac x="v2" in meta_spec)
+       apply(drule_tac x="c" in meta_spec)
+       apply(drule meta_mp)
+        apply(simp)
+       apply(drule sym)
+       apply(simp)
+       apply(subst retrieve_afuse2)
+        apply (simp add: aerase_ader)
+       apply (simp add: Qa)
+  using anullable_correctness apply auto[1]
+     apply(auto elim!: Prf_elims)[1]
+  using anullable_correctness apply auto[1]
+    apply(auto elim!: Prf_elims)[1]
+   apply(auto elim!: Prf_elims)[1]
+  apply(auto elim!: Prf_elims)[1]
+  by (simp add: retrieve_afuse2 aerase_ader)
+
+
+
+
+lemma MAIN:
+  assumes "\<Turnstile> v : ders s r"
+  shows "code (flex r id s v) = retrieve (alex (internalise r) s) v"
+  using assms
+  apply(induct s arbitrary: r v rule: rev_induct)
+   apply(simp)
+   apply (simp add: retrieve_encode)
+  apply(simp add: flex_append alex_append)
+  apply(subst Qb)
+  apply (simp add: aerase_internalise ders_append aerase_alex)
+  apply(simp add: aerase_alex aerase_internalise)
+  apply(drule_tac x="r" in meta_spec)
+  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+  apply(drule meta_mp)
+   apply (simp add: Prf_injval ders_append)
+  apply(simp)
+  done
+
+fun alexer where
+ "alexer r s = (if anullable (alex (internalise r) s) then 
+                decode (amkeps (alex (internalise r) s)) r else None)"
+
+
+lemma FIN:
+  "alexer r s = lexer r s"
+  apply(auto split: prod.splits)
+  apply (smt MAIN Q00 Qa aerase_alex aerase_internalise anullable_correctness decode_code lexer_correctness(1) lexer_flex mkeps_nullable)
+  apply (simp add: aerase_internalise anullable_correctness[symmetric] lexer_flex aerase_alex)
+  done
+
+unused_thms
+  
 end
\ No newline at end of file

Binary file thys/journal.pdf has changed