src/HOL/Library/Sublist.thy

--- a/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:15 2014 +0200
+++ b/src/HOL/Library/Sublist.thy	Thu Jul 03 09:55:16 2014 +0200
@@ -514,34 +514,31 @@
   by (induct rule: list_emb.induct) auto
 
 lemma list_emb_trans:
-  assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
-  shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
-    list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
+  assumes "\<And>x y z. \<lbrakk>x \<in> set xs; y \<in> set ys; z \<in> set zs; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
+  shows "\<lbrakk>list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"
 proof -
-  fix xs ys zs
   assume "list_emb P xs ys" and "list_emb P ys zs"
-    and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
-  then show "list_emb P xs zs"
+  then show "list_emb P xs zs" using assms
   proof (induction arbitrary: zs)
     case list_emb_Nil show ?case by blast
   next
     case (list_emb_Cons xs ys y)
     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
-      where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
+      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast
     then have "list_emb P ys (v#vs)" by blast
     then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)
-    from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
+    from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto
   next
     case (list_emb_Cons2 x y xs ys)
     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
       where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast
-    with list_emb_Cons2 have "list_emb P xs vs" by simp
+    with list_emb_Cons2 have "list_emb P xs vs" by auto
     moreover have "P x v"
     proof -
-      from zs and `zs \<in> lists A` have "v \<in> A" by auto
-      moreover have "x \<in> A" and "y \<in> A" using list_emb_Cons2 by simp_all
+      from zs have "v \<in> set zs" by auto
+      moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all
       ultimately show ?thesis
-        using `P x y` and `P y v` and assms
+        using `P x y` and `P y v` and list_emb_Cons2
         by blast
     qed
     ultimately have "list_emb P (x#xs) (v#vs)" by blast
@@ -549,6 +546,11 @@
   qed
 qed
 
+lemma list_emb_set:
+  assumes "list_emb P xs ys" and "x \<in> set xs"
+  obtains y where "y \<in> set ys" and "P x y"
+  using assms by (induct) auto
+
 
 subsection {* Sublists (special case of homeomorphic embedding) *}
 
@@ -607,7 +609,7 @@
 qed
 
 lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
-  by (rule list_emb_trans [of UNIV "op ="]) auto
+  by (rule list_emb_trans [of _ _ _ "op ="]) auto
 
 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   by (auto dest: list_emb_length)