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

author | haftmann |

Tue, 22 Apr 2008 08:33:21 +0200 | |

changeset 26735 | 39be3c7e643a |

parent 26734 | a92057c1ee21 |

child 26736 | e6091328718f |

added theory Sublist_Order

--- a/src/HOL/IsaMakefile Tue Apr 22 08:33:20 2008 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 22 08:33:21 2008 +0200 @@ -226,7 +226,7 @@ Library/Library/ROOT.ML Library/Library/document/root.tex \ Library/Library/document/root.bib Library/While_Combinator.thy \ Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \ - Library/Option_ord.thy \ + Library/Option_ord.thy Library/Sublist_Order.thy \ Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Parity.thy Library/GCD.thy Library/Binomial.thy \

--- a/src/HOL/Library/Library/ROOT.ML Tue Apr 22 08:33:20 2008 +0200 +++ b/src/HOL/Library/Library/ROOT.ML Tue Apr 22 08:33:21 2008 +0200 @@ -1,3 +1,3 @@ (* $Id$ *) -use_thys ["Library", "List_Prefix", "List_lexord"]; +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Sublist_Order.thy Tue Apr 22 08:33:21 2008 +0200 @@ -0,0 +1,187 @@ +(* Title: HOL/Library/Sublist_Order.thy + ID: $Id$ + Authors: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> + Florian Haftmann, TU München +*) + +header {* Sublist Ordering *} + +theory Sublist_Order +imports Main +begin + +text {* + This theory defines sublist ordering on lists. + A list @{text ys} is a sublist of a list @{text xs}, + iff one obtains @{text ys} by erasing some elements from @{text xs}. +*} + +subsection {* Definitions and basic lemmas *} + +instantiation list :: (type) order +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" + +lemmas ileq_empty = empty +lemmas ileq_drop = drop +lemmas ileq_take = take + +lemma ileq_cases [cases set, case_names empty drop take]: + assumes "xs \<le> ys" + and "xs = [] \<Longrightarrow> P" + and "\<And>z zs. ys = z # zs \<Longrightarrow> xs \<le> zs \<Longrightarrow> P" + and "\<And>x zs ws. xs = x # zs \<Longrightarrow> ys = x # ws \<Longrightarrow> zs \<le> ws \<Longrightarrow> P" + shows P + using assms by (blast elim: less_eq_list.cases) + +lemma ileq_induct [induct set, case_names empty drop take]: + assumes "xs \<le> ys" + and "\<And>zs. P [] zs" + and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P ws (z # zs)" + and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P (z # ws) (z # zs)" + shows "P xs ys" + using assms by (induct rule: less_eq_list.induct) blast+ + +definition + [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" + +lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys" + by (induct rule: ileq_induct) auto +lemma ileq_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []" + by (auto dest: ileq_length) + +instance proof + fix xs ys :: "'a list" + show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def .. +next + fix xs :: "'a list" + show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take) +next + fix xs ys :: "'a list" + (* TODO: Is there a simpler proof ? *) + { fix n + have "!!l l'. \<lbrakk>l\<le>l'; l'\<le>l; n=length l + length l'\<rbrakk> \<Longrightarrow> 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'\<le>length l" "length l \<le> 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' \<le> 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' \<le> l2'" "l2' \<le> 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 \<le> ys" "ys \<le> xs" + ultimately show "xs = ys" by blast +next + fix xs ys zs :: "'a list" + { + fix n + have "!!x y z. \<lbrakk>x \<le> y; y \<le> z; n=length x + length y + length z\<rbrakk> \<Longrightarrow> x \<le> 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\<le>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\<le>y'" "y'\<le>z'" "length x + length y' + length z' < length x + length y + length z" by auto + with I.hyps I.prems(3) have "x\<le>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'\<le>y'" "y'\<le>z'" "length x' + length y' + length z' < length x + length y + length z" by auto + with I.hyps I.prems(3) have "x'\<le>z'" by blast + with 2 take(2) show ?thesis by (auto intro: ileq_take) + qed + qed + qed + } + moreover assume "xs \<le> ys" "ys \<le> zs" + ultimately show "xs \<le> zs" by blast +qed + +end + +lemmas ileq_intros = ileq_empty ileq_drop ileq_take + +lemma ileq_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys" + by (induct zs) (auto intro: ileq_drop) +lemma ileq_take_many: "xs \<le> ys \<Longrightarrow> zs @ xs \<le> zs @ ys" + by (induct zs) (auto intro: ileq_take) + +lemma ileq_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys" + by (induct rule: ileq_induct) (auto dest: ileq_length) +lemma ileq_same_append [simp]: "x # xs \<le> xs \<longleftrightarrow> False" + by (auto dest: ileq_length) + +lemma ilt_length [intro]: + assumes "xs < ys" + shows "length xs < length ys" +proof - + from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def) + moreover with ileq_length have "length xs \<le> length ys" by auto + ultimately show ?thesis by (auto intro: ileq_same_length) +qed + +lemma ilt_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" + by (unfold less_list_def, auto) +lemma ilt_emptyI: "xs \<noteq> [] \<Longrightarrow> [] < xs" + by (unfold less_list_def, auto) +lemma ilt_emptyD: "[] < xs \<Longrightarrow> xs \<noteq> []" + by (unfold less_list_def, auto) +lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False" + by (auto dest: ilt_length) +lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys" + by (unfold less_list_def) (auto intro: ileq_intros) +lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys" + by (unfold less_list_def) (auto intro: ileq_intros) +lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" + by (induct zs) (auto intro: ilt_drop) +lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys" + by (induct zs) (auto intro: ilt_take) + + +subsection {* Appending elements *} + +lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]" + by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many) +lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]" + by (unfold less_list_def) (auto dest: ileq_rev_take) +lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]" + by (induct rule: ileq_induct) (auto intro: ileq_intros) +lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs" + by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop) + + +subsection {* Relation to standard list operations *} + +lemma ileq_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys" + by (induct rule: ileq_induct) (auto intro: ileq_intros) +lemma ileq_filter_left[simp]: "filter f xs \<le> xs" + by (induct xs) (auto intro: ileq_intros) +lemma ileq_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys" + by (induct rule: ileq_induct) (auto intro: ileq_intros) + +end