| author | Fahad Ausaf <fahad.ausaf@kcl.ac.uk> |
| Mon, 26 Jan 2015 15:41:16 +0000 | |
| changeset 50 | c603b27083f3 |
| parent 49 | c616ec6b1e3c |
| child 51 | 3810b37511cb |
| Fahad/Scala/Chapter5.sc | file | annotate | diff | comparison | revisions | |
| Fahad/Scala/Chapter6.sc | file | annotate | diff | comparison | revisions | |
| Fahad/Scala/POSIX.sc | file | annotate | diff | comparison | revisions | |
| Fahad/Scala/WorkSheet.sc | file | annotate | diff | comparison | revisions | |
| thys/#Re1.thy# | file | annotate | diff | comparison | revisions | |
| thys/Chap03.thy | file | annotate | diff | comparison | revisions | |
| thys/PosixTest.thy | file | annotate | diff | comparison | revisions |
--- a/Fahad/Scala/Chapter5.sc Wed Jan 21 12:32:17 2015 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,107 +0,0 @@ - -package greeter - -object Chapter5 { - println("Welcome to the Scala worksheet") //> Welcome to the Scala worksheet - - ///////////////////////////////////////////////////////////////////////////// - // CHAPTER 5: FIRST-CLASS FUNCTIONS - - /* - // Write a function to sumall integers between two given numbers a and b - def sumInts(a: Int, b: Int): Int = - if (a > b) 0 else a + sumInts(a + 1, b) - - sumInts(1, 5) - - //Write a function to sum the squares of all integers between two given numbers a and b - def square(x: Int): Int = x * x - def sumSquares(a: Int, b: Int): Int = - if (a > b) 0 else square(a) + sumSquares(a + 1, b) - - square(5) - - //Write a function to sum the powers 2n of all integers n between two given numbers a and b: - def powerOfTwo(x: Int): Int = if (x == 0) 1 else 2 * powerOfTwo(x - 1) - def sumPowersOfTwo(a: Int, b: Int): Int = - if (a > b) 0 else powerOfTwo(a) + sumPowersOfTwo(a + 1, b) - - sumPowersOfTwo(2, 4) - */ - - /* - def sum(f: Int => Int, a: Int, b: Int): Int = - if (a > b) 0 else f(a) + sum(f, a + 1, b) - - //def sumInts(a: Int, b: Int): Int = sum(id, a, b) - //def sumInts(a: Int, b: Int): Int = sum((x: Int) => x, a, b) - def sumInts(a: Int, b: Int): Int = sum(x => x, a, b) - //def sumSquares(a: Int, b: Int): Int = sum(square, a, b) - //def sumSquares(a: Int, b: Int): Int = sum((x: Int) => x * x, a, b) - def sumSquares(a: Int, b: Int): Int = sum(x => x * x, a, b) - def sumPowersOfTwo(a: Int, b: Int): Int = sum(powerOfTwo, a, b) - - def id(x: Int): Int = x - def square(x: Int): Int = x * x - */ - def powerOfTwo(x: Int): Int = if (x == 0) 1 else 2 * powerOfTwo(x - 1) - //> powerOfTwo: (x: Int)Int - - - // 5.2: Currying - - def sum(f: Int => Int): (Int, Int) => Int = { - def sumF(a: Int, b: Int): Int = - if (a > b) 0 else f(a) + sumF(a + 1, b) - sumF - } //> sum: (f: Int => Int)(Int, Int) => Int - - def sumInts = sum(x => x) //> sumInts: => (Int, Int) => Int - def sumSquares = sum(x => x * x) //> sumSquares: => (Int, Int) => Int - def sumPowersOfTwo = sum(powerOfTwo) //> sumPowersOfTwo: => (Int, Int) => Int - - sumSquares(1,10) + sumPowersOfTwo(10,20) //> res0: Int = 2096513 - sum(x => x * x)(2,4) //> res1: Int = 29 - - // 5.3: Finding Fixed Points of Functions - - val tolerance = 0.001 //> tolerance : Double = 0.001 - def isCloseEnough(x: Double, y: Double) = Math.abs((x-y) / x) < tolerance - //> isCloseEnough: (x: Double, y: Double)Boolean - def fixedPoint(f: Double => Double)(firstGuess: Double) = { - def iterate(guess: Double): Double = { - val next = f(guess) - if (isCloseEnough(guess, next)) next - else iterate(next) - } - iterate(firstGuess) - } //> fixedPoint: (f: Double => Double)(firstGuess: Double)Double - - - - - - - - - - - - - - - - - - - - - - - - - - - - -}
--- a/Fahad/Scala/Chapter6.sc Wed Jan 21 12:32:17 2015 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -package greeter - - -object Chapter6 { - println("Classes and Objects") //> Classes and Objects - - class Rational(n: Int, d: Int) { - private def gcd(x: Int, y: Int): Int = { - if (x == 0) y - else if (x < 0) gcd(-x, y) - else if (y < 0) -gcd(x, -y) - else gcd(y % x, x) - } - private val g = gcd(n, d) - - val numer: Int = n / g - val denom: Int = d / g - def +(that: Rational) = new Rational(numer * that.denom + that.numer * denom, denom * that.denom) - def -(that: Rational) = new Rational(numer * that.denom - that.numer * denom, denom * that.denom) - def *(that: Rational) = new Rational(numer * that.numer, denom * that.denom) - def /(that: Rational) = new Rational(numer * that.denom, denom * that.numer) - - //Inheritance and Overriding - override def toString = "" + numer + "/" + denom - //Parameterless Methods - def square = new Rational(numer * numer, denom * denom) - } - //Inheritance and Overriding - var i = 1 //> i : Int = 1 - var x = new Rational(0, 1) //> x : greeter.Chapter6.Rational = 0/1 - while (i <= 10) { - x += new Rational(1, i) - i += 1 - } - println("" + x.numer + "/" + x.denom) //> 7381/2520 - //Parameterless Methods - val r = new Rational(3, 4) //> r : greeter.Chapter6.Rational = 3/4 - println(r.square) //> 9/16 - - //Abstract Classes - abstract class IntSet { - def incl(x: Int): IntSet - def contains(x: Int): Boolean - } - - //Triats - trait IntSett { - def incl(x: Int): IntSet - def contains(x: Int): Boolean - } - - //Implementing abstract class - class EmptySet extends IntSet { - def contains(x: Int): Boolean = false - def incl(x: Int): IntSet = new NonEmptySet(x, new EmptySet, new EmptySet) - } - - class NonEmptySet(elem: Int, left: IntSet, right: IntSet) extends IntSet { - def contains(x: Int): Boolean = - if (x < elem) left contains x - else if (x > elem) right contains x - else true - def incl(x: Int): IntSet = - if (x < elem) new NonEmptySet(elem, left incl x, right) - else if (x > elem) new NonEmptySet(elem, left, right incl x) - else this - } - -}
--- a/Fahad/Scala/POSIX.sc Wed Jan 21 12:32:17 2015 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,305 +0,0 @@ -package greeter - - -object POSIX { - println("Posix Algorithm") //> Posix Algorithm - - abstract class Rexp - case object NULL extends Rexp - case object EMPTY extends Rexp - case class CHAR(c: Char) extends Rexp - 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 Val - case object Void 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 charlist2rexp(s: List[Char]): Rexp = s match { - case Nil => EMPTY - case c :: Nil => CHAR(c) - case c :: s => SEQ(CHAR(c), charlist2rexp(s)) - } //> charlist2rexp: (s: List[Char])greeter.POSIX.Rexp - implicit def string2rexp(s: String): Rexp = charlist2rexp(s.toList) - //> string2rexp: (s: String)greeter.POSIX.Rexp - - implicit def RexpOps(r: Rexp) = new { - def |(s: Rexp) = ALT(r, s) - def % = STAR(r) - def ~(s: Rexp) = SEQ(r, s) - } //> RexpOps: (r: greeter.POSIX.Rexp)AnyRef{def |(s: greeter.POSIX.Rexp): greete - //| r.POSIX.ALT; def %: greeter.POSIX.STAR; def ~(s: greeter.POSIX.Rexp): greet - //| er.POSIX.SEQ} - - 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) - } //> stringOps: (s: String)AnyRef{def |(r: greeter.POSIX.Rexp): greeter.POSIX.AL - //| T; def |(r: String): greeter.POSIX.ALT; def %: greeter.POSIX.STAR; def ~(r: - //| greeter.POSIX.Rexp): greeter.POSIX.SEQ; def ~(r: String): greeter.POSIX.SE - //| Q; def $(r: greeter.POSIX.Rexp): greeter.POSIX.RECD} - - // size of a regular expressions - for testing purposes - def size(r: Rexp): Int = r match { - case NULL => 1 - case EMPTY => 1 - case CHAR(_) => 1 - case ALT(r1, r2) => 1 + size(r1) + size(r2) - case SEQ(r1, r2) => 1 + size(r1) + size(r2) - case STAR(r) => 1 + size(r) - case RECD(_, r) => 1 + size(r) - } //> size: (r: greeter.POSIX.Rexp)Int - - // nullable function: tests whether the regular - // expression can recognise the empty string - def nullable(r: Rexp): Boolean = r match { - case NULL => false - case EMPTY => true - case CHAR(_) => false - case ALT(r1, r2) => nullable(r1) || nullable(r2) - case SEQ(r1, r2) => nullable(r1) && nullable(r2) - case STAR(_) => true - case RECD(_, r1) => nullable(r1) - } //> nullable: (r: greeter.POSIX.Rexp)Boolean - - // derivative of a regular expression w.r.t. a character - def der(c: Char, r: Rexp): Rexp = r match { - case NULL => NULL - case EMPTY => NULL - case CHAR(d) => if (c == d) EMPTY else NULL - 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)) - case RECD(_, r1) => der(c, r1) - } //> der: (c: Char, r: greeter.POSIX.Rexp)greeter.POSIX.Rexp - - // 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)) - } //> ders: (s: List[Char], r: greeter.POSIX.Rexp)greeter.POSIX.Rexp - - // extracts a string from value - def flatten(v: Val): String = v match { - case Void => "" - 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) - } //> flatten: (v: greeter.POSIX.Val)String - - // extracts an environment from a value - def env(v: Val): List[(String, String)] = v match { - case Void => 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) - } //> env: (v: greeter.POSIX.Val)List[(String, String)] - - def mkeps(r: Rexp): Val = r match { - case EMPTY => Void - 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) - case RECD(x, r) => Rec(x, mkeps(r)) - } //> mkeps: (r: greeter.POSIX.Rexp)greeter.POSIX.Val - - 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), Void) => Chr(d) - case (RECD(x, r1), _) => Rec(x, inj(r1, c, v)) - } //> inj: (r: greeter.POSIX.Rexp, c: Char, v: greeter.POSIX.Val)greeter.POSIX.Va - //| l - - // main lexing function (produces a value) - 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)) - } //> lex: (r: greeter.POSIX.Rexp, s: List[Char])greeter.POSIX.Val - - def lexing(r: Rexp, s: String): Val = lex(r, s.toList) - //> lexing: (r: greeter.POSIX.Rexp, s: String)greeter.POSIX.Val - - val r = (("1" $ "a") | (("2" $ "b") | ("3" $ "ab"))).% - //> r : greeter.POSIX.STAR = STAR(ALT(RECD(1,CHAR(a)),ALT(RECD(2,CHAR(b)),RECD - //| (3,SEQ(CHAR(a),CHAR(b)))))) - env(lexing(r, "ba")) //> res0: List[(String, String)] = List((2,b), (1,a)) - - val r1 = "a" | "b" //> r1 : greeter.POSIX.ALT = ALT(CHAR(a),CHAR(b)) - lexing(r1, "a") //> res1: greeter.POSIX.Val = Left(Chr(a)) - - // Lexing Rules for a Small While Language - - def PLUS(r: Rexp) = r ~ r.% //> PLUS: (r: greeter.POSIX.Rexp)greeter.POSIX.SEQ - 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" - //> SYM : greeter.POSIX.ALT = ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT( - //| ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(a),CHAR(b)),CHAR(c - //| )),CHAR(d)),CHAR(e)),CHAR(f)),CHAR(g)),CHAR(h)),CHAR(i)),CHAR(j)),CHAR(k)), - //| CHAR(l)),CHAR(m)),CHAR(n)),CHAR(o)),CHAR(p)),CHAR(q)),CHAR(r)),CHAR(s)),CHA - //| R(t)),CHAR(u)),CHAR(v)),CHAR(w)),CHAR(x)),CHAR(y)),CHAR(z)) - val DIGIT = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" - //> DIGIT : greeter.POSIX.ALT = ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(0),CH - //| AR(1)),CHAR(2)),CHAR(3)),CHAR(4)),CHAR(5)),CHAR(6)),CHAR(7)),CHAR(8)),CHAR( - //| 9)) - val ID = SYM ~ (SYM | DIGIT).% //> ID : greeter.POSIX.SEQ = SEQ(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(A - //| LT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(a),CHAR(b)),CHA - //| R(c)),CHAR(d)),CHAR(e)),CHAR(f)),CHAR(g)),CHAR(h)),CHAR(i)),CHAR(j)),CHAR(k - //| )),CHAR(l)),CHAR(m)),CHAR(n)),CHAR(o)),CHAR(p)),CHAR(q)),CHAR(r)),CHAR(s)), - //| CHAR(t)),CHAR(u)),CHAR(v)),CHAR(w)),CHAR(x)),CHAR(y)),CHAR(z)),STAR(ALT(ALT - //| (ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(AL - //| T(ALT(ALT(ALT(ALT(ALT(CHAR(a),CHAR(b)),CHAR(c)),CHAR(d)),CHAR(e)),CHAR(f)), - //| CHAR(g)),CHAR(h)),CHAR(i)),CHAR(j)),CHAR(k)),CHAR(l)),CHAR(m)),CHAR(n)),CHA - //| R(o)),CHAR(p)),CHAR(q)),CHAR(r)),CHAR(s)),CHAR(t)),CHAR(u)),CHAR(v)),CHAR(w - //| )),CHAR(x)),CHAR(y)),CHAR(z)),ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(0),C - //| HAR(1)),CHAR(2)),CHAR(3)),CHAR(4)),CHAR(5)),CHAR(6)),CHAR(7)),CHAR(8)),CHAR - //| (9))))) - val NUM = PLUS(DIGIT) //> NUM : greeter.POSIX.SEQ = SEQ(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(0), - //| CHAR(1)),CHAR(2)),CHAR(3)),CHAR(4)),CHAR(5)),CHAR(6)),CHAR(7)),CHAR(8)),CHA - //| R(9)),STAR(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(CHAR(0),CHAR(1)),CHAR(2)),CH - //| AR(3)),CHAR(4)),CHAR(5)),CHAR(6)),CHAR(7)),CHAR(8)),CHAR(9)))) - val KEYWORD: Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false" - //> KEYWORD : greeter.POSIX.Rexp = ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(SEQ(CHA - //| R(s),SEQ(CHAR(k),SEQ(CHAR(i),CHAR(p)))),SEQ(CHAR(w),SEQ(CHAR(h),SEQ(CHAR(i) - //| ,SEQ(CHAR(l),CHAR(e)))))),SEQ(CHAR(d),CHAR(o))),SEQ(CHAR(i),CHAR(f))),SEQ(C - //| HAR(t),SEQ(CHAR(h),SEQ(CHAR(e),CHAR(n))))),SEQ(CHAR(e),SEQ(CHAR(l),SEQ(CHAR - //| (s),CHAR(e))))),SEQ(CHAR(r),SEQ(CHAR(e),SEQ(CHAR(a),CHAR(d))))),SEQ(CHAR(w) - //| ,SEQ(CHAR(r),SEQ(CHAR(i),SEQ(CHAR(t),CHAR(e)))))),SEQ(CHAR(t),SEQ(CHAR(r),S - //| EQ(CHAR(u),CHAR(e))))),SEQ(CHAR(f),SEQ(CHAR(a),SEQ(CHAR(l),SEQ(CHAR(s),CHAR - //| (e)))))) - val SEMI: Rexp = ";" //> SEMI : greeter.POSIX.Rexp = CHAR(;) - val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/" - //> OP : greeter.POSIX.Rexp = ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(SEQ( - //| CHAR(:),CHAR(=)),SEQ(CHAR(=),CHAR(=))),CHAR(-)),CHAR(+)),CHAR(*)),SEQ(CHAR( - //| !),CHAR(=))),CHAR(<)),CHAR(>)),SEQ(CHAR(<),CHAR(=))),SEQ(CHAR(>),CHAR(=))), - //| CHAR(%)),CHAR(/)) - val WHITESPACE = PLUS(" " | "\n" | "\t") //> WHITESPACE : greeter.POSIX.SEQ = SEQ(ALT(ALT(CHAR( ),CHAR( - //| )),CHAR( )),STAR(ALT(ALT(CHAR( ),CHAR( - //| )),CHAR( )))) - val RPAREN: Rexp = ")" //> RPAREN : greeter.POSIX.Rexp = CHAR()) - val LPAREN: Rexp = "(" //> LPAREN : greeter.POSIX.Rexp = CHAR(() - val BEGIN: Rexp = "{" //> BEGIN : greeter.POSIX.Rexp = CHAR({) - val END: Rexp = "}" //> END : greeter.POSIX.Rexp = CHAR(}) - - /* - * val WHILE_REGS = (("k" $ KEYWORD) | - ("i" $ ID) | - ("o" $ OP) | - ("n" $ NUM) | - ("s" $ SEMI) | - ("p" $ (LPAREN | RPAREN)) | - ("b" $ (BEGIN | END)) | - ("w" $ WHITESPACE)).% -*/ - - val WHILE_REGS = (KEYWORD | - ID | - OP | - NUM | - SEMI | - LPAREN | RPAREN | - BEGIN | END | - WHITESPACE).% //> WHILE_REGS : greeter.POSIX.STAR = STAR(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT - //| (ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(SEQ(CHAR(s),SEQ(CHAR(k),SEQ(CHAR(i),CH - //| AR(p)))),SEQ(CHAR(w),SEQ(CHAR(h),SEQ(CHAR(i),SEQ(CHAR(l),CHAR(e)))))),SEQ(C - //| HAR(d),CHAR(o))),SEQ(CHAR(i),CHAR(f))),SEQ(CHAR(t),SEQ(CHAR(h),SEQ(CHAR(e), - //| CHAR(n))))),SEQ(CHAR(e),SEQ(CHAR(l),SEQ(CHAR(s),CHAR(e))))),SEQ(CHAR(r),SEQ - //| (CHAR(e),SEQ(CHAR(a),CHAR(d))))),SEQ(CHAR(w),SEQ(CHAR(r),SEQ(CHAR(i),SEQ(CH - //| AR(t),CHAR(e)))))),SEQ(CHAR(t),SEQ(CHAR(r),SEQ(CHAR(u),CHAR(e))))),SEQ(CHAR - //| (f),SEQ(CHAR(a),SEQ(CHAR(l),SEQ(CHAR(s),CHAR(e)))))),SEQ(ALT(ALT(ALT(ALT(AL - //| T(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(ALT(A - //| LT(ALT(CHAR(a),CHAR(b)),CHAR(c)),CHAR(d)),CHAR(e)),CHAR(f)),CHAR(g)),CHAR(h - //| )),CHAR(i)),CHAR(j)),CHAR(k)),CHAR(l)),CHAR(m)),CHAR(n)),CHAR(o)),CHAR(p)), - //| CHAR(q)),CHAR(r)),CHAR(s)),CHAR(t)),CHAR(u)),CHAR(v)),CHAR(w)),CHAR(x)),CHA - //| R(y)),CHAR(z)),STAR(ALT - //| Output exceeds cutoff limit. - - // Some Tests - //============ - - def time[T](code: => T) = { - val start = System.nanoTime() - val result = code - val end = System.nanoTime() - println((end - start) / 1.0e9) - result - } //> time: [T](code: => T)T - - - val abc = List('a', 'b', 'c') //> abc : List[Char] = List(a, b, c) - val nullRexp = null //> nullRexp : Null = null - val myRexp = charlist2rexp(abc) //> myRexp : greeter.POSIX.Rexp = SEQ(CHAR(a),SEQ(CHAR(b),CHAR(c))) - val myRexp2 = string2rexp("FahadAusaf") //> myRexp2 : greeter.POSIX.Rexp = SEQ(CHAR(F),SEQ(CHAR(a),SEQ(CHAR(h),SEQ(CHA - //| R(a),SEQ(CHAR(d),SEQ(CHAR(A),SEQ(CHAR(u),SEQ(CHAR(s),SEQ(CHAR(a),CHAR(f)))) - //| )))))) - - RexpOps(myRexp2) //> res2: AnyRef{def |(s: greeter.POSIX.Rexp): greeter.POSIX.ALT; def %: greete - //| r.POSIX.STAR; def ~(s: greeter.POSIX.Rexp): greeter.POSIX.SEQ} = greeter.PO - //| SIX$$anonfun$main$1$$anon$1@37ecb28e - - stringOps("Fahad") //> res3: AnyRef{def |(r: greeter.POSIX.Rexp): greeter.POSIX.ALT; def |(r: Stri - //| ng): greeter.POSIX.ALT; def %: greeter.POSIX.STAR; def ~(r: greeter.POSIX.R - //| exp): greeter.POSIX.SEQ; def ~(r: String): greeter.POSIX.SEQ; def $(r: gree - //| ter.POSIX.Rexp): greeter.POSIX.RECD} = greeter.POSIX$$anonfun$main$1$$anon$ - //| 2@14bea551 - - size(myRexp2) //> res4: Int = 19 - nullable(nullRexp) //> scala.MatchError: null - //| at greeter.POSIX$$anonfun$main$1.nullable$1(greeter.POSIX.scala:59) - //| at greeter.POSIX$$anonfun$main$1.apply$mcV$sp(greeter.POSIX.scala:202) - //| at org.scalaide.worksheet.runtime.library.WorksheetSupport$$anonfun$$exe - //| cute$1.apply$mcV$sp(WorksheetSupport.scala:76) - //| at org.scalaide.worksheet.runtime.library.WorksheetSupport$.redirected(W - //| orksheetSupport.scala:65) - //| at org.scalaide.worksheet.runtime.library.WorksheetSupport$.$execute(Wor - //| ksheetSupport.scala:75) - //| at greeter.POSIX$.main(greeter.POSIX.scala:3) - //| at greeter.POSIX.main(greeter.POSIX.scala) - - val newRexp = der('a',myRexp) - - - - - - - - - - - - - - - - - - - - - - //this is some crap -}
--- a/Fahad/Scala/WorkSheet.sc Wed Jan 21 12:32:17 2015 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,81 +0,0 @@ -package greeter - -object WorkSheet { - println("Welcome to the Scala worksheet") //> Welcome to the Scala worksheet - - val x = 5 //> x : Int = 5 - def increase(i: Int) = i + 1 //> increase: (i: Int)Int - increase(x) //> res0: Int = 6 - - // Expressions And Simple Functions - - 87 + 145 //> res1: Int(232) = 232 - 5 + 2 * 3 //> res2: Int = 11 - - "Hello" + " World!" //> res3: String("Hello World!") = Hello World! - - def scale = 5 //> scale: => Int - 7 * scale //> res4: Int = 35 - - def pi = 3.141592653589793 //> pi: => Double - def radius = 10 //> radius: => Int - 2 * pi * radius //> res5: Double = 62.83185307179586 - - // PARAMETERS - - def square(x: Double) = x * x //> square: (x: Double)Double - square(2) //> res6: Double = 4.0 - square(square(4)) //> res7: Double = 256.0 - - def sumOfSquares(x: Double, y: Double) = square(x) + square(y) - //> sumOfSquares: (x: Double, y: Double)Double - sumOfSquares(3, 2 + 2) //> res8: Double = 25.0 - - def loop: Int = loop //> loop: => Int - def first(x: Int, y: Int) = x //> first: (x: Int, y: Int)Int - def constOne(x: Int, y: => Int) = 1 //> constOne: (x: Int, y: => Int)Int - constOne(1, loop) //> res9: Int = 1 - - // 4.3 CONDITIONAL EXPRESSIONS - - def abs(x: Double) = if (x >= 5) x + 1 else x - 1 - //> abs: (x: Double)Double - abs(4) //> res10: Double = 3.0 - - // 4.4: Square Roots by Newton's Method - - def sqrtIter(guess: Double, x: Double): Double = - if (isGoodEnough(guess, x)) guess - else sqrtIter(improve(guess, x), x) //> sqrtIter: (guess: Double, x: Double)Double - - def improve(guess: Double, x: Double) = - (guess + x / guess) / 2 //> improve: (guess: Double, x: Double)Double - - def isGoodEnough(guess: Double, x: Double) = - abs(square(guess) - x) < 0.001 //> isGoodEnough: (guess: Double, x: Double)Boolean - - //def sqrt(x: Double) = sqrtIter(1.0, x) - //sqrt(25) - - // 4.5: Nested Functions - - def sqrt(x: Double) = { - def sqrtIter(guess: Double): Double = - if (isGoodEnough(guess)) guess - else sqrtIter(improve(guess)) - def improve(guess: Double) = - (guess + x / guess) / 2 - def isGoodEnough(guess: Double) = - abs(square(guess) - x) < 0.001 - sqrtIter(1.0) - } //> sqrt: (x: Double)Double - sqrt(25) //> res11: Double = 1.0 - - // 4.6: Tail Recursion - - def gcd(a: Int, b: Int): Int = if (b == 0) a else gcd(b, a % b) - //> gcd: (a: Int, b: Int)Int - - gcd(21, 36) //> res12: Int = 3 - -} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/#Re1.thy# Mon Jan 26 15:41:16 2015 +0000 @@ -0,0 +1,897 @@ + +theory Re1 + imports "Main" +begin + +section {* Sequential Composition of Sets *} + +definition + Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) +where + "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" + +text {* Two Simple Properties about Sequential Composition *} + +lemma seq_empty [simp]: + shows "A ;; {[]} = A" + and "{[]} ;; A = A" +by (simp_all add: Sequ_def) + +lemma seq_null [simp]: + shows "A ;; {} = {}" + and "{} ;; A = {}" +by (simp_all add: Sequ_def) + +section {* Regular Expressions *} + +datatype rexp = + NULL +| EMPTY +| CHAR char +| SEQ rexp rexp +| ALT rexp rexp + +section {* Semantics of Regular Expressions *} + +fun + L :: "rexp \<Rightarrow> string set" +where + "L (NULL) = {}" +| "L (EMPTY) = {[]}" +| "L (CHAR c) = {[c]}" +| "L (SEQ r1 r2) = (L r1) ;; (L r2)" +| "L (ALT r1 r2) = (L r1) \<union> (L r2)" + +value "L(CHAR c)" +value "L(SEQ(CHAR c)(CHAR b))" + + +section {* Values *} + +datatype val = + Void +| Char char +| Seq val val +| Right val +| Left val + +section {* Relation between values and regular expressions *} + +inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) +where + "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" +| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" +| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" +| "\<turnstile> Void : EMPTY" +| "\<turnstile> Char c : CHAR c" + +section {* The string behind a value *} + +fun flat :: "val \<Rightarrow> string" +where + "flat(Void) = []" +| "flat(Char c) = [c]" +| "flat(Left v) = flat(v)" +| "flat(Right v) = flat(v)" +| "flat(Seq v1 v2) = flat(v1) @ flat(v2)" + +value "flat(Seq(Char c)(Char b))" +value "flat(Right(Void))" + +fun flats :: "val \<Rightarrow> string list" +where + "flats(Void) = [[]]" +| "flats(Char c) = [[c]]" +| "flats(Left v) = flats(v)" +| "flats(Right v) = flats(v)" +| "flats(Seq v1 v2) = (flats v1) @ (flats v2)" + +value "flats(Seq(Char c)(Char b))" + +lemma Prf_flat_L: + assumes "\<turnstile> v : r" shows "flat v \<in> L r" +using assms +apply(induct) +apply(auto simp add: Sequ_def) +done + +lemma L_flat_Prf: + "L(r) = {flat v | v. \<turnstile> v : r}" +apply(induct r) +apply(auto dest: Prf_flat_L simp add: Sequ_def) +apply (metis Prf.intros(4) flat.simps(1)) +apply (metis Prf.intros(5) flat.simps(2)) +apply (metis Prf.intros(1) flat.simps(5)) +apply (metis Prf.intros(2) flat.simps(3)) +apply (metis Prf.intros(3) flat.simps(4)) +apply(erule Prf.cases) +apply(auto) +done + +definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) +where + "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" + +section {* Ordering of values *} + +inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) +where + "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" +| "v1 \<succ>r1 v1' \<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)" + +section {* The ordering is reflexive *} + +lemma ValOrd_refl: + assumes "\<turnstile> v : r" + shows "v \<succ>r v" +using assms +apply(induct) +apply(auto intro: ValOrd.intros) +done + +lemma ValOrd_flats: + assumes "v1 \<succ>r v2" + shows "hd (flats v2) = hd (flats v1)" +using assms +apply(induct) +apply(auto) +oops + + +section {* Posix definition *} + +definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" +where + "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')" + +(* +an alternative definition: might cause problems +with theorem mkeps_POSIX +*) + +definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" +where + "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" + +definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" +where + "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> length (flat v') \<le> length(flat v)) \<longrightarrow> v \<succ>r v')" + + +lemma POSIX_SEQ: + assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" + shows "POSIX v1 r1 \<and> POSIX v2 r2" +using assms +unfolding POSIX_def +apply(auto) +apply(drule_tac x="Seq v' v2" in spec) +apply(simp) +apply(erule impE) +apply(rule Prf.intros) +apply(simp) +apply(simp) +apply(erule ValOrd.cases) +apply(simp_all) +apply(clarify) +defer +apply(drule_tac x="Seq v1 v'" in spec) +apply(simp) +apply(erule impE) +apply(rule Prf.intros) +apply(simp) +apply(simp) +apply(erule ValOrd.cases) +apply(simp_all) +apply(clarify) +oops (*not true*) + +lemma POSIX_SEQ_I: + assumes "POSIX v1 r1" "POSIX v2 r2" + shows "POSIX (Seq v1 v2) (SEQ r1 r2)" +using assms +unfolding POSIX_def +apply(auto) +apply(rotate_tac 2) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(rule ValOrd.intros) +oops (* maybe also not true *) + +lemma POSIX3_SEQ_I: + assumes "POSIX3 v1 r1" "POSIX3 v2 r2" + shows "POSIX3 (Seq v1 v2) (SEQ r1 r2)" +using assms +unfolding POSIX3_def +apply(auto) +apply (metis Prf.intros(1)) +apply(rotate_tac 4) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(case_tac "v1 = v1a") +apply(auto) +apply (metis ValOrd.intros(1)) +apply (rule ValOrd.intros(2)) +oops + +lemma POSIX_ALT2: + assumes "POSIX (Left v1) (ALT r1 r2)" + shows "POSIX v1 r1" +using assms +unfolding POSIX_def +apply(auto) +apply(drule_tac x="Left v'" in spec) +apply(simp) +apply(drule mp) +apply(rule Prf.intros) +apply(auto) +apply(erule ValOrd.cases) +apply(simp_all) +done + +lemma POSIX2_ALT: + assumes "POSIX2 (Left v1) (ALT r1 r2)" + shows "POSIX2 v1 r1" +using assms +unfolding POSIX2_def +apply(auto) +oops + +lemma POSIX_ALT: + assumes "POSIX (Left v1) (ALT r1 r2)" + shows "POSIX v1 r1" +using assms +unfolding POSIX_def +apply(auto) +apply(drule_tac x="Left v'" in spec) +apply(simp) +apply(drule mp) +apply(rule Prf.intros) +apply(auto) +apply(erule ValOrd.cases) +apply(simp_all) +done + +lemma POSIX2_ALT: + assumes "POSIX2 (Left v1) (ALT r1 r2)" + shows "POSIX2 v1 r1" +using assms +apply(simp add: POSIX2_def) +apply(auto) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(drule_tac x="Left v'" in spec) +apply(drule mp) +apply(rule Prf.intros) +apply(auto) +apply(erule ValOrd.cases) +apply(simp_all) +done + + +lemma POSIX_ALT1a: + assumes "POSIX (Right v2) (ALT r1 r2)" + shows "POSIX v2 r2" +using assms +unfolding POSIX_def +apply(auto) +apply(drule_tac x="Right v'" in spec) +apply(simp) +apply(drule mp) +apply(rule Prf.intros) +apply(auto) +apply(erule ValOrd.cases) +apply(simp_all) +done + +lemma POSIX2_ALT1a: + assumes "POSIX2 (Right v2) (ALT r1 r2)" + shows "POSIX2 v2 r2" +using assms +unfolding POSIX2_def +apply(auto) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(drule_tac x="Right v'" in spec) +apply(drule mp) +apply(rule Prf.intros) +apply(auto) +apply(erule ValOrd.cases) +apply(simp_all) +done + + +lemma POSIX_ALT1b: + assumes "POSIX (Right v2) (ALT r1 r2)" + shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" +using assms +apply(drule_tac POSIX_ALT1a) +unfolding POSIX_def +apply(auto) +done + +lemma POSIX_ALT_I1: + assumes "POSIX v1 r1" + shows "POSIX (Left v1) (ALT r1 r2)" +using assms +unfolding POSIX_def +apply(auto) +apply(rotate_tac 3) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply(rule ValOrd.intros) +apply(auto) +apply(rule ValOrd.intros) +by simp + +lemma POSIX2_ALT_I1: + assumes "POSIX2 v1 r1" + shows "POSIX2 (Left v1) (ALT r1 r2)" +using assms +unfolding POSIX2_def +apply(auto) +apply(rule Prf.intros) +apply(simp) +apply(rotate_tac 2) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply(rule ValOrd.intros) +apply(auto) +apply(rule ValOrd.intros) +oops + +lemma POSIX_ALT_I2: + assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" + shows "POSIX (Right v2) (ALT r1 r2)" +using assms +unfolding POSIX_def +apply(auto) +apply(rotate_tac 3) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply(rule ValOrd.intros) +apply metis +done + + + + + +section {* The Matcher *} + +fun + nullable :: "rexp \<Rightarrow> bool" +where + "nullable (NULL) = False" +| "nullable (EMPTY) = True" +| "nullable (CHAR c) = False" +| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" +| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" + +lemma nullable_correctness: + shows "nullable r \<longleftrightarrow> [] \<in> (L r)" +apply (induct r) +apply(auto simp add: Sequ_def) +done + +fun mkeps :: "rexp \<Rightarrow> val" +where + "mkeps(EMPTY) = Void" +| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" +| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" + +lemma mkeps_nullable: + assumes "nullable(r)" shows "\<turnstile> mkeps r : r" +using assms +apply(induct rule: nullable.induct) +apply(auto intro: Prf.intros) +done + +lemma mkeps_flat: + assumes "nullable(r)" shows "flat (mkeps r) = []" +using assms +apply(induct rule: nullable.induct) +apply(auto) +done + +text {* + The value mkeps returns is always the correct POSIX + value. +*} + +lemma mkeps_POSIX2: + assumes "nullable r" + shows "POSIX2 (mkeps r) r" +using assms +apply(induct r) +apply(auto)[1] +apply(simp add: POSIX2_def) +oops + +lemma mkeps_POSIX3: + assumes "nullable r" + shows "POSIX3 (mkeps r) r" +using assms +apply(induct r) +apply(auto)[1] +apply(simp add: POSIX3_def) +apply(auto)[1] +apply (metis Prf.intros(4)) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros) +apply(simp add: POSIX3_def) +apply(auto)[1] +apply(simp add: POSIX3_def) +apply(auto)[1] +apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5)) +apply(rotate_tac 6) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros(2) add_leE gen_length_code(1) gen_length_def mkeps_flat) +apply(auto) +apply(simp add: POSIX3_def) +apply(auto) +apply (metis Prf.intros(2)) +apply(rotate_tac 4) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros(6)) +apply(auto)[1] +apply (metis ValOrd.intros(3)) +apply(simp add: POSIX3_def) +apply(auto) +apply (metis Prf.intros(2)) +apply(rotate_tac 6) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros(6)) +apply (metis ValOrd.intros(3)) +apply(simp add: POSIX3_def) +apply(auto) +apply (metis Prf.intros(3)) +apply(rotate_tac 5) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis Prf_flat_L drop_0 drop_all list.size(3) mkeps_flat nullable_correctness) +by (metis ValOrd.intros(5)) + + +lemma mkeps_POSIX: + assumes "nullable r" + shows "POSIX (mkeps r) r" +using assms +apply(induct r) +apply(auto)[1] +apply(simp add: POSIX_def) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros) +apply(simp add: POSIX_def) +apply(auto)[1] +apply(simp add: POSIX_def) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply (simp add: ValOrd.intros(2) mkeps_flat) +apply(simp add: POSIX_def) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply (simp add: ValOrd.intros(6)) +apply (simp add: ValOrd.intros(3)) +apply(simp add: POSIX_def) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply (simp add: ValOrd.intros(6)) +apply (simp add: ValOrd.intros(3)) +apply(simp add: POSIX_def) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto) +apply (metis Prf_flat_L mkeps_flat nullable_correctness) +by (simp add: ValOrd.intros(5)) + + +lemma mkeps_POSIX2: + assumes "nullable r" + shows "POSIX2 (mkeps r) r" +using assms +apply(induct r) +apply(simp) +apply(simp) +apply(simp add: POSIX2_def) +apply(rule conjI) +apply(rule Prf.intros) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(rule ValOrd.intros) +apply(simp) +apply(simp) +apply(simp add: POSIX2_def) +apply(rule conjI) +apply(rule Prf.intros) +apply(simp add: mkeps_nullable) +apply(simp add: mkeps_nullable) +apply(auto)[1] +apply(rotate_tac 6) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(rule ValOrd.intros(2)) +apply(simp) +apply(simp only: nullable.simps) +apply(erule disjE) +apply(simp) +thm POSIX2_ALT1a +apply(rule POSIX2_ALT) +apply(simp add: POSIX2_def) +apply(rule conjI) +apply(rule Prf.intros) +apply(simp add: mkeps_nullable) +oops + + +section {* Derivatives *} + +fun + der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" +where + "der c (NULL) = NULL" +| "der c (EMPTY) = NULL" +| "der c (CHAR c') = (if c = c' then EMPTY else NULL)" +| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" +| "der c (SEQ r1 r2) = + (if nullable r1 + then ALT (SEQ (der c r1) r2) (der c r2) + else SEQ (der c r1) r2)" + +fun + ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" +where + "ders [] r = r" +| "ders (c # s) r = ders s (der c r)" + +section {* Injection function *} + +fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" +where + "injval (CHAR d) c Void = Char d" +| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" +| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" +| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" +| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" +| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" + +section {* Projection function *} + +fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" +where + "projval (CHAR d) c _ = Void" +| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)" +| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)" +| "projval (SEQ r1 r2) c (Seq v1 v2) = + (if flat v1 = [] then Right(projval r2 c v2) + else if nullable r1 then Left (Seq (projval r1 c v1) v2) + else Seq (projval r1 c v1) v2)" + +text {* + Injection value is related to r +*} + +lemma v3: + assumes "\<turnstile> v : der c r" shows "\<turnstile> (injval r c v) : r" +using assms +apply(induct arbitrary: v rule: der.induct) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(case_tac "c = c'") +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis Prf.intros(5)) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis Prf.intros(2)) +apply (metis Prf.intros(3)) +apply(simp) +apply(case_tac "nullable r1") +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply (metis Prf.intros(1)) +apply(auto)[1] +apply (metis Prf.intros(1) mkeps_nullable) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(rule Prf.intros) +apply(auto)[2] +done + +text {* + The string behin the injection value is an added c +*} + +lemma v4: + 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(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(case_tac "c = c'") +apply(simp) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(case_tac "nullable r1") +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply (metis mkeps_flat) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +done + +text {* + Injection followed by projection is the identity. +*} + +lemma proj_inj_id: + assumes "\<turnstile> v : der c r" + shows "projval r c (injval r c v) = v" +using assms +apply(induct r arbitrary: c v rule: rexp.induct) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(case_tac "c = char") +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +defer +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(case_tac "nullable rexp1") +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply (metis list.distinct(1) v4) +apply(auto)[1] +apply (metis mkeps_flat) +apply(auto) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(auto)[1] +apply(simp add: v4) +done + +lemma "L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIX3 v r" +apply(induct r) +apply(simp) +apply(simp add: POSIX3_def) +apply(rule_tac x="Void" in exI) +apply(auto)[1] +apply (metis Prf.intros(4)) +apply (metis POSIX3_def flat.simps(1) mkeps.simps(1) mkeps_POSIX3 nullable.simps(2) order_refl) +apply(simp add: POSIX3_def) +apply(rule_tac x="Char char" in exI) +apply(auto)[1] +apply (metis Prf.intros(5)) +apply(erule Prf.cases) +apply(simp_all)[5] +apply (metis ValOrd.intros(8)) +apply(simp add: Sequ_def) +apply(auto)[1] +apply(drule meta_mp) +apply(auto)[2] +apply(drule meta_mp) +apply(auto)[2] +apply(rule_tac x="Seq v va" in exI) +apply(simp (no_asm) add: POSIX3_def) +apply(auto)[1] +apply (metis POSIX3_def Prf.intros(1)) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(clarify) +apply(case_tac "v \<succ>r1a v1") +apply(rule ValOrd.intros(2)) +apply(simp) +apply(case_tac "v = v1") +apply(rule ValOrd.intros(1)) +apply(simp) +apply(simp) +apply (metis ValOrd_refl) +apply(simp add: POSIX3_def) + + +lemma "\<exists>v. POSIX v r" +apply(induct r) +apply(rule exI) +apply(simp add: POSIX_def) +apply (metis (full_types) Prf_flat_L der.simps(1) der.simps(2) der.simps(3) flat.simps(1) nullable.simps(1) nullable_correctness proj_inj_id projval.simps(1) v3 v4) +apply(rule_tac x = "Void" in exI) +apply(simp add: POSIX_def) +apply (metis POSIX_def flat.simps(1) mkeps.simps(1) mkeps_POSIX nullable.simps(2)) +apply(rule_tac x = "Char char" in exI) +apply(simp add: POSIX_def) +apply(auto) [1] +apply(erule Prf.cases) +apply(simp_all) [5] +apply (metis ValOrd.intros(8)) +defer +apply(auto) +apply (metis POSIX_ALT_I1) +(* maybe it is too early to instantiate this existential quantifier *) +(* potentially this is the wrong POSIX value *) +apply(case_tac "r1 = NULL") +apply(simp add: POSIX_def) +apply(auto)[1] +apply (metis L.simps(1) L.simps(4) Prf_flat_L mkeps_flat nullable.simps(1) nullable.simps(2) nullable_correctness seq_null(2)) +apply(case_tac "r1 = EMPTY") +apply(rule_tac x = "Seq Void va" in exI ) +apply(simp (no_asm) add: POSIX_def) +apply(auto) +apply(erule Prf.cases) +apply(simp_all) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all) +apply(rule ValOrd.intros(2)) +apply(rule ValOrd.intros) +apply(case_tac "\<exists>c. r1 = CHAR c") +apply(auto) +apply(rule_tac x = "Seq (Char c) va" in exI ) +apply(simp (no_asm) add: POSIX_def) +apply(auto) +apply(erule Prf.cases) +apply(simp_all) +apply(auto)[1] +apply(erule Prf.cases) +apply(simp_all) +apply(auto)[1] +apply(rule ValOrd.intros(2)) +apply(rule ValOrd.intros) +apply(case_tac "\<exists>r1a r1b. r1 = ALT r1a r1b") +apply(auto) +oops (* not sure if this can be proved by induction *) + +text {* + + HERE: Crucial lemma that does not go through in the sequence case. + +*} +lemma v5: + assumes "\<turnstile> v : der c r" "POSIX v (der c r)" + shows "POSIX (injval r c v) r" +using assms +apply(induct arbitrary: v rule: der.induct) +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(erule Prf.cases) +apply(simp_all)[5] +apply(simp) +apply(case_tac "c = c'") +apply(auto simp add: POSIX_def)[1] +apply(erule Prf.cases) +apply(simp_all)[5] +apply(erule Prf.cases) +apply(simp_all)[5] +using ValOrd.simps apply blast +apply(auto) +apply(erule Prf.cases) +apply(simp_all)[5] +(* base cases done *) +(* ALT case *) +apply(erule Prf.cases) +apply(simp_all)[5] +using POSIX_ALT POSIX_ALT_I1 apply blast +apply(clarify) +apply(subgoal_tac "POSIX v2 (der c r2)") +prefer 2 +apply(auto simp add: POSIX_def)[1] +apply (metis POSIX_ALT1a POSIX_def flat.simps(4)) +apply(frule POSIX_ALT1a) +apply(drule POSIX_ALT1b) +apply(rule POSIX_ALT_I2) +apply(rotate_tac 1) +apply(drule_tac x="v2" in meta_spec) +apply(simp) +apply(subgoal_tac "\<turnstile> Right (injval r2 c v2) : (ALT r1 r2)") +prefer 2 +apply (metis Prf.intros(3) v3) + +apply auto[1] +apply(subst v4) +apply(auto)[2] +apply(subst (asm) (4) POSIX_def) +apply(subst (asm) v4) +apply(drule_tac x="v2" in meta_spec) +apply(simp) + +apply(auto)[2] + +thm POSIX_ALT_I2 +apply(rule POSIX_ALT_I2) + +apply(rule ccontr) +apply(auto simp add: POSIX_def)[1] + +apply(rule allI) +apply(rule impI) +apply(erule conjE) +thm POSIX_ALT_I2 +apply(frule POSIX_ALT1a) +apply(drule POSIX_ALT1b) +apply(rule POSIX_ALT_I2) +apply auto[1] +apply(subst v4) +apply(auto)[2] +apply(rotate_tac 1) +apply(drule_tac x="v2" in meta_spec) +apply(simp) +apply(subst (asm) (4) POSIX_def) +apply(subst (asm) v4) +apply(auto)[2] +(* stuck in the ALT case *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/Chap03.thy Mon Jan 26 15:41:16 2015 +0000 @@ -0,0 +1,167 @@ +theory Chap03 +imports Main +begin + +lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs" +apply simp +done + +lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []" +apply (simp (no_asm)) +done + +definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where +"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)" + +lemma "xor A (\<not>A)" +apply(simp only: xor_def) +apply(simp add: xor_def) +done + +lemma "(let xs = [] in xs@ys@xs) = ys" +apply(simp only: Let_def) +apply(simp add: Let_def) +done + +(* 3.1.8 Conditioal Simplification Rules *) + +lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" +using [[simp_trace=true]] +apply(case_tac xs) +apply(simp) +apply(simp) +done + +lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs" +apply(case_tac xs) +using [[simp_trace=true]] +apply(simp) +apply(simp) +done + +(* 3.1.9 Automatic Case Splits *) + +lemma "\<forall> xs. if xs = [] then rev xs = [] else rev xs \<noteq> []" +apply(split split_if) +apply(simp) +done + +lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs" +apply(split list.split) +apply(simp split: list.split) +done + +lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []" +apply(split split_if_asm) +apply(simp) +apply(auto) +done + +(* 3.2 Induction Heuristics *) + +primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where +"itrev [] ys = ys" | +"itrev (x#xs) ys = itrev xs (x#ys)" + +lemma "itrev xs [] = rev xs" +apply(induct_tac xs) +apply(simp) +apply(auto) +oops + +lemma "itrev xs ys = rev xs @ ys" +apply(induct_tac xs) +apply(simp_all) +oops + +lemma "\<forall> ys. itrev xs ys = rev xs @ ys" +apply(induct_tac xs) +apply(simp) +apply(simp) +done + +primrec add1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where +"add1 m 0 = m" | +"add1 m (Suc n) = add1 (Suc m) n" + +value "add1 1 3" +value "1 + 3" + +lemma abc [simp]: "add1 m 0 = m" +apply(induction m) +apply(simp) +apply(simp) +done + +lemma abc2 "add1 m n = m+n" +apply(induction n) +apply(auto) + +oops + +(* 3.3 Case Study: Compiling Expressions *) + +type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v" +datatype ('a, 'v)expr = + Cex 'v +| Vex 'a +| Bex "'v binop" "('a,'v)expr" "('a,'v)expr" + +primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where +"value (Cex v) env = v" | +"value (Vex a) env = env a" | +"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)" + +datatype ('a,'v)instr = + Const 'v +| Load 'a +| Apply "'v binop" + +primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" where +"exec [] s vs = vs" | +"exec (i#is) s vs = (case i of + Const v \<Rightarrow> exec is s (v#vs) + | Load a \<Rightarrow> exec is s ((s a)#vs) + | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))" + +primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where +"compile (Cex v) = [Const v]" | +"compile (Vex a) = [Load a]" | +"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]" + +theorem "exec (compile e) s [] = [value e s]" +(*the theorem needs to be generalized*) +oops + +(*more generalized theorem*) +theorem "\<forall> vs. exec (compile e) s vs = (value e s) # vs" +apply(induct_tac e) +apply(simp) +apply(simp) +oops + +lemma exec_app[simp]: "\<forall> vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" +apply(induct_tac xs) +apply(simp) +apply(simp) +apply(simp split: instr.split) +done + +(* 2.5.6 Case Study: Boolean Expressions *) + +datatype boolex = Const bool | Var nat | Neg boolex +| And boolex boolex + +primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where +"value2 (Const b) env = b" | +"value2 (Var x) env = env x" | +"value2 (Neg b) env = (\<not> value2 b env)" | +"value2 (And b c) env = (value2 b env \<and> value2 c env)" + +value "Const true" +value "Suc(Suc(0))" + +'b::Const = "true" + +value "value2 (Const true) (env = true)" +