# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1432566563 -3600
# Node ID 4b4c677501e78fba389b19c95e0441f1163eb030
# Parent  39cef7b9212affb410bbba43ccb767d748892167
proved some basic properties (totality and trichonomity) for the orderings

diff -r 39cef7b9212a -r 4b4c677501e7 Literature/pattern-match.pdf
Binary file Literature/pattern-match.pdf has changed
diff -r 39cef7b9212a -r 4b4c677501e7 progs/scala/re.scala
--- a/progs/scala/re.scala	Sat Apr 25 10:58:48 2015 +0100
+++ b/progs/scala/re.scala	Mon May 25 16:09:23 2015 +0100
@@ -130,6 +130,17 @@
   case Rec(_, v) => flatten(v)
 }
 
+def flattens(v: Val) : List[String] = v match {
+  case Void => List("")
+  case Chr(c) => List(c.toString)
+  case Left(v) => flattens(v)
+  case Right(v) => flattens(v)
+  case Sequ(v1, v2) => flattens(v1) ::: flattens(v2)
+  case Stars(vs) => vs.flatMap(flattens)
+  case Rec(_, v) => flattens(v)
+}
+
+
 // extracts an environment from a value
 def env(v: Val) : List[(String, String)] = v match {
   case Void => Nil
@@ -257,26 +268,37 @@
   case _ => false
 }     
 
-def tst(r: Rexp, c: Char) : Set[(Rexp, Val, Val, Val, Val)] = {
+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)))  
+}
+
+def tst2(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)))) 
-  yield (r, v1, v2, inj(r, c, v1), inj(r, c, v2))  
+       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)))  
 }
 
-def comp(r1: (Rexp, Val, Val, Val, Val), r2: (Rexp, Val, Val, Val, Val)) = size(r1._1) < size(r2._1)
+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)
 
 
-val smallest = enum(3, "a").flatMap(tst(_, 'a')).toList.sortWith { comp }.head
+val smallest = enum(3, "a").flatMap(tst(_, 'a')).toList.sortWith { comp }
 
 smallest match {
-  case (r, v1, v2, v3, v4) => List(pretty(r),
+  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)).mkString("\n") }
+                                   vpretty(v4), s1, s2).mkString("\n") }
 
 // Lexing Rules for a Small While Language
 
diff -r 39cef7b9212a -r 4b4c677501e7 thys/Re1.thy
--- a/thys/Re1.thy	Sat Apr 25 10:58:48 2015 +0100
+++ b/thys/Re1.thy	Mon May 25 16:09:23 2015 +0100
@@ -140,19 +140,36 @@
 
 value "flats(Seq(Char c)(Char b))"
 
-inductive StrOrd :: "string list \<Rightarrow> string list \<Rightarrow> bool" ("_ \<sqsupset> _" [100, 100] 100)
+section {* Relation between values and regular expressions *}
+
+inductive Prfs :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile>_ _ : _" [100, 100, 100] 100)
 where
-   "[] \<sqsupset> []"
-|  "xs \<sqsupset> ys \<Longrightarrow> (x#xs) \<sqsupset> (x#ys)"
-|  "length x \<ge> length y \<Longrightarrow> (x#xs) \<sqsupset> (y#xs)"
+ "\<lbrakk>\<Turnstile>s1 v1 : r1; \<Turnstile>s2 v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>(s1 @ s2) (Seq v1 v2) : SEQ r1 r2"
+| "\<Turnstile>s v1 : r1 \<Longrightarrow> \<Turnstile>s (Left v1) : ALT r1 r2"
+| "\<Turnstile>s v2 : r2 \<Longrightarrow> \<Turnstile>s (Right v2) : ALT r1 r2"
+| "\<Turnstile>[] Void : EMPTY"
+| "\<Turnstile>[c] (Char c) : CHAR c"
 
