src/HOL/List.ML
author lcp
Thu Jun 29 16:33:17 1995 +0200 (1995-06-29)
changeset 1169 5873833cf37f
parent 995 95c148a7b9c4
child 1202 968cd786a748
permissions -rw-r--r--
Added function rev and its properties length_rev, etc.
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
val list_ss = HOL_ss addsimps list.simps;
clasohm@923
    19
clasohm@923
    20
goal List.thy "!x. xs ~= x#xs";
clasohm@923
    21
by (list.induct_tac "xs" 1);
clasohm@923
    22
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    23
qed "not_Cons_self";
clasohm@923
    24
clasohm@923
    25
goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
clasohm@923
    26
by (list.induct_tac "xs" 1);
lcp@1169
    27
by (simp_tac list_ss 1);
lcp@1169
    28
by (asm_simp_tac list_ss 1);
lcp@1169
    29
by (REPEAT(resolve_tac [exI,refl,conjI] 1));
clasohm@923
    30
qed "neq_Nil_conv";
clasohm@923
    31
clasohm@923
    32
val list_ss = arith_ss addsimps list.simps @
clasohm@923
    33
  [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons,
clasohm@923
    34
   mem_Nil, mem_Cons,
clasohm@923
    35
   append_Nil, append_Cons,
lcp@1169
    36
   rev_Nil, rev_Cons,
clasohm@923
    37
   map_Nil, map_Cons,
clasohm@923
    38
   flat_Nil, flat_Cons,
clasohm@923
    39
   list_all_Nil, list_all_Cons,
nipkow@962
    40
   filter_Nil, filter_Cons,
nipkow@974
    41
   foldl_Nil, foldl_Cons,
nipkow@962
    42
   length_Nil, length_Cons];
clasohm@923
    43
clasohm@923
    44
clasohm@923
    45
(** @ - append **)
clasohm@923
    46
clasohm@923
    47
goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
clasohm@923
    48
by (list.induct_tac "xs" 1);
lcp@1169
    49
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    50
qed "append_assoc";
clasohm@923
    51
clasohm@923
    52
goal List.thy "xs @ [] = xs";
clasohm@923
    53
by (list.induct_tac "xs" 1);
lcp@1169
    54
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    55
qed "append_Nil2";
clasohm@923
    56
clasohm@923
    57
goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
clasohm@923
    58
by (list.induct_tac "xs" 1);
lcp@1169
    59
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    60
qed "append_is_Nil";
clasohm@923
    61
clasohm@923
    62
goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
clasohm@923
    63
by (list.induct_tac "xs" 1);
lcp@1169
    64
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    65
qed "same_append_eq";
clasohm@923
    66
clasohm@923
    67
lcp@1169
    68
(** rev **)
lcp@1169
    69
lcp@1169
    70
goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
lcp@1169
    71
by (list.induct_tac "xs" 1);
lcp@1169
    72
by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_Nil2,append_assoc])));
lcp@1169
    73
qed "rev_append";
lcp@1169
    74
lcp@1169
    75
goal List.thy "rev(rev l) = l";
lcp@1169
    76
by (list.induct_tac "l" 1);
lcp@1169
    77
by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_append])));
lcp@1169
    78
qed "rev_rev_ident";
lcp@1169
    79
lcp@1169
    80
clasohm@923
    81
(** mem **)
clasohm@923
    82
clasohm@923
    83
goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
clasohm@923
    84
by (list.induct_tac "xs" 1);
lcp@1169
    85
by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
clasohm@923
    86
qed "mem_append";
clasohm@923
    87
clasohm@923
    88
goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
clasohm@923
    89
by (list.induct_tac "xs" 1);
lcp@1169
    90
by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
clasohm@923
    91
qed "mem_filter";
clasohm@923
    92
clasohm@923
    93
(** list_all **)
clasohm@923
    94
clasohm@923
    95
goal List.thy "(Alls x:xs.True) = True";
clasohm@923
    96
by (list.induct_tac "xs" 1);
lcp@1169
    97
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
    98
qed "list_all_True";
clasohm@923
    99
clasohm@923
   100
goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
clasohm@923
   101
by (list.induct_tac "xs" 1);
lcp@1169
   102
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
   103
qed "list_all_conj";
clasohm@923
   104
clasohm@923
   105
goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
clasohm@923
   106
by (list.induct_tac "xs" 1);
lcp@1169
   107
by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
lcp@1169
   108
by (fast_tac HOL_cs 1);
clasohm@923
   109
qed "list_all_mem_conv";
clasohm@923
   110
clasohm@923
   111
clasohm@923
   112
(** list_case **)
clasohm@923
   113
clasohm@923
   114
goal List.thy
clasohm@923
   115
 "P(list_case a f xs) = ((xs=[] --> P(a)) & \
clasohm@923
   116
\                         (!y ys. xs=y#ys --> P(f y ys)))";
clasohm@923
   117
by (list.induct_tac "xs" 1);
lcp@1169
   118
by (ALLGOALS (asm_simp_tac list_ss));
lcp@1169
   119
by (fast_tac HOL_cs 1);
clasohm@923
   120
qed "expand_list_case";
clasohm@923
   121
clasohm@923
   122
goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
lcp@1169
   123
by (list.induct_tac "xs" 1);
lcp@1169
   124
by (fast_tac HOL_cs 1);
lcp@1169
   125
by (fast_tac HOL_cs 1);
clasohm@923
   126
bind_thm("list_eq_cases",
clasohm@923
   127
  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
clasohm@923
   128
clasohm@923
   129
(** flat **)
clasohm@923
   130
clasohm@923
   131
goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
clasohm@923
   132
by (list.induct_tac "xs" 1);
lcp@1169
   133
by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_assoc])));
clasohm@923
   134
qed"flat_append";
clasohm@923
   135
nipkow@962
   136
(** length **)
nipkow@962
   137
nipkow@962
   138
goal List.thy "length(xs@ys) = length(xs)+length(ys)";
nipkow@962
   139
by (list.induct_tac "xs" 1);
lcp@1169
   140
by (ALLGOALS (asm_simp_tac list_ss));
nipkow@962
   141
qed"length_append";
nipkow@962
   142
lcp@1169
   143
goal List.thy "length(rev xs) = length(xs)";
lcp@1169
   144
by (list.induct_tac "xs" 1);
lcp@1169
   145
by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_append])));
lcp@1169
   146
qed "length_rev";
lcp@1169
   147
clasohm@923
   148
(** nth **)
clasohm@923
   149
clasohm@923
   150
val [nth_0,nth_Suc] = nat_recs nth_def; 
clasohm@923
   151
store_thm("nth_0",nth_0);
clasohm@923
   152
store_thm("nth_Suc",nth_Suc);
clasohm@923
   153
clasohm@923
   154
(** Additional mapping lemmas **)
clasohm@923
   155
nipkow@995
   156
goal List.thy "map (%x.x) = (%xs.xs)";
nipkow@995
   157
by (rtac ext 1);
clasohm@923
   158
by (list.induct_tac "xs" 1);
clasohm@923
   159
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
   160
qed "map_ident";
clasohm@923
   161
clasohm@923
   162
goal List.thy "map f (xs@ys) = map f xs @ map f ys";
clasohm@923
   163
by (list.induct_tac "xs" 1);
clasohm@923
   164
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
   165
qed "map_append";
clasohm@923
   166
clasohm@923
   167
goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
clasohm@923
   168
by (list.induct_tac "xs" 1);
clasohm@923
   169
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@923
   170
qed "map_compose";
clasohm@923
   171
lcp@1169
   172
goal List.thy "rev(map f l) = map f (rev l)";
lcp@1169
   173
by (list.induct_tac "l" 1);
lcp@1169
   174
by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_append])));
lcp@1169
   175
qed "rev_map_distrib";
lcp@1169
   176
lcp@1169
   177
goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
lcp@1169
   178
by (list.induct_tac "ls" 1);
lcp@1169
   179
by (ALLGOALS (asm_simp_tac (list_ss addsimps 
lcp@1169
   180
       [map_append, flat_append, rev_append, append_Nil2])));
lcp@1169
   181
qed "rev_flat";
lcp@1169
   182
clasohm@923
   183
val list_ss = list_ss addsimps
clasohm@923
   184
  [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
clasohm@923
   185
   mem_append, mem_filter,
clasohm@923
   186
   map_ident, map_append, map_compose,
nipkow@962
   187
   flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
clasohm@923
   188