# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1428701916 -3600
# Node ID f95a405c3180e9ba285831cec3db3c47d6bb457f
# Parent  dfa9dbb8f8e6f4d7c31755ec379e32e8bfb6a74f
updated

diff -r dfa9dbb8f8e6 -r f95a405c3180 Literature/stal-extended.pdf
Binary file Literature/stal-extended.pdf has changed
diff -r dfa9dbb8f8e6 -r f95a405c3180 progs/scala/re.scala
--- a/progs/scala/re.scala	Fri Mar 13 21:27:03 2015 +0000
+++ b/progs/scala/re.scala	Fri Apr 10 22:38:36 2015 +0100
@@ -233,6 +233,51 @@
 def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
 
 
+// brute force infrastructure
+
+def enum(n: Int, s: String) : Set[Rexp] = n match {
+  case 0 => Set(NULL, EMPTY) ++ s.toSet.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))
+  }
+}
+
+def ord(v1: Val, r: Rexp, v2: Val) : Boolean = (v1, r, v2) match {
+  case (Void, EMPTY, Void) => true
+  case (Chr(c1), CHAR(c2), Chr(c3)) if (c1==c2 && c1==c3) => true
+  case (Left(v1), ALT(r1,r2), Left(v2)) => ord(v1,r1,v2)
+  case (Right(v1), ALT(r1,r2), Right(v2)) => ord(v1,r2,v2)
+  case (Left(v1), ALT(r1,r2), Right(v2)) => flatten(v2).length <= flatten(v1).length
+  case (Right(v1), ALT(r1,r2), Left(v2)) => flatten(v2).length < flatten(v1).length
+  case (Sequ(v1,v2), SEQ(r1,r2), Sequ(v3,v4)) if(v1==v3) => ord(v2, r2, v4)
+  case (Sequ(v1,v2), SEQ(r1,r2), Sequ(v3,v4)) if(v1!=v3) => ord(v1, r1, v3)
+  case _ => false
+}     
+
+def tst(r: Rexp, c: Char) : Set[(Rexp, Val, Val, Val, Val)] = {
+  val r_der = der(c, r)
+  val vs = values(r_der)
+  for (v1 <- vs; v2 <- vs; 
+       if (v1 != v2 && ord(v1, r_der, v2) && ord(inj(r, c, v2), r, inj(r, c, v1)))) 
+  yield (r, v1, v2, inj(r, c, v1), inj(r, c, v2))  
+}
+
+def comp(r1: (Rexp, Val, Val, Val, Val), r2: (Rexp, Val, Val, Val, Val)) = size(r1._1) < size(r2._1)
+
+
+val smallest = enum(3, "a").flatMap(tst(_, 'a')).toList.sortWith { comp }.head
+
+smallest match {
+  case (r, v1, v2, v3, v4) => List(pretty(r),
+                                   pretty(der('a', r)),
+                                   vpretty(v1),
+                                   vpretty(v2),
+                                   vpretty(v3),
+                                   vpretty(v4)).mkString("\n") }
+
 // Lexing Rules for a Small While Language
 
 def PLUS(r: Rexp) = r ~ r.%
@@ -371,7 +416,16 @@
   time(lexing_simp(WHILE_REGS, prog2 * i))
 }
 
-val a0 = (EMPTY | "a") ~ ("b" | "abc")
+
+val a0 = (EMPTY | "a") ~ (EMPTY | "ab")
+val a1 = der('a', a0)
+pretty(a1)
+val m = mkeps(a1)
+vpretty(m)
+val v = inj(a0, 'a', m)
+vpretty(v)
+
+val a0 = (EMPTY | "a") ~ (EMPTY | "ab")
 val a1 = der('a', a0)
 pretty(a1)
 values(a1).toList
@@ -381,3 +435,15 @@
 vpretty(inj(a0,'a',u1))
 vpretty(inj(a0,'a',u2))
 
