(* 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 Plain "~~/src/HOL/List"
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 del]: "(xs \ 'a list) < ys \ xs \ ys \ \ ys \ xs"
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 \ \ ys \ xs" 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_le)
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_le) (auto intro: ileq_intros)
lemma ilt_take: "xs < ys \ x # xs < x # ys"
by (unfold less_le) (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_le) (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