# HG changeset patch # User Christian Sternagel # Date 1346210666 -32400 # Node ID e3973567ed4f6215dc1c807ea6e0602c7cb49417 # Parent 01081bca31b65268c19a65f60c1690a9f3b503c8 base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation) diff -r 01081bca31b6 -r e3973567ed4f src/HOL/Library/Sublist_Order.thy --- a/src/HOL/Library/Sublist_Order.thy Wed Aug 29 12:23:14 2012 +0900 +++ b/src/HOL/Library/Sublist_Order.thy Wed Aug 29 12:24:26 2012 +0900 @@ -6,7 +6,7 @@ header {* Sublist Ordering *} theory Sublist_Order -imports Main +imports Main Sublist begin text {* @@ -20,23 +20,35 @@ instantiation list :: (type) ord begin -inductive less_eq_list where - empty [simp, intro!]: "[] \ xs" - | drop: "ys \ xs \ ys \ x # xs" - | take: "ys \ xs \ x # ys \ x # xs" +definition + "(xs :: 'a list) \ ys \ emb (op =) xs ys" definition - "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs" + "(xs :: 'a list) < ys \ xs \ ys \ \ ys \ xs" instance proof qed 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: less_eq_list.induct) auto + by (induct rule: le_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) + 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) @@ -45,10 +57,10 @@ by (auto dest: le_list_length) lemma le_list_drop_many: "xs \ ys \ xs \ zs @ ys" -by (induct zs) (auto intro: drop) +by (induct zs) (auto simp: less_eq_list_def) lemma [code]: "[] <= xs \ True" -by(metis less_eq_list.empty) +by (simp add: less_eq_list_def) lemma [code]: "(x#xs) <= [] \ False" by simp @@ -58,11 +70,13 @@ { fix xs' ys' assume "xs' <= ys" hence "ALL x xs. xs' = x#xs \ xs <= ys" - proof induct + proof (induct rule: le_list_induct) case empty thus ?case by simp next - case drop thus ?case by (metis less_eq_list.drop) + 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 @@ -71,13 +85,13 @@ lemma le_list_drop_Cons2: assumes "x#xs <= x#ys" shows "xs <= ys" using assms -proof cases +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 proof cases qed auto +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)" @@ -91,7 +105,7 @@ 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 + proof (induct rule: le_list_induct) case empty show ?case by simp next case take thus ?case by (metis list.inject self_append_conv2) @@ -109,12 +123,12 @@ show "xs < ys \ xs \ ys \ \ ys \ xs" unfolding less_list_def .. next fix xs :: "'a list" - show "xs \ xs" by (induct xs) (auto intro!: less_eq_list.drop) + show "xs \ xs" by (induct xs) (auto intro!: drop) next fix xs ys :: "'a list" assume "xs <= ys" hence "ys <= xs \ xs = ys" - proof induct + proof (induct rule: le_list_induct) case empty show ?case by simp next case take thus ?case by simp @@ -128,14 +142,15 @@ fix xs ys zs :: "'a list" assume "xs <= ys" hence "ys <= zs \ xs <= zs" - proof (induct arbitrary:zs) + proof (induct arbitrary:zs rule: le_list_induct) case empty show ?case by simp next - case (take xs ys x) show ?case + note take' = take + case (take x y xs ys) show ?case proof - assume "x # ys <= zs" + assume "y # 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)) + by(metis le_list_Cons_EX le_list_drop_many take') qed next case drop thus ?case by (metis le_list_drop_Cons) @@ -150,7 +165,7 @@ by (auto dest: le_list_length) lemma le_list_append_mono: "\ xs <= xs'; ys <= ys' \ \ xs@ys <= xs'@ys'" -apply (induct rule:less_eq_list.induct) +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 @@ -166,7 +181,7 @@ 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) +by (unfold less_le) (auto intro: drop) lemma less_list_take_iff: "x # xs < x # ys \ xs < ys" by (metis le_list_Cons2_iff less_list_def) @@ -184,23 +199,24 @@ 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) + 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: less_eq_list.drop) } + hence ?case using drop(2) by(simp add: drop') } ultimately show ?case by (auto simp:Cons_eq_append_conv) next - case (take xs' ys' x) + 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(2) by auto} + { 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 by (auto simp:Cons_eq_append_conv) + ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv) qed } moreover assume ?L ultimately show ?R by blast @@ -218,19 +234,19 @@ subsection {* Relation to standard list operations *} 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) +by (induct rule: le_list_induct) (auto intro: drop) lemma le_list_filter_left[simp]: "filter f xs \ xs" -by (induct xs) (auto intro: less_eq_list.drop) +by (induct xs) (auto intro: 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) +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 + proof (induct rule: le_list_induct) case empty show ?case by (metis sublist_empty) next case (drop xs ys x) @@ -239,11 +255,11 @@ by (clarsimp simp add:sublist_Cons inj_image_mem_iff) thus ?case by blast next - case (take xs ys x) + 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 by blast + thus ?case unfolding `x = y` by blast qed next assume ?R