--- a/thys/Re1.thy	Fri Apr 10 22:38:36 2015 +0100
+++ b/thys/Re1.thy	Sat Apr 25 10:58:48 2015 +0100
@@ -140,6 +140,18 @@
 
 value "flats(Seq(Char c)(Char b))"
 
+inductive StrOrd :: "string list \<Rightarrow> string list \<Rightarrow> bool" ("_ \<sqsupset> _" [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)"
+
+lemma StrOrd_append: 
+  "xs \<sqsupset> ys \<Longrightarrow> (zs @ xs) \<sqsupset> (zs @ ys)"
+apply(induct zs)
+apply(auto intro: StrOrd.intros) 
+done
+
 section {* Relation between values and regular expressions *}
 
 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
@@ -233,35 +245,35 @@
 | "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)
+inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [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)"
+  "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" 
+| "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)"
+| "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')"
+| "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')"
+| "Void 2\<succ> Void"
+| "(Char c) 2\<succ> (Char c)"
 
-lemma 
-  assumes "v1 \<sqsupset>r,n v2"
-  shows "length(flat v1) = n"
-using assms
-apply(induct)
-apply(auto)
+lemma Ord1:
+  "v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2"
+apply(induct rule: ValOrd.induct)
+apply(auto intro: ValOrd2.intros)
 done
 
-lemma 
-  assumes "v1 \<sqsupset>r,n v2"
-  shows "length(flat v2) <= n"
-using assms
-apply(induct)
-apply(auto)
-oops
+lemma Ord2:
+  "v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2"
+apply(induct v1 v2 rule: ValOrd2.induct)
+apply(auto intro: ValOrd.intros)
+done
 
+lemma Ord3:
+  "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2"
+apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct)
+apply(auto intro: ValOrd.intros elim: Prf.cases)
+done
 
-section {* The ordering is reflexive *}
 
 lemma ValOrd_refl:
   assumes "\<turnstile> v : r"
@@ -277,6 +289,19 @@
 where
   "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))"
 
+definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" 
+where
+  "POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))"
+
+lemma "POSIX v r = POSIX2 v r"
+unfolding POSIX_def POSIX2_def
+apply(auto)
+apply(rule Ord1)
+apply(auto)
+apply(rule Ord3)
+apply(auto)
+done
+
 (*
 an alternative definition: might cause problems
 with theorem mkeps_POSIX
@@ -885,6 +910,37 @@
 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"
+using assms
+unfolding POSIX2_def
+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
+apply(subst v4_proj)
+apply(simp)
+apply(rule_tac x="flat v" in exI)
+apply(simp)
+apply(simp)
+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"