--- a/thys/ReStar.thy	Mon Mar 07 18:56:41 2016 +0000
+++ b/thys/ReStar.thy	Mon Mar 07 21:54:50 2016 +0000
@@ -460,6 +460,14 @@
 apply(auto intro: Prf.intros)
 done
 
+lemma PMatch1a:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "s \<in> L r"
+using assms
+apply(induct s r v rule: PMatch.induct)
+apply(auto simp add: Sequ_def)
+done
+
 lemma PMatch_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
@@ -482,105 +490,60 @@
 apply(metis PMatch.intros(7))
 done
 
-find_theorems Stars
-thm compat_val_list.induct compat_val.induct
-
-
 lemma PMatch_determ:
-  shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
-  and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
-apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: compat_val.induct compat_val_list.induct)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(erule PMatch.cases)
-apply(simp_all)[7]
+  assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
+  shows "v1 = v2"
+using assms
+apply(induct s r v1 arbitrary: v2 rule: PMatch.induct)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(erule PMatch.cases)
 apply(simp_all)[7]
-apply(clarify)
-apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
-apply metis
-apply(rule conjI)
-apply(simp add: append_eq_append_conv2)
-apply(auto)[1]
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
-apply(simp add: append_eq_append_conv2)
-apply(auto)[1]
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(rotate_tac 2)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(force)
 apply(clarify)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis PMatch1(1) PMatch1(2) Prf_flat_L)
-(* star case *)
-defer
+apply(drule PMatch1a)
+apply(simp)
+apply(rotate_tac 3)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis PMatch1(2))
-apply(rotate_tac  3)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
+apply(simp_all (no_asm_use))[7]
+apply(drule PMatch1a)+
+apply(simp)
+apply(simp)
+apply(rotate_tac 5)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
+apply(simp_all (no_asm_use))[7]
 apply(clarify)
-apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
-apply metis
+apply(subgoal_tac "s1 = s1a")
+apply(blast)
 apply(simp add: append_eq_append_conv2)
-apply(auto)[1]
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
+apply(clarify)
+apply (metis PMatch1a append_self_conv)
+apply(rotate_tac 6)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis PMatch1(2))
-apply(erule PMatch.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(erule PMatch.cases)
-apply(simp_all)[7]
+apply(simp_all (no_asm_use))[7]
 apply(clarify)
-apply(subgoal_tac "s1 = s1a \<and> s2 = s2a")
-apply(drule_tac x="s1 @ s2" in meta_spec)
-apply(drule_tac x="rb" in meta_spec)
-apply(drule_tac x="(va#vsa)" in meta_spec)
+apply(subgoal_tac "s1 = s1a")
 apply(simp)
-apply(drule meta_mp)
-apply (metis L.simps(6) PMatch.intros(6))
-apply (metis L.simps(6) PMatch.intros(6))
-apply(simp add: append_eq_append_conv2)
-apply(auto)[1]
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L)
-apply (metis PMatch1(2))
+apply(blast)
+apply(simp  (no_asm_use) add: append_eq_append_conv2)
+apply(clarify)
+apply (metis L.simps(6) PMatch1a append_self_conv)
+apply(clarify)
+apply(rotate_tac 2)
 apply(erule PMatch.cases)
-apply(simp_all)[7]
+apply(simp_all (no_asm_use))[7]
+using PMatch1(2) apply auto[1]
+using PMatch1(2) apply blast
+apply(erule PMatch.cases)
+apply(simp_all (no_asm_use))[7]
 apply(clarify)
-by (metis PMatch1(2))
+apply (simp add: PMatch1(2))
+apply(simp)
+done
 
 (* a proof that does not need proj *)
 lemma PMatch2_roy_version: