# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1450569091 0
# Node ID 56dd3d1d479b70de6f15820f71a0cd322c66b5e3
# Parent  53d5f9a5bbd389ba60cf89968a31b6788df50567
added a proof about Values and PMatch

diff -r 53d5f9a5bbd3 -r 56dd3d1d479b thys/Re.thy
--- a/thys/Re.thy	Fri Dec 18 14:25:22 2015 +0000
+++ b/thys/Re.thy	Sat Dec 19 23:51:31 2015 +0000
@@ -434,6 +434,12 @@
                     None \<Rightarrow> None
                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
+fun 
+  lex2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
+where
+  "lex2 r [] = mkeps r"
+| "lex2 r (c#s) = injval r c (lex2 (der c r) s)"
+
 
 section {* Projection function *}
 
@@ -614,6 +620,7 @@
     \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
 
+
 lemma PMatch_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
@@ -648,7 +655,14 @@
 apply (metis Prf.intros(1))
 done
 
-lemma PMAtch2:
+lemma PMatch_Values:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "v \<in> Values r s"
+using assms
+apply(simp add: Values_def PMatch1)
+by (metis append_Nil2 prefix_def)
+
+lemma PMatch2:
   assumes "s \<in> (der c r) \<rightarrow> v"
   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 using assms
@@ -749,21 +763,73 @@
 apply(simp)
 by (metis Cons_eq_append_conv)
 
-lemma lex_correct:
+lemma lex_correct1:
+  assumes "s \<notin> L r"
+  shows "lex r s = None"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply (metis nullable_correctness)
+apply(auto)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+apply(auto)
+apply(simp add: L_flat_Prf)
+by (metis v3 v4)
+
+
+lemma lex_correct2:
   assumes "s \<in> L r"
-  shows "\<exists>v. lex r s = Some(v) \<and> flat v = s"
+  shows "\<exists>v. lex r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
-apply (metis mkeps_flat nullable_correctness)
+apply (metis mkeps_flat mkeps_nullable nullable_correctness)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+apply(simp add: L_flat_Prf)
+apply(auto)
+apply (metis v3_proj v4_proj2)
+apply (metis v3)
+apply(rule v4)
+by metis
+
+lemma lex_correct3:
+  assumes "s \<in> L r"
+  shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply (metis PMatch_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-defer
-apply(auto)[1]
-oops
+apply(simp add: L_flat_Prf)
+apply(auto)
+apply (metis v3_proj v4_proj2)
+apply(rule PMatch2)
+apply(simp)
+done
+
+lemma lex_correct4:
+  assumes "s \<in> L r"
+  shows "s \<in> r \<rightarrow> (lex2 r s)"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply (metis PMatch_mkeps nullable_correctness)
+apply(simp)
+apply(rule PMatch2)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+apply(simp add: L_flat_Prf)
+apply(auto)
+apply (metis v3_proj v4_proj2)
+done
 
 section {* Sulzmann's Ordering of values *}
 
+thm PMatch.intros
+
 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')"