--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Literature/LINKS	Mon Jun 08 14:37:19 2015 +0100
@@ -0,0 +1,2 @@
+https://swtch.com/~rsc/regexp/
+https://wiki.haskell.org/Regex_Posix
\ No newline at end of file

--- a/progs/scala/re.scala	Mon May 25 16:09:23 2015 +0100
+++ b/progs/scala/re.scala	Mon Jun 08 14:37:19 2015 +0100
@@ -39,7 +39,7 @@
   def | (r: String) = ALT(s, r)
   def % = STAR(s)
   def ~ (r: Rexp) = SEQ(s, r)
-  def ~ (r: String) = SEQ(s, r)
+  def ~ (r: String) = SEQ(s, r)n jjjjjjj=99999ij9999ijn0n
   def $ (r: Rexp) = RECD(s, r)
 }
 
@@ -87,6 +87,18 @@
   case RECD(_, r) => values(r)
 }
 
+// zeroable function: tests whether the regular 
+// expression cannot regognise any string
+def zeroable (r: Rexp) : Boolean = r match {
+  case NULL => true
+  case EMPTY => false
+  case CHAR(_) => false
+  case ALT(r1, r2) => zeroable(r1) && zeroable(r2)
+  case SEQ(r1, r2) => zeroable(r1) || zeroable(r2)
+  case STAR(_) => false
+  case RECD(_, r1) => zeroable(r1)
+}
+
 
 // nullable function: tests whether the regular 
 // expression can recognise the empty string
@@ -244,8 +256,9 @@
 def lexing_simp(r: Rexp, s: String) : Val = lex_simp(r, s.toList)
 
 
-// brute force infrastructure
+// brute force search infrastructure
 
+// enumerates regular expressions until a certain depth
 def enum(n: Int, s: String) : Set[Rexp] = n match {
   case 0 => Set(NULL, EMPTY) ++ s.toSet.map(CHAR)
   case n => {
@@ -256,49 +269,120 @@
   }
 }
 
-def ord(v1: Val, r: Rexp, v2: Val) : Boolean = (v1, r, v2) match {
+def ordr(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 (Chr(c1), CHAR(c2), Chr(c3)) if (c1 == c2 && c1 == c3) => true
+  case (Left(v1), ALT(r1, r2), Left(v2)) => ordr(v1, r1, v2)
+  case (Right(v1), ALT(r1, r2), Right(v2)) => ordr(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) => ordr(v2, r2, v4)
+  case (Sequ(v1, v2), SEQ(r1, r2), Sequ(v3, v4)) if (v1 != v3) => ordr(v1, r1, v3)
+  case _ => false
+}     
+
+def ord(v1: Val, v2: Val) : Boolean = (v1, v2) match {
+  case (Void, Void) => true
+  case (Chr(c1), Chr(c2)) if (c1 == c2) => true
+  case (Left(v1), Left(v2)) => ord(v1, v2)
+  case (Right(v1), Right(v2)) => ord(v1, v2)
+  case (Left(v1), Right(v2)) => flatten(v2).length <= flatten(v1).length
+  case (Right(v1), Left(v2)) => flatten(v2).length < flatten(v1).length
+  case (Sequ(v1, v2), Sequ(v3, v4)) if (v1 == v3) => ord(v2, v4)
+  case (Sequ(v1, v2), Sequ(v3, v4)) if (v1 != v3) => ord(v1, v3)
   case _ => false
 }     
 
-def tst(r: Rexp, c: Char) : Set[(Rexp, Val, Val, Val, Val, List[String], List[String])] = {
-  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)) && 
-           (flatten(inj(r, c, v1)) == flatten(inj(r, c, v2))))) 
-  yield (r, v1, v2, inj(r, c, v1), inj(r, c, v2), flattens(inj(r, c, v1)), flattens(inj(r, c, v2)))  
+// exhaustively tests values of a regular expression
+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)
+}
+
+def vfilter3(f: Rexp => Val => Val => Val => Boolean)(r: Rexp) : Set[(Rexp, Val, Val, Val)] = {
+  val vs = values(r)
+  for (v1 <- vs; v2 <- vs; v3 <- vs; if (f(r)(v1)(v2)(v3))) yield (r, v1, v2, v3)
+}
+
+// number of test cases
+enum(3, "a").size
+enum(2, "ab").size
+enum(2, "abc").size
+//enum(3, "ab").size
+
+
+// tests for totality
+def totality_test(r: Rexp)(v1: Val)(v2: Val) : Boolean =
+  !(ord(v1, v2) || ord(v2, v1))
+
+enum(2, "ab").flatMap(vfilter2(totality_test))
+enum(3, "a").flatMap(vfilter2(totality_test))
+
+
+//tests for transitivity (simple transitivity fails)
+def transitivity_test(r: Rexp)(v1: Val)(v2: Val)(v3: Val) : Boolean = 
+  ord(v1, v2) && ord(v2, v3) && !ord(v1, v3)
+
+def transitivity_test_extended(r: Rexp)(v1: Val)(v2: Val)(v3: Val) : Boolean = {
+  flatten(v1) == flatten(v2) && flatten(v2) == flatten(v3) && 
+  ord(v1, v2) && ord(v2, v3) && !ord(v1, v3)
 }
 
