haftmann@26735: (* Title: HOL/Library/Sublist_Order.thy haftmann@26735: Authors: Peter Lammich, Uni Muenster haftmann@30738: Florian Haftmann, 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: haftmann@26735: instantiation list :: (type) order 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: lemmas ileq_empty = empty haftmann@26735: lemmas ileq_drop = drop haftmann@26735: lemmas ileq_take = take haftmann@26735: haftmann@26735: lemma ileq_cases [cases set, case_names empty drop take]: haftmann@26735: assumes "xs \ ys" haftmann@26735: and "xs = [] \ P" haftmann@26735: and "\z zs. ys = z # zs \ xs \ zs \ P" haftmann@26735: and "\x zs ws. xs = x # zs \ ys = x # ws \ zs \ ws \ P" haftmann@26735: shows P haftmann@26735: using assms by (blast elim: less_eq_list.cases) haftmann@26735: haftmann@26735: lemma ileq_induct [induct set, case_names empty drop take]: haftmann@26735: assumes "xs \ ys" haftmann@26735: and "\zs. P [] zs" haftmann@26735: and "\z zs ws. ws \ zs \ P ws zs \ P ws (z # zs)" haftmann@26735: and "\z zs ws. ws \ zs \ P ws zs \ P (z # ws) (z # zs)" haftmann@26735: shows "P xs ys" haftmann@26735: using assms by (induct rule: less_eq_list.induct) blast+ haftmann@26735: haftmann@26735: definition haftmann@28562: [code del]: "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" haftmann@26735: haftmann@26735: lemma ileq_length: "xs \ ys \ length xs \ length ys" haftmann@26735: by (induct rule: ileq_induct) auto haftmann@26735: lemma ileq_below_empty [simp]: "xs \ [] \ xs = []" haftmann@26735: by (auto dest: ileq_length) 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" haftmann@26735: show "xs \ xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take) haftmann@26735: next haftmann@26735: fix xs ys :: "'a list" haftmann@26735: (* TODO: Is there a simpler proof ? *) haftmann@26735: { fix n haftmann@26735: have "!!l l'. \l\l'; l'\l; n=length l + length l'\ \ l=l'" haftmann@26735: proof (induct n rule: nat_less_induct) haftmann@26735: case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases) haftmann@26735: case empty with "1.prems"(2) show ?thesis by auto haftmann@26735: next haftmann@26735: case (drop a l2') with "1.prems"(2) have "length l'\length l" "length l \ length l2'" "1+length l2' = length l'" by (auto dest: ileq_length) haftmann@26735: hence False by simp thus ?thesis .. haftmann@26735: next haftmann@26735: case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp haftmann@26735: from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length) haftmann@26735: from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take']) haftmann@26735: case empty' with take LEN show ?thesis by simp haftmann@26735: next haftmann@26735: case (drop' ah l2h) with take LEN have "length l1' \ length l2h" "1+length l2h = length l2'" "length l2' = length l1'" by (auto dest: ileq_length) haftmann@26735: hence False by simp thus ?thesis .. haftmann@26735: next haftmann@26735: case (take' ah l1h l2h) haftmann@26735: with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \ l2'" "l2' \ l1'" by auto haftmann@26735: with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast haftmann@26735: with take 2 show ?thesis by simp haftmann@26735: qed haftmann@26735: qed haftmann@26735: qed haftmann@26735: } haftmann@26735: moreover assume "xs \ ys" "ys \ xs" haftmann@26735: ultimately show "xs = ys" by blast haftmann@26735: next haftmann@26735: fix xs ys zs :: "'a list" haftmann@26735: { haftmann@26735: fix n haftmann@26735: have "!!x y z. \x \ y; y \ z; n=length x + length y + length z\ \ x \ z" haftmann@26735: proof (induct rule: nat_less_induct[case_names I]) haftmann@26735: case (I n x y z) haftmann@26735: from I.prems(2) show ?case proof (cases rule: ileq_cases) haftmann@26735: case empty with I.prems(1) show ?thesis by auto haftmann@26735: next haftmann@26735: case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp haftmann@26735: with I.hyps I.prems(3,1) drop(2) have "x\z'" by blast haftmann@26735: with drop(1) show ?thesis by (auto intro: ileq_drop) haftmann@26735: next haftmann@26735: case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take']) haftmann@26735: case empty' thus ?thesis by auto haftmann@26735: next haftmann@26735: case (drop' ah y'h) with take have "x\y'" "y'\z'" "length x + length y' + length z' < length x + length y + length z" by auto haftmann@26735: with I.hyps I.prems(3) have "x\z'" by (blast) haftmann@26735: with take(2) show ?thesis by (auto intro: ileq_drop) haftmann@26735: next haftmann@26735: case (take' ah x' y'h) with take have 2: "x=a#x'" "x'\y'" "y'\z'" "length x' + length y' + length z' < length x + length y + length z" by auto haftmann@26735: with I.hyps I.prems(3) have "x'\z'" by blast haftmann@26735: with 2 take(2) show ?thesis by (auto intro: ileq_take) haftmann@26735: qed haftmann@26735: qed haftmann@26735: qed haftmann@26735: } haftmann@26735: moreover assume "xs \ ys" "ys \ zs" haftmann@26735: ultimately show "xs \ zs" by blast haftmann@26735: qed haftmann@26735: haftmann@26735: end haftmann@26735: haftmann@26735: lemmas ileq_intros = ileq_empty ileq_drop ileq_take haftmann@26735: haftmann@26735: lemma ileq_drop_many: "xs \ ys \ xs \ zs @ ys" haftmann@26735: by (induct zs) (auto intro: ileq_drop) haftmann@26735: lemma ileq_take_many: "xs \ ys \ zs @ xs \ zs @ ys" haftmann@26735: by (induct zs) (auto intro: ileq_take) haftmann@26735: haftmann@26735: lemma ileq_same_length: "xs \ ys \ length xs = length ys \ xs = ys" haftmann@26735: by (induct rule: ileq_induct) (auto dest: ileq_length) haftmann@26735: lemma ileq_same_append [simp]: "x # xs \ xs \ False" haftmann@26735: by (auto dest: ileq_length) haftmann@26735: haftmann@26735: lemma ilt_length [intro]: haftmann@26735: assumes "xs < ys" haftmann@26735: shows "length xs < length ys" haftmann@26735: proof - haftmann@27682: from assms have "xs \ ys" and "xs \ ys" by (simp_all add: less_le) haftmann@26735: moreover with ileq_length have "length xs \ length ys" by auto haftmann@26735: ultimately show ?thesis by (auto intro: ileq_same_length) haftmann@26735: qed haftmann@26735: haftmann@26735: lemma ilt_empty [simp]: "[] < xs \ xs \ []" haftmann@26735: by (unfold less_list_def, auto) haftmann@26735: lemma ilt_emptyI: "xs \ [] \ [] < xs" haftmann@26735: by (unfold less_list_def, auto) haftmann@26735: lemma ilt_emptyD: "[] < xs \ xs \ []" haftmann@26735: by (unfold less_list_def, auto) haftmann@26735: lemma ilt_below_empty[simp]: "xs < [] \ False" haftmann@26735: by (auto dest: ilt_length) haftmann@26735: lemma ilt_drop: "xs < ys \ xs < x # ys" haftmann@27682: by (unfold less_le) (auto intro: ileq_intros) haftmann@26735: lemma ilt_take: "xs < ys \ x # xs < x # ys" haftmann@27682: by (unfold less_le) (auto intro: ileq_intros) haftmann@26735: lemma ilt_drop_many: "xs < ys \ xs < zs @ ys" haftmann@26735: by (induct zs) (auto intro: ilt_drop) haftmann@26735: lemma ilt_take_many: "xs < ys \ zs @ xs < zs @ ys" haftmann@26735: by (induct zs) (auto intro: ilt_take) haftmann@26735: haftmann@26735: haftmann@26735: subsection {* Appending elements *} haftmann@26735: haftmann@26735: lemma ileq_rev_take: "xs \ ys \ xs @ [x] \ ys @ [x]" haftmann@26735: by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many) haftmann@26735: lemma ilt_rev_take: "xs < ys \ xs @ [x] < ys @ [x]" haftmann@27682: by (unfold less_le) (auto dest: ileq_rev_take) haftmann@26735: lemma ileq_rev_drop: "xs \ ys \ xs \ ys @ [x]" haftmann@26735: by (induct rule: ileq_induct) (auto intro: ileq_intros) haftmann@26735: lemma ileq_rev_drop_many: "xs \ ys \ xs \ ys @ zs" haftmann@26735: by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop) haftmann@26735: haftmann@26735: haftmann@26735: subsection {* Relation to standard list operations *} haftmann@26735: haftmann@26735: lemma ileq_map: "xs \ ys \ map f xs \ map f ys" haftmann@26735: by (induct rule: ileq_induct) (auto intro: ileq_intros) haftmann@26735: lemma ileq_filter_left[simp]: "filter f xs \ xs" haftmann@26735: by (induct xs) (auto intro: ileq_intros) haftmann@26735: lemma ileq_filter: "xs \ ys \ filter f xs \ filter f ys" haftmann@26735: by (induct rule: ileq_induct) (auto intro: ileq_intros) haftmann@26735: haftmann@26735: end