-lemma StrOrd_append: 
-  "xs \<sqsupset> ys \<Longrightarrow> (zs @ xs) \<sqsupset> (zs @ ys)"
-apply(induct zs)
-apply(auto intro: StrOrd.intros) 
+lemma Prfs_flat:
+  "\<Turnstile>s v : r \<Longrightarrow> flat v = s"
+apply(induct s v r rule: Prfs.induct)
+apply(auto)
 done
 
-section {* Relation between values and regular expressions *}
+
+inductive Prfn :: "nat \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> bool" ("\<TTurnstile>_ _ : _" [100, 100, 100] 100)
+where
+ "\<lbrakk>\<TTurnstile>n1 v1 : r1; \<TTurnstile>n2 v2 : r2\<rbrakk> \<Longrightarrow> \<TTurnstile>(n1 + n2) (Seq v1 v2) : SEQ r1 r2"
+| "\<TTurnstile>n v1 : r1 \<Longrightarrow> \<TTurnstile>n (Left v1) : ALT r1 r2"
+| "\<TTurnstile>n v2 : r2 \<Longrightarrow> \<TTurnstile>n (Right v2) : ALT r1 r2"
+| "\<TTurnstile>0 Void : EMPTY"
+| "\<TTurnstile>1 (Char c) : CHAR c"
+
+lemma Prfn_flat:
+  "\<TTurnstile>n v : r \<Longrightarrow> length(flat v) = n"
+apply(induct rule: Prfn.induct)
+apply(auto)
+done
 
 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
@@ -162,10 +179,29 @@
 | "\<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)"
+lemma Prf_Prfn:
+  shows "\<turnstile> v : r \<Longrightarrow> \<TTurnstile>(length (flat v)) v : r"
+apply(induct v r rule: Prf.induct)
+apply(auto intro: Prfn.intros)
+by (metis One_nat_def Prfn.intros(5))
+
+lemma Prfn_Prf:
+  shows "\<TTurnstile>n v : r \<Longrightarrow> \<turnstile> v : r"
+apply(induct n v r rule: Prfn.induct)
+apply(auto intro: Prf.intros)
+done
+
+lemma Prf_Prfs:
+  shows "\<turnstile> v : r \<Longrightarrow> \<Turnstile>(flat v) v : r"
+apply(induct v r rule: Prf.induct)
+apply(auto intro: Prfs.intros)
+done
+
+lemma Prfs_Prf:
+  shows "\<Turnstile>s v : r \<Longrightarrow> \<turnstile> v : r"
+apply(induct s v r rule: Prfs.induct)
+apply(auto intro: Prf.intros)
+done
 
 fun mkeps :: "rexp \<Rightarrow> val"
 where
@@ -180,8 +216,25 @@
 apply(auto intro: Prf.intros)
 done
 
-value "flat(Seq(Char c)(Char b))"
-value "flat(Right(Void))"
+lemma mkeps_nullable_n:
+  assumes "nullable(r)" shows "\<TTurnstile>0 (mkeps r) : r"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto intro: Prfn.intros)
+apply(drule Prfn.intros(1))
+apply(assumption)
+apply(simp)
+done
+
+lemma mkeps_nullable_s:
+  assumes "nullable(r)" shows "\<Turnstile>[] (mkeps r) : r"
+using assms
+apply(induct rule: nullable.induct)
+apply(auto intro: Prfs.intros)
+apply(drule Prfs.intros(1))
+apply(assumption)
+apply(simp)
+done
 
 lemma mkeps_flat:
   assumes "nullable(r)" shows "flat (mkeps r) = []"
@@ -197,17 +250,11 @@
 apply(auto)
 done
 
-
-
 text {*
   The value mkeps returns is always the correct POSIX
   value.
 *}
 
-
-
-
-
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
@@ -283,6 +330,255 @@
 apply(auto intro: ValOrd.intros)
 done
 
