# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1469021407 -3600
# Node ID cd9e40280784724003c2cd2a153442c2a7619e67
# Parent  115cf53a69d6cc956b243a5d91944ce215115ead
added paper about size derivatives

diff -r 115cf53a69d6 -r cd9e40280784 Literature/size-derivatives.pdf
Binary file Literature/size-derivatives.pdf has changed
diff -r 115cf53a69d6 -r cd9e40280784 TODO
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TODO	Wed Jul 20 14:30:07 2016 +0100
@@ -0,0 +1,1 @@
+Regular Path Queries & regular expressions
diff -r 115cf53a69d6 -r cd9e40280784 progs/scala/re-bit.scala
--- a/progs/scala/re-bit.scala	Fri Jun 24 12:35:16 2016 +0100
+++ b/progs/scala/re-bit.scala	Wed Jul 20 14:30:07 2016 +0100
@@ -151,6 +151,7 @@
   case c::cs => lex(der(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))
 
 
@@ -212,9 +213,13 @@
 }
 
 
-
+val rf = ("a" | "ab") ~ ("ab" | "")
+println(pre_lexing(rf, "ab"))
+println(lexing(rf, "ab"))
+println(lexing_simp(rf, "ab"))
 
 val r0 = ("a" | "ab") ~ ("b" | "")
+println(pre_lexing(r0, "ab"))
 println(lexing(r0, "ab"))
 println(lexing_simp(r0, "ab"))
 
diff -r 115cf53a69d6 -r cd9e40280784 thys/Lexer.thy
--- a/thys/Lexer.thy	Fri Jun 24 12:35:16 2016 +0100
+++ b/thys/Lexer.thy	Wed Jul 20 14:30:07 2016 +0100
@@ -31,6 +31,11 @@
 where
   "Der c A \<equiv> {s. c # s \<in> A}"
 
+definition
+  Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
+where
+  "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
 lemma Der_null [simp]:
   shows "Der c {} = {}"
 unfolding Der_def
@@ -104,6 +109,18 @@
 | ALT rexp rexp
 | STAR rexp
 
+fun ALTS :: "rexp list \<Rightarrow> rexp"
+where 
+  "ALTS [] = ZERO"
+| "ALTS [r] = r"
+| "ALTS (r # rs) = ALT r (ALTS rs)"
+
+fun SEQS :: "rexp list \<Rightarrow> rexp"
+where 
+  "SEQS [] = ONE"
+| "SEQS [r] = r"
+| "SEQS (r # rs) = SEQ r (SEQS rs)"
+
 section {* Semantics of Regular Expressions *}
  
 fun
@@ -116,6 +133,19 @@
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 
+lemma L_ALTS:
+  "L (ALTS rs) = (\<Union>r \<in> set rs. L(r))"
+by(induct rs rule: ALTS.induct)(simp_all)
+
+lemma L_SEQS:
+  "L (SEQS []) = {[]}"
+  "L (SEQS (r # rs)) = (L r) ;; (L (SEQS rs))"
+apply(simp)
+apply(case_tac rs)
+apply(simp)
+apply(simp)
+done
+
 
 section {* Nullable, Derivatives *}
 
@@ -154,11 +184,376 @@
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 by (induct r) (auto simp add: Sequ_def) 
 
-
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
 by (induct r) (simp_all add: nullable_correctness)
 
