src/HOL/Library/Sublist.thy
 changeset 57500 5a8b3e9d82a4 parent 57499 7e22776f2d32 child 58881 b9556a055632
equal inserted replaced
57499:7e22776f2d32 57500:5a8b3e9d82a4
`   512 `
`   512 `
`   513 lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"`
`   513 lemma list_emb_length: "list_emb P xs ys \<Longrightarrow> length xs \<le> length ys"`
`   514   by (induct rule: list_emb.induct) auto`
`   514   by (induct rule: list_emb.induct) auto`
`   515 `
`   515 `
`   516 lemma list_emb_trans:`
`   516 lemma list_emb_trans:`
`   517   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"`
`   517   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"`
`   518   shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;`
`   518   shows "\<lbrakk>list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"`
`   519     list_emb P xs ys; list_emb P ys zs\<rbrakk> \<Longrightarrow> list_emb P xs zs"`
`       `
`   520 proof -`
`   519 proof -`
`   522   assume "list_emb P xs ys" and "list_emb P ys zs"`
`   520   assume "list_emb P xs ys" and "list_emb P ys zs"`
`   523     and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"`
`   521   then show "list_emb P xs zs" using assms`
`   524   then show "list_emb P xs zs"`
`       `
`   525   proof (induction arbitrary: zs)`
`   522   proof (induction arbitrary: zs)`
`   526     case list_emb_Nil show ?case by blast`
`   523     case list_emb_Nil show ?case by blast`
`   527   next`
`   524   next`
`   528     case (list_emb_Cons xs ys y)`
`   525     case (list_emb_Cons xs ys y)`
`   529     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs`
`   526     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs`
`   530       where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast`
`   527       where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_emb P ys vs" by blast`
`   531     then have "list_emb P ys (v#vs)" by blast`
`   528     then have "list_emb P ys (v#vs)" by blast`
`   532     then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)`
`   529     then have "list_emb P ys zs" unfolding zs by (rule list_emb_append2)`
`   533     from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp`
`   530     from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto`
`   534   next`
`   531   next`
`   535     case (list_emb_Cons2 x y xs ys)`
`   532     case (list_emb_Cons2 x y xs ys)`
`   536     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs`
`   533     from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs`
`   537       where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast`
`   534       where zs: "zs = us @ v # vs" and "P y v" and "list_emb P ys vs" by blast`
`   538     with list_emb_Cons2 have "list_emb P xs vs" by simp`
`   535     with list_emb_Cons2 have "list_emb P xs vs" by auto`
`   539     moreover have "P x v"`
`   536     moreover have "P x v"`
`   540     proof -`
`   537     proof -`
`   541       from zs and `zs \<in> lists A` have "v \<in> A" by auto`
`   538       from zs have "v \<in> set zs" by auto`
`   542       moreover have "x \<in> A" and "y \<in> A" using list_emb_Cons2 by simp_all`
`   539       moreover have "x \<in> set (x#xs)" and "y \<in> set (y#ys)" by simp_all`
`   543       ultimately show ?thesis`
`   540       ultimately show ?thesis`
`   544         using `P x y` and `P y v` and assms`
`   541         using `P x y` and `P y v` and list_emb_Cons2`
`   545         by blast`
`   542         by blast`
`   546     qed`
`   543     qed`
`   547     ultimately have "list_emb P (x#xs) (v#vs)" by blast`
`   544     ultimately have "list_emb P (x#xs) (v#vs)" by blast`
`   548     then show ?case unfolding zs by (rule list_emb_append2)`
`   545     then show ?case unfolding zs by (rule list_emb_append2)`
`   549   qed`
`   546   qed`
`   550 qed`
`   547 qed`
`       `
`   548 `
`       `
`   549 lemma list_emb_set:`
`       `
`   550   assumes "list_emb P xs ys" and "x \<in> set xs"`
`       `
`   551   obtains y where "y \<in> set ys" and "P x y"`
`       `
`   552   using assms by (induct) auto`
`   551 `
`   553 `
`   552 `
`   554 `
`   553 subsection {* Sublists (special case of homeomorphic embedding) *}`
`   555 subsection {* Sublists (special case of homeomorphic embedding) *}`
`   554 `
`   556 `
`   555 abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"`
`   557 abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"`
`   605   hence False using sublisteq_Cons' by fastforce`
`   607   hence False using sublisteq_Cons' by fastforce`
`   606   thus ?case ..`
`   608   thus ?case ..`
`   607 qed`
`   609 qed`
`   608 `
`   610 `
`   609 lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"`
`   611 lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"`
`   610   by (rule list_emb_trans [of UNIV "op ="]) auto`
`   612   by (rule list_emb_trans [of _ _ _ "op ="]) auto`
`   611 `
`   613 `
`   612 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"`
`   614 lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"`
`   613   by (auto dest: list_emb_length)`
`   615   by (auto dest: list_emb_length)`
`   614 `
`   616 `
`   615 lemma list_emb_append_mono:`
`   617 lemma list_emb_append_mono:`