diff -r 80218dddbb15 -r 489dfa0d7ec9 thys/ReStar.thy
--- a/thys/ReStar.thy	Thu Feb 25 12:17:31 2016 +0000
+++ b/thys/ReStar.thy	Thu Feb 25 20:13:41 2016 +0000
@@ -4,17 +4,13 @@
 begin
 
 
-section {* Sequential Composition of Sets *}
+section {* Sequential Composition of Languages *}
 
 definition
   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
-fun spow where
-  "spow s 0 = []"
-| "spow s (Suc n) = s @ spow s n"
-
 text {* Two Simple Properties about Sequential Composition *}
 
 lemma seq_empty [simp]:
@@ -27,6 +23,9 @@
   and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
 
+
+section {* Semantic Derivatives of Languages *}
+
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 where
@@ -57,26 +56,13 @@
 unfolding Der_def
 by auto
 
-lemma Der_seq [simp]:
+lemma Der_Sequ [simp]:
   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
 unfolding Der_def Sequ_def
-apply (auto simp add: Cons_eq_append_conv)
-done
+by (auto simp add: Cons_eq_append_conv)
 
-lemma seq_image:
-  assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-  shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"
-apply(auto simp add: Sequ_def image_def)
-apply(rule_tac x="f s1" in exI)
-apply(rule_tac x="f s2" in exI)
-using assms
-apply(auto)
-apply(rule_tac x="xa @ xb" in exI)
-using assms
-apply(auto)
-done
 
-section {* Kleene Star for Sets *}
+section {* Kleene Star for Languages *}
 
 inductive_set
   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
@@ -90,66 +76,6 @@
 unfolding Sequ_def
 by (auto) (metis Star.simps)
 
-
-fun 
-  pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)
-where
-  "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) = A ;; (A \<up> n)"  
-
-lemma star1: 
-  shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"
-  apply(induct rule: Star.induct)
-  apply (metis pow.simps(1) insertI1)
-  apply(auto)
-  apply(rule_tac x="Suc n" in exI)
-  apply(auto simp add: Sequ_def)
-  done
-
-lemma star2:
-  shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"
-  apply(induct n arbitrary: s)
-  apply (metis pow.simps(1) Star.simps empty_iff insertE)
-  apply(auto simp add: Sequ_def)
-  done
-
-lemma star3:
-  shows "A\<star> = (\<Union>i. A \<up> i)"
-using star1 star2
-apply(auto)
-done
-
-lemma star4:
-  shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"
-  apply(induct n arbitrary: s)
-  apply(auto simp add: Sequ_def)
-  apply(rule_tac x="[]" in exI)
-  apply(auto)
-  apply(drule_tac x="s2" in meta_spec)
-  apply(auto)
-by (metis concat.simps(2) insertE set_simps(2))
-
-lemma star5:
-  assumes "f [] = []"
-  assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-  shows "(f ` A) \<up> n = f ` (A \<up> n)"
-apply(induct n)
-apply(simp add: assms)
-apply(simp)
-apply(subst seq_image[OF assms(2)])
-apply(simp)
-done
-
-lemma star6:
-  assumes "f [] = []"
-  assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-  shows "(f ` A)\<star> = f ` (A\<star>)"
-apply(simp add: star3)
-apply(simp add: image_UN)
-apply(subst star5[OF assms])
-apply(simp)
-done
-
 lemma star_decomp: 
   assumes a: "c # x \<in> A\<star>" 
   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
@@ -174,7 +100,6 @@
 qed
 
 
-
 section {* Regular Expressions *}
 
 datatype rexp =
@@ -209,10 +134,7 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-apply (induct r) 
-apply(auto simp add: Sequ_def) 
-done
-
+by (induct r) (auto simp add: Sequ_def) 
 
 
 section {* Values *}
@@ -238,28 +160,13 @@
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
 
-lemma [simp]:
+lemma flat_Stars [simp]:
  "flat (Stars vs) = concat (map flat vs)"
-apply(induct vs)
-apply(auto)
-done
+by (induct vs) (auto)
+
 
 section {* Relation between values and regular expressions *}
 
-(* non-problematic values...needed in order to fix the *) 
-(* proj lemma in Sulzmann & lu *)
-
-inductive 
-  NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
-where
- "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
-| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
-| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
-| "\<Turnstile> Void : EMPTY"
-| "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
-
 inductive 
   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
