haftmann@26735: (* Title: HOL/Library/Sublist_Order.thy
haftmann@26735: Authors: Peter Lammich, Uni Muenster
nipkow@33431: Florian Haftmann, Tobias Nipkow, TU Muenchen
haftmann@26735: *)
haftmann@26735:
haftmann@26735: header {* Sublist Ordering *}
haftmann@26735:
haftmann@26735: theory Sublist_Order
haftmann@30738: imports Main
haftmann@26735: begin
haftmann@26735:
haftmann@26735: text {*
haftmann@26735: This theory defines sublist ordering on lists.
haftmann@26735: A list @{text ys} is a sublist of a list @{text xs},
haftmann@26735: iff one obtains @{text ys} by erasing some elements from @{text xs}.
haftmann@26735: *}
haftmann@26735:
haftmann@26735: subsection {* Definitions and basic lemmas *}
haftmann@26735:
nipkow@33431: instantiation list :: (type) ord
haftmann@26735: begin
haftmann@26735:
haftmann@26735: inductive less_eq_list where
haftmann@26735: empty [simp, intro!]: "[] \ xs"
haftmann@26735: | drop: "ys \ xs \ ys \ x # xs"
haftmann@26735: | take: "ys \ xs \ x # ys \ x # xs"
haftmann@26735:
haftmann@26735: definition
haftmann@28562: [code del]: "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs"
haftmann@26735:
nipkow@33431: instance proof qed
nipkow@33431:
nipkow@33431: end
nipkow@33431:
nipkow@33431: lemma le_list_length: "xs \ ys \ length xs \ length ys"
nipkow@33431: by (induct rule: less_eq_list.induct) auto
nipkow@33431:
nipkow@33431: lemma le_list_same_length: "xs \ ys \ length xs = length ys \ xs = ys"
nipkow@33431: by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
nipkow@33431:
nipkow@33431: lemma not_le_list_length[simp]: "length ys < length xs \ ~ xs <= ys"
nipkow@33431: by (metis le_list_length linorder_not_less)
nipkow@33431:
nipkow@33431: lemma le_list_below_empty [simp]: "xs \ [] \ xs = []"
nipkow@33431: by (auto dest: le_list_length)
nipkow@33431:
nipkow@33431: lemma le_list_drop_many: "xs \ ys \ xs \ zs @ ys"
nipkow@33431: by (induct zs) (auto intro: drop)
nipkow@33431:
nipkow@33431: lemma [code]: "[] <= xs \ True"
nipkow@33431: by(metis less_eq_list.empty)
nipkow@33431:
nipkow@33431: lemma [code]: "(x#xs) <= [] \ False"
nipkow@33431: by simp
nipkow@33431:
nipkow@33431: lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
nipkow@33431: proof-
nipkow@33431: { fix xs' ys'
nipkow@33431: assume "xs' <= ys"
nipkow@33431: hence "ALL x xs. xs' = x#xs \ xs <= ys"
nipkow@33431: proof induct
nipkow@33431: case empty thus ?case by simp
nipkow@33431: next
nipkow@33431: case drop thus ?case by (metis less_eq_list.drop)
nipkow@33431: next
nipkow@33431: case take thus ?case by (simp add: drop)
nipkow@33431: qed }
nipkow@33431: from this[OF assms] show ?thesis by simp
nipkow@33431: qed
nipkow@33431:
nipkow@33431: lemma le_list_drop_Cons2:
nipkow@33431: assumes "x#xs <= x#ys" shows "xs <= ys"
nipkow@33431: using assms
nipkow@33431: proof cases
nipkow@33431: case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
nipkow@33431: qed simp_all
nipkow@33431:
nipkow@33431: lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
nipkow@33431: shows "x ~= y \ x # xs <= ys"
nipkow@33431: using assms proof cases qed auto
nipkow@33431:
nipkow@33431: lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \
nipkow@33431: (if x=y then xs <= ys else (x#xs) <= ys)"
nipkow@33431: by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
nipkow@33431:
nipkow@33431: lemma le_list_take_many_iff: "zs @ xs \ zs @ ys \ xs \ ys"
nipkow@33431: by (induct zs) (auto intro: take)
nipkow@33431:
nipkow@33431: lemma le_list_Cons_EX:
nipkow@33431: assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
nipkow@33431: proof-
nipkow@33431: { fix xys zs :: "'a list" assume "xys <= zs"
nipkow@33431: hence "ALL x ys. xys = x#ys \ (EX us vs. zs = us @ x # vs & ys <= vs)"
nipkow@33431: proof induct
nipkow@33431: case empty show ?case by simp
nipkow@33431: next
nipkow@33431: case take thus ?case by (metis list.inject self_append_conv2)
nipkow@33431: next
nipkow@33431: case drop thus ?case by (metis append_eq_Cons_conv)
nipkow@33431: qed
nipkow@33431: } with assms show ?thesis by blast
nipkow@33431: qed
nipkow@33431:
nipkow@33431: instantiation list :: (type) order
nipkow@33431: begin
haftmann@26735:
haftmann@26735: instance proof
haftmann@26735: fix xs ys :: "'a list"
haftmann@27682: show "xs < ys \ xs \ ys \ \ ys \ xs" unfolding less_list_def ..
haftmann@26735: next
haftmann@26735: fix xs :: "'a list"
nipkow@33431: show "xs \ xs" by (induct xs) (auto intro!: less_eq_list.drop)
haftmann@26735: next
haftmann@26735: fix xs ys :: "'a list"
nipkow@33431: assume "xs <= ys"
nipkow@33431: hence "ys <= xs \ xs = ys"
nipkow@33431: proof induct
nipkow@33431: case empty show ?case by simp
nipkow@33431: next
nipkow@33431: case take thus ?case by simp
nipkow@33431: next
nipkow@33431: case drop thus ?case
nipkow@33431: by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
nipkow@33431: qed
nipkow@33431: moreover assume "ys <= xs"
haftmann@26735: ultimately show "xs = ys" by blast
haftmann@26735: next
haftmann@26735: fix xs ys zs :: "'a list"
nipkow@33431: assume "xs <= ys"
nipkow@33431: hence "ys <= zs \ xs <= zs"
nipkow@33431: proof (induct arbitrary:zs)
nipkow@33431: case empty show ?case by simp
nipkow@33431: next
nipkow@33431: case (take xs ys x) show ?case
nipkow@33431: proof
nipkow@33431: assume "x # ys <= zs"
nipkow@33431: with take show "x # xs <= zs"
nipkow@33431: by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
haftmann@26735: qed
nipkow@33431: next
nipkow@33431: case drop thus ?case by (metis le_list_drop_Cons)
nipkow@33431: qed
nipkow@33431: moreover assume "ys <= zs"
nipkow@33431: ultimately show "xs <= zs" by blast
haftmann@26735: qed
haftmann@26735:
haftmann@26735: end
haftmann@26735:
nipkow@33431: lemma le_list_append_le_same_iff: "xs @ ys <= ys \ xs=[]"
nipkow@33431: by (auto dest: le_list_length)
haftmann@26735:
nipkow@33431: lemma le_list_append_mono: "\ xs <= xs'; ys <= ys' \ \ xs@ys <= xs'@ys'"
nipkow@33431: apply (induct rule:less_eq_list.induct)
nipkow@33431: apply (metis eq_Nil_appendI le_list_drop_many)
nipkow@33431: apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
nipkow@33431: apply simp
nipkow@33431: done
haftmann@26735:
nipkow@33431: lemma less_list_length: "xs < ys \ length xs < length ys"
nipkow@33431: by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
haftmann@26735:
nipkow@33431: lemma less_list_empty [simp]: "[] < xs \ xs \ []"
nipkow@33431: by (metis empty order_less_le)
nipkow@33431:
nipkow@33431: lemma less_list_below_empty[simp]: "xs < [] \ False"
nipkow@33431: by (metis empty less_list_def)
nipkow@33431:
nipkow@33431: lemma less_list_drop: "xs < ys \ xs < x # ys"
nipkow@33431: by (unfold less_le) (auto intro: less_eq_list.drop)
haftmann@26735:
nipkow@33431: lemma less_list_take_iff: "x # xs < x # ys \ xs < ys"
nipkow@33431: by (metis le_list_Cons2_iff less_list_def)
nipkow@33431:
nipkow@33431: lemma less_list_drop_many: "xs < ys \ xs < zs @ ys"
nipkow@33431: by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
nipkow@33431:
nipkow@33431: lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys"
nipkow@33431: by (metis le_list_take_many_iff less_list_def)
haftmann@26735:
haftmann@26735:
haftmann@26735: subsection {* Appending elements *}
haftmann@26735:
nipkow@33431: lemma le_list_rev_take_iff[simp]: "xs @ zs \ ys @ zs \ xs \ ys" (is "?L = ?R")
nipkow@33431: proof
nipkow@33431: { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
nipkow@33431: hence "xs' = xs @ zs & ys' = ys @ zs \ xs <= ys"
nipkow@33431: proof (induct arbitrary: xs ys zs)
nipkow@33431: case empty show ?case by simp
nipkow@33431: next
nipkow@33431: case (drop xs' ys' x)
nipkow@33431: { assume "ys=[]" hence ?case using drop(1) by auto }
nipkow@33431: moreover
nipkow@33431: { fix us assume "ys = x#us"
nipkow@33431: hence ?case using drop(2) by(simp add: less_eq_list.drop) }
nipkow@33431: ultimately show ?case by (auto simp:Cons_eq_append_conv)
nipkow@33431: next
nipkow@33431: case (take xs' ys' x)
nipkow@33431: { assume "xs=[]" hence ?case using take(1) by auto }
nipkow@33431: moreover
nipkow@33431: { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
nipkow@33431: moreover
nipkow@33431: { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
nipkow@33431: ultimately show ?case by (auto simp:Cons_eq_append_conv)
nipkow@33431: qed }
nipkow@33431: moreover assume ?L
nipkow@33431: ultimately show ?R by blast
nipkow@33431: next
nipkow@33431: assume ?R thus ?L by(metis le_list_append_mono order_refl)
nipkow@33431: qed
nipkow@33431:
nipkow@33431: lemma less_list_rev_take: "xs @ zs < ys @ zs \ xs < ys"
nipkow@33431: by (unfold less_le) auto
nipkow@33431:
nipkow@33431: lemma le_list_rev_drop_many: "xs \ ys \ xs \ ys @ zs"
nipkow@33431: by (metis append_Nil2 empty le_list_append_mono)
haftmann@26735:
haftmann@26735:
haftmann@26735: subsection {* Relation to standard list operations *}
haftmann@26735:
nipkow@33431: lemma le_list_map: "xs \ ys \ map f xs \ map f ys"
nipkow@33431: by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
nipkow@33431:
nipkow@33431: lemma le_list_filter_left[simp]: "filter f xs \ xs"
nipkow@33431: by (induct xs) (auto intro: less_eq_list.drop)
nipkow@33431:
nipkow@33431: lemma le_list_filter: "xs \ ys \ filter f xs \ filter f ys"
nipkow@33431: by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
nipkow@33431:
nipkow@33431:
nipkow@33431: lemma "xs <= ys \ (EX N. xs = sublist ys N)" (is "?L = ?R")
nipkow@33431: proof
nipkow@33431: assume ?L
nipkow@33431: thus ?R
nipkow@33431: proof induct
nipkow@33431: case empty show ?case by (metis sublist_empty)
nipkow@33431: next
nipkow@33431: case (drop xs ys x)
nipkow@33431: then obtain N where "xs = sublist ys N" by blast
nipkow@33431: hence "xs = sublist (x#ys) (Suc ` N)"
nipkow@33431: by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
nipkow@33431: thus ?case by blast
nipkow@33431: next
nipkow@33431: case (take xs ys x)
nipkow@33431: then obtain N where "xs = sublist ys N" by blast
nipkow@33431: hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
nipkow@33431: by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
nipkow@33431: thus ?case by blast
nipkow@33431: qed
nipkow@33431: next
nipkow@33431: assume ?R
nipkow@33431: then obtain N where "xs = sublist ys N" ..
nipkow@33431: moreover have "sublist ys N <= ys"
nipkow@33431: proof (induct ys arbitrary:N)
nipkow@33431: case Nil show ?case by simp
nipkow@33431: next
nipkow@33431: case Cons thus ?case by (auto simp add:sublist_Cons drop)
nipkow@33431: qed
nipkow@33431: ultimately show ?L by simp
nipkow@33431: qed
haftmann@26735:
haftmann@26735: end