# HG changeset patch # User nipkow # Date 1257322726 -3600 # Node ID a9a002f4b71551b0510002f1b51fe112648fe516 # Parent c7dfeb7b0b0e9a9d081db5a15ab795bacfed9fdf# Parent af516ed40e72879c04cf78c0998583e4bf9e8d87 merged diff -r c7dfeb7b0b0e -r a9a002f4b715 src/HOL/Library/Sublist_Order.thy --- a/src/HOL/Library/Sublist_Order.thy Tue Nov 03 19:01:06 2009 -0800 +++ b/src/HOL/Library/Sublist_Order.thy Wed Nov 04 09:18:46 2009 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/Library/Sublist_Order.thy Authors: Peter Lammich, Uni Muenster - Florian Haftmann, TU Muenchen + Florian Haftmann, Tobias Nipkow, TU Muenchen *) header {* Sublist Ordering *} @@ -17,7 +17,7 @@ subsection {* Definitions and basic lemmas *} -instantiation list :: (type) order +instantiation list :: (type) ord begin inductive less_eq_list where @@ -25,162 +25,237 @@ | drop: "ys \ xs \ ys \ x # xs" | take: "ys \ xs \ x # ys \ x # xs" -lemmas ileq_empty = empty -lemmas ileq_drop = drop -lemmas ileq_take = take - -lemma ileq_cases [cases set, case_names empty drop take]: - assumes "xs \ ys" - and "xs = [] \ P" - and "\z zs. ys = z # zs \ xs \ zs \ P" - and "\x zs ws. xs = x # zs \ ys = x # ws \ zs \ ws \ P" - shows P - using assms by (blast elim: less_eq_list.cases) - -lemma ileq_induct [induct set, case_names empty drop take]: - assumes "xs \ ys" - and "\zs. P [] zs" - and "\z zs ws. ws \ zs \ P ws zs \ P ws (z # zs)" - and "\z zs ws. ws \ zs \ P ws zs \ P (z # ws) (z # zs)" - shows "P xs ys" - using assms by (induct rule: less_eq_list.induct) blast+ - definition [code del]: "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" -lemma ileq_length: "xs \ ys \ length xs \ length ys" - by (induct rule: ileq_induct) auto -lemma ileq_below_empty [simp]: "xs \ [] \ xs = []" - by (auto dest: ileq_length) +instance proof qed + +end + +lemma le_list_length: "xs \ ys \ length xs \ length ys" +by (induct rule: less_eq_list.induct) auto + +lemma le_list_same_length: "xs \ ys \ length xs = length ys \ xs = ys" +by (induct rule: less_eq_list.induct) (auto dest: le_list_length) + +lemma not_le_list_length[simp]: "length ys < length xs \ ~ xs <= ys" +by (metis le_list_length linorder_not_less) + +lemma le_list_below_empty [simp]: "xs \ [] \ xs = []" +by (auto dest: le_list_length) + +lemma le_list_drop_many: "xs \ ys \ xs \ zs @ ys" +by (induct zs) (auto intro: drop) + +lemma [code]: "[] <= xs \ True" +by(metis less_eq_list.empty) + +lemma [code]: "(x#xs) <= [] \ False" +by simp + +lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys" +proof- + { fix xs' ys' + assume "xs' <= ys" + hence "ALL x xs. xs' = x#xs \ xs <= ys" + proof induct + case empty thus ?case by simp + next + case drop thus ?case by (metis less_eq_list.drop) + next + case take thus ?case by (simp add: drop) + qed } + from this[OF assms] show ?thesis by simp +qed + +lemma le_list_drop_Cons2: +assumes "x#xs <= x#ys" shows "xs <= ys" +using assms +proof cases + case drop thus ?thesis by (metis le_list_drop_Cons list.inject) +qed simp_all + +lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys" +shows "x ~= y \ x # xs <= ys" +using assms proof cases qed auto + +lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \ + (if x=y then xs <= ys else (x#xs) <= ys)" +by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq) + +lemma le_list_take_many_iff: "zs @ xs \ zs @ ys \ xs \ ys" +by (induct zs) (auto intro: take) + +lemma le_list_Cons_EX: + assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs" +proof- + { fix xys zs :: "'a list" assume "xys <= zs" + hence "ALL x ys. xys = x#ys \ (EX us vs. zs = us @ x # vs & ys <= vs)" + proof induct + case empty show ?case by simp + next + case take thus ?case by (metis list.inject self_append_conv2) + next + case drop thus ?case by (metis append_eq_Cons_conv) + qed + } with assms show ?thesis by blast +qed + +instantiation list :: (type) order +begin instance proof fix xs ys :: "'a list" show "xs < ys \ xs \ ys \ \ ys \ xs" unfolding less_list_def .. next fix xs :: "'a list" - show "xs \ xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take) + show "xs \ xs" by (induct xs) (auto intro!: less_eq_list.drop) next fix xs ys :: "'a list" - (* TODO: Is there a simpler proof ? *) - { fix n - have "!!l l'. \l\l'; l'\l; n=length l + length l'\ \ l=l'" - proof (induct n rule: nat_less_induct) - case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases) - case empty with "1.prems"(2) show ?thesis by auto - next - 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) - hence False by simp thus ?thesis .. - next - case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp - from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length) - from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take']) - case empty' with take LEN show ?thesis by simp - next - 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) - hence False by simp thus ?thesis .. - next - case (take' ah l1h l2h) - with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \ l2'" "l2' \ l1'" by auto - with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast - with take 2 show ?thesis by simp - qed - qed - qed - } - moreover assume "xs \ ys" "ys \ xs" + assume "xs <= ys" + hence "ys <= xs \ xs = ys" + proof induct + case empty show ?case by simp + next + case take thus ?case by simp + next + case drop thus ?case + by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n) + qed + moreover assume "ys <= xs" ultimately show "xs = ys" by blast next fix xs ys zs :: "'a list" - { - fix n - have "!!x y z. \x \ y; y \ z; n=length x + length y + length z\ \ x \ z" - proof (induct rule: nat_less_induct[case_names I]) - case (I n x y z) - from I.prems(2) show ?case proof (cases rule: ileq_cases) - case empty with I.prems(1) show ?thesis by auto - next - case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp - with I.hyps I.prems(3,1) drop(2) have "x\z'" by blast - with drop(1) show ?thesis by (auto intro: ileq_drop) - next - case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take']) - case empty' thus ?thesis by auto - next - 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 - with I.hyps I.prems(3) have "x\z'" by (blast) - with take(2) show ?thesis by (auto intro: ileq_drop) - next - 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 - with I.hyps I.prems(3) have "x'\z'" by blast - with 2 take(2) show ?thesis by (auto intro: ileq_take) - qed - qed + assume "xs <= ys" + hence "ys <= zs \ xs <= zs" + proof (induct arbitrary:zs) + case empty show ?case by simp + next + case (take xs ys x) show ?case + proof + assume "x # ys <= zs" + with take show "x # xs <= zs" + by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2)) qed - } - moreover assume "xs \ ys" "ys \ zs" - ultimately show "xs \ zs" by blast + next + case drop thus ?case by (metis le_list_drop_Cons) + qed + moreover assume "ys <= zs" + ultimately show "xs <= zs" by blast qed end -lemmas ileq_intros = ileq_empty ileq_drop ileq_take +lemma le_list_append_le_same_iff: "xs @ ys <= ys \ xs=[]" +by (auto dest: le_list_length) -lemma ileq_drop_many: "xs \ ys \ xs \ zs @ ys" - by (induct zs) (auto intro: ileq_drop) -lemma ileq_take_many: "xs \ ys \ zs @ xs \ zs @ ys" - by (induct zs) (auto intro: ileq_take) +lemma le_list_append_mono: "\ xs <= xs'; ys <= ys' \ \ xs@ys <= xs'@ys'" +apply (induct rule:less_eq_list.induct) + apply (metis eq_Nil_appendI le_list_drop_many) + apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans) +apply simp +done -lemma ileq_same_length: "xs \ ys \ length xs = length ys \ xs = ys" - by (induct rule: ileq_induct) (auto dest: ileq_length) -lemma ileq_same_append [simp]: "x # xs \ xs \ False" - by (auto dest: ileq_length) +lemma less_list_length: "xs < ys \ length xs < length ys" +by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def) -lemma ilt_length [intro]: - assumes "xs < ys" - shows "length xs < length ys" -proof - - from assms have "xs \ ys" and "xs \ ys" by (simp_all add: less_le) - moreover with ileq_length have "length xs \ length ys" by auto - ultimately show ?thesis by (auto intro: ileq_same_length) -qed +lemma less_list_empty [simp]: "[] < xs \ xs \ []" +by (metis empty order_less_le) + +lemma less_list_below_empty[simp]: "xs < [] \ False" +by (metis empty less_list_def) + +lemma less_list_drop: "xs < ys \ xs < x # ys" +by (unfold less_le) (auto intro: less_eq_list.drop) -lemma ilt_empty [simp]: "[] < xs \ xs \ []" - by (unfold less_list_def, auto) -lemma ilt_emptyI: "xs \ [] \ [] < xs" - by (unfold less_list_def, auto) -lemma ilt_emptyD: "[] < xs \ xs \ []" - by (unfold less_list_def, auto) -lemma ilt_below_empty[simp]: "xs < [] \ False" - by (auto dest: ilt_length) -lemma ilt_drop: "xs < ys \ xs < x # ys" - by (unfold less_le) (auto intro: ileq_intros) -lemma ilt_take: "xs < ys \ x # xs < x # ys" - by (unfold less_le) (auto intro: ileq_intros) -lemma ilt_drop_many: "xs < ys \ xs < zs @ ys" - by (induct zs) (auto intro: ilt_drop) -lemma ilt_take_many: "xs < ys \ zs @ xs < zs @ ys" - by (induct zs) (auto intro: ilt_take) +lemma less_list_take_iff: "x # xs < x # ys \ xs < ys" +by (metis le_list_Cons2_iff less_list_def) + +lemma less_list_drop_many: "xs < ys \ xs < zs @ ys" +by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2) + +lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys" +by (metis le_list_take_many_iff less_list_def) subsection {* Appending elements *} -lemma ileq_rev_take: "xs \ ys \ xs @ [x] \ ys @ [x]" - by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many) -lemma ilt_rev_take: "xs < ys \ xs @ [x] < ys @ [x]" - by (unfold less_le) (auto dest: ileq_rev_take) -lemma ileq_rev_drop: "xs \ ys \ xs \ ys @ [x]" - by (induct rule: ileq_induct) (auto intro: ileq_intros) -lemma ileq_rev_drop_many: "xs \ ys \ xs \ ys @ zs" - by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop) +lemma le_list_rev_take_iff[simp]: "xs @ zs \ ys @ zs \ xs \ ys" (is "?L = ?R") +proof + { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'" + hence "xs' = xs @ zs & ys' = ys @ zs \ xs <= ys" + proof (induct arbitrary: xs ys zs) + case empty show ?case by simp + next + case (drop xs' ys' x) + { assume "ys=[]" hence ?case using drop(1) by auto } + moreover + { fix us assume "ys = x#us" + hence ?case using drop(2) by(simp add: less_eq_list.drop) } + ultimately show ?case by (auto simp:Cons_eq_append_conv) + next + case (take xs' ys' x) + { assume "xs=[]" hence ?case using take(1) by auto } + moreover + { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto} + moreover + { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp } + ultimately show ?case by (auto simp:Cons_eq_append_conv) + qed } + moreover assume ?L + ultimately show ?R by blast +next + assume ?R thus ?L by(metis le_list_append_mono order_refl) +qed + +lemma less_list_rev_take: "xs @ zs < ys @ zs \ xs < ys" +by (unfold less_le) auto + +lemma le_list_rev_drop_many: "xs \ ys \ xs \ ys @ zs" +by (metis append_Nil2 empty le_list_append_mono) subsection {* Relation to standard list operations *} -lemma ileq_map: "xs \ ys \ map f xs \ map f ys" - by (induct rule: ileq_induct) (auto intro: ileq_intros) -lemma ileq_filter_left[simp]: "filter f xs \ xs" - by (induct xs) (auto intro: ileq_intros) -lemma ileq_filter: "xs \ ys \ filter f xs \ filter f ys" - by (induct rule: ileq_induct) (auto intro: ileq_intros) +lemma le_list_map: "xs \ ys \ map f xs \ map f ys" +by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop) + +lemma le_list_filter_left[simp]: "filter f xs \ xs" +by (induct xs) (auto intro: less_eq_list.drop) + +lemma le_list_filter: "xs \ ys \ filter f xs \ filter f ys" +by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop) + + +lemma "xs <= ys \ (EX N. xs = sublist ys N)" (is "?L = ?R") +proof + assume ?L + thus ?R + proof induct + case empty show ?case by (metis sublist_empty) + next + case (drop xs ys x) + then obtain N where "xs = sublist ys N" by blast + hence "xs = sublist (x#ys) (Suc ` N)" + by (clarsimp simp add:sublist_Cons inj_image_mem_iff) + thus ?case by blast + next + case (take xs ys x) + then obtain N where "xs = sublist ys N" by blast + hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))" + by (clarsimp simp add:sublist_Cons inj_image_mem_iff) + thus ?case by blast + qed +next + assume ?R + then obtain N where "xs = sublist ys N" .. + moreover have "sublist ys N <= ys" + proof (induct ys arbitrary:N) + case Nil show ?case by simp + next + case Cons thus ?case by (auto simp add:sublist_Cons drop) + qed + ultimately show ?L by simp +qed end