+lexing(a0, "ab")
+val aa = der('a', a0)
+pretty(aa)
+val ab = der('b', aa)
+pretty(ab)
+nullable(ab)
+val m = mkeps(ab)
+vpretty(m)
+val vb = inj(aa, 'b', m)
+vpretty(vb)
+val va = inj(a0, 'a', vb)
+vpretty(va)
diff -r dfa9dbb8f8e6 -r f95a405c3180 thys/Re1.thy
--- a/thys/Re1.thy	Fri Mar 13 21:27:03 2015 +0000
+++ b/thys/Re1.thy	Fri Apr 10 22:38:36 2015 +0100
@@ -31,6 +31,11 @@
 | SEQ rexp rexp
 | ALT rexp rexp
 
+fun SEQS :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp"
+where
+  "SEQS r [] = r"
+| "SEQS r (r'#rs) = SEQ r (SEQS r' rs)"
+
 section {* Semantics of Regular Expressions *}
  
 fun
@@ -51,6 +56,22 @@
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
+fun
+ nullable_left :: "rexp \<Rightarrow> bool"
+where
+  "nullable_left (NULL) = False"
+| "nullable_left (EMPTY) = True"
+| "nullable_left (CHAR c) = False"
+| "nullable_left (ALT r1 r2) = (nullable_left r1 \<or> nullable_left r2)"
+| "nullable_left (SEQ r1 r2) = nullable_left r1"
+
+lemma nullable_left:
+  "nullable r \<Longrightarrow> nullable_left r"
+apply(induct r)
+apply(auto)
+done
+
+
 value "L(CHAR c)"
 value "L(SEQ(CHAR c)(CHAR b))"
 
@@ -69,6 +90,12 @@
 | Right val
 | Left val
 
+fun Seqs :: "val \<Rightarrow> val list \<Rightarrow> val"
+where
+  "Seqs v [] = v"
+| "Seqs v (v'#vs) = Seq v (Seqs v' vs)"
+
+
 section {* The string behind a value *}
 
 fun flat :: "val \<Rightarrow> string"
@@ -79,6 +106,22 @@
 | "flat(Right v) = flat(v)"
 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)"
 
+fun flat_left :: "val \<Rightarrow> string"
+where
+  "flat_left(Void) = []"
+| "flat_left(Char c) = [c]"
+| "flat_left(Left v) = flat_left(v)"
+| "flat_left(Right v) = flat_left(v)"
+| "flat_left(Seq v1 v2) = flat_left(v1)"
+
+fun flat_right :: "val \<Rightarrow> string"
+where
+  "flat_right(Void) = []"
+| "flat_right(Char c) = [c]"
+| "flat_right(Left v) = flat(v)"
+| "flat_right(Right v) = flat(v)"
+| "flat_right(Seq v1 v2) = flat(v2)"
+
 fun head :: "val \<Rightarrow> string"
 where
   "head(Void) = []"
@@ -107,6 +150,11 @@
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
 
+inductive Prfs :: "val list \<Rightarrow> rexp list \<Rightarrow> bool"  ("\<Turnstile> _ : _" [100, 100] 100)
+where
+  "\<Turnstile> [] : []"
+| "\<lbrakk>\<turnstile>v : r; \<Turnstile> vs : rs\<rbrakk> \<Longrightarrow> \<Turnstile> (v#vs) : (r#rs)"
+
 fun mkeps :: "rexp \<Rightarrow> val"
 where
   "mkeps(EMPTY) = Void"
@@ -130,6 +178,15 @@
 apply(auto)
 done
 
+lemma mkeps_flat_left:
+  assumes "nullable(r)" shows "flat_left (mkeps r) = []"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto)
+done
+
+
+
 text {*
   The value mkeps returns is always the correct POSIX
   value.
@@ -142,7 +199,7 @@
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-apply(induct)
+apply(induct v r rule: Prf.induct)
 apply(auto simp add: Sequ_def)
 done
 
@@ -176,6 +233,33 @@
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
 
+inductive ValOrd2 :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsupset>_,_ _" [100, 100, 100, 100] 100)
+where
+  "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(length (flat v1) + n) (Seq v1 v2')" 
+| "\<lbrakk>v1 \<sqsupset>r1,n v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(n + length (flat v2)) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),(length (flat v1)) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),(length (flat v2)) (Left v1)"
+| "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),n (Right v2')"
+| "v1 \<sqsupset>r1,n v1' \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),n (Left v1')"
+| "Void \<sqsupset>EMPTY,0 Void"
+| "(Char c) \<sqsupset>(CHAR c),1 (Char c)"
+
+lemma 
+  assumes "v1 \<sqsupset>r,n v2"
+  shows "length(flat v1) = n"
+using assms
+apply(induct)
+apply(auto)
+done
+
+lemma 
+  assumes "v1 \<sqsupset>r,n v2"
+  shows "length(flat v2) <= n"
+using assms
+apply(induct)
+apply(auto)
+oops
+
 
 section {* The ordering is reflexive *}
 
@@ -541,10 +625,12 @@
 apply(case_tac "nullable r1")
 apply(simp)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all (no_asm_use))[5]
 apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps flat.simps)
 apply(auto)[1]
 apply (metis mkeps_flat)
 apply(simp)
@@ -552,6 +638,41 @@
 apply(simp_all)[5]
 done
 
+lemma v4_flat_left:
+  assumes "\<turnstile> v : der c r" "\<not>(nullable_left r)" shows "flat_left (injval r c v) = c # (flat_left v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+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 (no_asm_use))[5]
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps)
+apply (metis nullable_left)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+done
+
+
 lemma v4_proj:
   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
   shows "c # flat (projval r c v) = flat v"
@@ -682,61 +803,6 @@
 apply(simp add: v4)
 done
 
-(*
-lemma 
- assumes "\<turnstile> v : der c r" "flat v \<noteq> []"
- shows "injval r c v \<succ>r mkeps r"
-using assms
-apply(induct c r arbitrary: v rule: der.induct)
-apply(simp_all)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(case_tac "c = c'")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis ValOrd.intros(6))
-apply(clarify)
-apply (metis ValOrd.intros(4) drop_0 drop_all le_add2 list.distinct(1) list.size(3) mkeps_flat monoid_add_class.add.right_neutral nat_less_le v4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-defer
-apply(rule ValOrd.intros)
-apply metis
-apply(case_tac "nullable r1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply(subst mkeps_flat)
-oops
-*)
-
-
 lemma LeftRight:
   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
   and "\<turnstile> v1 : der c r1" "\<turnstile> v2 : der c r2" 
@@ -820,15 +886,92 @@
 by (metis h)
 
 lemma Prf_inj_test:
-  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2"
-  shows "(injval r c v1) \<succ>r (injval r c v2)"
-sorry
+  assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"  "\<Turnstile> vs : rs" "flat v1 = flat v2"
+  shows "Seqs (injval r c v1) vs \<succ>(SEQS r rs) Seqs (injval r c v2) vs"
+using assms
+apply(induct arbitrary: v1 v2 vs rs rule: der.induct)
+(* NULL case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* EMPTY case *)
+apply(simp)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+(* CHAR case *)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* ALT case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis ValOrd.intros(6))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis LeftRight ValOrd.intros(3) der.simps(4) injval.simps(2) injval.simps(3))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis RightLeft ValOrd.intros(4) der.simps(4) injval.simps(2) injval.simps(3))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis ValOrd.intros(5))
+(* SEQ case *)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros)
+apply(simp)
+apply(clarify)
+apply(rule ValOrd.intros(2))
+apply(rotate_tac 2)
+apply(drule_tac x="v1c" in meta_spec)
+apply(rotate_tac 10)
+apply(drule_tac x="v1'" in meta_spec)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(assumption)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(subst v4)
+apply(simp)
+apply(subst (asm) v4)
+apply(simp)
+apply(simp)
+apply(simp add: prefix_def)
+oops
 
 lemma Prf_inj:
   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*)
   shows "(injval r c v1) \<succ>r (injval r c v2)"
 using assms
