# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1450448722 0
# Node ID 53d5f9a5bbd389ba60cf89968a31b6788df50567
# Parent  f89372781a4c6a2d46fb4497abb6a120735eb27b
updated

diff -r f89372781a4c -r 53d5f9a5bbd3 thys/Re.thy
--- a/thys/Re.thy	Fri Dec 18 10:11:01 2015 +0000
+++ b/thys/Re.thy	Fri Dec 18 14:25:22 2015 +0000
@@ -426,6 +426,14 @@
 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
+fun 
+  lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+  "lex r [] = (if nullable r then Some(mkeps r) else None)"
+| "lex r (c#s) = (case (lex (der c r) s) of  
+                    None \<Rightarrow> None
+                  | Some(v) \<Rightarrow> Some(injval r c v))"
+
 
 section {* Projection function *}
 
@@ -608,7 +616,7 @@
 
 lemma PMatch_mkeps:
   assumes "nullable r"
-  shows " [] \<in> r \<rightarrow> mkeps r"
+  shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(induct r)
 apply(auto)
@@ -741,7 +749,18 @@
 apply(simp)
 by (metis Cons_eq_append_conv)
 
-
+lemma lex_correct:
+  assumes "s \<in> L r"
+  shows "\<exists>v. lex r s = Some(v) \<and> flat v = s"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply (metis mkeps_flat nullable_correctness)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+defer
+apply(auto)[1]
+oops
 
 section {* Sulzmann's Ordering of values *}
 
@@ -890,6 +909,51 @@
 apply(simp_all)[8]
 done
 
+
+lemma ValOrd_PMatch:
+  assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s"
+  shows "v1 \<succ>r v2"
+using assms
+apply(induct arbitrary: v2 rule: PMatch.induct)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(7))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply (metis ValOrd.intros(8))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis ValOrd.intros(6))
+apply(clarify)
+apply (metis PMatch1(2) ValOrd.intros(3) order_refl)
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(clarify)
+apply (metis Prf_flat_L)
+apply (metis ValOrd.intros(5))
+apply(erule Prf.cases)
+apply(simp_all)[5]
+apply(auto)
+apply(case_tac "v1 = v1a")
+apply(auto)
+apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq)
+apply(rule ValOrd.intros(2))
+apply(auto)
+thm L_flat_Prf
+apply(simp add: L_flat_Prf)
+thm append_eq_append_conv2
+apply(simp add: append_eq_append_conv2)
+apply(auto)
+apply(drule_tac x="us" in spec)
+apply(drule mp)
+apply metis
+apply (metis append_Nil2)
+apply(case_tac "us = []")
+apply(auto)
+apply(drule_tac x="v1a" in meta_spec)
+apply(simp)
+
 lemma refl_on_ValOrd:
   "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}"
 unfolding refl_on_def