@@ -271,99 +178,11 @@
 | "\<turnstile> Stars [] : STAR r"
 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
-lemma NPrf_imp_Prf:
-  assumes "\<Turnstile> v : r" 
-  shows "\<turnstile> v : r"
-using assms
-apply(induct)
-apply(auto intro: Prf.intros)
-done
-
-lemma NPrf_Prf_val:
-  shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
-  and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
-using assms
-apply(induct v and vs arbitrary: r and r rule: val.inducts)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule_tac x="Void" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule_tac x="Char c" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(drule_tac x="r1" in meta_spec)
-apply(drule_tac x="r2" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Seq v' v'a" in exI)
-apply(simp)
-apply (metis NPrf.intros(1))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule_tac x="r2" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Right v'" in exI)
-apply(simp)
-apply (metis NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule_tac x="r1" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Left v'" in exI)
-apply(simp)
-apply (metis NPrf.intros)
-apply(drule_tac x="r" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Stars vs'" in exI)
-apply(simp)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis NPrf.intros(6))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(drule_tac x="ra" in meta_spec)
-apply(simp)
-apply(drule_tac x="STAR ra" in meta_spec)
-apply(simp)
-apply(auto)
-apply(case_tac "flat v = []")
-apply(rule_tac x="vs'" in exI)
-apply(simp)
-apply(rule_tac x="v' # vs'" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(auto)
-done
-
-lemma NPrf_Prf:
-  shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
-apply(auto)
-apply (metis NPrf_Prf_val(1))
-by (metis NPrf_imp_Prf)
-
-
 lemma not_nullable_flat:
-  assumes "\<turnstile> v : r" "\<not>nullable r"
+  assumes "\<turnstile> v : r" "\<not> nullable r"
   shows "flat v \<noteq> []"
 using assms
-apply(induct)
-apply(auto)
-done
+by (induct) (auto)
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -372,11 +191,6 @@
 apply(auto simp add: Sequ_def)
 done
 
-lemma NPrf_flat_L:
-  assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
-using assms
-by (metis NPrf_imp_Prf Prf_flat_L)
-
 lemma Prf_Stars:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
   shows "\<turnstile> Stars vs : STAR r"
@@ -406,14 +220,6 @@
 apply (metis empty_iff list.set(1))
 by (metis concat.simps(2) list.simps(9) set_ConsD)
 
-lemma Star_valN:
-  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
-  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"
-using assms
-apply(induct ss)
-apply(auto)
-apply (metis empty_iff list.set(1))
-by (metis concat.simps(2) list.simps(9) set_ConsD)
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
@@ -438,9 +244,6 @@
 apply(simp)
 done
 
-lemma L_flat_NPrf:
-  "L(r) = {flat v | v. \<Turnstile> v : r}"
-by (metis L_flat_Prf NPrf_Prf)
 
 section {* Values Sets *}
 
@@ -517,20 +320,6 @@
 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
-definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
-  "SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
-
-definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
-  "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
-
-lemma NValues_STAR_Nil:
-  "NValues (STAR r) [] = {Stars []}"
-apply(auto simp add: NValues_def prefix_def)
-apply(erule NPrf.cases)
-apply(auto)
-by (metis NPrf.intros(6))
-
-
 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
   "rest v s \<equiv> drop (length (flat v)) s"
 
@@ -544,18 +333,6 @@
 unfolding rest_def
 by (metis Suffixes_in append_take_drop_id)
 
-lemma rest_SSuffixes:
-  assumes "flat v \<noteq> []" "s \<noteq> []"
-  shows "rest v s \<in> SSuffixes s"
-using assms
-unfolding rest_def
-thm SSuffixes_in
-apply(rule_tac SSuffixes_in)
-apply(rule_tac x="take (length (flat v)) s" in exI)
-apply(simp add: sprefix_def)
-done
-
-
 lemma Values_recs:
   "Values (NULL) s = {}"
   "Values (EMPTY) s = {Void}"
@@ -605,182 +382,10 @@
 apply (metis Prf.intros(7))
 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
-lemma NValues_recs:
-  "NValues (NULL) s = {}"
-  "NValues (EMPTY) s = {Void}"
-  "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 = 
-  {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Stars vs \<in> NValues (STAR r) (rest v s)}"
-unfolding NValues_def
-apply(auto)
-(*NULL*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-(*EMPTY*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply(rule NPrf.intros)
-apply (metis append_Nil prefix_def)
-(*CHAR*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply(rule NPrf.intros)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-(*ALT*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply (metis NPrf.intros(2))
-apply (metis NPrf.intros(3))
-(*SEQ*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-apply (metis NPrf.intros(1))
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-(*STAR*)
-apply(erule NPrf.cases)
-apply(simp_all)
-apply(rule conjI)
-apply(simp add: prefix_def)
-apply(auto)[1]
-apply(simp add: prefix_def)
-apply(auto)[1]
-apply (metis append_eq_conv_conj rest_def)
-apply (metis NPrf.intros(6))
-apply (metis append_Nil prefix_def)
-apply (metis NPrf.intros(7))
-by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
-
-lemma SValues_recs:
- "SValues (NULL) s = {}"
- "SValues (EMPTY) s = (if s = [] then {Void} else {})"
- "SValues (CHAR c) s = (if [c] = s then {Char c} else {})" 
- "SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"
- "SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"
- "SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union> 
-   {Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"
-unfolding SValues_def
-apply(auto)
-(*NULL*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*EMPTY*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*CHAR*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(5))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*ALT*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply metis
-apply(erule Prf.intros)
-apply(erule Prf.intros)
-(* SEQ case *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(1))
-(* STAR case *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply (metis Prf.intros(7))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(7))
-by (metis Prf.intros(7))
-
 lemma finite_image_set2:
   "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
   by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
 
-
-lemma NValues_finite_aux:
-  "(\<lambda>(r, s). finite (NValues r s)) (r, s)"
-apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
-apply (metis wf_lex_prod wf_measure)
-apply(auto)
-apply(case_tac a)
-apply(simp_all)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
-               A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
-prefer 2
-apply(auto)[1]
-apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)
-apply(auto)[1]
-apply (metis rest_Suffixes)
-apply(rule finite_UN_I)
-apply(rule finite_Suffixes)
-apply(simp)
-apply(simp add: NValues_recs)
-apply(clarify)
-apply(subst NValues_recs)
-apply(simp)
-apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and 
-               A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
-prefer 2
-apply(auto)[1]
-apply(auto)
-apply(case_tac b)
-apply(simp)
-defer
-apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)
-apply(auto)[1]
-apply(rule_tac x="rest aa (a # list)" in bexI)
-apply(simp)
-apply (rule rest_SSuffixes)
-apply(simp)
-apply(simp)
-apply(rule finite_UN_I)
-defer
-apply(frule_tac x="rexp" in spec)
-apply(drule_tac x="b" in spec)
-apply(drule conjunct1)
-apply(drule mp)
-apply(simp)
-apply(drule_tac x="STAR rexp" in spec)
-apply(drule_tac x="sp" in spec)
-apply(drule conjunct2)
-apply(drule mp)
-apply(simp)
-apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
-apply(auto)[1]
-apply (metis length_Cons length_rev length_sprefix rev.simps(2))
-apply(simp)
-apply(rule finite_cartesian_product)
-apply(simp)
-apply(rule_tac f="Stars" in finite_imageD)
-prefer 2
-apply(auto simp add: inj_on_def)[1]
-apply (metis finite_subset image_Collect_subsetI)
-apply(simp add: rest_Nil)
-apply(simp add: NValues_STAR_Nil)
-apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
-apply(auto)[1]
-apply(simp)
-apply(rule_tac B="Suffixes b" in finite_subset)
-apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
-by (metis finite_Suffixes)
-
-lemma NValues_finite:
-  "finite (NValues r s)"
-using NValues_finite_aux
-apply(simp)
-done
-
 section {* Sulzmann functions *}
 
 fun 
@@ -938,38 +543,7 @@
 apply (metis Prf.intros(6) Prf.intros(7))
 by (metis Prf.intros(7))
 
-lemma v3_proj:
-  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-  shows "\<Turnstile> (projval r c v) : der c r"
-using assms
-apply(induct rule: NPrf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-apply (metis NPrf.intros(4))
-prefer 2
-apply(simp)
-apply (metis NPrf.intros(2))
-prefer 2
-apply(simp)
-apply (metis NPrf.intros(3))
-apply(auto)
-apply(rule NPrf.intros)
-apply(simp)
-apply (metis NPrf_imp_Prf not_nullable_flat)
-apply(rule NPrf.intros)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-(* Stars case *)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(auto)
-done
+
 
 lemma v4:
   assumes "\<turnstile> v : der c r" 
@@ -1018,30 +592,6 @@
 apply(simp_all)[7]
 done
 
-lemma v4_proj:
-  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-  shows "c # flat (projval r c v) = flat v"
-using assms
-apply(induct rule: NPrf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-prefer 2
-apply(simp)
-prefer 2
-apply(simp)
-apply(auto)
-apply (metis Cons_eq_append_conv)
-apply(simp add: append_eq_Cons_conv)
-apply(auto)
-done
-
-lemma v4_proj2:
-  assumes "\<Turnstile> v : r" and "(flat v) = c # s"
-  shows "flat (projval r c v) = s"
-using assms
-by (metis list.inject v4_proj)
 
 
 section {* Our Alternative Posix definition *}
@@ -1193,6 +743,401 @@
 apply(clarify)
 by (metis PMatch1(2))
 
+
+
+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)
+
+(* a proof that does not need proj *)
+lemma PMatch2_roy_version:
+  assumes "s \<in> (der c r) \<rightarrow> v"
+  shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
+using assms
+apply(induct r arbitrary: s v c rule: rexp.induct)
+apply(auto)
+(* NULL case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* EMPTY case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* CHAR case *)
+apply(case_tac "c = char")
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply (metis PMatch.intros(2))
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* ALT case *)
+prefer 2
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply (metis PMatch.intros(3))
+apply(clarify)
+apply(rule PMatch.intros)
+apply metis
+apply(simp add: der_correctness Der_def)
+(* SEQ case *)
+apply(case_tac "nullable rexp1")
+apply(simp)
+prefer 2
+(* not-nullbale case *)
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(auto)[1]
+apply(simp add: der_correctness Der_def)
+apply(auto)[1]
+(* nullable case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* left case *)
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[4]
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+apply(clarify)
+apply(simp (no_asm))
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(erule contrapos_nn)
+apply(erule exE)+
+apply(auto)[1]
+apply(simp add: der_correctness Der_def)
+apply metis
+(* right interesting case *)
+apply(clarify)
+apply(subst append.simps(1)[symmetric])
+apply(rule PMatch.intros)
+apply (metis PMatch_mkeps)
+apply metis
+apply(rule notI)
+apply(clarify)
+apply(simp)
+apply(simp add: der_correctness)
+apply(simp only: Der_def Sequ_def)
+apply(simp)
+apply (metis Cons_eq_append_conv)
+(* Stars case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rotate_tac 2)
+apply(frule_tac PMatch1)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply(auto)[1]
+apply(rule PMatch.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply (metis L.simps(6))
+apply(subst v4)
+apply (metis PMatch1)
+apply(simp)
+apply(auto)[1]
+apply(drule_tac x="s\<^sub>3" in spec)
+apply(drule mp)
+defer
+apply metis
+apply(clarify)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="c" in meta_spec)
+apply(simp)
+apply(rotate_tac 2)
+apply(drule PMatch.intros(6))
+apply(rule PMatch.intros(7))
+(* HERE *)
+apply (metis PMatch1(1) list.distinct(1) v4)
+apply (metis Nil_is_append_conv)
+apply(simp)
+apply(subst der_correctness)
+apply(simp add: Der_def)
+done 
+
+
+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> \<turnstile> v : r \<and> flat v = s"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+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: der_correctness Der_def)
+apply(auto)
+apply (metis v3)
+apply(rule v4)
+by simp
+
+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)
+apply(simp add: der_correctness Der_def)
+apply(auto)
+by (metis PMatch2_roy_version)
+
+lemma lex_correct5:
+  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_roy_version)
+apply(drule_tac x="der a r" in meta_spec)
+apply(drule meta_mp)
+apply(simp add: der_correctness Der_def)
+apply(auto)
+done
+
+lemma 
+  "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
+apply(simp)
+done
+
+
+
+section {* Connection with Sulzmann's Ordering of values *}
+
+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')" 
+| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
+| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
+| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
+| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
+| "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 (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
+| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
+| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
+| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
+| "(Stars []) \<succ>(STAR r) (Stars [])"
+
+
+(* non-problematic values...needed in order to fix the *) 
+(* proj lemma in Sulzmann & lu *)
+
+inductive 
+  NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
+| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
+| "\<Turnstile> Void : EMPTY"
+| "\<Turnstile> Char c : CHAR c"
+| "\<Turnstile> Stars [] : STAR r"
+| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
+
+lemma NPrf_imp_Prf:
+  assumes "\<Turnstile> v : r" 
+  shows "\<turnstile> v : r"
+using assms
+apply(induct)
+apply(auto intro: Prf.intros)
+done
+
+lemma Star_valN:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r)"
+using assms
+apply(induct ss)
+apply(auto)
+apply (metis empty_iff list.set(1))
+by (metis concat.simps(2) list.simps(9) set_ConsD)
+
+lemma NPrf_Prf_val:
+  shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
+  and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
+using assms
+apply(induct v and vs arbitrary: r and r rule: val.inducts)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Void" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Char c" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="r1" in meta_spec)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Seq v' v'a" in exI)
+apply(simp)
+apply (metis NPrf.intros(1))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r1" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Left v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(drule_tac x="r" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Stars vs'" in exI)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(6))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="ra" in meta_spec)
+apply(simp)
+apply(drule_tac x="STAR ra" in meta_spec)
+apply(simp)
+apply(auto)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs'" in exI)
+apply(simp)
+apply(rule_tac x="v' # vs'" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(auto)
+done
+
+lemma NPrf_Prf:
+  shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
+apply(auto)
+apply (metis NPrf_Prf_val(1))
+by (metis NPrf_imp_Prf)
+
+lemma NPrf_flat_L:
+  assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
+using assms
+by (metis NPrf_imp_Prf Prf_flat_L)
+
+
+lemma L_flat_NPrf:
+  "L(r) = {flat v | v. \<Turnstile> v : r}"
+by (metis L_flat_Prf NPrf_Prf)
+
+
+
+lemma v3_proj:
+  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  shows "\<Turnstile> (projval r c v) : der c r"
+using assms
+apply(induct rule: NPrf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+apply (metis NPrf.intros(4))
+prefer 2
+apply(simp)
+apply (metis NPrf.intros(2))
+prefer 2
+apply(simp)
+apply (metis NPrf.intros(3))
+apply(auto)
+apply(rule NPrf.intros)
+apply(simp)
+apply (metis NPrf_imp_Prf not_nullable_flat)
+apply(rule NPrf.intros)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+(* Stars case *)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(auto)
+done
+
+lemma v4_proj:
+  assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+  shows "c # flat (projval r c v) = flat v"
+using assms
+apply(induct rule: NPrf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+prefer 2
+apply(simp)
+prefer 2
+apply(simp)
+apply(auto)
+apply (metis Cons_eq_append_conv)
+apply(simp add: append_eq_Cons_conv)
+apply(auto)
+done
+
+lemma v4_proj2:
+  assumes "\<Turnstile> v : r" and "(flat v) = c # s"
+  shows "flat (projval r c v) = s"
+using assms
+by (metis list.inject v4_proj)
+
 lemma PMatch1N:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<Turnstile> v : r" 
@@ -1211,13 +1156,7 @@
 apply(rule NPrf.intros)
 done
 
-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)
-
+(* this version needs proj *)
 lemma PMatch2:
   assumes "s \<in> (der c r) \<rightarrow> v"
   shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
@@ -1346,54 +1285,7 @@
 apply(simp)
 apply(subst der_correctness)
 apply(simp add: Der_def)
-done
-
-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> \<turnstile> v : r \<and> flat v = s"
-using assms
-apply(induct s arbitrary: r)
-apply(simp)
-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_NPrf)
-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)
-apply(simp add: L_flat_NPrf)
-apply(auto)
-apply (metis v3_proj v4_proj2)
-apply(rule PMatch2)
-apply(simp)
-done
+done 
 
 lemma lex_correct4:
   assumes "s \<in> L r"
@@ -1404,45 +1296,4 @@
 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)
-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_NPrf)
-apply(auto)
-apply (metis v3_proj v4_proj2)
-done
-
-lemma 
-  "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
-apply(simp)
-done
-
-section {* Sulzmann's Ordering of values *}
-
-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')" 
-| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
-| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
-| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
-| "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 (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
-| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
-| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
-| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
-| "(Stars []) \<succ>(STAR r) (Stars [])"
-
-
-
 end
\ No newline at end of file