-def tst2(r: Rexp, c: Char) : Set[(Rexp, Val, Val, Val, Val, List[String], List[String])] = {
+// smallest(?) example where simple transitivity fails 
+val test1 = enum(3, "a").flatMap(vfilter3(transitivity_test))
+val test1_smallest = test1.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head
+
+pretty(test1_smallest._1)
+vpretty(test1_smallest._2)
+vpretty(test1_smallest._3)
+vpretty(test1_smallest._4)
+
+ord(test1_smallest._2, test1_smallest._3)
+ord(test1_smallest._3, test1_smallest._4)
+ord(test1_smallest._2, test1_smallest._4)
+ordr(test1_smallest._3, test1_smallest._1, test1_smallest._4)
+
+// with flatten test
+enum(3, "a").flatMap(vfilter3(transitivity_test_extended))
+
+//injection tests
+def injection_test(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = {
+  v1 != v2 && 
+  ord(v1, v2) && 
+  ord(inj(r, c, v2), inj(r, c, v1)) && 
+  flatten(v1) == flatten(v2)
+}
+
+def injection_testA(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = {
+  v1 != v2 && 
+  ord(v1, v2) && 
+  ord(inj(r, c, v2), inj(r, c, v1)) && 
+  flatten(v1).length == flatten(v2).length
+}
+
+def injection_test2(r: Rexp)(c: Char)(v1: Val)(v2: Val) : Boolean = {
+  v1 != v2 && 
+  ord(v1, v2) && 
+  ord(inj(r, c, v2), inj(r, c, v1))
+}
+def vfilter4(f: Rexp => Char => Val => Val => Boolean)(c: Char)(r: Rexp) : Set[(Rexp, Rexp, 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(proj(r, c, v2), r_der, proj(r, c, v1))) 
-  yield (r, v1, v2, proj(r, c, v1), proj(r, c, v2), flattens(inj(r, c, v1)), flattens(inj(r, c, v2)))  
-}
+  for (v1 <- vs; v2 <- vs; if (f(r)(c)(v1)(v2))) yield (r, r_der, v1, v2)
+} 
 
-def comp(r1: (Rexp, Val, Val, Val, Val, List[String], List[String]), 
-         r2: (Rexp, Val, Val, Val, Val, List[String], List[String])) = size(r1._1) < size(r2._1)
-
+enum(3, "a").flatMap(vfilter4(injection_test)('a'))
+enum(3, "a").flatMap(vfilter4(injection_testA)('a'))
 
-val smallest = enum(3, "a").flatMap(tst(_, 'a')).toList.sortWith { comp }
+val test2 = enum(3, "a").flatMap(vfilter4(injection_test2)('a'))
+val test2_smallest = test2.toList.sortWith { (x,y) => size(x._1) < size(y._1) }.head
 
-smallest match {
-  case Nil => "none"
-  case (r, v1, v2, v3, v4, s1, s2)::_ => List(pretty(r),
-                                   pretty(der('a', r)),
-                                   vpretty(v1),
-                                   vpretty(v2),
-                                   vpretty(v3),
-                                   vpretty(v4), s1, s2).mkString("\n") }
+pretty(test2_smallest._1)
+pretty(test2_smallest._2)
+vpretty(test2_smallest._3)
+vpretty(test2_smallest._4)
+vpretty(inj(test2_smallest._1, 'a', test2_smallest._3))
+vpretty(inj(test2_smallest._1, 'a', test2_smallest._4))
 
 // Lexing Rules for a Small While Language
 
@@ -469,3 +553,13 @@
 vpretty(vb)
 val va = inj(a0, 'a', vb)
 vpretty(va)
+
+
+/* ord is not transitive in general: counter-example
+ *
+ * (1)  Left(Right(Right(())))
+ * (2)  Right(Left(()) ~ Left(()))
+ * (3)  Right(Right(()) ~ Right(a))
+ *
+ * (1) > (2); (2) > (3) but not (1) > (3)
+*/

--- a/thys/Re1.thy	Mon May 25 16:09:23 2015 +0100
+++ b/thys/Re1.thy	Mon Jun 08 14:37:19 2015 +0100
@@ -434,111 +434,120 @@
 apply(simp_all)[8]
 done
 
-lemma ValOrd_max:
-  shows "\<exists>v. \<forall>v'. (v' \<succ>r v \<longrightarrow> v = v')" 
-apply(induct r)
-apply(auto)
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
+lemma
+  "s \<in> L r \<longrightarrow> (\<exists>vmax \<in> {v. \<turnstile> v : r \<and> flat v = s}. \<forall>v \<in> {v. \<turnstile> v : r \<and> flat v = s}. vmax 2\<succ> v)"
+apply(induct s arbitrary: r rule: length_induct)
+apply(induct_tac r rule: rexp.induct)
 apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
-apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
-apply(rule allI)
+apply(simp)
+apply(simp)
 apply(rule impI)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-done
-
-lemma ValOrd_max:
-  assumes "L r \<noteq> {}"
-  shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. ((\<turnstile> v' : r \<and> v' \<succ>r v) \<longrightarrow> v = v'))" 
-using assms
-apply(induct r)
-apply(auto)
-apply(rule exI)
+apply(simp)
+apply(rule_tac x="Void" in exI)
+apply(simp)
 apply(rule conjI)
-apply(rule Prf.intros)
+apply (metis Prf.intros(4))
 apply(rule allI)
 apply(rule impI)
 apply(erule conjE)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rule exI)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(7))
+apply(simp)
+apply(rule impI)
+apply(rule_tac x="Char char" in exI)
+apply(simp)
 apply(rule conjI)
-apply(rule Prf.intros)
+apply (metis Prf.intros)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(simp)
+apply(rule impI)
+apply(simp add: Sequ_def)[1]
+apply(erule exE)+
+apply(erule conjE)+
+apply(clarify)
+defer
+apply(simp)
+apply(rule conjI)
+apply(rule impI)
+apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(rule_tac x="Left vmax" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(2))
+apply(simp)
 apply(rule allI)
 apply(rule impI)
 apply(erule conjE)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto simp add: Sequ_def)[1]
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(auto)[1]
-apply(drule_tac x="Seq v va" in spec)
-apply(drule mp)
-apply (metis Prf.intros(1))
-apply(auto)[1]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(rotate_tac 6)
+apply(rotate_tac 5)
 apply(erule Prf.cases)
 apply(simp_all)[5]
