src/HOL/Library/Subseq_Order.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 67399 eab6ce8368fa
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Subseq_Order.thy
     2     Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     3     Author:     Florian Haftmann, TU Muenchen
     4     Author:     Tobias Nipkow, TU Muenchen
     5 *)
     6 
     7 section \<open>Subsequence Ordering\<close>
     8 
     9 theory Subseq_Order
    10 imports Sublist
    11 begin
    12 
    13 text \<open>
    14   This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a
    15   list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
    16 \<close>
    17 
    18 subsection \<open>Definitions and basic lemmas\<close>
    19 
    20 instantiation list :: (type) ord
    21 begin
    22 
    23 definition "xs \<le> ys \<longleftrightarrow> subseq xs ys" for xs ys :: "'a list"
    24 definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
    25 
    26 instance ..
    27 
    28 end
    29 
    30 instance list :: (type) order
    31 proof
    32   fix xs ys zs :: "'a list"
    33   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    34     unfolding less_list_def ..
    35   show "xs \<le> xs"
    36     by (simp add: less_eq_list_def)
    37   show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
    38     using that unfolding less_eq_list_def by (rule subseq_order.antisym)
    39   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
    40     using that unfolding less_eq_list_def by (rule subseq_order.order_trans)
    41 qed
    42 
    43 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
    44   list_emb.induct [of "(=)", folded less_eq_list_def]
    45 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def]
    46 lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
    47 lemmas le_list_map = subseq_map [folded less_eq_list_def]
    48 lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
    49 lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]
    50 
    51 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    52   by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    53 
    54 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    55   by (metis less_eq_list_def list_emb_Nil order_less_le)
    56 
    57 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    58   by (metis list_emb_Nil less_eq_list_def less_list_def)
    59 
    60 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    61   by (unfold less_le less_eq_list_def) (auto)
    62 
    63 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
    64   by (metis subseq_Cons2_iff less_list_def less_eq_list_def)
    65 
    66 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    67   by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
    68       self_append_conv2 less_eq_list_def)
    69 
    70 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
    71   by (metis less_list_def less_eq_list_def subseq_append')
    72 
    73 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
    74   by (unfold less_le less_eq_list_def) auto
    75 
    76 end