+lemma 
+  "flat Void = []"
+  "flat (Seq Void Void) = []"
+apply(simp_all)
+done
+
+
+lemma ValOrd_total:
+  shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r\<rbrakk>  \<Longrightarrow> v1 \<succ>r v2 \<or> v2 \<succ>r v1"
+apply(induct r arbitrary: v1 v2)
+apply(auto)
+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 (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(case_tac "v1a = v1b")
+apply(simp)
+apply(rule ValOrd.intros(1))
+apply (metis ValOrd.intros(1))
+apply(rule ValOrd.intros(2))
+apply(auto)[2]
+apply(erule contrapos_np)
+apply(rule ValOrd.intros(2))
+apply(auto)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis Ord1 Ord3 Prf.intros(2) ValOrd2.intros(6))
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply (metis le_eq_less_or_eq neq_iff)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+apply (metis le_eq_less_or_eq neq_iff)
+apply(rule ValOrd.intros)
+apply(erule contrapos_np)
+apply(rule ValOrd.intros)
+by metis
+
+lemma ValOrd_anti:
+  shows "\<lbrakk>\<turnstile> v1 : r; \<turnstile> v2 : r; v1 \<succ>r v2; v2 \<succ>r v1\<rbrakk> \<Longrightarrow> v1 = v2"
+apply(induct r arbitrary: v1 v2)
+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 Prf.cases)
+apply(simp_all)[5]
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+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)
+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(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(rule conjI)
+apply(rule Prf.intros)
+apply(rule allI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(rule exI)
+apply(rule conjI)
+apply(rule Prf.intros)
+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(erule Prf.cases)
+apply(simp_all)[5]
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+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
+
+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 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"
+  shows "v1 \<succ>r v3"
+using assms
+apply(induct r arbitrary: v1 v2 v3)
+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 Prf.cases)
+apply(simp_all)[5]
+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 Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply (metis ValOrd.intros(1))
+apply(clarify)
+apply (metis ValOrd.intros(2))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis ValOrd.intros(2))
+apply(clarify)
+apply(case_tac "v1d = v1'a")
+apply(simp)
+apply (metis ValOrd_anti)
+apply (rule ValOrd.intros(2))
+prefer 2
+apply(auto)[1]
+prefer 2
+oops
+
+
+
 section {* Posix definition *}
 
 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
@@ -302,22 +598,71 @@
 apply(auto)
 done
 
-(*
-an alternative definition: might cause problems
-with theorem mkeps_POSIX
-*)
+definition POSIXs :: "val \<Rightarrow> rexp \<Rightarrow> string \<Rightarrow> bool" 
+where
+  "POSIXs v r s \<equiv> (\<Turnstile>s v : r \<and> (\<forall>v'. (\<Turnstile>s v' : r \<longrightarrow> v 2\<succ> v')))"
 
-(*
-definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+definition POSIXn :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> bool" 
 where
-  "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')"
-*)
+  "POSIXn v r n \<equiv> (\<TTurnstile>n v : r \<and> (\<forall>v'. (\<TTurnstile>n v' : r \<longrightarrow> v 2\<succ> v')))"
+
+lemma "POSIXn v r (length (flat v)) \<Longrightarrow> POSIX2 v r"
+unfolding POSIXn_def POSIX2_def
+apply(auto)
+apply (metis Prfn_Prf)
+by (metis Prf_Prfn)
+
+lemma Prfs_POSIX:
+  "POSIXs v r s \<Longrightarrow> \<Turnstile>s v: r \<and> flat v = s"
+apply(simp add: POSIXs_def)
+by (metis Prfs_flat)
+
+
+lemma "POSIXs v r (flat v) =  POSIX2 v r"
+unfolding POSIXs_def POSIX2_def
+apply(auto)
+apply (metis Prfs_Prf)
+apply (metis Prf_Prfs)
+apply (metis Prf_Prfs)
+by (metis Prfs_Prf Prfs_flat)
+
+lemma 
+  assumes "POSIX v1 r1" "\<turnstile> v1' : r1"
+  shows "Seq v1 v2 \<succ>(SEQ r1 r2) Seq v1' v2'"
+using assms
+apply(rule_tac ValOrd.intros)
+apply(simp add: POSIX_def)
+oops
 
