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