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 - |
521 fix xs ys zs |
|
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" |