Theory Subseq_Order

(*  Title:      HOL/Library/Subseq_Order.thy
    Author:     Peter Lammich, Uni Muenster <>
    Author:     Florian Haftmann, TU Muenchen
    Author:     Tobias Nipkow, TU Muenchen

section ‹Subsequence Ordering›

theory Subseq_Order
imports Sublist

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

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


instance list :: (type) order
  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)

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