--- a/progs/scala/re.scala	Tue Sep 13 11:49:22 2016 +0100
+++ b/progs/scala/re.scala	Thu Sep 22 00:40:03 2016 +0100
@@ -182,10 +182,24 @@
   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) 
+  case (CHAR(d), Empty) => Chr(d) 
   case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
 }
 
+def prj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
+  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(prj(r, c, v1)::vs)
+  case (SEQ(r1, r2), Sequ(v1, v2)) => 
+    if (flatten(v1) == "") Right(prj(r2, c, v2))      
+    else { if (nullable(r1)) Left(Sequ(prj(r1, c, v1), v2))
+           else Sequ(prj(r1, c, v1), v2)
+    }
+  case (ALT(r1, r2), Left(v1)) => Left(prj(r1, c, v1))
+  case (ALT(r1, r2), Right(v2)) => Right(prj(r2, c, v2))
+  case (CHAR(d), _) => Empty 
+  case (RECD(x, r1), _) => Rec(x, prj(r1, c, v))
+}
+
+
 // 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")
@@ -255,7 +269,11 @@
 
 def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
 
-lexing_sim(("a" + "ab") | ("b" + ""), "ab")
+lexing(("a" | "ab") ~ ("b" | ""), "ab")
+lexing_simp(("a" | "ab") ~ ("b" | ""), "ab")
+
+
+
 // brute force search infrastructure
 
 // enumerates regular expressions until a certain depth
@@ -294,6 +312,11 @@
 }     
 
 // exhaustively tests values of a regular expression
+def vfilter1(f: Rexp => Val => Boolean)(r: Rexp) : Set[(Rexp, Val)] = {
+  val vs = values(r)
+  for (v <- vs; if (f(r)(v))) yield (r, v)
+}
+
 def vfilter2(f: Rexp => Val => Val => Boolean)(r: Rexp) : Set[(Rexp, Val, Val)] = {
   val vs = values(r)
   for (v1 <- vs; v2 <- vs; if (f(r)(v1)(v2))) yield (r, v1, v2)
@@ -310,6 +333,18 @@
 enum(2, "abc").size
 //enum(3, "ab").size
 
+// test for inj/prj
+def injprj_test(r:Rexp)(v:Val) : Boolean =
+  if (flatten(v) != "") (inj(r, 'a', prj(r, 'a', v)) != v) else false
+
+val injprj_tst = enum(2, "ab").flatMap(vfilter1(injprj_test))
+val injprj_smallest = injprj_tst.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head
+
+prj(CHAR('b'), 'a', Chr('b'))
+inj(CHAR('b'), 'a', Empty)
+
+prj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Sequ(Right(Empty),Chr('a')))
+inj(SEQ(ALT(ONE,ONE),CHAR('a')), 'a', Right(Empty))
 
 // tests for totality
 def totality_test(r: Rexp)(v1: Val)(v2: Val) : Boolean =

--- a/thys/Re.thy	Tue Sep 13 11:49:22 2016 +0100
+++ b/thys/Re.thy	Thu Sep 22 00:40:03 2016 +0100
@@ -842,52 +842,6 @@
 
 section {* Sulzmann's Ordering of values *}
 
-thm PMatch.intros
-
-inductive ValOrds :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100] 100)
-where
-  "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
-| "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = s2; (flat v1' @ flat v2') \<sqsubseteq> (s1 @ s2)\<rbrakk> 
-   \<Longrightarrow> s1 @ s2 \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "\<lbrakk>(flat v2) \<sqsubseteq> (flat v1); flat v1 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
-| "\<lbrakk>(flat v1) \<sqsubset> (flat v2); flat v2 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
-| "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
-| "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
-| "[] \<turnstile> Void \<succ>EMPTY Void"
-| "[c] \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
-
-lemma valord_prefix:
-  assumes "s \<turnstile> v1 \<succ>r v2"
-  shows "flat v1 \<sqsubseteq> s"  and "flat v2 \<sqsubseteq> s"
-using assms
-apply(induct)
-apply(auto)
-apply(simp add: prefix_def rest_def)
-apply(auto)[1]
-apply(simp add: prefix_def rest_def)
-apply(auto)[1]
-apply(auto simp add: prefix_def rest_def)
-done
-
-lemma valord_prefix2:
-  assumes "s \<turnstile> v1 \<succ>r v2"
-  shows "flat v2 \<sqsubseteq> flat v1"
-using assms
-apply(induct)
-apply(auto)
-apply(simp add: prefix_def rest_def)
-apply(simp add: prefix_def rest_def)
-apply(auto)[1]
-defer
-apply(simp add: prefix_def rest_def)
-apply(auto)[1]
-apply (metis append_eq_append_conv_if append_eq_conv_conj)
-apply(simp add: prefix_def rest_def)
-apply(auto)[1]
-apply (metis append_eq_append_conv_if append_take_drop_id le_eq_less_or_eq)
-apply(simp add: prefix_def rest_def)
-apply(simp add: prefix_def rest_def)
-
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
@@ -1073,6 +1027,271 @@
 apply metis
 done
 
