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