--- a/thys/Paper/Paper.thy	Mon Mar 07 21:54:50 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Mar 07 22:20:15 2016 +0000
@@ -541,7 +541,7 @@
   \begin{proof}
   Both properties are by routine inductions: the first one, for example,
   by an induction over the definition of @{term derivatives}; the second by
-  induction on @{term r}. There are no interesting cases.
+  induction on @{term r}. There are no interesting cases.\qed
   \end{proof}
 
   Having defined the @{const mkeps} and @{text inj} function we can extend
@@ -641,14 +641,16 @@
 
   \begin{proof}
   By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and a case
-  analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}.
+  analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}.\qed
   \end{proof}
 
   \begin{lemma}
   @{thm[mode=IfThen] PMatch_mkeps}
   \end{lemma}
 
-  
+  \begin{proof}
+  By routine induction on @{term r}.\qed 
+  \end{proof}
 
   \begin{lemma}
   @{thm[mode=IfThen] PMatch2_roy_version}

--- a/thys/ReStar.thy	Mon Mar 07 21:54:50 2016 +0000
+++ b/thys/ReStar.thy	Mon Mar 07 22:20:15 2016 +0000
@@ -454,18 +454,18 @@
 
 lemma PMatch1:
   assumes "s \<in> r \<rightarrow> v"
-  shows "\<turnstile> v : r" "flat v = s"
+  shows "s \<in> L r" "flat v = s"
 using assms
 apply(induct s r v rule: PMatch.induct)
-apply(auto intro: Prf.intros)
+apply(auto simp add: Sequ_def)
 done
 
 lemma PMatch1a:
   assumes "s \<in> r \<rightarrow> v"
-  shows "s \<in> L r"
+  shows "\<turnstile> v : r"
 using assms
 apply(induct s r v rule: PMatch.induct)
-apply(auto simp add: Sequ_def)
+apply(auto intro: Prf.intros)
 done
 
 lemma PMatch_mkeps:
@@ -473,21 +473,10 @@
   shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(induct r)
-apply(auto)
-apply (metis PMatch.intros(1))
+apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def)
 apply(subst append.simps(1)[symmetric])
 apply (rule PMatch.intros)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply (rule PMatch.intros)
-apply(simp)
-apply (rule PMatch.intros)
-apply(simp)
-apply (rule PMatch.intros)
-apply(simp)
-apply (metis nullable_correctness)
-apply(metis PMatch.intros(7))
+apply(auto)
 done
 
 lemma PMatch_determ:
@@ -505,12 +494,12 @@
 apply(clarify)
 apply(force)
 apply(clarify)
-apply(drule PMatch1a)
+apply(drule PMatch1(1))
 apply(simp)
 apply(rotate_tac 3)
 apply(erule PMatch.cases)
 apply(simp_all (no_asm_use))[7]
-apply(drule PMatch1a)+
+apply(drule PMatch1(1))+
 apply(simp)
 apply(simp)
 apply(rotate_tac 5)
@@ -521,7 +510,7 @@
 apply(blast)
 apply(simp add: append_eq_append_conv2)
 apply(clarify)
-apply (metis PMatch1a append_self_conv)
+apply (metis PMatch1(1) append_self_conv)
 apply(rotate_tac 6)
 apply(erule PMatch.cases)
 apply(simp_all (no_asm_use))[7]
@@ -531,7 +520,7 @@
 apply(blast)
 apply(simp  (no_asm_use) add: append_eq_append_conv2)
 apply(clarify)
-apply (metis L.simps(6) PMatch1a append_self_conv)
+apply (metis L.simps(6) PMatch1(1) append_self_conv)
 apply(clarify)
 apply(rotate_tac 2)
 apply(erule PMatch.cases)
@@ -791,525 +780,5 @@
 done
 
 
