# HG changeset patch # User haftmann # Date 1208846001 -7200 # Node ID 39be3c7e643ab75e7ea5b054dc0777e6989c995c # Parent a92057c1ee217edcc1ae996daccc672c60c23675 added theory Sublist_Order diff -r a92057c1ee21 -r 39be3c7e643a src/HOL/IsaMakefile --- 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 \ diff -r a92057c1ee21 -r 39be3c7e643a src/HOL/Library/Library/ROOT.ML --- 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"]; diff -r a92057c1ee21 -r 39be3c7e643a src/HOL/Library/Sublist_Order.thy --- /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 + 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!]: "[] \ xs" + | 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 func del]: "(xs \ 'a list) < ys \ xs \ ys \ xs \ ys" + +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 + fix xs ys :: "'a list" + show "xs < ys \ xs \ ys \ xs \ ys" unfolding less_list_def .. +next + fix xs :: "'a list" + show "xs \ 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'. \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" + 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 + qed + } + moreover assume "xs \ ys" "ys \ zs" + ultimately show "xs \ zs" by blast +qed + +end + +lemmas ileq_intros = ileq_empty ileq_drop ileq_take + +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 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 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_list_def) + moreover with ileq_length have "length xs \ length ys" by auto + ultimately show ?thesis by (auto intro: ileq_same_length) +qed + +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_list_def) (auto intro: ileq_intros) +lemma ilt_take: "xs < ys \ x # xs < x # ys" + by (unfold less_list_def) (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) + + +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_list_def) (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) + + +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) + +end