src/HOL/Library/Sublist_Order.thy
author nipkow
Wed, 04 Nov 2009 09:18:03 +0100
changeset 33431 af516ed40e72
parent 30738 0842e906300c
child 33499 30e6e070bdb6
permissions -rw-r--r--
Completely overhauled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Sublist_Order.thy
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     2
    Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
     3
                Florian Haftmann, Tobias Nipkow, TU Muenchen
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     4
*)
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     5
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     6
header {* Sublist Ordering *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     7
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
     8
theory Sublist_Order
30738
0842e906300c normalized imports
haftmann
parents: 28562
diff changeset
     9
imports Main
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    10
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    11
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    12
text {*
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    13
  This theory defines sublist ordering on lists.
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    14
  A list @{text ys} is a sublist of a list @{text xs},
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    15
  iff one obtains @{text ys} by erasing some elements from @{text xs}.
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    16
*}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    17
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    18
subsection {* Definitions and basic lemmas *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    19
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    20
instantiation list :: (type) ord
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    21
begin
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    22
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    23
inductive less_eq_list where
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    24
  empty [simp, intro!]: "[] \<le> xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    25
  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    26
  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    27
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    28
definition
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 27682
diff changeset
    29
  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
    30
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    31
instance proof qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    32
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    33
end
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    34
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    35
lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    36
by (induct rule: less_eq_list.induct) auto
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    37
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    38
lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    39
by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    40
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    41
lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    42
by (metis le_list_length linorder_not_less)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    43
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    44
lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    45
by (auto dest: le_list_length)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    46
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    47
lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    48
by (induct zs) (auto intro: drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    49
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    50
lemma [code]: "[] <= xs \<longleftrightarrow> True"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    51
by(metis less_eq_list.empty)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    52
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    53
lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    54
by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    55
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    56
lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    57
proof-
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    58
  { fix xs' ys'
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    59
    assume "xs' <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    60
    hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    61
    proof induct
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    62
      case empty thus ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    63
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    64
      case drop thus ?case by (metis less_eq_list.drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    65
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    66
      case take thus ?case by (simp add: drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    67
    qed }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    68
  from this[OF assms] show ?thesis by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    69
qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    70
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    71
lemma le_list_drop_Cons2:
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    72
assumes "x#xs <= x#ys" shows "xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    73
using assms
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    74
proof cases
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    75
  case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    76
qed simp_all
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    77
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    78
lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    79
shows "x ~= y \<Longrightarrow> x # xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    80
using assms proof cases qed auto
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    81
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    82
lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    83
  (if x=y then xs <= ys else (x#xs) <= ys)"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    84
by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    85
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    86
lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    87
by (induct zs) (auto intro: take)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    88
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    89
lemma le_list_Cons_EX:
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    90
  assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    91
proof-
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    92
  { fix xys zs :: "'a list" assume "xys <= zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    93
    hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    94
    proof induct
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    95
      case empty show ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    96
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    97
      case take thus ?case by (metis list.inject self_append_conv2)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    98
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
    99
      case drop thus ?case by (metis append_eq_Cons_conv)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   100
    qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   101
  } with assms show ?thesis by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   102
qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   103
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   104
instantiation list :: (type) order
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   105
begin
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   106
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   107
instance proof
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   108
  fix xs ys :: "'a list"
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
   109
  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   110
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   111
  fix xs :: "'a list"
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   112
  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   113
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   114
  fix xs ys :: "'a list"
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   115
  assume "xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   116
  hence "ys <= xs \<longrightarrow> xs = ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   117
  proof induct
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   118
    case empty show ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   119
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   120
    case take thus ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   121
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   122
    case drop thus ?case
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   123
      by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   124
  qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   125
  moreover assume "ys <= xs"
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   126
  ultimately show "xs = ys" by blast
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   127
next
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   128
  fix xs ys zs :: "'a list"
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   129
  assume "xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   130
  hence "ys <= zs \<longrightarrow> xs <= zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   131
  proof (induct arbitrary:zs)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   132
    case empty show ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   133
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   134
    case (take xs ys x) show ?case
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   135
    proof
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   136
      assume "x # ys <= zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   137
      with take show "x # xs <= zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   138
        by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   139
    qed
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   140
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   141
    case drop thus ?case by (metis le_list_drop_Cons)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   142
  qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   143
  moreover assume "ys <= zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   144
  ultimately show "xs <= zs" by blast
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   145
qed
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   146
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   147
end
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   148
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   149
lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   150
by (auto dest: le_list_length)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   151
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   152
lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   153
apply (induct rule:less_eq_list.induct)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   154
  apply (metis eq_Nil_appendI le_list_drop_many)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   155
 apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   156
apply simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   157
done
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   158
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   159
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   160
by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   161
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   162
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   163
by (metis empty order_less_le)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   164
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   165
lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   166
by (metis empty less_list_def)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   167
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   168
lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   169
by (unfold less_le) (auto intro: less_eq_list.drop)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   170
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   171
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   172
by (metis le_list_Cons2_iff less_list_def)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   173
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   174
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   175
by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   176
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   177
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   178
by (metis le_list_take_many_iff less_list_def)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   179
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   180
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   181
subsection {* Appending elements *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   182
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   183
lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   184
proof
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   185
  { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   186
    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   187
    proof (induct arbitrary: xs ys zs)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   188
      case empty show ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   189
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   190
      case (drop xs' ys' x)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   191
      { assume "ys=[]" hence ?case using drop(1) by auto }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   192
      moreover
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   193
      { fix us assume "ys = x#us"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   194
        hence ?case using drop(2) by(simp add: less_eq_list.drop) }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   195
      ultimately show ?case by (auto simp:Cons_eq_append_conv)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   196
    next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   197
      case (take xs' ys' x)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   198
      { assume "xs=[]" hence ?case using take(1) by auto }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   199
      moreover
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   200
      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   201
      moreover
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   202
      { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   203
      ultimately show ?case by (auto simp:Cons_eq_append_conv)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   204
    qed }
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   205
  moreover assume ?L
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   206
  ultimately show ?R by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   207
next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   208
  assume ?R thus ?L by(metis le_list_append_mono order_refl)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   209
qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   210
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   211
lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   212
by (unfold less_le) auto
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   213
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   214
lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   215
by (metis append_Nil2 empty le_list_append_mono)
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   216
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   217
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   218
subsection {* Relation to standard list operations *}
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   219
33431
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   220
lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   221
by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   222
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   223
lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   224
by (induct xs) (auto intro: less_eq_list.drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   225
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   226
lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   227
by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   228
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   229
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   230
lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   231
proof
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   232
  assume ?L
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   233
  thus ?R
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   234
  proof induct
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   235
    case empty show ?case by (metis sublist_empty)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   236
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   237
    case (drop xs ys x)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   238
    then obtain N where "xs = sublist ys N" by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   239
    hence "xs = sublist (x#ys) (Suc ` N)"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   240
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   241
    thus ?case by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   242
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   243
    case (take xs ys x)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   244
    then obtain N where "xs = sublist ys N" by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   245
    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   246
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   247
    thus ?case by blast
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   248
  qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   249
next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   250
  assume ?R
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   251
  then obtain N where "xs = sublist ys N" ..
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   252
  moreover have "sublist ys N <= ys"
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   253
  proof (induct ys arbitrary:N)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   254
    case Nil show ?case by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   255
  next
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   256
    case Cons thus ?case by (auto simp add:sublist_Cons drop)
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   257
  qed
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   258
  ultimately show ?L by simp
af516ed40e72 Completely overhauled
nipkow
parents: 30738
diff changeset
   259
qed
26735
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   260
39be3c7e643a added theory Sublist_Order
haftmann
parents:
diff changeset
   261
end