(* Title: HOL/Library/Subseq_Order.thy
Author: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
Author: Florian Haftmann, TU Muenchen
Author: Tobias Nipkow, TU Muenchen
*)
section ‹Subsequence Ordering
›
theory Subseq_Order
imports Sublist
begin
text ‹
This
theory defines subsequence ordering on lists. A list
‹ys
› is a subsequence of a
list
‹xs
›, iff one
obtains ‹ys
› by erasing some elements
from ‹xs
›.
›
subsection ‹Definitions
and basic
lemmas›
instantiation list :: (type) ord
begin
definition less_eq_list
where ‹xs
≤ ys
⟷ subseq xs ys
› for xs ys ::
‹'a list\
definition less_list
where ‹xs < ys
⟷ xs
≤ ys
∧ ¬ ys
≤ xs
› for xs ys ::
‹'a list\
instance ..
end
instance list :: (type) order
proof
fix xs ys zs ::
"'a list"
show "xs < ys \ xs \ ys \ \ ys \ xs"
unfolding less_list_def ..
show "xs \ xs"
by (simp add: less_eq_list_def)
show "xs = ys" if "xs \ ys" and "ys \ xs"
using that
unfolding less_eq_list_def
by (rule subseq_order.antisym)
show "xs \ zs" if "xs \ ys" and "ys \ zs"
using that
unfolding less_eq_list_def
by (rule subseq_order.order_trans)
qed
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
list_emb.induct [of
"(=)", folded less_eq_list_def]
lemma less_eq_list_empty [code]:
‹[]
≤ xs
⟷ True
›
by (simp add: less_eq_list_def)
lemma less_eq_list_below_empty [code]:
‹x # xs
≤ []
⟷ False
›
by (simp add: less_eq_list_def)
lemma le_list_Cons2_iff [simp, code]:
‹x # xs
≤ y # ys
⟷ (
if x = y
then xs
≤ ys else x # xs
≤ ys)
›
by (simp add: less_eq_list_def)
lemma less_list_empty [simp]:
‹[] < xs
⟷ xs
≠ []
›
by (metis less_eq_list_def list_emb_Nil order_less_le)
lemma less_list_empty_Cons [code]:
‹[] < x # xs
⟷ True
›
by simp_all
lemma less_list_below_empty [simp, code]:
‹xs < []
⟷ False
›
by (metis list_emb_Nil less_eq_list_def less_list_def)
lemma less_list_Cons2_iff [code]:
‹x # xs < y # ys
⟷ (
if x = y
then xs < ys else x # xs
≤ ys)
›
by (simp add: less_le)
lemmas less_eq_list_drop = list_emb.list_emb_Cons [of
"(=)", folded less_eq_list_def]
lemmas le_list_map = subseq_map [folded less_eq_list_def]
lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
lemmas le_list_length = list_emb_length [of
"(=)", folded less_eq_list_def]
lemma less_list_length:
"xs < ys \ length xs < length ys"
by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq
_list_def)
lemma less_list_drop: "xs < ys \ xs < x # ys"
by (unfold less_le less_eq_list_def) (auto)
lemma less_list_take_iff: "x # xs < x # ys \ xs < ys"
by (metis subseq_Cons2_iff less_list_def less_eq_list_def)
lemma less_list_drop_many: "xs < ys \ xs < zs @ ys"
by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
self_append_conv2 less_eq_list_def)
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys"
by (metis less_list_def less_eq_list_def subseq_append')
lemma less_list_rev_take: "xs @ zs < ys @ zs \ xs < ys"
by (unfold less_le less_eq_list_def) auto
end
