weaker assumption for "list_emb_trans"; added lemma
authorChristian Sternagel
Thu Jul 03 09:55:16 2014 +0200 (2014-07-03)
changeset 575005a8b3e9d82a4
parent 57499 7e22776f2d32
child 57501 b69a1272cb04
weaker assumption for "list_emb_trans"; added lemma
src/HOL/Library/Sublist.thy
     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)