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