src/HOL/List.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1985 84cf16192e03
child 2512 0231e4f467f2
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
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
clasohm@923
     9
open List;
clasohm@923
    10
paulson@1985
    11
AddIffs list.distinct;
paulson@1985
    12
AddIffs list.inject;
clasohm@923
    13
clasohm@923
    14
bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
clasohm@923
    15
clasohm@923
    16
goal List.thy "!x. xs ~= x#xs";
clasohm@923
    17
by (list.induct_tac "xs" 1);
clasohm@1264
    18
by (ALLGOALS Asm_simp_tac);
clasohm@923
    19
qed "not_Cons_self";
clasohm@923
    20
clasohm@923
    21
goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
clasohm@923
    22
by (list.induct_tac "xs" 1);
clasohm@1264
    23
by (Simp_tac 1);
clasohm@1264
    24
by (Asm_simp_tac 1);
lcp@1169
    25
by (REPEAT(resolve_tac [exI,refl,conjI] 1));
clasohm@923
    26
qed "neq_Nil_conv";
clasohm@923
    27
clasohm@923
    28
clasohm@923
    29
(** @ - append **)
clasohm@923
    30
clasohm@923
    31
goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
clasohm@923
    32
by (list.induct_tac "xs" 1);
clasohm@1264
    33
by (ALLGOALS Asm_simp_tac);
clasohm@923
    34
qed "append_assoc";
clasohm@923
    35
clasohm@923
    36
goal List.thy "xs @ [] = xs";
clasohm@923
    37
by (list.induct_tac "xs" 1);
clasohm@1264
    38
by (ALLGOALS Asm_simp_tac);
clasohm@923
    39
qed "append_Nil2";
clasohm@923
    40
clasohm@923
    41
goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
clasohm@923
    42
by (list.induct_tac "xs" 1);
clasohm@1264
    43
by (ALLGOALS Asm_simp_tac);
clasohm@923
    44
qed "append_is_Nil";
clasohm@923
    45
clasohm@923
    46
goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
clasohm@923
    47
by (list.induct_tac "xs" 1);
clasohm@1264
    48
by (ALLGOALS Asm_simp_tac);
clasohm@923
    49
qed "same_append_eq";
clasohm@923
    50
nipkow@1327
    51
goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
nipkow@1327
    52
by (list.induct_tac "xs" 1);
nipkow@1327
    53
by (ALLGOALS Asm_simp_tac);
nipkow@1327
    54
qed "hd_append";
clasohm@923
    55
lcp@1169
    56
(** rev **)
lcp@1169
    57
lcp@1169
    58
goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
lcp@1169
    59
by (list.induct_tac "xs" 1);
clasohm@1264
    60
by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc])));
lcp@1169
    61
qed "rev_append";
lcp@1169
    62
lcp@1169
    63
goal List.thy "rev(rev l) = l";
lcp@1169
    64
by (list.induct_tac "l" 1);
clasohm@1264
    65
by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append])));
lcp@1169
    66
qed "rev_rev_ident";
lcp@1169
    67
lcp@1169
    68
clasohm@923
    69
(** mem **)
clasohm@923
    70
clasohm@923
    71
goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
clasohm@923
    72
by (list.induct_tac "xs" 1);
clasohm@1264
    73
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@923
    74
qed "mem_append";
clasohm@923
    75
clasohm@923
    76
goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
clasohm@923
    77
by (list.induct_tac "xs" 1);
clasohm@1264
    78
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
clasohm@923
    79
qed "mem_filter";
clasohm@923
    80
paulson@1908
    81
(** set_of_list **)
paulson@1812
    82
paulson@1908
    83
goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
paulson@1812
    84
by (list.induct_tac "xs" 1);
paulson@1812
    85
by (ALLGOALS Asm_simp_tac);
paulson@1812
    86
by (Fast_tac 1);
paulson@1908
    87
qed "set_of_list_append";
paulson@1812
    88
paulson@1908
    89
goal thy "(x mem xs) = (x: set_of_list xs)";
paulson@1812
    90
by (list.induct_tac "xs" 1);
paulson@1812
    91
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
paulson@1812
    92
by (Fast_tac 1);
paulson@1908
    93
qed "set_of_list_mem_eq";
paulson@1812
    94
paulson@1936
    95
goal List.thy "set_of_list l <= set_of_list (x#l)";
paulson@1936
    96
by (Simp_tac 1);
paulson@1936
    97
by (Fast_tac 1);
paulson@1936
    98
qed "set_of_list_subset_Cons";
paulson@1936
    99
paulson@1812
   100
clasohm@923
   101