-(*
-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
+"L r \<noteq> {} \<Longrightarrow> \<exists>v. POSIXs v r (flat v)"
+apply(induct r arbitrary: )
+apply(simp)
+apply(rule_tac x="Void" in exI)
+apply(simp add: POSIXs_def)
+apply(rule conjI)
+apply (metis Prfs.intros(4))
+apply(auto)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(7))
+apply(simp)
+apply(rule_tac x="Char char" in exI)
+apply(simp add: POSIXs_def)
+apply(rule conjI)
+apply (metis Prfs.intros(5))
+apply(auto)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros)
+apply(auto simp add: Sequ_def)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(drule meta_mp)
+apply (metis empty_iff)
+apply(auto)
+
+section {* POSIX for some constructors *}
 
 lemma POSIX_SEQ1:
   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2"
@@ -336,6 +681,38 @@
 apply(clarify)
 by (metis ValOrd_refl)
 
+lemma POSIXn_SEQ1:
+  assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2"
+  shows "POSIXn v1 r1 n1"
+using assms
+unfolding POSIXn_def
+apply(auto)
+apply(drule_tac x="Seq v' v2" in spec)
+apply(erule impE)
+apply(rule Prfn.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+apply(clarify)
+by (metis Ord1 Prfn_Prf ValOrd_refl)
+
+lemma POSIXs_SEQ1:
+  assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2"
+  shows "POSIXs v1 r1 s1"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply(drule_tac x="Seq v' v2" in spec)
+apply(erule impE)
+apply(rule Prfs.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+apply(clarify)
+by (metis Ord1 Prfs_Prf ValOrd_refl)
+
 lemma POSIX_SEQ2:
   assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" 
   shows "POSIX v2 r2"
@@ -352,6 +729,36 @@
 apply(simp_all)
 done
 
+lemma POSIXn_SEQ2:
+  assumes "POSIXn (Seq v1 v2) (SEQ r1 r2) (n1 + n2)" "\<TTurnstile>n1 v1 : r1" "\<TTurnstile>n2 v2 : r2" 
+  shows "POSIXn v2 r2 n2"
+using assms
+unfolding POSIXn_def
+apply(auto)
+apply(drule_tac x="Seq v1 v'" in spec)
+apply(erule impE)
+apply(rule Prfn.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+done
+
+lemma POSIXs_SEQ2:
+  assumes "POSIXs (Seq v1 v2) (SEQ r1 r2) (s1 @ s2)" "\<Turnstile>s1 v1 : r1" "\<Turnstile>s2 v2 : r2" 
+  shows "POSIXs v2 r2 s2"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply(drule_tac x="Seq v1 v'" in spec)
+apply(erule impE)
+apply(rule Prfs.intros)
+apply(simp)
+apply(simp)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+done
+
 lemma POSIX_ALT2:
   assumes "POSIX (Left v1) (ALT r1 r2)"
   shows "POSIX v1 r1"
@@ -369,6 +776,38 @@
 apply(simp_all)
 done
 
+lemma POSIXn_ALT2:
+  assumes "POSIXn (Left v1) (ALT r1 r2) n"
+  shows "POSIXn v1 r1 n"
+using assms
+unfolding POSIXn_def
+apply(auto)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Left v'" in spec)
+apply(drule mp)
+apply(rule Prfn.intros)
+apply(auto)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+done
+
+lemma POSIXs_ALT2:
+  assumes "POSIXs (Left v1) (ALT r1 r2) s"
+  shows "POSIXs v1 r1 s"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Left v'" in spec)
+apply(drule mp)
+apply(rule Prfs.intros)
+apply(auto)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+done
+
 lemma POSIX_ALT1a:
   assumes "POSIX (Right v2) (ALT r1 r2)"
   shows "POSIX v2 r2"
@@ -386,6 +825,38 @@
 apply(simp_all)
 done
 
+lemma POSIXn_ALT1a:
+  assumes "POSIXn (Right v2) (ALT r1 r2) n"
+  shows "POSIXn v2 r2 n"
+using assms
+unfolding POSIXn_def
+apply(auto)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Right v'" in spec)
+apply(drule mp)
+apply(rule Prfn.intros)
+apply(auto)
+apply(erule ValOrd2.cases)
+apply(simp_all)
+done
+
+lemma POSIXs_ALT1a:
+  assumes "POSIXs (Right v2) (ALT r1 r2) s"
+  shows "POSIXs v2 r2 s"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(drule_tac x="Right v'" in spec)
+apply(drule mp)
+apply(rule Prfs.intros)
+apply(auto)
+apply(erule ValOrd2.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')"
@@ -395,6 +866,24 @@
 apply(auto)
 done
 
+lemma POSIXn_ALT1b:
+  assumes "POSIXn (Right v2) (ALT r1 r2) n"
+  shows "(\<forall>v'. (\<TTurnstile>n v' : r2 \<longrightarrow> v2 2\<succ> v'))"
+using assms
+apply(drule_tac POSIXn_ALT1a)
+unfolding POSIXn_def
+apply(auto)
+done
+
+lemma POSIXs_ALT1b:
+  assumes "POSIXs (Right v2) (ALT r1 r2) s"
+  shows "(\<forall>v'. (\<Turnstile>s v' : r2 \<longrightarrow> v2 2\<succ> v'))"
+using assms
+apply(drule_tac POSIXs_ALT1a)
+unfolding POSIXs_def
+apply(auto)
+done
+
 lemma POSIX_ALT_I1:
   assumes "POSIX v1 r1" 
   shows "POSIX (Left v1) (ALT r1 r2)"
@@ -411,6 +900,37 @@
 apply(rule ValOrd.intros)
 by simp
 
+lemma POSIXn_ALT_I1:
+  assumes "POSIXn v1 r1 n" 
+  shows "POSIXn (Left v1) (ALT r1 r2) n"
+using assms
+unfolding POSIXn_def
+apply(auto)
+apply (metis Prfn.intros(2))
+apply(rotate_tac 2)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd2.intros)
+apply(auto)
+apply(rule ValOrd2.intros)
+by (metis Prfn_flat order_refl)
+
+lemma POSIXs_ALT_I1:
+  assumes "POSIXs v1 r1 s" 
+  shows "POSIXs (Left v1) (ALT r1 r2) s"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply (metis Prfs.intros(2))
+apply(rotate_tac 2)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd2.intros)
+apply(auto)
+apply(rule ValOrd2.intros)
+by (metis Prfs_flat order_refl)
 
 lemma POSIX_ALT_I2:
   assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')"
@@ -427,10 +947,25 @@
 apply metis
 done
 
+lemma POSIXs_ALT_I2:
+  assumes "POSIXs v2 r2 s" "\<forall>s' v'. \<Turnstile>s' v' : r1 \<longrightarrow> length s > length s'"
+  shows "POSIXs (Right v2) (ALT r1 r2) s"
+using assms
+unfolding POSIXs_def
+apply(auto)
+apply (metis Prfs.intros)
+apply(rotate_tac 3)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(rule ValOrd2.intros)
+apply metis
+done
+
 
 lemma 
   "\<lbrakk>POSIX (mkeps r2) r2; nullable r2; \<not> nullable r1\<rbrakk>
-   \<Longrightarrow> POSIX (val.Right (mkeps r2)) (ALT r1 r2)" 
+   \<Longrightarrow> POSIX (Right (mkeps r2)) (ALT r1 r2)" 
 apply(auto simp add: POSIX_def)
 apply(rule Prf.intros(3))
 apply(auto)
@@ -591,6 +1126,88 @@
 apply(auto)[2]
 done
 
+lemma v3s:
+  assumes "\<Turnstile>s v : der c r" shows "\<Turnstile>(c#s) (injval r c v) : r"
+using assms
+apply(induct arbitrary: s v rule: der.induct)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis Prfs.intros(5))
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis Prfs.intros(2))
+apply (metis Prfs.intros(3))
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis Prfs.intros(1) append_Cons)
+apply(auto)[1]
+apply (metis Prfs.intros(1) append_Nil mkeps_nullable_s)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+by (metis Prfs.intros(1) append_Cons)
+
+lemma v3n:
+  assumes "\<TTurnstile>n v : der c r" shows "\<TTurnstile>(Suc n) (injval r c v) : r"
+using assms
+apply(induct arbitrary: n v rule: der.induct)
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply (metis One_nat_def Prfn.intros(5))
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply (metis Prfn.intros(2))
+apply (metis Prfn.intros(3))
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+apply (metis Prfn.intros(1) add.commute add_Suc_right)
+apply(auto)[1]
+apply (metis Prfn.intros(1) mkeps_nullable_n plus_nat.add_0)
+apply(simp)
+apply(erule Prfn.cases)
+apply(simp_all)[5]
+apply(auto)[1]
+by (metis Prfn.intros(1) add_Suc)
+
 lemma v3_proj:
   assumes "\<turnstile> v : r" and "\<exists>s. (flat v) = c # s"
   shows "\<turnstile> (projval r c v) : der c r"
