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