# Theory Subseq_Order

```(*  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"
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›

lemma less_eq_list_below_empty [code]:
‹x # xs ≤ [] ⟷ False›

lemma le_list_Cons2_iff [simp, code]:
‹x # xs ≤ y # ys ⟷ (if x = y then xs ≤ ys else x # xs ≤ ys)›

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)›

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
```