-apply(rotate_tac 6)
+apply (metis ValOrd2.intros(6))
+apply(clarify)
+apply (metis ValOrd2.intros(3) order_refl)
+apply(rule impI)
+apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(rule_tac x="Right vmax" in exI)
+apply(simp)
+apply(rule conjI)
+apply (metis Prf.intros(3))
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)+
+apply(rotate_tac 5)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(simp)
+apply(rule impI)
+apply(simp add: Sequ_def)[1]
+apply(erule exE)+
+apply(erule conjE)+
 apply(clarify)
-apply metis
-apply(drule meta_mp)
-apply (metis empty_iff)
-apply(auto)[1]
-apply(drule_tac x="Left v" in spec)
-apply(drule mp)
-apply (metis Prf.intros)
-apply(auto)[1]
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(auto)[1]
-oops
+
+
+inductive ValOrd3 :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ 3\<succ>_ _" [100, 100, 100] 100)
+where
+  "\<lbrakk>v2 3\<succ>r2 v2'; \<turnstile> v1 : r1\<rbrakk> \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1 v2')" 
+| "\<lbrakk>v1 3\<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = flat v2'; \<turnstile> v2 : r2; \<turnstile> v2' : r2\<rbrakk> 
+      \<Longrightarrow> (Seq v1 v2) 3\<succ>(SEQ r1 r2) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Left v1)"
+| "v2 3\<succ>r2 v2' \<Longrightarrow> (Right v2) 3\<succ>(ALT r1 r2) (Right v2')"
+| "v1 3\<succ>r1 v1' \<Longrightarrow> (Left v1) 3\<succ>(ALT r1 r2) (Left v1')"
+| "Void 3\<succ>EMPTY Void"
+| "(Char c) 3\<succ>(CHAR c) (Char c)"
+
 