(** list_all **)
clasohm@923
   102
clasohm@923
   103
goal List.thy "(Alls x:xs.True) = True";
clasohm@923
   104
by (list.induct_tac "xs" 1);
clasohm@1264
   105
by (ALLGOALS Asm_simp_tac);
clasohm@923
   106
qed "list_all_True";
clasohm@923
   107
clasohm@923
   108
goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
clasohm@923
   109
by (list.induct_tac "xs" 1);
clasohm@1264
   110
by (ALLGOALS Asm_simp_tac);
clasohm@923
   111
qed "list_all_conj";
clasohm@923
   112
clasohm@923
   113
goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
clasohm@923
   114
by (list.induct_tac "xs" 1);
clasohm@1264
   115
by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
berghofe@1760
   116
by (Fast_tac 1);
clasohm@923
   117
qed "list_all_mem_conv";
clasohm@923
   118
clasohm@923
   119
clasohm@923
   120
(** list_case **)
clasohm@923
   121
clasohm@923
   122
goal List.thy
clasohm@923
   123
 "P(list_case a f xs) = ((xs=[] --> P(a)) & \
clasohm@923
   124
\                         (!y ys. xs=y#ys --> P(f y ys)))";
clasohm@923
   125
by (list.induct_tac "xs" 1);
clasohm@1264
   126
by (ALLGOALS Asm_simp_tac);
berghofe@1760
   127
by (Fast_tac 1);
clasohm@923
   128
qed "expand_list_case";
clasohm@923
   129
clasohm@923
   130
goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
lcp@1169
   131
by (list.induct_tac "xs" 1);
berghofe@1760
   132
by (Fast_tac 1);
berghofe@1760
   133
by (Fast_tac 1);
clasohm@923
   134
bind_thm("list_eq_cases",
clasohm@923
   135
  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
clasohm@923
   136
clasohm@923
   137
(** flat **)
clasohm@923
   138
clasohm@923
   139
goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
clasohm@923
   140
by (list.induct_tac "xs" 1);
clasohm@1264
   141
by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc])));
clasohm@923
   142
qed"flat_append";
clasohm@923
   143
nipkow@962
   144
(** length **)
nipkow@962
   145
nipkow@962
   146
goal List.thy "length(xs@ys) = length(xs)+length(ys)";
nipkow@962
   147
by (list.induct_tac "xs" 1);
clasohm@1264
   148
by (ALLGOALS Asm_simp_tac);
nipkow@962
   149
qed"length_append";
nipkow@1301
   150
Addsimps [length_append];
nipkow@1301
   151
nipkow@1301
   152
goal List.thy "length (map f l) = length l";
nipkow@1301
   153
by (list.induct_tac "l" 1);
nipkow@1301
   154
by (ALLGOALS Simp_tac);
nipkow@1301
   155
qed "length_map";
nipkow@1301
   156
Addsimps [length_map];
nipkow@962
   157
lcp@1169
   158
goal List.thy "length(rev xs) = length(xs)";
lcp@1169
   159
by (list.induct_tac "xs" 1);
nipkow@1301
   160
by (ALLGOALS Asm_simp_tac);
lcp@1169
   161
qed "length_rev";
nipkow@1301
   162
Addsimps [length_rev];
lcp@1169
   163
clasohm@923
   164
(** nth **)
clasohm@923
   165
clasohm@923
   166
val [nth_0,nth_Suc] = nat_recs nth_def; 
clasohm@923
   167
store_thm("nth_0",nth_0);
clasohm@923
   168
store_thm("nth_Suc",nth_Suc);
nipkow@1301
   169
Addsimps [nth_0,nth_Suc];
nipkow@1301
   170
nipkow@1301
   171
goal List.thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
nipkow@1301
   172
by (list.induct_tac "xs" 1);
nipkow@1301
   173
(* case [] *)
nipkow@1301
   174
by (Asm_full_simp_tac 1);
nipkow@1301
   175