+lemma ders_correctness:
+  shows "L (ders s r) = Ders s (L r)"
+apply(induct s arbitrary: r)
+apply(simp_all add: Ders_def der_correctness Der_def)
+done
+
+lemma ders_ZERO:
+  shows "ders s (ZERO) = ZERO"
+apply(induct s)
+apply(simp_all)
+done
+
+lemma ders_ONE:
+  shows "ders s (ONE) = (if s = [] then ONE else ZERO)"
+apply(induct s)
+apply(simp_all add: ders_ZERO)
+done
+
+lemma ders_CHAR:
+  shows "ders s (CHAR c) = (if s = [c] then ONE else 
+                           (if s = [] then (CHAR c) else ZERO))"
+apply(induct s)
+apply(simp_all add: ders_ZERO ders_ONE)
+done
+
+lemma  ders_ALT:
+  shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"
+apply(induct s arbitrary: r1 r2)
+apply(simp_all)
+done
+
+
+
+definition
+  delta :: "rexp \<Rightarrow> rexp"
+where
+  "delta r \<equiv> (if nullable r then ONE else ZERO)"
+
+lemma delta_simp:
+  shows "nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = L r2"
+  and   "\<not>nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = {}"
+unfolding delta_def
+by simp_all
+
+fun str_split :: "string \<Rightarrow> string \<Rightarrow> (string * string) list"
+where
+  "str_split s1 [] = []"
+| "str_split s1 [c] = [(s1, [c])]"
+| "str_split s1 (c#s2) = (s1, c#s2) # str_split (s1 @ [c]) s2"
+
+fun ssplit :: "string \<Rightarrow> (string * string) list"
+where
+  "ssplit s = rev (str_split [] s)"  
+
+fun tsplit :: "string \<Rightarrow> (string * string) list"
+where
+  "tsplit s = tl (str_split [] s)" 
+
+
+value "ssplit([])"
+value "ssplit([a1])"
+value "ssplit([a1, a2])"
+value "ssplit([a1, a2, a3])"
+value "ssplit([a1, a2, a3, a4])"
+
+value "tsplit([])"
+value "tsplit([a1])"
+value "tsplit([a1, a2])"
+value "tsplit([a1, a2, a3])"
+value "tsplit([a1, a2, a3, a4])"
+
+function
+  D :: "string \<Rightarrow> rexp \<Rightarrow> rexp" 
+where
+  "D s (ZERO) = ZERO"
+| "D s (ONE) = (if s = [] then ONE else ZERO)"
+| "D s (CHAR c) = (if s = [c] then ONE else 
+                  (if s = [] then (CHAR c) else ZERO))"
+| "D s (ALT r1 r2) = ALT (D s r1) (D s r2)"
+| "D s (SEQ r1 r2) = ALTS ((SEQ (D s r1) r2) # [SEQ (delta (D s1 r1)) (D s2 r2). (s1, s2) \<leftarrow> (ssplit s)])"
+| "D [] (STAR r) = STAR r"
+| "D (c#s) (STAR r) = ALTS (SEQ (D (c#s) r) (STAR r) # 
+      [SEQS ((map (\<lambda>c. delta (D [c] r)) s1) @ [D s2 (STAR r)]). (s1, s2) \<leftarrow> (tsplit (c#s))])"
+sorry
+
+termination sorry
+
+thm D.simps
+thm tl_def
+
+lemma D_Nil:
+  shows "D [] r = r"
+apply(induct r)
+apply(simp_all)
+done
+
+lemma D_ALTS:
+  shows "D s (ALTS rs) = ALTS [D s r. r \<leftarrow> rs]"
+apply(induct rs rule: ALTS.induct)
+apply(simp_all)
+done
+
+(*
+lemma 
+  "D [a] (SEQ E F) = ALT (SEQ (D [a] E) F) (SEQ (delta E) (D [a] F))"
+apply(simp add: D_Nil)
+done
+
+lemma 
+  "D [a1, a2] (SEQ E F) = ALT (SEQ (D [a1, a2] E) F)
+     (ALT (SEQ (delta (D [a1] E)) (D [a2] F)) (SEQ (delta E) (D [a1, a2] F)))"
+apply(simp add: D_Nil)
+done
+*)
+(*
+lemma D_Der1:
+  shows "L(D [c] r) = L(der c r)"
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp)
+prefer 2
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(simp add: D_Nil)
+apply(simp add: delta_def)
+apply(simp add: D_Nil)
+apply(simp add: delta_def)
+apply(simp add: D_Nil)
+apply(simp add: delta_def)
+apply(simp)
+done
+
+lemma D_Der2:
+  shows "L(D [a1, a2] r) = L(der a2 (der a1 r))"
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp)
+prefer 2
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(simp add: delta_def)
+apply(auto split: if_splits)[1]
+apply(simp add: der_correctness Der_def D_Der1 D_Nil)
+apply(simp add: der_correctness Der_def D_Der1 D_Nil)
+apply (simp add: delta_def)
+apply(simp add: der_correctness Der_def D_Der1 D_Nil)
+apply (simp add: D_Der1 delta_def nullable_correctness)
+apply (simp add: D_Der1 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Nil)
+apply(simp add: der_correctness Der_def D_Der1 D_Nil)
+apply (simp add: D_Der1 delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(auto)[1]
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
+done
+
+lemma D_Der3:
+  shows "L(D [a1, a2, a3] r) = L(ders [a1, a2, a3] r)"
+apply(induct r)
+apply(simp)
+apply(simp)
+apply(simp)
+prefer 2
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+(* star case *)
+apply(simp)
+apply(auto)[1]
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply(simp add: Sequ_def)
+apply(auto)[1]
+defer
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+defer
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+defer
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+apply (simp add: D_Der2 delta_def nullable_correctness)
+apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
+defer
+done
+
+lemma D_Ders:
+  shows "L (D (s1 @ s2) r) = L (D s2 (D s1 r))"
+apply(induct r arbitrary: s1 s2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply (metis Cons_eq_append_conv append_is_Nil_conv)
+apply(simp)
+apply(auto)[1]
+apply(simp add: L_ALTS D_ALTS)
+apply(auto)[1]
+apply(simp add: L_ALTS)
+oops
+
+
+lemma D_cons:
+  shows "L (D (c # s) r) = L (D s (der c r))"
+apply(induct r arbitrary: c s)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+sorry
+
+lemma D_Zero:
+  shows "lang (D s Zero) = lang (derivs s Zero)"
+by (induct s) (simp_all)
+
+lemma D_One:
+  shows "lang (D s One) = lang (derivs s One)"
+by (induct s) (simp_all add: D_Zero[symmetric])
+
+lemma D_Atom:
+  shows "lang (D s (Atom c)) = lang (derivs s (Atom c))"
+by (induct s) (simp_all add: D_Zero[symmetric] D_One[symmetric])
+
+lemma D_Plus:
+  shows "lang (D s (Plus r1 r2)) = lang (derivs s (Plus r1 r2))"
+by (induct s arbitrary: r1 r2) (simp_all add: D_empty D_cons)
+
+lemma D_Times:
+  shows "lang (D s (Times r1 r2)) = lang (derivs s (Times r1 r2))"
+apply(induct s arbitrary: r1 r2) 
+apply(simp_all add: D_empty D_cons)
+apply(auto simp add: conc_def)[1]
+apply(simp only: D_Plus[symmetric])
+apply(simp only: D.simps)
+apply(simp)
+*)
+
 
 section {* Values *}
 
diff -r 115cf53a69d6 -r cd9e40280784 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Fri Jun 24 12:35:16 2016 +0100
+++ b/thys/Sulzmann.thy	Wed Jul 20 14:30:07 2016 +0100
@@ -1,6 +1,6 @@
    
 theory Sulzmann
-  imports "Lexer" 
+  imports "Lexer" "~~/src/HOL/Library/Multiset"
 begin
 
 
@@ -82,6 +82,10 @@
                                     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: