diff -r 5b01f7c233f8 -r a33d3040bf7e thys/ReStar.thy
--- a/thys/ReStar.thy	Tue Feb 02 02:27:16 2016 +0000
+++ b/thys/ReStar.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -540,8 +540,8 @@
   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
-  "Values (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> 
-                                                               Star vs \<in> Values (STAR r) (rest v s)}"
+  "Values (STAR r) s = 
+      {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> Star vs \<in> Values (STAR r) (rest v s)}"
 unfolding Values_def
 apply(auto)
 (*NULL*)
@@ -589,8 +589,8 @@
   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
-  "NValues (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and> 
-                                                               Star vs \<in> NValues (STAR r) (rest v s)}"
+  "NValues (STAR r) s = 
+  {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Star vs \<in> NValues (STAR r) (rest v s)}"
 unfolding NValues_def
 apply(auto)
 (*NULL*)
@@ -1217,6 +1217,15 @@
 
 lemma lex_correct4:
   assumes "s \<in> L r"
+  shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
+using lex_correct3[OF assms]
+apply(auto)
+apply (metis PMatch1N)
+by (metis PMatch1(2))
+
+
+lemma lex_correct5:
+  assumes "s \<in> L r"
   shows "s \<in> r \<rightarrow> (lex2 r s)"
 using assms
 apply(induct s arbitrary: r)
@@ -1243,6 +1252,7 @@
 
 thm PMatch.intros
 
+(*
 inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 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')" 
@@ -1253,7 +1263,7 @@
 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "s \<turnstile> Void \<succ>EMPTY Void"
 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
-
+*)
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
@@ -1265,6 +1275,13 @@
 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
+| "flat (Star (v # vs)) = [] \<Longrightarrow> (Star []) \<succ>(STAR r) (Star (v # vs))"
+| "flat (Star (v # vs)) \<noteq> [] \<Longrightarrow> (Star (v # vs)) \<succ>(STAR r) (Star [])"
+| "v1 \<succ>r v2 \<Longrightarrow> (Star (v1 # vs1)) \<succ>(STAR r) (Star (v2 # vs2))"
+| "(Star vs1) \<succ>(STAR r) (Star vs2) \<Longrightarrow> (Star (v # vs1)) \<succ>(STAR r) (Star (v # vs2))"
+| "(Star []) \<succ>(STAR r) (Star [])"
+
+(*
 
 lemma ValOrd_PMatch:
   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
@@ -1272,30 +1289,55 @@
 using assms
 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(7))
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(8))
 defer
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(6))
 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 apply(clarify)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 apply(clarify)
 apply (metis ValOrd.intros(5))
+(* Star case *)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
+apply (metis ValOrd.intros(13))
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)
+prefer 2
+apply(rule ValOrd.intros)
+apply(simp add: prefix_def)
+apply(rule ValOrd.intros)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="va" in meta_spec)
+apply(drule_tac x="v" in meta_spec)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp add: prefix_def)
+apply(auto)[1]
+prefer 3
 (* Seq case *)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -2870,4 +2912,7 @@
 apply(auto simp add: POSIX_def)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
-oops
\ No newline at end of file
+oops
+*)
+
+end
\ No newline at end of file