author | Christian Sternagel |

Thu Jul 03 09:55:16 2014 +0200 (2014-07-03) | |

changeset 57500 | 5a8b3e9d82a4 |

parent 57499 | 7e22776f2d32 |

child 57501 | b69a1272cb04 |

weaker assumption for "list_emb_trans"; added lemma

1.1 --- a/src/HOL/Library/Sublist.thy Thu Jul 03 09:55:15 2014 +0200 1.2 +++ b/src/HOL/Library/Sublist.thy Thu Jul 03 09:55:16 2014 +0200 1.3 @@ -514,34 +514,31 @@ 1.4 by (induct rule: list_emb.induct) auto 1.5 1.6 lemma list_emb_trans: 1.7 - 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" 1.8 - shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A; 1.9 - list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs" 1.10 + 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" 1.11 + shows "\<lbrakk>list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs" 1.12 proof - 1.13 - fix xs ys zs 1.14 assume "list_emb P xs ys" and "list_emb P ys zs" 1.15 - and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A" 1.16 - then show "list_emb P xs zs" 1.17 + then show "list_emb P xs zs" using assms 1.18 proof (induction arbitrary: zs) 1.19 case list_emb_Nil show ?case by blast 1.20 next 1.21 case (list_emb_Cons xs ys y) 1.22 from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs 1.23 - where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast 1.24 + where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast 1.25 then have "list_emb P ys (v#vs)" by blast 1.26 then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2) 1.27 - from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp 1.28 + from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto 1.29 next 1.30 case (list_emb_Cons2 x y xs ys) 1.31 from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs 1.32 where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast 1.33 - with list_emb_Cons2 have "list_emb P xs vs" by simp 1.34 + with list_emb_Cons2 have "list_emb P xs vs" by auto 1.35 moreover have "P x v" 1.36 proof - 1.37 - from zs and `zs \<in> lists A` have "v \<in> A" by auto 1.38 - moreover have "x \<in> A" and "y \<in> A" using list_emb_Cons2 by simp_all 1.39 + from zs have "v \<in> set zs" by auto 1.40 + moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all 1.41 ultimately show ?thesis 1.42 - using `P x y` and `P y v` and assms 1.43 + using `P x y` and `P y v` and list_emb_Cons2 1.44 by blast 1.45 qed 1.46 ultimately have "list_emb P (x#xs) (v#vs)" by blast 1.47 @@ -549,6 +546,11 @@ 1.48 qed 1.49 qed 1.50 1.51 +lemma list_emb_set: 1.52 + assumes "list_emb P xs ys" and "x \<in> set xs" 1.53 + obtains y where "y \<in> set ys" and "P x y" 1.54 + using assms by (induct) auto 1.55 + 1.56 1.57 subsection {* Sublists (special case of homeomorphic embedding) *} 1.58 1.59 @@ -607,7 +609,7 @@ 1.60 qed 1.61 1.62 lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs" 1.63 - by (rule list_emb_trans [of UNIV "op ="]) auto 1.64 + by (rule list_emb_trans [of _ _ _ "op ="]) auto 1.65 1.66 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []" 1.67 by (auto dest: list_emb_length)