-apply(induct arbitrary: v1 v2 rule: der.induct)
+apply(induct c r arbitrary: v1 v2 rule: der.induct)
 (* NULL case *)
 apply(simp)
 apply(erule ValOrd.cases)
@@ -970,6 +1113,7 @@
 apply (metis list.distinct(1) mkeps_flat v4)
 oops
 
+
 lemma POSIX_der:
   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
   shows "POSIX (injval r c v) r"
@@ -977,7 +1121,7 @@
 unfolding POSIX_def
 apply(auto)
 thm v3
-apply (metis v3)
+apply (erule v3)
 thm v4
 apply(subst (asm) v4)
 apply(assumption)
@@ -998,10 +1142,123 @@
 apply(rule_tac x="flat v" in exI)
 apply(simp)
 apply(simp)
-thm Prf_inj_test
-apply(drule Prf_inj_test)
+oops
+
+lemma POSIX_der:
+  assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
+  shows "POSIX (injval r c v) r"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+(* null case*)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* empty case *)
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* char case *)
+apply(simp add: POSIX_def)
+apply(case_tac "c = c'")
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* alt case *)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(2) v3)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis POSIX_ALT2 POSIX_def ValOrd.intros(6))
+apply (metis ValOrd.intros(3) order_refl)
+apply(simp (no_asm) add: POSIX_def)
+apply(auto)[1]
+apply (metis Prf.intros(3) v3)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+defer
+apply (metis POSIX_ALT1a POSIX_def ValOrd.intros(5))
+prefer 2
+apply(subst (asm) (5) POSIX_def)
+apply(auto)[1]
+apply(rotate_tac 5)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(subst (asm) v4)
 apply(simp)
-apply (metis v3_proj)
+apply(drule_tac x="Left (projval r1a c v1)" in spec)
+apply(clarify)
+apply(drule mp)
+apply(rule conjI)
+apply (metis Prf.intros(2) v3_proj)
+apply(simp)
+apply (metis v4_proj2)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis less_not_refl v4_proj2)
+(* seq case *)
+apply(case_tac "nullable r1")
+defer
+apply(simp add: POSIX_def)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Prf.intros(1) v3)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(subst (asm) (3) v4)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "flat v1a \<noteq> []")
+prefer 2
+apply (metis Prf_flat_L nullable_correctness)
+apply(subgoal_tac "\<exists>s. flat v1a = c # s")
+prefer 2
+apply (metis append_eq_Cons_conv)
+apply(auto)[1]
+ 
+
+apply(auto)
+thm v3
+apply (erule v3)
+thm v4
+apply(subst (asm) v4)
+apply(assumption)
+apply(drule_tac x="projval r c v'" in spec)
+apply(drule mp)
+apply(rule conjI)
+thm v3_proj
+apply(rule v3_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+thm t
 apply(rule_tac c="c" in  t)
 apply(simp)
 thm v4_proj
@@ -1010,10 +1267,7 @@
 apply(rule_tac x="flat v" in exI)
 apply(simp)
 apply(simp)
-
-apply(simp add: Cons_eq_append_conv)
-apply(auto)[1]
-
+oops
 
 
 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r"
diff -r dfa9dbb8f8e6 -r f95a405c3180 thys/notes.pdf
Binary file thys/notes.pdf has changed
diff -r dfa9dbb8f8e6 -r f95a405c3180 thys/notes.tex
--- a/thys/notes.tex	Fri Mar 13 21:27:03 2015 +0000
+++ b/thys/notes.tex	Fri Apr 10 22:38:36 2015 +0100
@@ -435,9 +435,7 @@
       Many of such rule are called intro-rules and end with 
       an ``$I$'', or in case of inductive predicates $\_.intros$.
       
-      
-       
-       
+   
 \end{itemize}