@@ -620,10 +1237,83 @@
 apply(simp)
 done
 
+lemma v3s_proj:
+  assumes "\<Turnstile>(c#s) v : r"
+  shows "\<Turnstile>s (projval r c v) : der c r"
+using assms
+apply(induct s\<equiv>"c#s" v r arbitrary: s rule: Prfs.induct)
+prefer 4
+apply(simp)
+apply (metis Prfs.intros(4))
+prefer 2
+apply(simp)
+apply (metis Prfs.intros(2))
+prefer 2
+apply(simp)
+apply (metis Prfs.intros(3))
+apply(auto)
+apply(rule Prfs.intros)
+apply (metis Prfs_flat append_Nil)
+prefer 2
+apply(rule Prfs.intros)
+apply(subst (asm) append_eq_Cons_conv)
+apply(auto)[1]
+apply (metis Prfs_flat)
+apply(rule Prfs.intros)
+apply metis
+apply(simp)
+apply(subst (asm) append_eq_Cons_conv)
+apply(auto)[1]
+apply (metis Prf_flat_L Prfs_Prf nullable_correctness)
+apply (metis Prfs_flat list.distinct(1))
+apply(subst (asm) append_eq_Cons_conv)
+apply(auto)[1]
+apply (metis Prfs_flat)
+by (metis Prfs.intros(1))
+
 text {*
   The string behind the injection value is an added c
 *}
 
+lemma v4s:
+  assumes "\<Turnstile>s v : der c r" shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct arbitrary: s v rule: der.induct)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "c = c'")
+apply(simp)
+apply(auto)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all (no_asm_use))[5]
+apply(auto)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(simp only: injval.simps flat.simps)
+apply(auto)[1]
+apply (metis mkeps_flat)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+done
+
 lemma v4:
   assumes "\<turnstile> v : der c r" shows "flat (injval r c v) = c # (flat v)"
 using assms
@@ -663,6 +1353,36 @@
 apply(simp_all)[5]
 done
 
+lemma v4_flats:
+  assumes "\<turnstile> v : der c r" "\<not>nullable r" shows "hd (flats (injval r c v)) \<noteq> []"
+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(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(clarify)
+oops
+
 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
@@ -771,6 +1491,145 @@
 apply(simp_all)[5]
 done
 
+lemma 
+  assumes "POSIXs v (der c r) s" 
+  shows "POSIXs (injval r c v) r (c # s)"
+using assms
+apply(induct c r arbitrary: v s rule: der.induct)
+apply(auto simp add: POSIXs_def)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto simp add: POSIXs_def)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(case_tac "c = c'")
+apply(auto simp add: POSIXs_def)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis Prfs.intros(5))
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply (metis ValOrd2.intros(8))
+apply(auto simp add: POSIXs_def)[1]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(frule Prfs_POSIX)
+apply(drule conjunct1)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(rule POSIXs_ALT_I1)
+apply (metis POSIXs_ALT2)
+apply(rule POSIXs_ALT_I2)
+apply (metis POSIXs_ALT1a)
+apply(frule POSIXs_ALT1b)
+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
+
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
 
@@ -787,46 +1646,6 @@
 lemma "\<not>(nullable r) \<Longrightarrow> \<not>(\<exists>v. \<turnstile> v : r \<and> flat v = [])"
 by (metis Prf_flat_L nullable_correctness)
 
-lemma proj_inj_id:
-  assumes "\<turnstile> v : der c r" 
-  shows "projval r c (injval r c v) = v"
-using assms
-apply(induct c r 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(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 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 LeftRight:
   assumes "(Left v1) \<succ>(der c (ALT r1 r2)) (Right v2)"
@@ -910,52 +1729,247 @@
 apply (metis list.distinct(1) mkeps_flat v4)
 by (metis h)
 
-lemma POSIX_der:
-  assumes "POSIX2 v (der c r)" "\<turnstile> v : der c r"
-  shows "POSIX2 (injval r c v) r"
+lemma rr1: 
+  assumes "\<turnstile> v : r" "\<not>nullable r" 
+  shows "flat v \<noteq> []"
 using assms
-unfolding POSIX2_def
+by (metis Prf_flat_L nullable_correctness)
+
+lemma rr2: "hd (flats v) \<noteq> [] \<Longrightarrow> flats v \<noteq> []"
+apply(induct v)
 apply(auto)
-thm v3
-apply (erule v3)
-thm v4
-apply(subst (asm) v4)
-apply(assumption)
+done
+
+lemma rr3: "flats v = [] \<Longrightarrow> flat v = []"
+apply(induct v)
+apply(auto)
+done
+
+lemma POSIXs_der:
+  assumes "POSIXs v (der c r) s" "\<Turnstile>s v : der c r"
+  shows "POSIXs (injval r c v) r (c#s)"
+using assms
+unfolding POSIXs_def
+apply(auto)
+thm v3s 
+apply (erule v3s)
 apply(drule_tac x="projval r c v'" in spec)
 apply(drule mp)
-apply(rule conjI)
-thm v3_proj
-apply(rule v3_proj)
+thm v3s_proj
+apply(rule v3s_proj)
+apply(simp)
+thm v3s_proj
+apply(drule v3s_proj)
+oops
+
+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
+apply(induct c r arbitrary: s1 s2 v1 v2 rule: der.induct)
+(* NULL case *)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+(* EMPTY case *)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+(* CHAR case *)
+apply(case_tac "c = c'")
 apply(simp)
-apply(rule_tac x="flat v" in exI)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+(* ALT case *)
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule Prfs.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 Prfs_Prf)
+apply(subst v4)
+apply (metis Prfs_Prf)
 apply(simp)
-thm t
-apply(rule_tac c="c" in  t)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(auto)[2]
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply(subst v4)
+apply (metis Prfs_Prf)
+apply(subst v4)
+apply (metis Prfs_Prf)
+apply(simp)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(rule ValOrd2.intros)
+apply metis
+(* SEQ case*)
+apply(simp)
+apply(case_tac "nullable r1")
+apply(simp)
+defer
+apply(simp)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd2.intros)
 apply(simp)
-thm v4_proj
-apply(subst v4_proj)
+apply(rule ValOrd2.intros)
+apply(auto)[1]
+defer
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(erule Prfs.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
+defer
+apply(clarify)
 apply(simp)
-apply(rule_tac x="flat v" in exI)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rule ValOrd2.intros)
+apply(rule Ord1)
+apply(rule h)
 apply(simp)
 apply(simp)
