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