-section {* Attic stuff below *}
-
-section {* Projection function *}
-
-fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
-where
-  "projval (CHAR d) c _ = Void"
-| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
-| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
-| "projval (SEQ r1 r2) c (Seq v1 v2) = 
-     (if flat v1 = [] then Right(projval r2 c v2) 
-      else if nullable r1 then Left (Seq (projval r1 c v1) v2)
-                          else Seq (projval r1 c v1) v2)"
-| "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
-
-
-
-section {* Values Sets *}
-
-definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
-where
-  "s1 \<sqsubseteq> s2 \<equiv> \<exists>s3. s1 @ s3 = s2"
-
-definition sprefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100)
-where
-  "s1 \<sqsubset> s2 \<equiv> (s1 \<sqsubseteq> s2 \<and> s1 \<noteq> s2)"
-
-lemma length_sprefix:
-  "s1 \<sqsubset> s2 \<Longrightarrow> length s1 < length s2"
-unfolding sprefix_def prefix_def
-by (auto)
-
-definition Prefixes :: "string \<Rightarrow> string set" where
-  "Prefixes s \<equiv> {sp. sp \<sqsubseteq> s}"
-
-definition Suffixes :: "string \<Rightarrow> string set" where
-  "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
-
-definition SPrefixes :: "string \<Rightarrow> string set" where
-  "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
-
-definition SSuffixes :: "string \<Rightarrow> string set" where
-  "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
-
-lemma Suffixes_in: 
-  "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
-unfolding Suffixes_def Prefixes_def prefix_def image_def
-apply(auto)
-by (metis rev_rev_ident)
-
-lemma SSuffixes_in: 
-  "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
-unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
-apply(auto)
-by (metis append_self_conv rev.simps(1) rev_rev_ident)
-
-lemma Prefixes_Cons:
-  "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
-unfolding Prefixes_def prefix_def
-apply(auto simp add: append_eq_Cons_conv) 
-done
-
-lemma finite_Prefixes:
-  "finite (Prefixes s)"
-apply(induct s)
-apply(auto simp add: Prefixes_def prefix_def)[1]
-apply(simp add: Prefixes_Cons)
-done
-
-lemma finite_Suffixes:
-  "finite (Suffixes s)"
-unfolding Suffixes_def
-apply(rule finite_imageI)
-apply(rule finite_Prefixes)
-done
-
-lemma prefix_Cons:
-  "((c # s1) \<sqsubseteq> (c # s2)) = (s1 \<sqsubseteq> s2)"
-apply(auto simp add: prefix_def)
-done
-
-lemma prefix_append:
-  "((s @ s1) \<sqsubseteq> (s @ s2)) = (s1 \<sqsubseteq> s2)"
-apply(induct s)
-apply(simp)
-apply(simp add: prefix_Cons)
-done
-
-
-definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
-  "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
-
-definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
-  "rest v s \<equiv> drop (length (flat v)) s"
-
-lemma rest_Nil:
-  "rest v [] = []"
-apply(simp add: rest_def)
-done
-
-lemma rest_Suffixes:
-  "rest v s \<in> Suffixes s"
-unfolding rest_def
-by (metis Suffixes_in append_take_drop_id)
-
-lemma Values_recs:
-  "Values (ZERO) s = {}"
-  "Values (ONE) s = {Void}"
-  "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 = 
-      {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
-unfolding Values_def
-apply(auto)
-(*ZERO*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*ONE*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply (metis append_Nil prefix_def)
-(*CHAR*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*ALT*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(2))
-apply (metis Prf.intros(3))
-(*SEQ*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-apply (metis Prf.intros(1))
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-(*STAR*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-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 Prf.intros(6))
-apply (metis append_Nil prefix_def)
-apply (metis Prf.intros(7))
-by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
-
-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 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
-
-
-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>ONE 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 : ONE"
-| "\<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: compat_val.induct compat_val_list.induct)
-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" 
-using assms
-apply(induct s r v rule: PMatch.induct)
-apply(auto)
-apply (metis NPrf.intros(4))
-apply (metis NPrf.intros(5))
-apply (metis NPrf.intros(2))
-apply (metis NPrf.intros(3))
-apply (metis NPrf.intros(1))
-apply(rule NPrf.intros)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(rule NPrf.intros)
-done
-
-(* this version needs proj *)
-lemma PMatch2:
-  assumes "s \<in> (der c r) \<rightarrow> v"
-  shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
-using assms
-apply(induct c r arbitrary: s v rule: der.induct)
-apply(auto)
-(* ZERO case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* ONE case *)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-(* CHAR case *)
-apply(case_tac "c = d")
-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 *)
-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 r1")
-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(simp)
-apply(subst (asm) L.simps(4)[symmetric])
-apply(simp only: L_flat_Prf)
-apply(simp)
-apply(subst append.simps(1)[symmetric])
-apply(rule PMatch.intros)
-apply (metis PMatch_mkeps)
-apply metis
-apply(auto)
-apply(simp only: L_flat_NPrf)
-apply(simp)
-apply(auto)
-apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
-apply(drule mp)
-apply(simp)
-apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
-apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
-apply (metis NPrf_imp_Prf Prf.intros(1))
-apply(rule NPrf_imp_Prf)
-apply(rule v3_proj)
-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 Prf_injval_flat)
-apply (metis NPrf_imp_Prf PMatch1N)
-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(simp)
-apply(rotate_tac 2)
-apply(drule PMatch.intros(6))
-apply(rule PMatch.intros(7))
-apply (metis PMatch1(1) list.distinct(1) Prf_injval_flat)
-apply (metis Nil_is_append_conv)
-apply(simp)
-apply(subst der_correctness)
-apply(simp add: Der_def)
-done 
-
-lemma lex_correct4:
-  assumes "s \<in> L r"
-  shows "\<exists>v. matcher 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))
-
 
 end
\ No newline at end of file

Binary file thys/paper.pdf has changed