src/HOL/List.ML
author nipkow
Thu Apr 24 18:06:46 1997 +0200 (1997-04-24)
changeset 3040 7d48671753da
parent 3011 a3b73ba44a11
child 3196 c522bc46aea7
permissions -rw-r--r--
Introduced a generic "induct_tac" which picks up the right induction scheme
automatically. Also changed nat_ind_tac, which does no longer append a "1" to
the name of the induction variable. This caused some changes...
clasohm@1465
     1
(*  Title:      HOL/List
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow
clasohm@923
     4
    Copyright   1994 TU Muenchen
clasohm@923
     5
clasohm@923
     6
List lemmas
clasohm@923
     7
*)
clasohm@923
     8
nipkow@3011
     9
goal thy "!x. xs ~= x#xs";
nipkow@3040
    10
by (induct_tac "xs" 1);
clasohm@1264
    11
by (ALLGOALS Asm_simp_tac);
nipkow@2608
    12
qed_spec_mp "not_Cons_self";
nipkow@2512
    13
Addsimps [not_Cons_self];
clasohm@923
    14
nipkow@3011
    15
goal thy "(xs ~= []) = (? y ys. xs = y#ys)";
nipkow@3040
    16
by (induct_tac "xs" 1);
clasohm@1264
    17
by (Simp_tac 1);
clasohm@1264
    18
by (Asm_simp_tac 1);
clasohm@923
    19
qed "neq_Nil_conv";
clasohm@923
    20
clasohm@923
    21
nipkow@2608
    22
(** list_case **)
nipkow@2608
    23
nipkow@3011
    24
goal thy
nipkow@2608
    25
 "P(list_case a f xs) = ((xs=[] --> P(a)) & \
paulson@2891
    26
