# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1450433461 0
# Node ID f89372781a4c6a2d46fb4497abb6a120735eb27b
# Parent  a8bcb5a0f9b9507e619a8d2896222c7248f39006
the algorithm is correct according to the Type Inference definition

diff -r a8bcb5a0f9b9 -r f89372781a4c thys/Re.thy
--- a/thys/Re.thy	Fri Dec 18 00:37:35 2015 +0000
+++ b/thys/Re.thy	Fri Dec 18 10:11:01 2015 +0000
@@ -603,7 +603,7 @@
 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
-    \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s2) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
+    \<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:
@@ -638,7 +638,7 @@
 apply (metis Prf.intros(2))
 apply (metis Prf.intros(3))
 apply (metis Prf.intros(1))
-by (metis Prf.intros(1))
+done
 
 lemma PMAtch2:
   assumes "s \<in> (der c r) \<rightarrow> v"
@@ -689,10 +689,13 @@
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="projval r1 c v" in spec)
+apply(drule_tac x="s3" in spec)
 apply(drule mp)
+apply(rule_tac x="projval r1 c v" in exI)
+apply(rule conjI)
 apply (metis v4_proj2)
 apply(simp)
+apply metis
 (* nullable case *)
 apply(erule PMatch.cases)
 apply(simp_all)[5]
@@ -709,7 +712,7 @@
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="projval r1 c v" in spec)
+apply(drule_tac x="s3" in spec)
 apply(drule mp)
 apply (metis v4_proj2)
 apply(simp)
@@ -728,33 +731,15 @@
 apply(simp only: L_flat_Prf)
 apply(simp)
 apply(auto)
-apply(drule_tac x="projval r1 c v" in spec)
+apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 apply(drule mp)
-apply (metis v4_proj2)
-apply(rotate_tac 1)
-apply(drule_tac x="sa" in meta_spec)
-apply(drule_tac x="va" in meta_spec)
 apply(simp)
-apply(rotate_tac 2)
-apply(drule_tac x="sa" in meta_spec)
-apply(drule_tac x="projval r1 c v" in meta_spec)
-apply(drule meta_mp)
-apply(frule_tac c="c" in v3_proj)
-apply metis
-
-apply(frule PMatch1(1))
-apply(drule PMatch1(2))
-apply(clarify)
-apply(subst (asm) (2) not_def)
-apply(drule mp)
-thm v3_proj
+apply (metis append_Cons butlast_snoc last_snoc neq_Nil_conv rotate1.simps(2) v4_proj2)
+apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
+apply (metis Prf.intros(1))
 apply(rule v3_proj)
-apply(rule conjI)
-apply (metis v4_proj2)
-apply (metis v3_proj)
-v3_proj
-
-
+apply(simp)
+by (metis Cons_eq_append_conv)