-lemma ValOrd_max2:
-  shows "\<exists>v. \<turnstile> v : r \<and> (\<forall>v'. v \<succ>r v')" 
-using ValOrd_max[where r="r"]
-apply -
-apply(auto)
-apply(rule_tac x="v" in exI)
-apply(auto)
-oops
+lemma "v1 3\<succ>r v2 \<Longrightarrow> v1 \<succ>r v2 \<and> \<turnstile> v1 : r \<and> \<turnstile> v2 : r \<and> flat v1 = flat v2"
+apply(induct rule: ValOrd3.induct)
+prefer 8
+apply(simp)
+apply (metis Prf.intros(5) ValOrd.intros(8))
+prefer 7
+apply(simp)
+apply (metis Prf.intros(4) ValOrd.intros(7))
+apply(simp)
+apply (metis Prf.intros(1) ValOrd.intros(1))
+apply(simp)
+
+
+
 
 lemma ValOrd_trans:
-  assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" "flat v1 = flat v2" "flat v2 = flat v3"
+  assumes "v1 \<succ>r v2" "v2 \<succ>r v3" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r" 
+     "flat v1 = flat v2" "flat v2 = flat v3"
   shows "v1 \<succ>r v3"
 using assms
-apply(induct r arbitrary: v1 v2 v3)
+apply(induct r arbitrary: v1 v2 v3 s1 s2 s3)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(erule Prf.cases)
@@ -574,10 +583,89 @@
 apply (rule ValOrd.intros(2))
 prefer 2
 apply(auto)[1]
-prefer 2
+apply metis
+apply(erule Prf.cases)
+apply(simp_all)[5]
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (rule ValOrd.intros)
+apply(clarify)
 oops
 
 
+lemma ValOrd_max:
+  shows "L r \<noteq> {} \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<longrightarrow> v' \<succ>r v \<longrightarrow> v = v'))" 
+using assms
+apply(induct r)
+apply(auto)[3]
+apply(rule_tac x="Void" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(4))
+apply(rule allI)
+apply(rule impI)+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule_tac x="Char char" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(5))
+apply(rule allI)
+apply(rule impI)+
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(simp add: L.simps)
+apply(auto simp: Sequ_def)[1]
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(erule exE)+
+apply(rule_tac x="Seq v va" in exI)
+apply(rule conjI)
+apply (metis Prf.intros(1))
+apply(rule allI)
+apply(rule impI)+
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply metis
+apply(simp only: L.simps Lattices.bounded_lattice_bot_class.sup_eq_bot_iff HOL.de_Morgan_conj)
+apply(erule disjE)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(erule exE)+
+apply(rule exI)
+apply(rule conjI)
+apply(rule Prf.intros)
+apply(erule conjE)+
+apply(assumption)
+apply(rule allI)
+apply(rule impI)+
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(drule meta_mp)
+apply (metis Prf_flat_L empty_iff)
+apply(auto)[1]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+oops
 
 section {* Posix definition *}
 
@@ -661,6 +749,7 @@
 apply(drule meta_mp)
 apply (metis empty_iff)
 apply(auto)
+oops
 
 section {* POSIX for some constructors *}
 
@@ -1533,102 +1622,7 @@
 apply(auto)
 apply(frule POSIXs_ALT1a)
 (* HERE *)
-apply(auto)
-apply(rule ccontr)
-apply(simp)
-apply(auto)[1]
-apply(drule POSIXs_ALT1a)
-thm ValOrd2.intros
-
-apply(simp (no_asm) add: POSIXs_def)
-apply(auto)[1]
-apply (metis POSIXs_def 
-der.simps(4) v3s)
-apply(subst (asm) (5) POSIXs_def)
-apply(auto)[1]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(drule_tac x="v1a" in meta_spec)
-apply(drule_tac x="sb" in meta_spec)
-apply(drule_tac meta_mp)
-defer
-apply (metis POSIXs_def)
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(subst v4)
-apply (metis Prfs_Prf)
-apply(simp)
-apply(drule_tac x="Left (injval r1a c v1)" in spec)
-apply(drule mp)
-apply(rule Prfs.intros)
-defer
-apply(erule ValOrd2.cases)
-apply(simp_all)[8] 
-apply(clarify)
-thm v4s
-apply(subst (asm) v4s[of "sb"])
-apply(assumption)
-apply(simp)
-apply(clarify)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(auto)[1]
-apply(rule ValOrd2.intros)
-apply(subst v4)
-apply (metis Prfs_Prf)
-apply(simp)
-apply(drule_tac x="Right (injval r2a c v2)" in spec)
-apply(drule mp)
-apply(rule Prfs.intros)
-defer
-apply(erule ValOrd2.cases)
-apply(simp_all)[8] 
-apply(clarify)
-apply(subst (asm) v4)
-defer
-apply(simp)
-apply(rule ValOrd2.intros)
-apply (metis POSIXs_ALT1a POSIXs_def Prfs.intros(3))
-apply(case_tac "nullable r1")
-apply(simp (no_asm) add: POSIXs_def)
-apply(auto)[1]
-apply(subst (asm) (6) POSIXs_def)
-apply(auto)[1]
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-defer
-apply (metis Prfs.intros(3) der.simps(5) injval.simps(6) v3s)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(subst (asm) (6) POSIXs_def)
-apply(auto)[1]
-apply(rotate_tac 7)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-apply(rotate_tac 8)
-apply(erule Prfs.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd2.intros(2))
-apply(drule_tac x="v1b" in meta_spec)
-apply(drule_tac x="s1a" in meta_spec)
-apply(drule meta_mp)
-defer
-apply(subst (asm) Cons_eq_append_conv)
-apply(auto)
-defer
-defer
-
-
-thm v4
+oops
 
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
@@ -1763,6 +1757,139 @@
 oops
 
 lemma Prf_inj_test:
+  assumes "v1 2\<succ> v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" 
+  "length (flat v1) = length (flat v2)"
+  shows "(injval r c v1) 2\<succ>  (injval r c v2)"
+using assms
+apply(induct c r arbitrary: v1 v2 rule: der.induct)
+(* NULL case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* EMPTY case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* 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(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+(* ALT case *)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(auto)[1]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(subst v4)
+apply metis
+apply(subst v4)
+apply (metis)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+(* 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 ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd2.intros)
+apply(simp)
+apply(rule ValOrd2.intros)
+apply(auto)[1]
+
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply (metis ValOrd2.intros(1))
+apply(rule ValOrd2.intros)
+apply metis
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+apply(clarify)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd2.intros)
+apply(rule Ord1)
+apply(rule h)
+apply(simp)
+apply(simp)
+apply (metis list.distinct(1) mkeps_flat v4)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 7)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+defer
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply (metis ValOrd2.intros(1))
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply (rule_tac ValOrd2.intros(2))
+prefer 2
+apply (metis list.distinct(1) mkeps_flat v4)
+
+
+lemma Prf_inj_test:
   assumes "v1 2\<succ> v2" "\<Turnstile>s1 v1 : der c r" "\<Turnstile>s2 v2 : der c r"  
   shows "(injval r c v1) 2\<succ>  (injval r c v2)"
 using assms