+section (* tryout with all-mkeps *)
+
+fun 
+  alleps :: "rexp \<Rightarrow> val set"
+where
+  "alleps(NULL) = {}"
+| "alleps(EMPTY) = {Void}"
+| "alleps(CHAR c) = {}"
+| "alleps(SEQ r1 r2) = {Seq v1 v2 | v1 v2. v1 \<in> alleps r1 \<and> v2 \<in> alleps r2}"
+| "alleps(ALT r1 r2) = {Left v1 | v1. v1 \<in> alleps r1} \<union> {Right v2 | v2. v2 \<in> alleps r2}"
+
+fun 
+  allvals :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where
+  "allvals r [] = alleps r"
+| "allvals r (c#s) = {injval r c v | v. v \<in> allvals (der c r) s}"
+
+
+lemma q1: 
+  assumes "v \<in> alleps r"
+  shows "\<turnstile> v : r \<and> flat v = []"
+using assms
+apply(induct r arbitrary: v)
+apply(auto intro: Prf.intros)
+done
+
+lemma q11:
+  assumes "nullable r" "\<turnstile> v : r" "flat v = []"
+  shows "v \<in> alleps r"
+using assms
+apply(induct r arbitrary: v)
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(subgoal_tac "nullable r2a")
+apply(auto)
+using not_nullable_flat apply auto[1]
+ apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(subgoal_tac "nullable r1a")
+apply(auto)
+using not_nullable_flat apply auto[1]
+done
+
+lemma q33:
+  assumes "nullable r"
+  shows "alleps r = {v. \<turnstile> v : r \<and> flat v = []}"
+using assms
+apply(auto)
+apply (simp_all add: q1)
+by (simp add: q11)
+
+lemma q22: 
+  assumes "v \<in> allvals r s"
+  shows "\<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s"
+using assms
+apply(induct s arbitrary: v r)
+apply(auto)
+apply(simp_all add: q1)
+using Prf_flat_L q1 apply fastforce
+apply (simp add: v3)
+apply (metis Prf_flat_L v3 v4)
+by (simp add: v4)
+
+
+lemma qa_oops:
+  assumes "\<turnstile> v : r" "\<exists>s. flat v = a # s \<and> a # s \<in> L r" "\<turnstile> projval r a v : der a r"
+  shows "injval r a (projval r a v) = v"
+using assms
+apply(induct v r arbitrary: )
+defer
+defer
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[4]
+apply(auto simp only:)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+
+done
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+using Prf_flat_L apply fastforce
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+using Prf_flat_L apply force
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)[1]
+apply(case_tac "nullable r1a")
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto simp add: Sequ_def)[1]
+apply(simp add: Cons_eq_append_conv)
+apply(auto)
+
+
+using Prf_flat_L 
+apply(erule Prf.cases)
+apply(simp_all)
+using Prf_flat_L
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(simp add: Sequ_def)
+apply(auto)[1]
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+sorry
+
+
+lemma q2:
+  assumes "s \<in> L(r)" 
+  shows "allvals r s = {v. \<turnstile> v : r \<and> s \<in> L (r) \<and> flat v = s}"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply(subst q33)
+using nullable_correctness apply blast
+apply(simp)
+apply(simp)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+using lex_correct1 lex_correct3 apply fastforce
+apply(simp)
+apply(auto)
+using v3 apply blast
+apply (simp add: v4)
+apply(rule_tac x="projval r a x" in exI)
+apply(rule conjI)
+defer
+apply(rule conjI)
+apply (simp add: v3_proj)
+apply (simp add: v4_proj2)
+apply(subgoal_tac "projval r a x \<in>  allvals (der a r) s")
+apply(simp)
+apply(subst qa_oops)
+apply(simp)
+apply(blast)
+
+lemma q2: 
+  assumes "\<turnstile> v : r" "s \<in> L (r)" "flat v = s"
+  shows "v \<in> allvals r s"
+using assms
+apply(induct s arbitrary: r v)
+apply(auto)
+apply(subgoal_tac "nullable r")
+apply(simp add: q11)
+using not_nullable_flat apply fastforce
+apply(drule sym)
+apply(simp)
+apply(case_tac s)
+apply(simp)
+
+apply(drule_tac x="projval r a v" in meta_spec) 
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+defer
+apply(drule meta_mp)
+using v3_proj apply blast
+apply(rule_tac x="projval r a v" in exI)
+apply(auto)
+defer
+apply(subst (asm) v4_proj2)
+apply(assumption)
+apply(assumption)
+apply(simp)
+apply(subst v4_proj2)
+apply(assumption)
+apply(assumption)
+apply(simp)
+apply(subst (asm) v4_proj2)
+apply(assumption)
+apply(assumption)
+sorry
+
+
+
+lemma
+ "{v. \<turnstile> v : r \<and> flat v = s} = allvals r s"
+apply(auto)
+apply(rule q2)
+apply(simp)
+
+
+definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" 
+where
+  "POSIX2 v r s \<equiv> (\<turnstile> v : r \<and> (\<forall>v'\<in>allvals r s. v \<succ>r v'))"
+
+lemma k1:
+  shows "POSIX2 v r [] \<Longrightarrow> \<forall>v' \<in> alleps r. v \<succ>r v'"
+using assms
+apply(induct r arbitrary: v)
+apply(simp_all)
+apply(simp add: POSIX2_def)
+apply(auto)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+apply(simp add: POSIX2_def)
+done
+
+lemma k2:
+  shows "POSIX2 v r s \<Longrightarrow> \<forall>v' \<in> allvals r s. v \<succ>r v'"
+using assms
+apply(induct s arbitrary: r v)
+apply(simp add: k1)
+apply(auto)
+apply(simp only: POSIX2_def)
+apply(simp)
+apply(clarify)
+apply(drule_tac x="injval r a va" in spec)
+apply(drule mp)
+defer
+apply(auto)
+done
+done
+
+lemma "s \<in> L(r) \<Longrightarrow> \<exists>v. POSIX2 v r s"
+apply(induct r arbitrary: s)
+apply(auto)
+apply(rule_tac x="Void" in exI)
+apply(simp add: POSIX2_def)
+apply (simp add: Prf.intros(4) ValOrd.intros(7))
+apply(rule_tac x="Char x" in exI)
+apply(simp add: POSIX2_def)
+apply (simp add: Prf.intros(5) ValOrd.intros(8))
+defer
+apply(drule_tac x="s" in meta_spec)
+apply(auto)[1]
+apply(rule_tac x="Left v" in exI)
+apply(simp add: POSIX2_def)
+apply(auto)[1]
+using Prf.intros(2) apply blast
+apply(case_tac s)
+apply(simp)
+apply(auto)[1]
+apply (simp add: ValOrd.intros(6))
+apply(rule ValOrd.intros)
+
 thm PMatch.intros[no_vars]
 
 lemma POSIX_PMatch: