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