# HG changeset patch # User Christian Sternagel # Date 1346225135 -32400 # Node ID 4eef5c2ff5add42894e1c4c88e631579d7600239 # Parent e3973567ed4f6215dc1c807ea6e0602c7cb49417 introduced "sub" as abbreviation for "emb (op =)"; Sublist_Order is now based on Sublist.sub; simplified and moved most lemmas on sub from Sublist_Order to Sublist; Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order diff -r e3973567ed4f -r 4eef5c2ff5ad src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Wed Aug 29 12:24:26 2012 +0900 +++ b/src/HOL/Library/Sublist.thy Wed Aug 29 16:25:35 2012 +0900 @@ -433,6 +433,17 @@ assumes "emb P xs []" shows "xs = []" using assms by (cases rule: emb.cases) auto +lemma emb_Cons_Nil [simp]: + "emb P (x#xs) [] = False" +proof - + { assume "emb P (x#xs) []" + from emb_Nil2 [OF this] have False by simp + } moreover { + assume False + hence "emb P (x#xs) []" by simp + } ultimately show ?thesis by blast +qed + lemma emb_append2 [intro]: "emb P xs ys \ emb P xs (zs @ ys)" by (induct zs) auto @@ -479,4 +490,202 @@ lemma emb_length: "emb P xs ys \ length xs \ length ys" by (induct rule: emb.induct) auto +(*FIXME: move*) +definition transp_on :: "('a \ 'a \ bool) \ 'a set \ bool" where + "transp_on P A \ \a\A. \b\A. \c\A. P a b \ P b c \ P a c" +lemma transp_onI [Pure.intro]: + "(\a b c. \a \ A; b \ A; c \ A; P a b; P b c\ \ P a c) \ transp_on P A" + unfolding transp_on_def by blast + +lemma transp_on_emb: + assumes "transp_on P A" + shows "transp_on (emb P) (lists A)" +proof + fix xs ys zs + assume "emb P xs ys" and "emb P ys zs" + and "xs \ lists A" and "ys \ lists A" and "zs \ lists A" + thus "emb P xs zs" + proof (induction arbitrary: zs) + case emb_Nil show ?case by blast + next + case (emb_Cons xs ys y) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + hence "emb P ys (v#vs)" by blast + hence "emb P ys zs" unfolding zs by (rule emb_append2) + from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp + next + case (emb_Cons2 x y xs ys) + from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs + where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast + with emb_Cons2 have "emb P xs vs" by simp + moreover have "P x v" + proof - + from zs and `zs \ lists A` have "v \ A" by auto + moreover have "x \ A" and "y \ A" using emb_Cons2 by simp_all + ultimately show ?thesis using `P x y` and `P y v` and assms + unfolding transp_on_def by blast + qed + ultimately have "emb P (x#xs) (v#vs)" by blast + thus ?case unfolding zs by (rule emb_append2) + qed +qed + + +subsection {* Sublists (special case of embedding) *} + +abbreviation sub :: "'a list \ 'a list \ bool" where + "sub xs ys \ emb (op =) xs ys" + +lemma sub_Cons2: "sub xs ys \ sub (x#xs) (x#ys)" by auto + +lemma sub_same_length: + assumes "sub xs ys" and "length xs = length ys" shows "xs = ys" + using assms by (induct) (auto dest: emb_length) + +lemma not_sub_length [simp]: "length ys < length xs \ \ sub xs ys" + by (metis emb_length linorder_not_less) + +lemma [code]: + "emb P [] ys \ True" + "emb P (x#xs) [] \ False" + by (simp_all) + +lemma sub_Cons': "sub (x#xs) ys \ sub xs ys" + by (induct xs) (auto dest: emb_ConsD) + +lemma sub_Cons2': + assumes "sub (x#xs) (x#ys)" shows "sub xs ys" + using assms by (cases) (rule sub_Cons') + +lemma sub_Cons2_neq: + assumes "sub (x#xs) (y#ys)" + shows "x \ y \ sub (x#xs) ys" + using assms by (cases) auto + +lemma sub_Cons2_iff [simp, code]: + "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)" + by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq) + +lemma sub_append': "sub (zs @ xs) (zs @ ys) \ sub xs ys" + by (induct zs) simp_all + +lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all + +lemma sub_antisym: + assumes "sub xs ys" and "sub ys xs" + shows "xs = ys" +using assms +proof (induct) + case emb_Nil + from emb_Nil2 [OF this] show ?case by simp +next + case emb_Cons2 thus ?case by simp +next + case emb_Cons thus ?case + by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n) +qed + +lemma transp_on_sub: "transp_on sub UNIV" +proof - + have "transp_on (op =) UNIV" by (simp add: transp_on_def) + from transp_on_emb [OF this] show ?thesis by simp +qed + +lemma sub_trans: "sub xs ys \ sub ys zs \ sub xs zs" + using transp_on_sub [unfolded transp_on_def] by blast + +lemma sub_append_le_same_iff: "sub (xs @ ys) ys \ xs = []" + by (auto dest: emb_length) + +lemma emb_append_mono: + "\ emb P xs xs'; emb P ys ys' \ \ emb P (xs@ys) (xs'@ys')" +apply (induct rule: emb.induct) + apply (metis eq_Nil_appendI emb_append2) + apply (metis append_Cons emb_Cons) +by (metis append_Cons emb_Cons2) + + +subsection {* Appending elements *} + +lemma sub_append [simp]: + "sub (xs @ zs) (ys @ zs) \ sub xs ys" (is "?l = ?r") +proof + { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'" + hence "xs' = xs @ zs & ys' = ys @ zs \ sub xs ys" + proof (induct arbitrary: xs ys zs) + case emb_Nil show ?case by simp + next + case (emb_Cons xs' ys' x) + { assume "ys=[]" hence ?case using emb_Cons(1) by auto } + moreover + { fix us assume "ys = x#us" + hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) } + ultimately show ?case by (auto simp:Cons_eq_append_conv) + next + case (emb_Cons2 x y xs' ys') + { assume "xs=[]" hence ?case using emb_Cons2(1) by auto } + moreover + { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto} + moreover + { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp } + ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv) + qed } + moreover assume ?l + ultimately show ?r by blast +next + assume ?r thus ?l by (metis emb_append_mono sub_refl) +qed + +lemma sub_drop_many: "sub xs ys \ sub xs (zs @ ys)" + by (induct zs) auto + +lemma sub_rev_drop_many: "sub xs ys \ sub xs (ys @ zs)" + by (metis append_Nil2 emb_Nil emb_append_mono) + + +subsection {* Relation to standard list operations *} + +lemma sub_map: + assumes "sub xs ys" shows "sub (map f xs) (map f ys)" + using assms by (induct) auto + +lemma sub_filter_left [simp]: "sub (filter P xs) xs" + by (induct xs) auto + +lemma sub_filter [simp]: + assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)" + using assms by (induct) auto + +lemma "sub xs ys \ (\ N. xs = sublist ys N)" (is "?L = ?R") +proof + assume ?L + thus ?R + proof (induct) + case emb_Nil show ?case by (metis sublist_empty) + next + case (emb_Cons 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 (emb_Cons2 x y xs ys) + 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 unfolding `x = y` by blast + qed +next + assume ?R + then obtain N where "xs = sublist ys N" .. + moreover have "sub (sublist ys N) ys" + proof (induct ys arbitrary:N) + case Nil show ?case by simp + next + case Cons thus ?case by (auto simp: sublist_Cons) + qed + ultimately show ?L by simp +qed + end diff -r e3973567ed4f -r 4eef5c2ff5ad src/HOL/Library/Sublist_Order.thy --- a/src/HOL/Library/Sublist_Order.thy Wed Aug 29 12:24:26 2012 +0900 +++ b/src/HOL/Library/Sublist_Order.thy Wed Aug 29 16:25:35 2012 +0900 @@ -6,7 +6,9 @@ header {* Sublist Ordering *} theory Sublist_Order -imports Main Sublist +imports + Main + Sublist begin text {* @@ -21,256 +23,54 @@ begin definition - "(xs :: 'a list) \ ys \ emb (op =) xs ys" + "(xs :: 'a list) \ ys \ sub xs ys" definition "(xs :: 'a list) < ys \ xs \ ys \ \ ys \ xs" -instance proof qed +instance .. end -lemma empty [simp, intro!]: "[] \ xs" by (auto simp: less_eq_list_def) - -lemma drop: "xs \ ys \ xs \ (y # ys)" - by (unfold less_eq_list_def) blast - -lemma take: "xs \ ys \ (x#xs) \ (x#ys)" - by (unfold less_eq_list_def) blast - -lemmas le_list_induct [consumes 1, case_names empty drop take] = - emb.induct [of "op =", folded less_eq_list_def] - -lemmas le_list_cases [consumes 1, case_names empty drop take] = - emb.cases [of "op =", folded less_eq_list_def] - -lemma le_list_length: "xs \ ys \ length xs \ length ys" - by (induct rule: le_list_induct) auto - -lemma le_list_same_length: "xs \ ys \ length xs = length ys \ xs = ys" - by (induct rule: le_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 simp: less_eq_list_def) - -lemma [code]: "[] <= xs \ True" -by (simp add: less_eq_list_def) - -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 rule: le_list_induct) - case empty thus ?case by simp - next - note drop' = drop - case drop thus ?case by (metis drop') - next - note t = take - 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 rule: le_list_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 by (cases rule: le_list_cases) 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 rule: le_list_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 +instance list :: (type) order +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!: drop) + show "xs \ xs" by (simp add: less_eq_list_def) next fix xs ys :: "'a list" - assume "xs <= ys" - hence "ys <= xs \ xs = ys" - proof (induct rule: le_list_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 + assume "xs <= ys" and "ys <= xs" + thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym) next fix xs ys zs :: "'a list" - assume "xs <= ys" - hence "ys <= zs \ xs <= zs" - proof (induct arbitrary:zs rule: le_list_induct) - case empty show ?case by simp - next - note take' = take - case (take x y xs ys) show ?case - proof - assume "y # ys <= zs" - with take show "x # xs <= zs" - by(metis le_list_Cons_EX le_list_drop_many take') - qed - next - case drop thus ?case by (metis le_list_drop_Cons) - qed - moreover assume "ys <= zs" - ultimately show "xs <= zs" by blast + assume "xs <= ys" and "ys <= zs" + thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans) qed -end - -lemma le_list_append_le_same_iff: "xs @ ys <= ys \ xs=[]" -by (auto dest: le_list_length) - -lemma le_list_append_mono: "\ xs <= xs'; ys <= ys' \ \ xs@ys <= xs'@ys'" -apply (induct rule: le_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 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) + by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def) lemma less_list_empty [simp]: "[] < xs \ xs \ []" -by (metis empty order_less_le) + by (metis less_eq_list_def emb_Nil order_less_le) -lemma less_list_below_empty[simp]: "xs < [] \ False" -by (metis empty less_list_def) +lemma less_list_below_empty [simp]: "xs < [] \ False" + by (metis emb_Nil less_eq_list_def less_list_def) lemma less_list_drop: "xs < ys \ xs < x # ys" -by (unfold less_le) (auto intro: drop) + by (unfold less_le less_eq_list_def) (auto) lemma less_list_take_iff: "x # xs < x # ys \ xs < ys" -by (metis le_list_Cons2_iff less_list_def) + by (metis sub_Cons2_iff less_list_def less_eq_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) + by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def) 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 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 rule: le_list_induct) - case empty show ?case by simp - next - note drop' = drop - 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: drop') } - ultimately show ?case by (auto simp:Cons_eq_append_conv) - next - case (take x y xs' ys') - { assume "xs=[]" hence ?case using take(1) by auto } - moreover - { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto} - moreover - { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp } - ultimately show ?case using `x = y` 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 + by (metis less_list_def less_eq_list_def sub_append') 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 le_list_map: "xs \ ys \ map f xs \ map f ys" -by (induct rule: le_list_induct) (auto intro: drop) - -lemma le_list_filter_left[simp]: "filter f xs \ xs" -by (induct xs) (auto intro: drop) - -lemma le_list_filter: "xs \ ys \ filter f xs \ filter f ys" -by (induct rule: le_list_induct) (auto intro: drop) - -lemma "xs \ ys \ (EX N. xs = sublist ys N)" (is "?L = ?R") -proof - assume ?L - thus ?R - proof (induct rule: le_list_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 x y xs ys) - 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 unfolding `x = y` 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 + by (unfold less_le less_eq_list_def) auto end