src/HOL/Library/Sublist_Order.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 37765 26bdfb7b680b
child 49084 e3973567ed4f
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
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
haftmann@30738
     9
imports Main
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
haftmann@26735
    23
inductive less_eq_list where
haftmann@26735
    24
  empty [simp, intro!]: "[] \<le> xs"
haftmann@26735
    25
  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
haftmann@26735
    26
  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
haftmann@26735
    27
haftmann@26735
    28
definition
haftmann@37765
    29
  "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
haftmann@26735
    30
nipkow@33431
    31
instance proof qed
nipkow@33431
    32
nipkow@33431
    33
end
nipkow@33431
    34
nipkow@33431
    35
lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
nipkow@33431
    36
by (induct rule: less_eq_list.induct) auto
nipkow@33431
    37
nipkow@33431
    38
lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
nipkow@33431
    39
by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
nipkow@33431
    40
nipkow@33431
    41
lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
nipkow@33431
    42
by (metis le_list_length linorder_not_less)
nipkow@33431
    43
nipkow@33431
    44
lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
nipkow@33431
    45
by (auto dest: le_list_length)
nipkow@33431
    46
nipkow@33431
    47
lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
nipkow@33431
    48
by (induct zs) (auto intro: drop)
nipkow@33431
    49
nipkow@33431
    50
lemma [code]: "[] <= xs \<longleftrightarrow> True"
nipkow@33431
    51
by(metis less_eq_list.empty)
nipkow@33431
    52
nipkow@33431
    53
lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
nipkow@33431
    54
by simp
nipkow@33431
    55
nipkow@33431
    56
lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
nipkow@33431
    57
proof-
nipkow@33431
    58
  { fix xs' ys'
nipkow@33431
    59
    assume "xs' <= ys"
nipkow@33431
    60
    hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
nipkow@33431
    61
    proof induct
nipkow@33431
    62
      case empty thus ?case by simp
nipkow@33431
    63
    next
nipkow@33431
    64
      case drop thus ?case by (metis less_eq_list.drop)
nipkow@33431
    65
    next
nipkow@33431
    66
      case take thus ?case by (simp add: drop)
nipkow@33431
    67
    qed }
nipkow@33431
    68
  from this[OF assms] show ?thesis by simp
nipkow@33431
    69
qed
nipkow@33431
    70
nipkow@33431
    71
lemma le_list_drop_Cons2:
nipkow@33431
    72
assumes "x#xs <= x#ys" shows "xs <= ys"
nipkow@33431
    73
using assms
nipkow@33431
    74
proof cases
nipkow@33431
    75
  case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
nipkow@33431
    76
qed simp_all
nipkow@33431
    77
nipkow@33431
    78
lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
nipkow@33431
    79
shows "x ~= y \<Longrightarrow> x # xs <= ys"
nipkow@33431
    80
using assms proof cases qed auto
nipkow@33431
    81
nipkow@33431
    82
lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
nipkow@33431
    83
  (if x=y then xs <= ys else (x#xs) <= ys)"
nipkow@33431
    84
by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
nipkow@33431
    85
nipkow@33431
    86
lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
nipkow@33431
    87
by (induct zs) (auto intro: take)
nipkow@33431
    88
nipkow@33431
    89
lemma le_list_Cons_EX:
nipkow@33431
    90
  assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
nipkow@33431
    91
proof-
nipkow@33431
    92
  { fix xys zs :: "'a list" assume "xys <= zs"
nipkow@33431
    93
    hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
nipkow@33431
    94
    proof induct
nipkow@33431
    95
      case empty show ?case by simp
nipkow@33431
    96
    next
nipkow@33431
    97
      case take thus ?case by (metis list.inject self_append_conv2)
nipkow@33431
    98
    next
nipkow@33431
    99
      case drop thus ?case by (metis append_eq_Cons_conv)
nipkow@33431
   100
    qed
nipkow@33431
   101
  } with assms show ?thesis by blast
nipkow@33431
   102
qed
nipkow@33431
   103
nipkow@33431
   104
instantiation list :: (type) order
nipkow@33431
   105
begin
haftmann@26735
   106
haftmann@26735
   107
instance proof
haftmann@26735
   108
  fix xs ys :: "'a list"
haftmann@27682
   109
  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
haftmann@26735
   110
next
haftmann@26735
   111
  fix xs :: "'a list"
nipkow@33431
   112
  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
haftmann@26735
   113
next
haftmann@26735
   114
  fix xs ys :: "'a list"
nipkow@33431
   115
  assume "xs <= ys"
nipkow@33431
   116
  hence "ys <= xs \<longrightarrow> xs = ys"
nipkow@33431
   117
  proof induct
nipkow@33431
   118
    case empty show ?case by simp
nipkow@33431
   119
  next
nipkow@33431
   120
    case take thus ?case by simp
nipkow@33431
   121
  next
nipkow@33431
   122
    case drop thus ?case
nipkow@33431
   123
      by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
nipkow@33431
   124
  qed
nipkow@33431
   125
  moreover assume "ys <= xs"
haftmann@26735
   126
  ultimately show "xs = ys" by blast
haftmann@26735
   127
next
haftmann@26735
   128
  fix xs ys zs :: "'a list"
nipkow@33431
   129
  assume "xs <= ys"
nipkow@33431
   130
  hence "ys <= zs \<longrightarrow> xs <= zs"
nipkow@33431
   131
  proof (induct arbitrary:zs)
nipkow@33431
   132
    case empty show ?case by simp
nipkow@33431
   133
  next
nipkow@33431
   134
    case (take xs ys x) show ?case
nipkow@33431
   135
    proof
nipkow@33431
   136
      assume "x # ys <= zs"
nipkow@33431
   137
      with take show "x # xs <= zs"
nipkow@33431
   138
        by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
haftmann@26735
   139
    qed
nipkow@33431
   140
  next
nipkow@33431
   141
    case drop thus ?case by (metis le_list_drop_Cons)
nipkow@33431
   142
  qed
nipkow@33431
   143
  moreover assume "ys <= zs"
nipkow@33431
   144
  ultimately show "xs <= zs" by blast
haftmann@26735
   145
qed
haftmann@26735
   146
haftmann@26735
   147
end
haftmann@26735
   148
nipkow@33431
   149
lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
nipkow@33431
   150
by (auto dest: le_list_length)
haftmann@26735
   151
nipkow@33431
   152
lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
nipkow@33431
   153
apply (induct rule:less_eq_list.induct)
nipkow@33431
   154
  apply (metis eq_Nil_appendI le_list_drop_many)
nipkow@33431
   155
 apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
nipkow@33431
   156
apply simp
nipkow@33431
   157
done
haftmann@26735
   158
nipkow@33431
   159
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
nipkow@33431
   160
by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
haftmann@26735
   161
nipkow@33431
   162
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
nipkow@33431
   163
by (metis empty order_less_le)
nipkow@33431
   164
nipkow@33431
   165
lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
nipkow@33431
   166
by (metis empty less_list_def)
nipkow@33431
   167
nipkow@33431
   168
lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
nipkow@33431
   169
by (unfold less_le) (auto intro: less_eq_list.drop)
haftmann@26735
   170
nipkow@33431
   171
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
nipkow@33431
   172
by (metis le_list_Cons2_iff less_list_def)
nipkow@33431
   173
nipkow@33431
   174
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
nipkow@33431
   175
by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
nipkow@33431
   176
nipkow@33431
   177
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
nipkow@33431
   178
by (metis le_list_take_many_iff less_list_def)
haftmann@26735
   179
haftmann@26735
   180
haftmann@26735
   181
subsection {* Appending elements *}
haftmann@26735
   182
nipkow@33431
   183
lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
nipkow@33431
   184
proof
nipkow@33431
   185
  { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
nipkow@33431
   186
    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
nipkow@33431
   187
    proof (induct arbitrary: xs ys zs)
nipkow@33431
   188
      case empty show ?case by simp
nipkow@33431
   189
    next
nipkow@33431
   190
      case (drop xs' ys' x)
nipkow@33431
   191
      { assume "ys=[]" hence ?case using drop(1) by auto }
nipkow@33431
   192
      moreover
nipkow@33431
   193
      { fix us assume "ys = x#us"
nipkow@33431
   194
        hence ?case using drop(2) by(simp add: less_eq_list.drop) }
nipkow@33431
   195
      ultimately show ?case by (auto simp:Cons_eq_append_conv)
nipkow@33431
   196
    next
nipkow@33431
   197
      case (take xs' ys' x)
nipkow@33431
   198
      { assume "xs=[]" hence ?case using take(1) by auto }
nipkow@33431
   199
      moreover
nipkow@33431
   200
      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
nipkow@33431
   201
      moreover
nipkow@33431
   202
      { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
nipkow@33431
   203
      ultimately show ?case by (auto simp:Cons_eq_append_conv)
nipkow@33431
   204
    qed }
nipkow@33431
   205
  moreover assume ?L
nipkow@33431
   206
  ultimately show ?R by blast
nipkow@33431
   207
next
nipkow@33431
   208
  assume ?R thus ?L by(metis le_list_append_mono order_refl)
nipkow@33431
   209
qed
nipkow@33431
   210
nipkow@33431
   211
lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
nipkow@33431
   212
by (unfold less_le) auto
nipkow@33431
   213
nipkow@33431
   214
lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
nipkow@33431
   215
by (metis append_Nil2 empty le_list_append_mono)
haftmann@26735
   216
haftmann@26735
   217
haftmann@26735
   218
subsection {* Relation to standard list operations *}
haftmann@26735
   219
nipkow@33431
   220
lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
nipkow@33431
   221
by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
nipkow@33431
   222
nipkow@33431
   223
lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
nipkow@33431
   224
by (induct xs) (auto intro: less_eq_list.drop)
nipkow@33431
   225
nipkow@33431
   226
lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
nipkow@33431
   227
by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
nipkow@33431
   228
haftmann@33499
   229
lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
nipkow@33431
   230
proof
nipkow@33431
   231
  assume ?L
nipkow@33431
   232
  thus ?R
nipkow@33431
   233
  proof induct
nipkow@33431
   234
    case empty show ?case by (metis sublist_empty)
nipkow@33431
   235
  next
nipkow@33431
   236
    case (drop xs ys x)
nipkow@33431
   237
    then obtain N where "xs = sublist ys N" by blast
nipkow@33431
   238
    hence "xs = sublist (x#ys) (Suc ` N)"
nipkow@33431
   239
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
nipkow@33431
   240
    thus ?case by blast
nipkow@33431
   241
  next
nipkow@33431
   242
    case (take xs ys x)
nipkow@33431
   243
    then obtain N where "xs = sublist ys N" by blast
nipkow@33431
   244
    hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
nipkow@33431
   245
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
nipkow@33431
   246
    thus ?case by blast
nipkow@33431
   247
  qed
nipkow@33431
   248
next
nipkow@33431
   249
  assume ?R
nipkow@33431
   250
  then obtain N where "xs = sublist ys N" ..
nipkow@33431
   251
  moreover have "sublist ys N <= ys"
nipkow@33431
   252
  proof (induct ys arbitrary:N)
nipkow@33431
   253
    case Nil show ?case by simp
nipkow@33431
   254
  next
nipkow@33431
   255
    case Cons thus ?case by (auto simp add:sublist_Cons drop)
nipkow@33431
   256
  qed
nipkow@33431
   257
  ultimately show ?L by simp
nipkow@33431
   258
qed
haftmann@26735
   259
haftmann@26735
   260
end