(* 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