(* case x#xl *)
nipkow@1301
   176
by (rtac allI 1);
nipkow@1301
   177
by (nat_ind_tac "n" 1);
nipkow@1301
   178
by (ALLGOALS Asm_full_simp_tac);
nipkow@1485
   179
qed_spec_mp "nth_map";
nipkow@1301
   180
Addsimps [nth_map];
nipkow@1301
   181
nipkow@1301
   182
goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
nipkow@1301
   183
by (list.induct_tac "xs" 1);
nipkow@1301
   184
(* case [] *)
nipkow@1301
   185
by (Simp_tac 1);
nipkow@1301
   186
(* case x#xl *)
nipkow@1301
   187
by (rtac allI 1);
nipkow@1301
   188
by (nat_ind_tac "n" 1);
nipkow@1301
   189
by (ALLGOALS Asm_full_simp_tac);
nipkow@1485
   190
qed_spec_mp "list_all_nth";
nipkow@1301
   191
nipkow@1301
   192
goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
nipkow@1301
   193
by (list.induct_tac "xs" 1);
nipkow@1301
   194
(* case [] *)
nipkow@1301
   195
by (Simp_tac 1);
nipkow@1301
   196
(* case x#xl *)
nipkow@1301
   197
by (rtac allI 1);
nipkow@1301
   198
by (nat_ind_tac "n" 1);
nipkow@1301
   199
(* case 0 *)
nipkow@1301
   200
by (Asm_full_simp_tac 1);
nipkow@1301
   201
(* case Suc x *)
nipkow@1301
   202
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1485
   203
qed_spec_mp "nth_mem";
nipkow@1301
   204
Addsimps [nth_mem];
nipkow@1301
   205
nipkow@1327
   206
(** drop **)
nipkow@1327
   207
nipkow@1419
   208
goal thy "drop 0 xs = xs";
nipkow@1419
   209
by (list.induct_tac "xs" 1);
nipkow@1419
   210
by (ALLGOALS Asm_simp_tac);
nipkow@1327
   211
qed "drop_0";
nipkow@1327
   212
nipkow@1419
   213
goal thy "drop (Suc n) (x#xs) = drop n xs";
paulson@1552
   214
by (Simp_tac 1);
nipkow@1419
   215
qed "drop_Suc_Cons";
nipkow@1327
   216
nipkow@1419
   217
Delsimps [drop_Cons];
nipkow@1419
   218
Addsimps [drop_0,drop_Suc_Cons];
nipkow@1327
   219
nipkow@1327
   220
(** take **)
nipkow@1327
   221
nipkow@1419
   222
goal thy "take 0 xs = []";
nipkow@1419
   223
by (list.induct_tac "xs" 1);
nipkow@1419
   224
by (ALLGOALS Asm_simp_tac);
nipkow@1327
   225
qed "take_0";
nipkow@1327
   226
nipkow@1419
   227
goal thy "take (Suc n) (x#xs) = x # take n xs";
paulson@1552
   228
by (Simp_tac 1);
nipkow@1419
   229
qed "take_Suc_Cons";
nipkow@1327
   230
nipkow@1419
   231
Delsimps [take_Cons];
nipkow@1419
   232
Addsimps [take_0,take_Suc_Cons];
clasohm@923
   233
clasohm@923
   234
(** Additional mapping lemmas **)
clasohm@923
   235
nipkow@995
   236
goal List.thy "map (%x.x) = (%xs.xs)";
nipkow@995
   237
by (rtac ext 1);
clasohm@923
   238
by (list.induct_tac "xs" 1);
clasohm@1264
   239
by (ALLGOALS Asm_simp_tac);
clasohm@923
   240
qed "map_ident";
clasohm@923
   241
clasohm@923
   242
goal List.thy "map f (xs@ys) = map f xs @ map f ys";
clasohm@923
   243
by (list.induct_tac "xs" 1);
clasohm@1264
   244
by (ALLGOALS Asm_simp_tac);
clasohm@923
   245
qed "map_append";
clasohm@923
   246
clasohm@923
   247
goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
clasohm@923
   248
by (list.induct_tac "xs" 1);
clasohm@1264
   249
by (ALLGOALS Asm_simp_tac);
clasohm@923
   250
qed "map_compose";
clasohm@923
   251
lcp@1169
   252
goal List.thy "rev(map f l) = map f (rev l)";
lcp@1169
   253
by (list.induct_tac "l" 1);
clasohm@1264
   254
by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append])));
lcp@1169
   255
qed "rev_map_distrib";
lcp@1169
   256
lcp@1169
   257
goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
lcp@1169
   258
by (list.induct_tac "ls" 1);
clasohm@1264
   259
by (ALLGOALS (asm_simp_tac (!simpset addsimps 
lcp@1169
   260
       [map_append, flat_append, rev_append, append_Nil2])));
lcp@1169
   261
qed "rev_flat";
lcp@1169
   262
clasohm@1264
   263
Addsimps
clasohm@923
   264
  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
clasohm@923
   265
   mem_append, mem_filter,
nipkow@1202
   266
   rev_append, rev_rev_ident,
clasohm@923
   267
   map_ident, map_append, map_compose,
nipkow@1301
   268
   flat_append, list_all_True, list_all_conj];
clasohm@923
   269