+apply (metis Prfs_Prf)
+defer
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 6)
+apply(erule Prfs.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+
+apply(erule ValOrd2.cases)
+apply(simp_all)[8]
+apply(simp)
+apply metis
+using injval_inj
+apply(simp add: inj_on_def)
+apply metis
+(* SEQ nullable case *)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(simp)
+apply(rule ValOrd.intros(2))
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply(rule ValOrd.intros(2))
+apply (metis h)
+apply (metis list.distinct(1) mkeps_flat v4)
+(* last case *)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 6)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+prefer 2
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(metis)
+apply(rule ValOrd.intros(2))
+prefer 2
+thm mkeps_flat v4
+apply (metis list.distinct(1) mkeps_flat v4)
 oops
 
 
 lemma Prf_inj_test:
-  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"
+  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 vs rs rule: der.induct)
+apply(induct v1 arbitrary: r v2 taking: "length o flat" rule: measure_induct_rule)
+apply(case_tac r)
 (* NULL case *)
 apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
+apply(erule Prf.cases)
+apply(simp_all)[5]
 (* EMPTY case *)
 apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
+apply(erule Prf.cases)
+apply(simp_all)[5]
 (* CHAR case *)
-apply(case_tac "c = c'")
+apply(case_tac "c = char")
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -966,24 +1980,40 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 (* ALT case *)
+prefer 2
 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(clarify)
 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(clarify)
+apply (rule ValOrd.intros(6))
+apply(drule_tac x="v1b" in meta_spec)
+apply(drule_tac x="rexp1" in meta_spec)
+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(clarify)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
-apply (metis RightLeft ValOrd.intros(4) der.simps(4) injval.simps(2) injval.simps(3))
+apply(clarify)
+apply (metis ValOrd.intros(3) monoid_add_class.add.right_neutral order_refl v4)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis RightLeft der.simps(4) injval.simps(2) injval.simps(3))
+apply(clarify)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+apply(clarify)
 apply (metis ValOrd.intros(5))
 (* SEQ case *)
 apply(simp)
@@ -1005,7 +2035,7 @@
 apply(rule ValOrd.intros(2))
 apply(rotate_tac 2)
 apply(drule_tac x="v1c" in meta_spec)
-apply(rotate_tac 10)
+apply(rotate_tac 9)
 apply(drule_tac x="v1'" in meta_spec)
 apply(drule_tac meta_mp)
 apply(assumption)
@@ -1015,6 +2045,66 @@
 apply(assumption)
 apply(drule_tac meta_mp)
 apply(simp)
+apply (metis POSIX_SEQ1)
+apply(simp)
+apply (metis proj_inj_id)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply(rotate_tac 6)
+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(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(simp)
+apply(clarify)
+apply (metis POSIX_ALT2 POSIX_SEQ1 ValOrd.intros(2) proj_inj_id)
+apply(clarify)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis Prf.intros(1) Prf.intros(2) ValOrd.intros(2) der.simps(5) h injval.simps(5) mkeps_flat proj_inj_id projval.simps(4) val.distinct(19))
+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)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(simp)
+apply(drule POSIX_ALT1a)
+apply(rule ValOrd.intros(2))
+defer
+apply (metis list.distinct(1) mkeps_flat v4)
+apply(rule ValOrd.intros(1))
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply (metis POSIX_ALT1a)
+
+apply(clarify)
+apply(erule ValOrd.cases)
+apply(simp_all)[8]
+apply(clarify)
+apply(rule ValOrd.intros(1))
+apply(simp)
+
+apply(subgoal_tac "flats v1c \<noteq> []")
+
+apply(simp)
 apply(subst v4)
 apply(simp)
 apply(subst (asm) v4)
@@ -1420,8 +2510,6 @@
 apply(drule mp)
 defer
 apply (metis Prf.intros(1))
-
-
 oops
 
 lemma POSIX_ALT_cases: