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