--- a/thys/Re.thy	Wed Jan 06 12:24:29 2016 +0000
+++ b/thys/Re.thy	Thu Jan 14 17:19:40 2016 +0000
@@ -324,6 +324,14 @@
 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
   "rest v s \<equiv> drop (length (flat v)) s"
 
+lemma rest_flat:
+  assumes "flat v1 \<sqsubseteq> s"
+  shows "flat v1 @ rest v1 s = s"
+using assms
+apply(auto simp add: rest_def prefix_def)
+done
+
+
 lemma rest_Suffixes:
   "rest v s \<in> Suffixes s"
 unfolding rest_def
@@ -836,6 +844,51 @@
 
 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
   "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
@@ -1023,10 +1076,69 @@
 thm PMatch.intros[no_vars]
 
 lemma POSIX_PMatch:
-  assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r"
-  shows "length (flat v') \<le> length (flat v)" 
+  assumes "s \<in> r \<rightarrow> v" "v' \<in> Values r s"
+  shows "v \<succ>r v' \<or> length (flat v') < length (flat v)" 
 using assms
-apply(induct arbitrary: s v v' rule: rexp.induct)
+apply(induct r arbitrary: s v v' rule: rexp.induct)
+apply(simp_all add: Values_recs)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(simp add: prefix_def)
+apply (metis ValOrd.intros(8))
+apply(auto)[1]
+defer
+apply(auto)[1]
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(6))
+apply (metis (no_types, lifting) PMatch1(2) Prf_flat_L Values_def length_sprefix mem_Collect_eq sprefix_def)
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply (metis (no_types, lifting) PMatch1(2) ValOrd.intros(3) Values_def length_sprefix mem_Collect_eq order_refl sprefix_def)
+apply (metis ValOrd.intros(5))
+apply(erule PMatch.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(case_tac "v1a = v1")
+apply(simp)
+apply(rule ValOrd.intros(1))
+apply (metis PMatch1(2) append_Nil comm_monoid_diff_class.diff_cancel drop_0 drop_all drop_append order_refl rest_def)
+apply(rule ValOrd.intros(2))
+apply(auto)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="v1a" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(auto)
+apply(drule meta_mp)
+defer
+apply(auto)[1]
+apply(frule PMatch1)
+apply(drule PMatch1(2))
+apply(frule PMatch1)
+apply(drule PMatch1(2))
+apply(auto)[1]
+apply(simp add: Values_def)
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply(simp add: append_eq_append_conv2)
+apply(auto)[1]
+apply(rotate_tac 10)
+apply(drule sym)
+apply(simp)
+apply(simp add: rest_def)
+apply(case_tac "s3a = []")
+apply(auto)[1]
+
+
+apply (metis ValOrd.intros(6))
+apply (metis (no_types, lifting) PMatch1(2) ValOrd.intros(3) Values_def length_sprefix mem_Collect_eq order_refl sprefix_def)
+apply(auto)[1]
+apply (metis (no_types, lifting) PMatch1(2) Prf_flat_L Values_def length_sprefix mem_Collect_eq sprefix_def)
+apply (metis ValOrd.intros(5))
+apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(erule Prf.cases)