\                        (!y ys. xs=y#ys --> P(f y ys)))";
nipkow@3040
    27
by (induct_tac "xs" 1);
nipkow@2608
    28
by (ALLGOALS Asm_simp_tac);
paulson@2891
    29
by (Blast_tac 1);
nipkow@2608
    30
qed "expand_list_case";
nipkow@2608
    31
nipkow@3011
    32
val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
nipkow@3040
    33
by(induct_tac "xs" 1);
nipkow@2608
    34
by(REPEAT(resolve_tac prems 1));
nipkow@2608
    35
qed "list_cases";
nipkow@2608
    36
nipkow@3011
    37
goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
nipkow@3040
    38
by (induct_tac "xs" 1);
paulson@2891
    39
by (Blast_tac 1);
paulson@2891
    40
by (Blast_tac 1);
nipkow@2608
    41
bind_thm("list_eq_cases",
nipkow@2608
    42
  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
nipkow@2608
    43
nipkow@2608
    44
clasohm@923
    45
(** @ - append **)
clasohm@923
    46
nipkow@3011
    47
goal thy "(xs@ys)@zs = xs@(ys@zs)";
nipkow@3040
    48
by (induct_tac "xs" 1);
clasohm@1264
    49
by (ALLGOALS Asm_simp_tac);
clasohm@923
    50
qed "append_assoc";
nipkow@2512
    51
Addsimps [append_assoc];
clasohm@923
    52
nipkow@3011
    53
goal thy "xs @ [] = xs";
nipkow@3040
    54
by (induct_tac "xs" 1);
clasohm@1264
    55
by (ALLGOALS Asm_simp_tac);
clasohm@923
    56
qed "append_Nil2";
nipkow@2512
    57
Addsimps [append_Nil2];
clasohm@923
    58
nipkow@3011
    59
goal thy "(xs@ys = []) = (xs=[] & ys=[])";
nipkow@3040
    60
by (induct_tac "xs" 1);
clasohm@1264
    61
by (ALLGOALS Asm_simp_tac);
nipkow@2608
    62
qed "append_is_Nil_conv";
nipkow@2608
    63
AddIffs [append_is_Nil_conv];
nipkow@2608
    64
nipkow@3011
    65
goal thy "([] = xs@ys) = (xs=[] & ys=[])";
nipkow@3040
    66
by (induct_tac "xs" 1);
nipkow@2608
    67
by (ALLGOALS Asm_simp_tac);
paulson@2891
    68
by(Blast_tac 1);
nipkow@2608
    69
qed "Nil_is_append_conv";
nipkow@2608
    70
AddIffs [Nil_is_append_conv];
clasohm@923
    71
nipkow@3011
    72
goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
nipkow@3040
    73
by (induct_tac "xs" 1);
clasohm@1264
    74
by (ALLGOALS Asm_simp_tac);
clasohm@923
    75
qed "same_append_eq";
nipkow@2608
    76
AddIffs [same_append_eq];
nipkow@2608
    77
nipkow@3011
    78
goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
nipkow@3040
    79
by(induct_tac "xs" 1);
nipkow@2608
    80
 br allI 1;
nipkow@3040
    81
 by(induct_tac "ys" 1);
nipkow@2608
    82
  by(ALLGOALS Asm_simp_tac);
nipkow@2608
    83
br allI 1;
nipkow@3040
    84
by(induct_tac "ys" 1);
nipkow@2608
    85
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
    86
qed_spec_mp "append1_eq_conv";
nipkow@2608
    87
AddIffs [append1_eq_conv];
nipkow@2608
    88
nipkow@3011
    89
goal thy "xs ~= [] --> hd xs # tl xs = xs";
nipkow@3040
    90
by(induct_tac "xs" 1);
nipkow@2608
    91
by(ALLGOALS Asm_simp_tac);
nipkow@2608
    92
qed_spec_mp "hd_Cons_tl";
nipkow@2608
    93
Addsimps [hd_Cons_tl];
clasohm@923
    94
nipkow@3011
    95
goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
nipkow@3040
    96
by (induct_tac "xs" 1);
nipkow@1327
    97
by (ALLGOALS Asm_simp_tac);
nipkow@1327
    98
qed "hd_append";
clasohm@923
    99
nipkow@3011
   100
goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
nipkow@2608
   101
by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
nipkow@2608
   102
qed "tl_append";
nipkow@2608
   103
nipkow@2608
   104
(** map **)
nipkow@2608
   105
nipkow@3011
   106
goal thy
nipkow@2608
   107
  "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
nipkow@3040
   108
by(induct_tac "xs" 1);
nipkow@2608
   109
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   110
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
nipkow@2608
   111
nipkow@3011
   112
goal thy "map (%x.x) = (%xs.xs)";
nipkow@2608
   113
by (rtac ext 1);
nipkow@3040
   114
by (induct_tac "xs" 1);
nipkow@2608
   115
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   116
qed "map_ident";
nipkow@2608
   117
Addsimps[map_ident];
nipkow@2608
   118
nipkow@3011
   119
goal thy "map f (xs@ys) = map f xs @ map f ys";
nipkow@3040
   120
by (induct_tac "xs" 1);
nipkow@2608
   121
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   122
qed "map_append";
nipkow@2608
   123
Addsimps[map_append];
nipkow@2608
   124
nipkow@3011
   125
goalw thy [o_def] "map (f o g) xs = map f (map g xs)";
nipkow@3040
   126
by (induct_tac "xs" 1);
nipkow@2608
   127
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   128
qed "map_compose";
nipkow@2608
   129
Addsimps[map_compose];
nipkow@2608
   130
nipkow@3011
   131
goal thy "rev(map f xs) = map f (rev xs)";
nipkow@3040
   132
by (induct_tac "xs" 1);
nipkow@2608
   133
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   134
qed "rev_map";
nipkow@2608
   135
lcp@1169
   136
(** rev **)
lcp@1169
   137
nipkow@3011
   138
goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
nipkow@3040
   139
by (induct_tac "xs" 1);
nipkow@2512
   140
by (ALLGOALS Asm_simp_tac);
lcp@1169
   141
qed "rev_append";
nipkow@2512
   142
Addsimps[rev_append];
lcp@1169
   143
nipkow@3011
   144
goal thy "rev(rev l) = l";
nipkow@3040
   145
by (induct_tac "l" 1);
nipkow@2512
   146
by (ALLGOALS Asm_simp_tac);
lcp@1169
   147
qed "rev_rev_ident";
nipkow@2512
   148
Addsimps[rev_rev_ident];
lcp@1169
   149
nipkow@2608
   150
clasohm@923
   151
(** mem **)
clasohm@923
   152
nipkow@3011
   153
goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
nipkow@3040
   154
by (induct_tac "xs" 1);
clasohm@1264
   155
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@923
   156
qed "mem_append";
nipkow@2512
   157
Addsimps[mem_append];
clasohm@923
   158
nipkow@3011
   159
goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
nipkow@3040
   160
by (induct_tac "xs" 1);
clasohm@1264
   161
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@923
   162
qed "mem_filter";
nipkow@2512
   163
Addsimps[mem_filter];
clasohm@923
   164
paulson@1908
   165
(** set_of_list **)
paulson@1812
   166
paulson@1908
   167
goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
nipkow@3040
   168
by (induct_tac "xs" 1);
paulson@1812
   169
by (ALLGOALS Asm_simp_tac);
paulson@2891
   170
by (Blast_tac 1);
paulson@1908
   171
qed "set_of_list_append";
nipkow@2512
   172
Addsimps[set_of_list_append];
paulson@1812
   173
paulson@1908
   174
goal thy "(x mem xs) = (x: set_of_list xs)";
nipkow@3040
   175
by (induct_tac "xs" 1);
paulson@1812
   176
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
paulson@2891
   177
by (Blast_tac 1);
paulson@1908
   178
qed "set_of_list_mem_eq";
paulson@1812
   179
nipkow@3011
   180
goal thy "set_of_list l <= set_of_list (x#l)";
paulson@1936
   181
by (Simp_tac 1);
paulson@2891
   182
by (Blast_tac 1);
paulson@1936
   183
qed "set_of_list_subset_Cons";
paulson@1936
   184
nipkow@3011
   185
goal thy "(set_of_list xs = {}) = (xs = [])";
nipkow@3040
   186
by(induct_tac "xs" 1);
nipkow@2608
   187
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   188
qed "set_of_list_empty";
nipkow@2608
   189
Addsimps [set_of_list_empty];
nipkow@2608
   190
nipkow@3011
   191
goal thy "set_of_list(rev xs) = set_of_list(xs)";
nipkow@3040
   192
by(induct_tac "xs" 1);
nipkow@2608
   193
by(ALLGOALS Asm_simp_tac);
paulson@2891
   194
by(Blast_tac 1);
nipkow@2608
   195
qed "set_of_list_rev";
nipkow@2608
   196
Addsimps [set_of_list_rev];
nipkow@2608
   197
nipkow@3011
   198
goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
nipkow@3040
   199
by(induct_tac "xs" 1);
nipkow@2608
   200
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   201
qed "set_of_list_map";
nipkow@2608
   202
Addsimps [set_of_list_map];
nipkow@2608
   203
paulson@1812
   204
clasohm@923
   205
(** list_all **)
clasohm@923
   206
nipkow@3011
   207
goal thy "list_all (%x.True) xs = True";
nipkow@3040
   208
by (induct_tac "xs" 1);
clasohm@1264
   209
by (ALLGOALS Asm_simp_tac);
clasohm@923
   210
qed "list_all_True";
nipkow@2512
   211
Addsimps [list_all_True];
clasohm@923
   212
nipkow@3011
   213
goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
nipkow@3040
   214
by (induct_tac "xs" 1);
clasohm@1264
   215
by (ALLGOALS Asm_simp_tac);
nipkow@2512
   216
qed "list_all_append";
nipkow@2512
   217
Addsimps [list_all_append];
clasohm@923
   218
nipkow@3011
   219
goal thy "list_all P xs = (!x. x mem xs --> P(x))";
nipkow@3040
   220
by (induct_tac "xs" 1);
clasohm@1264
   221
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
paulson@2891
   222
by (Blast_tac 1);
clasohm@923
   223
qed "list_all_mem_conv";
clasohm@923
   224
clasohm@923
   225
nipkow@2608
   226
(** filter **)
clasohm@923
   227
nipkow@3011
   228
goal thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]";
nipkow@3040
   229
by(induct_tac "xs" 1);
nipkow@2608
   230
 by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
nipkow@2608
   231
qed "filter_append";
nipkow@2608
   232
Addsimps [filter_append];
nipkow@2608
   233
nipkow@2608
   234
nipkow@2608
   235
(** concat **)
nipkow@2608
   236
nipkow@3011
   237
goal thy  "concat(xs@ys) = concat(xs)@concat(ys)";
nipkow@3040
   238
by (induct_tac "xs" 1);
clasohm@1264
   239
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   240
qed"concat_append";
nipkow@2608
   241
Addsimps [concat_append];
nipkow@2512
   242
nipkow@3011
   243
goal thy "rev(concat ls) = concat (map rev (rev ls))";
nipkow@3040
   244
by (induct_tac "ls" 1);
nipkow@2512
   245
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   246
qed "rev_concat";
clasohm@923
   247
nipkow@962
   248
(** length **)
nipkow@962
   249
nipkow@3011
   250
goal thy "length(xs@ys) = length(xs)+length(ys)";
nipkow@3040
   251
by (induct_tac "xs" 1);
clasohm@1264
   252
by (ALLGOALS Asm_simp_tac);
nipkow@962
   253
qed"length_append";
nipkow@1301
   254
Addsimps [length_append];
nipkow@1301
   255
nipkow@3011
   256
goal thy "length (map f l) = length l";
nipkow@3040
   257
by (induct_tac "l" 1);
nipkow@1301
   258
by (ALLGOALS Simp_tac);
nipkow@1301
   259
qed "length_map";
nipkow@1301
   260
Addsimps [length_map];
nipkow@962
   261
nipkow@3011
   262
goal thy "length(rev xs) = length(xs)";
nipkow@3040
   263
by (induct_tac "xs" 1);
nipkow@1301
   264
by (ALLGOALS Asm_simp_tac);
lcp@1169
   265
qed "length_rev";
nipkow@1301
   266
Addsimps [length_rev];
lcp@1169
   267
nipkow@3011
   268
goal thy "(length xs = 0) = (xs = [])";
nipkow@3040
   269
by(induct_tac "xs" 1);
nipkow@2608
   270
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   271
qed "length_0_conv";
nipkow@2608
   272
AddIffs [length_0_conv];
nipkow@2608
   273
nipkow@3011
   274
goal thy "(0 < length xs) = (xs ~= [])";
nipkow@3040
   275
by(induct_tac "xs" 1);
nipkow@2608
   276
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   277
qed "length_greater_0_conv";
nipkow@2608
   278
AddIffs [length_greater_0_conv];
nipkow@2608
   279
nipkow@2608
   280
clasohm@923
   281
(** nth **)
clasohm@923
   282
nipkow@3011
   283
goal thy
nipkow@2608
   284
  "!xs. nth n (xs@ys) = \
nipkow@2608
   285
\          (if n < length xs then nth n xs else nth (n - length xs) ys)";
nipkow@2608
   286
by(nat_ind_tac "n" 1);
nipkow@2608
   287
 by(Asm_simp_tac 1);
nipkow@2608
   288
 br allI 1;
nipkow@2608
   289
 by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   290
  by(ALLGOALS Asm_simp_tac);
nipkow@2608
   291
br allI 1;
nipkow@2608
   292
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   293
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   294
qed_spec_mp "nth_append";
nipkow@2608
   295
nipkow@3011
   296
goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
nipkow@3040
   297
by (induct_tac "xs" 1);
nipkow@1301
   298
(* case [] *)
nipkow@1301
   299
by (Asm_full_simp_tac 1);
nipkow@1301
   300
(* case x#xl *)
nipkow@1301
   301
by (rtac allI 1);
nipkow@1301
   302
by (nat_ind_tac "n" 1);
nipkow@1301
   303
by (ALLGOALS Asm_full_simp_tac);
nipkow@1485
   304
qed_spec_mp "nth_map";
nipkow@1301
   305
Addsimps [nth_map];
nipkow@1301
   306
nipkow@3011
   307
goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
nipkow@3040
   308
by (induct_tac "xs" 1);
nipkow@1301
   309
(* case [] *)
nipkow@1301
   310
by (Simp_tac 1);
nipkow@1301
   311
(* case x#xl *)
nipkow@1301
   312
by (rtac allI 1);
nipkow@1301
   313
by (nat_ind_tac "n" 1);
nipkow@1301
   314
by (ALLGOALS Asm_full_simp_tac);
nipkow@1485
   315
qed_spec_mp "list_all_nth";
nipkow@1301
   316
nipkow@3011
   317
goal thy "!n. n < length xs --> (nth n xs) mem xs";
nipkow@3040
   318
by (induct_tac "xs" 1);
nipkow@1301
   319
(* case [] *)
nipkow@1301
   320
by (Simp_tac 1);
nipkow@1301
   321
(* case x#xl *)
nipkow@1301
   322
by (rtac allI 1);
nipkow@1301
   323
by (nat_ind_tac "n" 1);
nipkow@1301
   324
(* case 0 *)
nipkow@1301
   325
by (Asm_full_simp_tac 1);
nipkow@1301
   326
(* case Suc x *)
nipkow@1301
   327
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1485
   328
qed_spec_mp "nth_mem";
nipkow@1301
   329
Addsimps [nth_mem];
nipkow@1301
   330
nipkow@1327
   331
nipkow@2608
   332
(** take  & drop **)
nipkow@2608
   333
section "take & drop";
nipkow@1327
   334
nipkow@1419
   335
goal thy "take 0 xs = []";
nipkow@3040
   336
by (induct_tac "xs" 1);
nipkow@1419
   337
by (ALLGOALS Asm_simp_tac);
nipkow@1327
   338
qed "take_0";
nipkow@1327
   339
nipkow@2608
   340
goal thy "drop 0 xs = xs";
nipkow@3040
   341
by (induct_tac "xs" 1);
nipkow@2608
   342
by (ALLGOALS Asm_simp_tac);
nipkow@2608
   343
qed "drop_0";
nipkow@2608
   344
nipkow@1419
   345
goal thy "take (Suc n) (x#xs) = x # take n xs";
paulson@1552
   346
by (Simp_tac 1);
nipkow@1419
   347
qed "take_Suc_Cons";
nipkow@1327
   348
nipkow@2608
   349
goal thy "drop (Suc n) (x#xs) = drop n xs";
nipkow@2608
   350
by (Simp_tac 1);
nipkow@2608
   351
qed "drop_Suc_Cons";
nipkow@2608
   352
nipkow@2608
   353
Delsimps [take_Cons,drop_Cons];
nipkow@2608
   354
Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
nipkow@2608
   355
nipkow@3011
   356
goal thy "!xs. length(take n xs) = min (length xs) n";
nipkow@2608
   357
by(nat_ind_tac "n" 1);
nipkow@2608
   358
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   359
br allI 1;
nipkow@2608
   360
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   361
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   362
qed_spec_mp "length_take";
nipkow@2608
   363
Addsimps [length_take];
clasohm@923
   364
nipkow@3011
   365
goal thy "!xs. length(drop n xs) = (length xs - n)";
nipkow@2608
   366
by(nat_ind_tac "n" 1);
nipkow@2608
   367
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   368
br allI 1;
nipkow@2608
   369
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   370
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   371
qed_spec_mp "length_drop";
nipkow@2608
   372
Addsimps [length_drop];
nipkow@2608
   373
nipkow@3011
   374
goal thy "!xs. length xs <= n --> take n xs = xs";
nipkow@2608
   375
by(nat_ind_tac "n" 1);
nipkow@2608
   376
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   377
br allI 1;
nipkow@2608
   378
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   379
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   380
qed_spec_mp "take_all";
clasohm@923
   381
nipkow@3011
   382
goal thy "!xs. length xs <= n --> drop n xs = []";
nipkow@2608
   383
by(nat_ind_tac "n" 1);
nipkow@2608
   384
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   385
br allI 1;
nipkow@2608
   386
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   387
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   388
qed_spec_mp "drop_all";
nipkow@2608
   389
nipkow@3011
   390
goal thy 
nipkow@2608
   391
  "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
nipkow@2608
   392
by(nat_ind_tac "n" 1);
nipkow@2608
   393
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   394
br allI 1;
nipkow@2608
   395
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   396
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   397
qed_spec_mp "take_append";
nipkow@2608
   398
Addsimps [take_append];
nipkow@2608
   399
nipkow@3011
   400
goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
nipkow@2608
   401
by(nat_ind_tac "n" 1);
nipkow@2608
   402
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   403
br allI 1;
nipkow@2608
   404
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   405
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   406
qed_spec_mp "drop_append";
nipkow@2608
   407
Addsimps [drop_append];
nipkow@2608
   408
nipkow@3011
   409
goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
nipkow@2608
   410
by(nat_ind_tac "m" 1);
nipkow@2608
   411
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   412
br allI 1;
nipkow@2608
   413
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   414
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   415
br allI 1;
nipkow@2608
   416
by(res_inst_tac [("n","n")]natE 1);
nipkow@2608
   417
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   418
qed_spec_mp "take_take";
nipkow@2608
   419
nipkow@3011
   420
goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
nipkow@2608
   421
by(nat_ind_tac "m" 1);
nipkow@2608
   422
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   423
br allI 1;
nipkow@2608
   424
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   425
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   426
qed_spec_mp "drop_drop";
clasohm@923
   427
nipkow@3011
   428
goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
nipkow@2608
   429
by(nat_ind_tac "m" 1);
nipkow@2608
   430
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   431
br allI 1;
nipkow@2608
   432
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   433
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   434
qed_spec_mp "take_drop";
nipkow@2608
   435
nipkow@3011
   436
goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
nipkow@2608
   437
by(nat_ind_tac "n" 1);
nipkow@2608
   438
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   439
br allI 1;
nipkow@2608
   440
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   441
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   442
qed_spec_mp "take_map"; 
nipkow@2608
   443
nipkow@3011
   444
goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
nipkow@2608
   445
by(nat_ind_tac "n" 1);
nipkow@2608
   446
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   447
br allI 1;
nipkow@2608
   448
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   449
by(ALLGOALS Asm_simp_tac);
nipkow@2608
   450
qed_spec_mp "drop_map";
nipkow@2608
   451
nipkow@3011
   452
goal thy
nipkow@2608
   453
  "!n i. i < n --> nth i (take n xs) = nth i xs";
nipkow@3040
   454
by(induct_tac "xs" 1);
nipkow@2608
   455
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   456
by(strip_tac 1);
nipkow@2608
   457
by(res_inst_tac [("n","n")] natE 1);
paulson@2891
   458
 by(Blast_tac 1);
nipkow@2608
   459
by(res_inst_tac [("n","i")] natE 1);
nipkow@2608
   460
by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
nipkow@2608
   461
qed_spec_mp "nth_take";
nipkow@2608
   462
Addsimps [nth_take];
clasohm@923
   463
nipkow@3011
   464
goal thy
nipkow@2608
   465
  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
nipkow@2608
   466
by(nat_ind_tac "n" 1);
nipkow@2608
   467
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   468
br allI 1;
nipkow@2608
   469
by(res_inst_tac [("xs","xs")]list_cases 1);
nipkow@2608
   470
 by(ALLGOALS Asm_simp_tac);
nipkow@2608
   471
qed_spec_mp "nth_drop";
nipkow@2608
   472
Addsimps [nth_drop];
nipkow@2608
   473
nipkow@2608
   474
(** takeWhile & dropWhile **)
nipkow@2608
   475
nipkow@3011
   476
goal thy
nipkow@2608
   477
  "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
nipkow@3040
   478
by(induct_tac "xs" 1);
nipkow@2608
   479
 by(Simp_tac 1);
nipkow@2608
   480
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
paulson@2891
   481
by(Blast_tac 1);
nipkow@2608
   482
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
nipkow@2608
   483
Addsimps [takeWhile_append1];
clasohm@923
   484
nipkow@3011
   485
goal thy
nipkow@2608
   486
  "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
nipkow@3040
   487
by(induct_tac "xs" 1);
nipkow@2608
   488
 by(Simp_tac 1);
nipkow@2608
   489
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@2608
   490
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
nipkow@2608
   491
Addsimps [takeWhile_append2];
lcp@1169
   492
nipkow@3011
   493
goal thy
nipkow@2608
   494
  "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
nipkow@3040
   495
by(induct_tac "xs" 1);
nipkow@2608
   496
 by(Simp_tac 1);
nipkow@2608
   497
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
paulson@2891
   498
by(Blast_tac 1);
nipkow@2608
   499
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
nipkow@2608
   500
Addsimps [dropWhile_append1];
nipkow@2608
   501
nipkow@3011
   502
goal thy
nipkow@2608
   503
  "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
nipkow@3040
   504
by(induct_tac "xs" 1);
nipkow@2608
   505
 by(Simp_tac 1);
nipkow@2608
   506
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@2608
   507
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
nipkow@2608
   508
Addsimps [dropWhile_append2];
nipkow@2608
   509
nipkow@3011
   510
goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
nipkow@3040
   511
by(induct_tac "xs" 1);
nipkow@2608
   512
 by(Simp_tac 1);
nipkow@2608
   513
by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@2608
   514
qed_spec_mp"set_of_list_take_whileD";
nipkow@2608
   515