summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Christian Sternagel |

Wed, 29 Aug 2012 12:24:26 +0900 | |

changeset 49084 | e3973567ed4f |

parent 49083 | 01081bca31b6 |

child 49085 | 4eef5c2ff5ad |

base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)

src/HOL/Library/Sublist.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Sublist_Order.thy | file | annotate | diff | comparison | revisions |

--- 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!]: "[] \<le> xs" - | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs" - | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs" +definition + "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys" definition - "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" + "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" instance proof qed end +lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def) + +lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)" + by (unfold less_eq_list_def) blast + +lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (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 \<le> ys \<Longrightarrow> length xs \<le> length ys" -by (induct rule: less_eq_list.induct) auto + by (induct rule: le_list_induct) auto lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> 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 \<Longrightarrow> ~ 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 \<le> ys \<Longrightarrow> xs \<le> zs @ ys" -by (induct zs) (auto intro: drop) +by (induct zs) (auto simp: less_eq_list_def) lemma [code]: "[] <= xs \<longleftrightarrow> True" -by(metis less_eq_list.empty) +by (simp add: less_eq_list_def) lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False" by simp @@ -58,11 +70,13 @@ { fix xs' ys' assume "xs' <= ys" hence "ALL x xs. xs' = x#xs \<longrightarrow> 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 \<Longrightarrow> 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) \<longleftrightarrow> (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 \<longrightarrow> (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 \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. next fix xs :: "'a list" - show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop) + show "xs \<le> xs" by (induct xs) (auto intro!: drop) next fix xs ys :: "'a list" assume "xs <= ys" hence "ys <= xs \<longrightarrow> 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 \<longrightarrow> 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: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<longleftrightarrow> 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 \<longrightarrow> 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 \<le> ys \<Longrightarrow> map f xs \<le> 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 \<le> xs" -by (induct xs) (auto intro: less_eq_list.drop) +by (induct xs) (auto intro: drop) lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> 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 \<le> ys \<longleftrightarrow> (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