src/HOL/Library/Sublist_Order.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 50516 ed6b40d15d1c
child 57497 4106a2bc066a
permissions -rw-r--r--
prefer Code.abort over code_abort
     1 (*  Title:      HOL/Library/Sublist_Order.thy
     2     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     3                 Florian Haftmann, Tobias Nipkow, TU Muenchen
     4 *)
     5 
     6 header {* Sublist Ordering *}
     7 
     8 theory Sublist_Order
     9 imports Sublist
    10 begin
    11 
    12 text {*
    13   This theory defines sublist ordering on lists.
    14   A list @{text ys} is a sublist of a list @{text xs},
    15   iff one obtains @{text ys} by erasing some elements from @{text xs}.
    16 *}
    17 
    18 subsection {* Definitions and basic lemmas *}
    19 
    20 instantiation list :: (type) ord
    21 begin
    22 
    23 definition
    24   "(xs :: 'a list) \<le> ys \<longleftrightarrow> sublisteq xs ys"
    25 
    26 definition
    27   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    28 
    29 instance ..
    30 
    31 end
    32 
    33 instance list :: (type) order
    34 proof
    35   fix xs ys :: "'a list"
    36   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
    37 next
    38   fix xs :: "'a list"
    39   show "xs \<le> xs" by (simp add: less_eq_list_def)
    40 next
    41   fix xs ys :: "'a list"
    42   assume "xs <= ys" and "ys <= xs"
    43   thus "xs = ys" by (unfold less_eq_list_def) (rule sublisteq_antisym)
    44 next
    45   fix xs ys zs :: "'a list"
    46   assume "xs <= ys" and "ys <= zs"
    47   thus "xs <= zs" by (unfold less_eq_list_def) (rule sublisteq_trans)
    48 qed
    49 
    50 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
    51   list_hembeq.induct [of "op =", folded less_eq_list_def]
    52 lemmas less_eq_list_drop = list_hembeq.list_hembeq_Cons [of "op =", folded less_eq_list_def]
    53 lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
    54 lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
    55 lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
    56 lemmas le_list_length = list_hembeq_length [of "op =", folded less_eq_list_def]
    57 
    58 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
    59   by (metis list_hembeq_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
    60 
    61 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
    62   by (metis less_eq_list_def list_hembeq_Nil order_less_le)
    63 
    64 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
    65   by (metis list_hembeq_Nil less_eq_list_def less_list_def)
    66 
    67 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    68   by (unfold less_le less_eq_list_def) (auto)
    69 
    70 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
    71   by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
    72 
    73 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    74   by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le self_append_conv2 less_eq_list_def)
    75 
    76 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
    77   by (metis less_list_def less_eq_list_def sublisteq_append')
    78 
    79 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
    80   by (unfold less_le less_eq_list_def) auto
    81 
    82 end