New class "order" and accompanying changes.
authornipkow
Wed Feb 12 18:53:59 1997 +0100 (1997-02-12)
changeset 2608450c9b682a92
parent 2607 a224a2865e05
child 2609 4370e5f0fa3f
New class "order" and accompanying changes.
In particular reflexivity of <= is now one rewrite rule.
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/NatDef.ML
src/HOL/NatDef.thy
src/HOL/Ord.ML
src/HOL/Ord.thy
src/HOL/Set.ML
     1.1 --- a/src/HOL/List.ML	Wed Feb 12 15:43:50 1997 +0100
     1.2 +++ b/src/HOL/List.ML	Wed Feb 12 18:53:59 1997 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  goal List.thy "!x. xs ~= x#xs";
     1.5  by (list.induct_tac "xs" 1);
     1.6  by (ALLGOALS Asm_simp_tac);
     1.7 -qed "not_Cons_self";
     1.8 +qed_spec_mp "not_Cons_self";
     1.9  Addsimps [not_Cons_self];
    1.10  
    1.11  goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
    1.12 @@ -27,6 +27,29 @@
    1.13  qed "neq_Nil_conv";
    1.14  
    1.15  
    1.16 +(** list_case **)
    1.17 +
    1.18 +goal List.thy
    1.19 + "P(list_case a f xs) = ((xs=[] --> P(a)) & \
    1.20 +\                         (!y ys. xs=y#ys --> P(f y ys)))";
    1.21 +by (list.induct_tac "xs" 1);
    1.22 +by (ALLGOALS Asm_simp_tac);
    1.23 +by (Fast_tac 1);
    1.24 +qed "expand_list_case";
    1.25 +
    1.26 +val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    1.27 +by(list.induct_tac "xs" 1);
    1.28 +by(REPEAT(resolve_tac prems 1));
    1.29 +qed "list_cases";
    1.30 +
    1.31 +goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    1.32 +by (list.induct_tac "xs" 1);
    1.33 +by (Fast_tac 1);
    1.34 +by (Fast_tac 1);
    1.35 +bind_thm("list_eq_cases",
    1.36 +  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    1.37 +
    1.38 +
    1.39  (** @ - append **)
    1.40  
    1.41  goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
    1.42 @@ -44,20 +67,80 @@
    1.43  goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
    1.44  by (list.induct_tac "xs" 1);
    1.45  by (ALLGOALS Asm_simp_tac);
    1.46 -qed "append_is_Nil";
    1.47 -Addsimps [append_is_Nil];
    1.48 +qed "append_is_Nil_conv";
    1.49 +AddIffs [append_is_Nil_conv];
    1.50 +
    1.51 +goal List.thy "([] = xs@ys) = (xs=[] & ys=[])";
    1.52 +by (list.induct_tac "xs" 1);
    1.53 +by (ALLGOALS Asm_simp_tac);
    1.54 +by(Fast_tac 1);
    1.55 +qed "Nil_is_append_conv";
    1.56 +AddIffs [Nil_is_append_conv];
    1.57  
    1.58  goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
    1.59  by (list.induct_tac "xs" 1);
    1.60  by (ALLGOALS Asm_simp_tac);
    1.61  qed "same_append_eq";
    1.62 -Addsimps [same_append_eq];
    1.63 +AddIffs [same_append_eq];
    1.64 +
    1.65 +goal List.thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    1.66 +by(list.induct_tac "xs" 1);
    1.67 + br allI 1;
    1.68 + by(list.induct_tac "ys" 1);
    1.69 +  by(ALLGOALS Asm_simp_tac);
    1.70 +br allI 1;
    1.71 +by(list.induct_tac "ys" 1);
    1.72 + by(ALLGOALS Asm_simp_tac);
    1.73 +qed_spec_mp "append1_eq_conv";
    1.74 +AddIffs [append1_eq_conv];
    1.75 +
    1.76 +goal List.thy "xs ~= [] --> hd xs # tl xs = xs";
    1.77 +by(list.induct_tac "xs" 1);
    1.78 +by(ALLGOALS Asm_simp_tac);
    1.79 +qed_spec_mp "hd_Cons_tl";
    1.80 +Addsimps [hd_Cons_tl];
    1.81  
    1.82  goal List.thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
    1.83  by (list.induct_tac "xs" 1);
    1.84  by (ALLGOALS Asm_simp_tac);
    1.85  qed "hd_append";
    1.86  
    1.87 +goal List.thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    1.88 +by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
    1.89 +qed "tl_append";
    1.90 +
    1.91 +(** map **)
    1.92 +
    1.93 +goal List.thy
    1.94 +  "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
    1.95 +by(list.induct_tac "xs" 1);
    1.96 +by(ALLGOALS Asm_simp_tac);
    1.97 +bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
    1.98 +
    1.99 +goal List.thy "map (%x.x) = (%xs.xs)";
   1.100 +by (rtac ext 1);
   1.101 +by (list.induct_tac "xs" 1);
   1.102 +by (ALLGOALS Asm_simp_tac);
   1.103 +qed "map_ident";
   1.104 +Addsimps[map_ident];
   1.105 +
   1.106 +goal List.thy "map f (xs@ys) = map f xs @ map f ys";
   1.107 +by (list.induct_tac "xs" 1);
   1.108 +by (ALLGOALS Asm_simp_tac);
   1.109 +qed "map_append";
   1.110 +Addsimps[map_append];
   1.111 +
   1.112 +goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
   1.113 +by (list.induct_tac "xs" 1);
   1.114 +by (ALLGOALS Asm_simp_tac);
   1.115 +qed "map_compose";
   1.116 +Addsimps[map_compose];
   1.117 +
   1.118 +goal List.thy "rev(map f xs) = map f (rev xs)";
   1.119 +by (list.induct_tac "xs" 1);
   1.120 +by (ALLGOALS Asm_simp_tac);
   1.121 +qed "rev_map";
   1.122 +
   1.123  (** rev **)
   1.124  
   1.125  goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
   1.126 @@ -72,6 +155,7 @@
   1.127  qed "rev_rev_ident";
   1.128  Addsimps[rev_rev_ident];
   1.129  
   1.130 +
   1.131  (** mem **)
   1.132  
   1.133  goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
   1.134 @@ -106,6 +190,25 @@
   1.135  by (Fast_tac 1);
   1.136  qed "set_of_list_subset_Cons";
   1.137  
   1.138 +goal List.thy "(set_of_list xs = {}) = (xs = [])";
   1.139 +by(list.induct_tac "xs" 1);
   1.140 +by(ALLGOALS Asm_simp_tac);
   1.141 +qed "set_of_list_empty";
   1.142 +Addsimps [set_of_list_empty];
   1.143 +
   1.144 +goal List.thy "set_of_list(rev xs) = set_of_list(xs)";
   1.145 +by(list.induct_tac "xs" 1);
   1.146 +by(ALLGOALS Asm_simp_tac);
   1.147 +by(Fast_tac 1);
   1.148 +qed "set_of_list_rev";
   1.149 +Addsimps [set_of_list_rev];
   1.150 +
   1.151 +goal List.thy "set_of_list(map f xs) = f``(set_of_list xs)";
   1.152 +by(list.induct_tac "xs" 1);
   1.153 +by(ALLGOALS Asm_simp_tac);
   1.154 +qed "set_of_list_map";
   1.155 +Addsimps [set_of_list_map];
   1.156 +
   1.157  
   1.158  (** list_all **)
   1.159  
   1.160 @@ -128,35 +231,27 @@
   1.161  qed "list_all_mem_conv";
   1.162  
   1.163  
   1.164 -(** list_case **)
   1.165 +(** filter **)
   1.166  
   1.167 -goal List.thy
   1.168 - "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   1.169 -\                         (!y ys. xs=y#ys --> P(f y ys)))";
   1.170 +goal List.thy "[x:xs@ys . P] = [x:xs . P] @ [y:ys . P]";
   1.171 +by(list.induct_tac "xs" 1);
   1.172 + by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   1.173 +qed "filter_append";
   1.174 +Addsimps [filter_append];
   1.175 +
   1.176 +
   1.177 +(** concat **)
   1.178 +
   1.179 +goal List.thy  "concat(xs@ys) = concat(xs)@concat(ys)";
   1.180  by (list.induct_tac "xs" 1);
   1.181  by (ALLGOALS Asm_simp_tac);
   1.182 -by (Fast_tac 1);
   1.183 -qed "expand_list_case";
   1.184 -
   1.185 -val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
   1.186 -by(list.induct_tac "xs" 1);
   1.187 -by(REPEAT(resolve_tac prems 1));
   1.188 -qed "list_cases";
   1.189 +qed"concat_append";
   1.190 +Addsimps [concat_append];
   1.191  
   1.192 -goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
   1.193 -by (list.induct_tac "xs" 1);
   1.194 -by (Fast_tac 1);
   1.195 -by (Fast_tac 1);
   1.196 -bind_thm("list_eq_cases",
   1.197 -  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
   1.198 -
   1.199 -(** flat **)
   1.200 -
   1.201 -goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
   1.202 -by (list.induct_tac "xs" 1);
   1.203 +goal List.thy "rev(concat ls) = concat (map rev (rev ls))";
   1.204 +by (list.induct_tac "ls" 1);
   1.205  by (ALLGOALS Asm_simp_tac);
   1.206 -qed"flat_append";
   1.207 -Addsimps [flat_append];
   1.208 +qed "rev_concat";
   1.209  
   1.210  (** length **)
   1.211  
   1.212 @@ -178,6 +273,19 @@
   1.213  qed "length_rev";
   1.214  Addsimps [length_rev];
   1.215  
   1.216 +goal List.thy "(length xs = 0) = (xs = [])";
   1.217 +by(list.induct_tac "xs" 1);
   1.218 +by(ALLGOALS Asm_simp_tac);
   1.219 +qed "length_0_conv";
   1.220 +AddIffs [length_0_conv];
   1.221 +
   1.222 +goal List.thy "(0 < length xs) = (xs ~= [])";
   1.223 +by(list.induct_tac "xs" 1);
   1.224 +by(ALLGOALS Asm_simp_tac);
   1.225 +qed "length_greater_0_conv";
   1.226 +AddIffs [length_greater_0_conv];
   1.227 +
   1.228 +
   1.229  (** nth **)
   1.230  
   1.231  val [nth_0,nth_Suc] = nat_recs nth_def; 
   1.232 @@ -185,6 +293,19 @@
   1.233  store_thm("nth_Suc",nth_Suc);
   1.234  Addsimps [nth_0,nth_Suc];
   1.235  
   1.236 +goal List.thy
   1.237 +  "!xs. nth n (xs@ys) = \
   1.238 +\          (if n < length xs then nth n xs else nth (n - length xs) ys)";
   1.239 +by(nat_ind_tac "n" 1);
   1.240 + by(Asm_simp_tac 1);
   1.241 + br allI 1;
   1.242 + by(res_inst_tac [("xs","xs")]list_cases 1);
   1.243 +  by(ALLGOALS Asm_simp_tac);
   1.244 +br allI 1;
   1.245 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.246 + by(ALLGOALS Asm_simp_tac);
   1.247 +qed_spec_mp "nth_append";
   1.248 +
   1.249  goal List.thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
   1.250  by (list.induct_tac "xs" 1);
   1.251  (* case [] *)
   1.252 @@ -220,61 +341,188 @@
   1.253  qed_spec_mp "nth_mem";
   1.254  Addsimps [nth_mem];
   1.255  
   1.256 -(** drop **)
   1.257  
   1.258 -goal thy "drop 0 xs = xs";
   1.259 -by (list.induct_tac "xs" 1);
   1.260 -by (ALLGOALS Asm_simp_tac);
   1.261 -qed "drop_0";
   1.262 -
   1.263 -goal thy "drop (Suc n) (x#xs) = drop n xs";
   1.264 -by (Simp_tac 1);
   1.265 -qed "drop_Suc_Cons";
   1.266 -
   1.267 -Delsimps [drop_Cons];
   1.268 -Addsimps [drop_0,drop_Suc_Cons];
   1.269 -
   1.270 -(** take **)
   1.271 +(** take  & drop **)
   1.272 +section "take & drop";
   1.273  
   1.274  goal thy "take 0 xs = []";
   1.275  by (list.induct_tac "xs" 1);
   1.276  by (ALLGOALS Asm_simp_tac);
   1.277  qed "take_0";
   1.278  
   1.279 +goal thy "drop 0 xs = xs";
   1.280 +by (list.induct_tac "xs" 1);
   1.281 +by (ALLGOALS Asm_simp_tac);
   1.282 +qed "drop_0";
   1.283 +
   1.284  goal thy "take (Suc n) (x#xs) = x # take n xs";
   1.285  by (Simp_tac 1);
   1.286  qed "take_Suc_Cons";
   1.287  
   1.288 -Delsimps [take_Cons];
   1.289 -Addsimps [take_0,take_Suc_Cons];
   1.290 +goal thy "drop (Suc n) (x#xs) = drop n xs";
   1.291 +by (Simp_tac 1);
   1.292 +qed "drop_Suc_Cons";
   1.293 +
   1.294 +Delsimps [take_Cons,drop_Cons];
   1.295 +Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
   1.296 +
   1.297 +goal List.thy "!xs. length(take n xs) = min (length xs) n";
   1.298 +by(nat_ind_tac "n" 1);
   1.299 + by(ALLGOALS Asm_simp_tac);
   1.300 +br allI 1;
   1.301 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.302 + by(ALLGOALS Asm_simp_tac);
   1.303 +qed_spec_mp "length_take";
   1.304 +Addsimps [length_take];
   1.305  
   1.306 -(** Additional mapping lemmas **)
   1.307 +goal List.thy "!xs. length(drop n xs) = (length xs - n)";
   1.308 +by(nat_ind_tac "n" 1);
   1.309 + by(ALLGOALS Asm_simp_tac);
   1.310 +br allI 1;
   1.311 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.312 + by(ALLGOALS Asm_simp_tac);
   1.313 +qed_spec_mp "length_drop";
   1.314 +Addsimps [length_drop];
   1.315 +
   1.316 +goal List.thy "!xs. length xs <= n --> take n xs = xs";
   1.317 +by(nat_ind_tac "n" 1);
   1.318 + by(ALLGOALS Asm_simp_tac);
   1.319 +br allI 1;
   1.320 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.321 + by(ALLGOALS Asm_simp_tac);
   1.322 +qed_spec_mp "take_all";
   1.323  
   1.324 -goal List.thy "map (%x.x) = (%xs.xs)";
   1.325 -by (rtac ext 1);
   1.326 -by (list.induct_tac "xs" 1);
   1.327 -by (ALLGOALS Asm_simp_tac);
   1.328 -qed "map_ident";
   1.329 -Addsimps[map_ident];
   1.330 +goal List.thy "!xs. length xs <= n --> drop n xs = []";
   1.331 +by(nat_ind_tac "n" 1);
   1.332 + by(ALLGOALS Asm_simp_tac);
   1.333 +br allI 1;
   1.334 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.335 + by(ALLGOALS Asm_simp_tac);
   1.336 +qed_spec_mp "drop_all";
   1.337 +
   1.338 +goal List.thy 
   1.339 +  "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   1.340 +by(nat_ind_tac "n" 1);
   1.341 + by(ALLGOALS Asm_simp_tac);
   1.342 +br allI 1;
   1.343 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.344 + by(ALLGOALS Asm_simp_tac);
   1.345 +qed_spec_mp "take_append";
   1.346 +Addsimps [take_append];
   1.347 +
   1.348 +goal List.thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   1.349 +by(nat_ind_tac "n" 1);
   1.350 + by(ALLGOALS Asm_simp_tac);
   1.351 +br allI 1;
   1.352 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.353 + by(ALLGOALS Asm_simp_tac);
   1.354 +qed_spec_mp "drop_append";
   1.355 +Addsimps [drop_append];
   1.356 +
   1.357 +goal List.thy "!xs n. take n (take m xs) = take (min n m) xs"; 
   1.358 +by(nat_ind_tac "m" 1);
   1.359 + by(ALLGOALS Asm_simp_tac);
   1.360 +br allI 1;
   1.361 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.362 + by(ALLGOALS Asm_simp_tac);
   1.363 +br allI 1;
   1.364 +by(res_inst_tac [("n","n")]natE 1);
   1.365 + by(ALLGOALS Asm_simp_tac);
   1.366 +qed_spec_mp "take_take";
   1.367 +
   1.368 +goal List.thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   1.369 +by(nat_ind_tac "m" 1);
   1.370 + by(ALLGOALS Asm_simp_tac);
   1.371 +br allI 1;
   1.372 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.373 + by(ALLGOALS Asm_simp_tac);
   1.374 +qed_spec_mp "drop_drop";
   1.375  
   1.376 -goal List.thy "map f (xs@ys) = map f xs @ map f ys";
   1.377 -by (list.induct_tac "xs" 1);
   1.378 -by (ALLGOALS Asm_simp_tac);
   1.379 -qed "map_append";
   1.380 -Addsimps[map_append];
   1.381 +goal List.thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   1.382 +by(nat_ind_tac "m" 1);
   1.383 + by(ALLGOALS Asm_simp_tac);
   1.384 +br allI 1;
   1.385 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.386 + by(ALLGOALS Asm_simp_tac);
   1.387 +qed_spec_mp "take_drop";
   1.388 +
   1.389 +goal List.thy "!xs. take n (map f xs) = map f (take n xs)"; 
   1.390 +by(nat_ind_tac "n" 1);
   1.391 +by(ALLGOALS Asm_simp_tac);
   1.392 +br allI 1;
   1.393 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.394 +by(ALLGOALS Asm_simp_tac);
   1.395 +qed_spec_mp "take_map"; 
   1.396 +
   1.397 +goal List.thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
   1.398 +by(nat_ind_tac "n" 1);
   1.399 +by(ALLGOALS Asm_simp_tac);
   1.400 +br allI 1;
   1.401 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.402 +by(ALLGOALS Asm_simp_tac);
   1.403 +qed_spec_mp "drop_map";
   1.404 +
   1.405 +goal List.thy
   1.406 +  "!n i. i < n --> nth i (take n xs) = nth i xs";
   1.407 +by(list.induct_tac "xs" 1);
   1.408 + by(ALLGOALS Asm_simp_tac);
   1.409 +by(strip_tac 1);
   1.410 +by(res_inst_tac [("n","n")] natE 1);
   1.411 + by(Fast_tac 1);
   1.412 +by(res_inst_tac [("n","i")] natE 1);
   1.413 +by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
   1.414 +qed_spec_mp "nth_take";
   1.415 +Addsimps [nth_take];
   1.416  
   1.417 -goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
   1.418 -by (list.induct_tac "xs" 1);
   1.419 -by (ALLGOALS Asm_simp_tac);
   1.420 -qed "map_compose";
   1.421 -Addsimps[map_compose];
   1.422 +goal List.thy
   1.423 +  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
   1.424 +by(nat_ind_tac "n" 1);
   1.425 + by(ALLGOALS Asm_simp_tac);
   1.426 +br allI 1;
   1.427 +by(res_inst_tac [("xs","xs")]list_cases 1);
   1.428 + by(ALLGOALS Asm_simp_tac);
   1.429 +qed_spec_mp "nth_drop";
   1.430 +Addsimps [nth_drop];
   1.431 +
   1.432 +(** takeWhile & dropWhile **)
   1.433 +
   1.434 +goal List.thy
   1.435 +  "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   1.436 +by(list.induct_tac "xs" 1);
   1.437 + by(Simp_tac 1);
   1.438 +by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   1.439 +by(Fast_tac 1);
   1.440 +bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   1.441 +Addsimps [takeWhile_append1];
   1.442  
   1.443 -goal List.thy "rev(map f l) = map f (rev l)";
   1.444 -by (list.induct_tac "l" 1);
   1.445 -by (ALLGOALS Asm_simp_tac);
   1.446 -qed "rev_map_distrib";
   1.447 +goal List.thy
   1.448 +  "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   1.449 +by(list.induct_tac "xs" 1);
   1.450 + by(Simp_tac 1);
   1.451 +by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   1.452 +bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   1.453 +Addsimps [takeWhile_append2];
   1.454  
   1.455 -goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
   1.456 -by (list.induct_tac "ls" 1);
   1.457 -by (ALLGOALS Asm_simp_tac);
   1.458 -qed "rev_flat";
   1.459 +goal List.thy
   1.460 +  "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   1.461 +by(list.induct_tac "xs" 1);
   1.462 + by(Simp_tac 1);
   1.463 +by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   1.464 +by(Fast_tac 1);
   1.465 +bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   1.466 +Addsimps [dropWhile_append1];
   1.467 +
   1.468 +goal List.thy
   1.469 +  "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   1.470 +by(list.induct_tac "xs" 1);
   1.471 + by(Simp_tac 1);
   1.472 +by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   1.473 +bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   1.474 +Addsimps [dropWhile_append2];
   1.475 +
   1.476 +goal List.thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
   1.477 +by(list.induct_tac "xs" 1);
   1.478 + by(Simp_tac 1);
   1.479 +by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   1.480 +qed_spec_mp"set_of_list_take_whileD";
   1.481 +
     2.1 --- a/src/HOL/List.thy	Wed Feb 12 15:43:50 1997 +0100
     2.2 +++ b/src/HOL/List.thy	Wed Feb 12 18:53:59 1997 +0100
     2.3 @@ -13,18 +13,19 @@
     2.4  consts
     2.5  
     2.6    "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
     2.7 -  drop        :: [nat, 'a list] => 'a list
     2.8    filter      :: ['a => bool, 'a list] => 'a list
     2.9 -  flat        :: 'a list list => 'a list
    2.10 +  concat      :: 'a list list => 'a list
    2.11    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
    2.12    hd          :: 'a list => 'a
    2.13    length      :: 'a list => nat
    2.14 -  set_of_list :: ('a list => 'a set)
    2.15 +  set_of_list :: 'a list => 'a set
    2.16    list_all    :: ('a => bool) => ('a list => bool)
    2.17    map         :: ('a=>'b) => ('a list => 'b list)
    2.18    mem         :: ['a, 'a list] => bool                    (infixl 55)
    2.19    nth         :: [nat, 'a list] => 'a
    2.20 -  take        :: [nat, 'a list] => 'a list
    2.21 +  take, drop  :: [nat, 'a list] => 'a list
    2.22 +  takeWhile,
    2.23 +  dropWhile   :: ('a => bool) => 'a list => 'a list
    2.24    tl,ttl      :: 'a list => 'a list
    2.25    rev         :: 'a list => 'a list
    2.26  
    2.27 @@ -81,9 +82,9 @@
    2.28  primrec length list
    2.29    "length([]) = 0"
    2.30    "length(x#xs) = Suc(length(xs))"
    2.31 -primrec flat list
    2.32 -  "flat([]) = []"
    2.33 -  "flat(x#xs) = x @ flat(xs)"
    2.34 +primrec concat list
    2.35 +  "concat([]) = []"
    2.36 +  "concat(x#xs) = x @ concat(xs)"
    2.37  primrec drop list
    2.38    drop_Nil  "drop n [] = []"
    2.39    drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
    2.40 @@ -92,4 +93,10 @@
    2.41    take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
    2.42  defs
    2.43    nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
    2.44 +primrec takeWhile list
    2.45 +  "takeWhile P [] = []"
    2.46 +  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
    2.47 +primrec dropWhile list
    2.48 +  "dropWhile P [] = []"
    2.49 +  "dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)"
    2.50  end
     3.1 --- a/src/HOL/Nat.ML	Wed Feb 12 15:43:50 1997 +0100
     3.2 +++ b/src/HOL/Nat.ML	Wed Feb 12 18:53:59 1997 +0100
     3.3 @@ -1,678 +1,22 @@
     3.4  (*  Title:      HOL/Nat.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     3.7 -    Copyright   1991  University of Cambridge
     3.8 -
     3.9 -For Nat.thy.  Type nat is defined as a set (Nat) over the type ind.
    3.10 +    Author:     Tobias Nipkow
    3.11 +    Copyright   1997 TU Muenchen
    3.12  *)
    3.13  
    3.14 -open Nat;
    3.15 -
    3.16 -goal Nat.thy "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";
    3.17 -by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    3.18 -qed "Nat_fun_mono";
    3.19 -
    3.20 -val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski);
    3.21 -
    3.22 -(* Zero is a natural number -- this also justifies the type definition*)
    3.23 -goal Nat.thy "Zero_Rep: Nat";
    3.24 -by (stac Nat_unfold 1);
    3.25 -by (rtac (singletonI RS UnI1) 1);
    3.26 -qed "Zero_RepI";
    3.27 -
    3.28 -val prems = goal Nat.thy "i: Nat ==> Suc_Rep(i) : Nat";
    3.29 -by (stac Nat_unfold 1);
    3.30 -by (rtac (imageI RS UnI2) 1);
    3.31 -by (resolve_tac prems 1);
    3.32 -qed "Suc_RepI";
    3.33 -
    3.34 -(*** Induction ***)
    3.35 -
    3.36 -val major::prems = goal Nat.thy
    3.37 -    "[| i: Nat;  P(Zero_Rep);   \
    3.38 -\       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
    3.39 -by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
    3.40 -by (fast_tac (!claset addIs prems) 1);
    3.41 -qed "Nat_induct";
    3.42 -
    3.43 -val prems = goalw Nat.thy [Zero_def,Suc_def]
    3.44 -    "[| P(0);   \
    3.45 -\       !!k. P(k) ==> P(Suc(k)) |]  ==> P(n)";
    3.46 -by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
    3.47 -by (rtac (Rep_Nat RS Nat_induct) 1);
    3.48 -by (REPEAT (ares_tac prems 1
    3.49 -     ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1));
    3.50 -qed "nat_induct";
    3.51 -
    3.52 -(*Perform induction on n. *)
    3.53 -fun nat_ind_tac a i = 
    3.54 -    EVERY [res_inst_tac [("n",a)] nat_induct i,
    3.55 -           rename_last_tac a ["1"] (i+1)];
    3.56 -
    3.57 -(*A special form of induction for reasoning about m<n and m-n*)
    3.58 -val prems = goal Nat.thy
    3.59 -    "[| !!x. P x 0;  \
    3.60 -\       !!y. P 0 (Suc y);  \
    3.61 -\       !!x y. [| P x y |] ==> P (Suc x) (Suc y)  \
    3.62 -\    |] ==> P m n";
    3.63 -by (res_inst_tac [("x","m")] spec 1);
    3.64 -by (nat_ind_tac "n" 1);
    3.65 -by (rtac allI 2);
    3.66 -by (nat_ind_tac "x" 2);
    3.67 -by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1));
    3.68 -qed "diff_induct";
    3.69 -
    3.70 -(*Case analysis on the natural numbers*)
    3.71 -val prems = goal Nat.thy 
    3.72 -    "[| n=0 ==> P;  !!x. n = Suc(x) ==> P |] ==> P";
    3.73 -by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1);
    3.74 -by (fast_tac (!claset addSEs prems) 1);
    3.75 -by (nat_ind_tac "n" 1);
    3.76 -by (rtac (refl RS disjI1) 1);
    3.77 -by (Fast_tac 1);
    3.78 -qed "natE";
    3.79 -
    3.80 -(*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    3.81 -
    3.82 -(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),
    3.83 -  since we assume the isomorphism equations will one day be given by Isabelle*)
    3.84 -
    3.85 -goal Nat.thy "inj(Rep_Nat)";
    3.86 -by (rtac inj_inverseI 1);
    3.87 -by (rtac Rep_Nat_inverse 1);
    3.88 -qed "inj_Rep_Nat";
    3.89 -
    3.90 -goal Nat.thy "inj_onto Abs_Nat Nat";
    3.91 -by (rtac inj_onto_inverseI 1);
    3.92 -by (etac Abs_Nat_inverse 1);
    3.93 -qed "inj_onto_Abs_Nat";
    3.94 -
    3.95 -(*** Distinctness of constructors ***)
    3.96 -
    3.97 -goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0";
    3.98 -by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
    3.99 -by (rtac Suc_Rep_not_Zero_Rep 1);
   3.100 -by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
   3.101 -qed "Suc_not_Zero";
   3.102 -
   3.103 -bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
   3.104 -
   3.105 -AddIffs [Suc_not_Zero,Zero_not_Suc];
   3.106 -
   3.107 -bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
   3.108 -val Zero_neq_Suc = sym RS Suc_neq_Zero;
   3.109 -
   3.110 -(** Injectiveness of Suc **)
   3.111 -
   3.112 -goalw Nat.thy [Suc_def] "inj(Suc)";
   3.113 -by (rtac injI 1);
   3.114 -by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1);
   3.115 -by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
   3.116 -by (dtac (inj_Suc_Rep RS injD) 1);
   3.117 -by (etac (inj_Rep_Nat RS injD) 1);
   3.118 -qed "inj_Suc";
   3.119 -
   3.120 -val Suc_inject = inj_Suc RS injD;
   3.121 -
   3.122 -goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)";
   3.123 -by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
   3.124 -qed "Suc_Suc_eq";
   3.125 -
   3.126 -AddIffs [Suc_Suc_eq];
   3.127 -
   3.128 -goal Nat.thy "n ~= Suc(n)";
   3.129 -by (nat_ind_tac "n" 1);
   3.130 -by (ALLGOALS Asm_simp_tac);
   3.131 -qed "n_not_Suc_n";
   3.132 -
   3.133 -bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
   3.134 -
   3.135 -(*** nat_case -- the selection operator for nat ***)
   3.136 -
   3.137 -goalw Nat.thy [nat_case_def] "nat_case a f 0 = a";
   3.138 -by (fast_tac (!claset addIs [select_equality]) 1);
   3.139 -qed "nat_case_0";
   3.140 -
   3.141 -goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
   3.142 -by (fast_tac (!claset addIs [select_equality]) 1);
   3.143 -qed "nat_case_Suc";
   3.144 -
   3.145 -(** Introduction rules for 'pred_nat' **)
   3.146 -
   3.147 -goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
   3.148 -by (Fast_tac 1);
   3.149 -qed "pred_natI";
   3.150 -
   3.151 -val major::prems = goalw Nat.thy [pred_nat_def]
   3.152 -    "[| p : pred_nat;  !!x n. [| p = (n, Suc(n)) |] ==> R \
   3.153 -\    |] ==> R";
   3.154 -by (rtac (major RS CollectE) 1);
   3.155 -by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
   3.156 -qed "pred_natE";
   3.157 -
   3.158 -goalw Nat.thy [wf_def] "wf(pred_nat)";
   3.159 -by (strip_tac 1);
   3.160 -by (nat_ind_tac "x" 1);
   3.161 -by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
   3.162 -by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
   3.163 -qed "wf_pred_nat";
   3.164 -
   3.165 -
   3.166 -(*** nat_rec -- by wf recursion on pred_nat ***)
   3.167 -
   3.168 -(* The unrolling rule for nat_rec *)
   3.169 -goal Nat.thy
   3.170 -   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
   3.171 -  by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
   3.172 -bind_thm("nat_rec_unfold", wf_pred_nat RS 
   3.173 -                            ((result() RS eq_reflection) RS def_wfrec));
   3.174 -
   3.175 -(*---------------------------------------------------------------------------
   3.176 - * Old:
   3.177 - * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); 
   3.178 - *---------------------------------------------------------------------------*)
   3.179 -
   3.180 -(** conversion rules **)
   3.181 -
   3.182 -goal Nat.thy "nat_rec c h 0 = c";
   3.183 -by (rtac (nat_rec_unfold RS trans) 1);
   3.184 -by (simp_tac (!simpset addsimps [nat_case_0]) 1);
   3.185 -qed "nat_rec_0";
   3.186 -
   3.187 -goal Nat.thy "nat_rec c h (Suc n) = h n (nat_rec c h n)";
   3.188 -by (rtac (nat_rec_unfold RS trans) 1);
   3.189 -by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
   3.190 -qed "nat_rec_Suc";
   3.191 -
   3.192 -(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
   3.193 -val [rew] = goal Nat.thy
   3.194 -    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
   3.195 -by (rewtac rew);
   3.196 -by (rtac nat_rec_0 1);
   3.197 -qed "def_nat_rec_0";
   3.198 -
   3.199 -val [rew] = goal Nat.thy
   3.200 -    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
   3.201 -by (rewtac rew);
   3.202 -by (rtac nat_rec_Suc 1);
   3.203 -qed "def_nat_rec_Suc";
   3.204 -
   3.205 -fun nat_recs def =
   3.206 -      [standard (def RS def_nat_rec_0),
   3.207 -       standard (def RS def_nat_rec_Suc)];
   3.208 -
   3.209 -
   3.210 -(*** Basic properties of "less than" ***)
   3.211 -
   3.212 -(** Introduction properties **)
   3.213 -
   3.214 -val prems = goalw Nat.thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
   3.215 -by (rtac (trans_trancl RS transD) 1);
   3.216 -by (resolve_tac prems 1);
   3.217 -by (resolve_tac prems 1);
   3.218 -qed "less_trans";
   3.219 -
   3.220 -goalw Nat.thy [less_def] "n < Suc(n)";
   3.221 -by (rtac (pred_natI RS r_into_trancl) 1);
   3.222 -qed "lessI";
   3.223 -AddIffs [lessI];
   3.224 -
   3.225 -(* i<j ==> i<Suc(j) *)
   3.226 -val less_SucI = lessI RSN (2, less_trans);
   3.227 -
   3.228 -goal Nat.thy "0 < Suc(n)";
   3.229 -by (nat_ind_tac "n" 1);
   3.230 -by (rtac lessI 1);
   3.231 -by (etac less_trans 1);
   3.232 -by (rtac lessI 1);
   3.233 -qed "zero_less_Suc";
   3.234 -AddIffs [zero_less_Suc];
   3.235 -
   3.236 -(** Elimination properties **)
   3.237 -
   3.238 -val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
   3.239 -by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
   3.240 -qed "less_not_sym";
   3.241 -
   3.242 -(* [| n<m; m<n |] ==> R *)
   3.243 -bind_thm ("less_asym", (less_not_sym RS notE));
   3.244 -
   3.245 -goalw Nat.thy [less_def] "~ n<(n::nat)";
   3.246 -by (rtac notI 1);
   3.247 -by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
   3.248 -qed "less_not_refl";
   3.249 -
   3.250 -(* n<n ==> R *)
   3.251 -bind_thm ("less_irrefl", (less_not_refl RS notE));
   3.252 -
   3.253 -goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
   3.254 -by (fast_tac (!claset addEs [less_irrefl]) 1);
   3.255 -qed "less_not_refl2";
   3.256 -
   3.257 -
   3.258 -val major::prems = goalw Nat.thy [less_def]
   3.259 -    "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   3.260 -\    |] ==> P";
   3.261 -by (rtac (major RS tranclE) 1);
   3.262 -by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
   3.263 -                  eresolve_tac (prems@[pred_natE, Pair_inject])));
   3.264 -by (rtac refl 1);
   3.265 -qed "lessE";
   3.266 -
   3.267 -goal Nat.thy "~ n<0";
   3.268 -by (rtac notI 1);
   3.269 -by (etac lessE 1);
   3.270 -by (etac Zero_neq_Suc 1);
   3.271 -by (etac Zero_neq_Suc 1);
   3.272 -qed "not_less0";
   3.273 -
   3.274 -AddIffs [not_less0];
   3.275 -
   3.276 -(* n<0 ==> R *)
   3.277 -bind_thm ("less_zeroE", not_less0 RS notE);
   3.278 -
   3.279 -val [major,less,eq] = goal Nat.thy
   3.280 -    "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
   3.281 -by (rtac (major RS lessE) 1);
   3.282 -by (rtac eq 1);
   3.283 -by (Fast_tac 1);
   3.284 -by (rtac less 1);
   3.285 -by (Fast_tac 1);
   3.286 -qed "less_SucE";
   3.287 -
   3.288 -goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
   3.289 -by (fast_tac (!claset addSIs [lessI]
   3.290 -                      addEs  [less_trans, less_SucE]) 1);
   3.291 -qed "less_Suc_eq";
   3.292 -
   3.293 -val prems = goal Nat.thy "m<n ==> n ~= 0";
   3.294 -by (res_inst_tac [("n","n")] natE 1);
   3.295 -by (cut_facts_tac prems 1);
   3.296 -by (ALLGOALS Asm_full_simp_tac);
   3.297 -qed "gr_implies_not0";
   3.298 -Addsimps [gr_implies_not0];
   3.299 -
   3.300 -qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [
   3.301 -        rtac iffI 1,
   3.302 -        etac gr_implies_not0 1,
   3.303 -        rtac natE 1,
   3.304 -        contr_tac 1,
   3.305 -        etac ssubst 1,
   3.306 -        rtac zero_less_Suc 1]);
   3.307 -
   3.308 -(** Inductive (?) properties **)
   3.309 -
   3.310 -val [prem] = goal Nat.thy "Suc(m) < n ==> m<n";
   3.311 -by (rtac (prem RS rev_mp) 1);
   3.312 -by (nat_ind_tac "n" 1);
   3.313 -by (ALLGOALS (fast_tac (!claset addSIs [lessI RS less_SucI]
   3.314 -                                addEs  [less_trans, lessE])));
   3.315 -qed "Suc_lessD";
   3.316 -
   3.317 -val [major,minor] = goal Nat.thy 
   3.318 -    "[| Suc(i)<k;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   3.319 -\    |] ==> P";
   3.320 -by (rtac (major RS lessE) 1);
   3.321 -by (etac (lessI RS minor) 1);
   3.322 -by (etac (Suc_lessD RS minor) 1);
   3.323 -by (assume_tac 1);
   3.324 -qed "Suc_lessE";
   3.325 -
   3.326 -goal Nat.thy "!!m n. Suc(m) < Suc(n) ==> m<n";
   3.327 -by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
   3.328 -qed "Suc_less_SucD";
   3.329 -
   3.330 -goal Nat.thy "!!m n. m<n ==> Suc(m) < Suc(n)";
   3.331 -by (etac rev_mp 1);
   3.332 -by (nat_ind_tac "n" 1);
   3.333 -by (ALLGOALS (fast_tac (!claset addSIs [lessI]
   3.334 -                                addEs  [less_trans, lessE])));
   3.335 -qed "Suc_mono";
   3.336 -
   3.337 -
   3.338 -goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
   3.339 -by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
   3.340 -qed "Suc_less_eq";
   3.341 -Addsimps [Suc_less_eq];
   3.342 -
   3.343 -goal Nat.thy "~(Suc(n) < n)";
   3.344 -by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
   3.345 -qed "not_Suc_n_less_n";
   3.346 -Addsimps [not_Suc_n_less_n];
   3.347 +goal thy "min 0 n = 0";
   3.348 +br min_leastL 1;
   3.349 +by(trans_tac 1);
   3.350 +qed "min_0L";
   3.351  
   3.352 -goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
   3.353 -by (nat_ind_tac "k" 1);
   3.354 -by (ALLGOALS (asm_simp_tac (!simpset)));
   3.355 -by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   3.356 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
   3.357 -qed_spec_mp "less_trans_Suc";
   3.358 -
   3.359 -(*"Less than" is a linear ordering*)
   3.360 -goal Nat.thy "m<n | m=n | n<(m::nat)";
   3.361 -by (nat_ind_tac "m" 1);
   3.362 -by (nat_ind_tac "n" 1);
   3.363 -by (rtac (refl RS disjI1 RS disjI2) 1);
   3.364 -by (rtac (zero_less_Suc RS disjI1) 1);
   3.365 -by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
   3.366 -qed "less_linear";
   3.367 -
   3.368 -qed_goal "nat_less_cases" Nat.thy 
   3.369 -   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
   3.370 -( fn prems =>
   3.371 -        [
   3.372 -        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
   3.373 -        (etac disjE 2),
   3.374 -        (etac (hd (tl (tl prems))) 1),
   3.375 -        (etac (sym RS hd (tl prems)) 1),
   3.376 -        (etac (hd prems) 1)
   3.377 -        ]);
   3.378 -
   3.379 -(*Can be used with less_Suc_eq to get n=m | n<m *)
   3.380 -goal Nat.thy "(~ m < n) = (n < Suc(m))";
   3.381 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   3.382 -by (ALLGOALS Asm_simp_tac);
   3.383 -qed "not_less_eq";
   3.384 -
   3.385 -(*Complete induction, aka course-of-values induction*)
   3.386 -val prems = goalw Nat.thy [less_def]
   3.387 -    "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
   3.388 -by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
   3.389 -by (eresolve_tac prems 1);
   3.390 -qed "less_induct";
   3.391 -
   3.392 -qed_goal "nat_induct2" Nat.thy 
   3.393 -"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
   3.394 -	cut_facts_tac prems 1,
   3.395 -	rtac less_induct 1,
   3.396 -	res_inst_tac [("n","n")] natE 1,
   3.397 -	 hyp_subst_tac 1,
   3.398 -	 atac 1,
   3.399 -	hyp_subst_tac 1,
   3.400 -	res_inst_tac [("n","x")] natE 1,
   3.401 -	 hyp_subst_tac 1,
   3.402 -	 atac 1,
   3.403 -	hyp_subst_tac 1,
   3.404 -	resolve_tac prems 1,
   3.405 -	dtac spec 1,
   3.406 -	etac mp 1,
   3.407 -	rtac (lessI RS less_trans) 1,
   3.408 -	rtac (lessI RS Suc_mono) 1]);
   3.409 -
   3.410 -(*** Properties of <= ***)
   3.411 -
   3.412 -goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)";
   3.413 -by (rtac not_less_eq 1);
   3.414 -qed "le_eq_less_Suc";
   3.415 -
   3.416 -goalw Nat.thy [le_def] "0 <= n";
   3.417 -by (rtac not_less0 1);
   3.418 -qed "le0";
   3.419 -
   3.420 -goalw Nat.thy [le_def] "~ Suc n <= n";
   3.421 -by (Simp_tac 1);
   3.422 -qed "Suc_n_not_le_n";
   3.423 -
   3.424 -goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
   3.425 -by (nat_ind_tac "i" 1);
   3.426 -by (ALLGOALS Asm_simp_tac);
   3.427 -qed "le_0_eq";
   3.428 -
   3.429 -Addsimps [less_not_refl,
   3.430 -          (*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
   3.431 -          Suc_n_not_le_n,
   3.432 -          n_not_Suc_n, Suc_n_not_n,
   3.433 -          nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   3.434 -
   3.435 -(*
   3.436 -goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
   3.437 -by (stac (less_Suc_eq RS sym) 1);
   3.438 -by (rtac Suc_less_eq 1);
   3.439 -qed "Suc_le_eq";
   3.440 -
   3.441 -this could make the simpset (with less_Suc_eq added again) more confluent,
   3.442 -but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
   3.443 -*)
   3.444 -
   3.445 -(*Prevents simplification of f and g: much faster*)
   3.446 -qed_goal "nat_case_weak_cong" Nat.thy
   3.447 -  "m=n ==> nat_case a f m = nat_case a f n"
   3.448 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   3.449 -
   3.450 -qed_goal "nat_rec_weak_cong" Nat.thy
   3.451 -  "m=n ==> nat_rec a f m = nat_rec a f n"
   3.452 -  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   3.453 -
   3.454 -qed_goal "expand_nat_case" Nat.thy
   3.455 -  "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
   3.456 -  (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
   3.457 -
   3.458 -val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
   3.459 -by (resolve_tac prems 1);
   3.460 -qed "leI";
   3.461 -
   3.462 -val prems = goalw Nat.thy [le_def] "m<=n ==> ~ n < (m::nat)";
   3.463 -by (resolve_tac prems 1);
   3.464 -qed "leD";
   3.465 -
   3.466 -val leE = make_elim leD;
   3.467 -
   3.468 -goal Nat.thy "(~n<m) = (m<=(n::nat))";
   3.469 -by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
   3.470 -qed "not_less_iff_le";
   3.471 -
   3.472 -goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   3.473 -by (Fast_tac 1);
   3.474 -qed "not_leE";
   3.475 -
   3.476 -goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   3.477 -by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   3.478 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   3.479 -qed "lessD";
   3.480 -
   3.481 -goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
   3.482 -by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   3.483 -qed "Suc_leD";
   3.484 -
   3.485 -(* stronger version of Suc_leD *)
   3.486 -goalw Nat.thy [le_def] 
   3.487 -        "!!m. Suc m <= n ==> m < n";
   3.488 -by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   3.489 -by (cut_facts_tac [less_linear] 1);
   3.490 -by (Fast_tac 1);
   3.491 -qed "Suc_le_lessD";
   3.492 -
   3.493 -goal Nat.thy "(Suc m <= n) = (m < n)";
   3.494 -by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   3.495 -qed "Suc_le_eq";
   3.496 -
   3.497 -goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
   3.498 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
   3.499 -qed "le_SucI";
   3.500 -Addsimps[le_SucI];
   3.501 -
   3.502 -bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
   3.503 -
   3.504 -goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
   3.505 -by (fast_tac (!claset addEs [less_asym]) 1);
   3.506 -qed "less_imp_le";
   3.507 -
   3.508 -goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
   3.509 -by (cut_facts_tac [less_linear] 1);
   3.510 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   3.511 -qed "le_imp_less_or_eq";
   3.512 -
   3.513 -goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
   3.514 -by (cut_facts_tac [less_linear] 1);
   3.515 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   3.516 -by (flexflex_tac);
   3.517 -qed "less_or_eq_imp_le";
   3.518 +goal thy "min n 0 = 0";
   3.519 +br min_leastR 1;
   3.520 +by(trans_tac 1);
   3.521 +qed "min_0R";
   3.522  
   3.523 -goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)";
   3.524 -by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
   3.525 -qed "le_eq_less_or_eq";
   3.526 -
   3.527 -goal Nat.thy "n <= (n::nat)";
   3.528 -by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   3.529 -qed "le_refl";
   3.530 -
   3.531 -val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
   3.532 -by (dtac le_imp_less_or_eq 1);
   3.533 -by (fast_tac (!claset addIs [less_trans]) 1);
   3.534 -qed "le_less_trans";
   3.535 -
   3.536 -goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
   3.537 -by (dtac le_imp_less_or_eq 1);
   3.538 -by (fast_tac (!claset addIs [less_trans]) 1);
   3.539 -qed "less_le_trans";
   3.540 -
   3.541 -goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
   3.542 -by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   3.543 -          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
   3.544 -qed "le_trans";
   3.545 -
   3.546 -val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
   3.547 -by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   3.548 -          fast_tac (!claset addEs [less_irrefl,less_asym])]);
   3.549 -qed "le_anti_sym";
   3.550 -
   3.551 -goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
   3.552 -by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   3.553 -qed "Suc_le_mono";
   3.554 -
   3.555 -AddIffs [le_refl,Suc_le_mono];
   3.556 -
   3.557 -
   3.558 -(** LEAST -- the least number operator **)
   3.559 -
   3.560 -val [prem1,prem2] = goalw Nat.thy [Least_def]
   3.561 -    "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
   3.562 -by (rtac select_equality 1);
   3.563 -by (fast_tac (!claset addSIs [prem1,prem2]) 1);
   3.564 -by (cut_facts_tac [less_linear] 1);
   3.565 -by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
   3.566 -qed "Least_equality";
   3.567 -
   3.568 -val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))";
   3.569 -by (rtac (prem RS rev_mp) 1);
   3.570 -by (res_inst_tac [("n","k")] less_induct 1);
   3.571 -by (rtac impI 1);
   3.572 -by (rtac classical 1);
   3.573 -by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   3.574 -by (assume_tac 1);
   3.575 -by (assume_tac 2);
   3.576 -by (Fast_tac 1);
   3.577 -qed "LeastI";
   3.578 -
   3.579 -(*Proof is almost identical to the one above!*)
   3.580 -val [prem] = goal Nat.thy "P(k) ==> (LEAST x.P(x)) <= k";
   3.581 -by (rtac (prem RS rev_mp) 1);
   3.582 -by (res_inst_tac [("n","k")] less_induct 1);
   3.583 -by (rtac impI 1);
   3.584 -by (rtac classical 1);
   3.585 -by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   3.586 -by (assume_tac 1);
   3.587 -by (rtac le_refl 2);
   3.588 -by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
   3.589 -qed "Least_le";
   3.590 -
   3.591 -val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)";
   3.592 -by (rtac notI 1);
   3.593 -by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
   3.594 -by (rtac prem 1);
   3.595 -qed "not_less_Least";
   3.596 +goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
   3.597 +by(split_tac [expand_if] 1);
   3.598 +by(Simp_tac 1);
   3.599 +qed "min_Suc_Suc";
   3.600  
   3.601 -qed_goalw "Least_Suc" Nat.thy [Least_def]
   3.602 - "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   3.603 - (fn _ => [
   3.604 -        rtac select_equality 1,
   3.605 -        fold_goals_tac [Least_def],
   3.606 -        safe_tac (!claset addSEs [LeastI]),
   3.607 -        res_inst_tac [("n","j")] natE 1,
   3.608 -        Fast_tac 1,
   3.609 -        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   3.610 -        res_inst_tac [("n","k")] natE 1,
   3.611 -        Fast_tac 1,
   3.612 -        hyp_subst_tac 1,
   3.613 -        rewtac Least_def,
   3.614 -        rtac (select_equality RS arg_cong RS sym) 1,
   3.615 -        safe_tac (!claset),
   3.616 -        dtac Suc_mono 1,
   3.617 -        Fast_tac 1,
   3.618 -        cut_facts_tac [less_linear] 1,
   3.619 -        safe_tac (!claset),
   3.620 -        atac 2,
   3.621 -        Fast_tac 2,
   3.622 -        dtac Suc_mono 1,
   3.623 -        Fast_tac 1]);
   3.624 -
   3.625 -
   3.626 -(*** Instantiation of transitivity prover ***)
   3.627 -
   3.628 -structure Less_Arith =
   3.629 -struct
   3.630 -val nat_leI = leI;
   3.631 -val nat_leD = leD;
   3.632 -val lessI = lessI;
   3.633 -val zero_less_Suc = zero_less_Suc;
   3.634 -val less_reflE = less_irrefl;
   3.635 -val less_zeroE = less_zeroE;
   3.636 -val less_incr = Suc_mono;
   3.637 -val less_decr = Suc_less_SucD;
   3.638 -val less_incr_rhs = Suc_mono RS Suc_lessD;
   3.639 -val less_decr_lhs = Suc_lessD;
   3.640 -val less_trans_Suc = less_trans_Suc;
   3.641 -val leI = lessD RS (Suc_le_mono RS iffD1);
   3.642 -val not_lessI = leI RS leD
   3.643 -val not_leI = prove_goal Nat.thy "!!m::nat. n < m ==> ~ m <= n"
   3.644 -  (fn _ => [etac swap2 1, etac leD 1]);
   3.645 -val eqI = prove_goal Nat.thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
   3.646 -  (fn _ => [etac less_SucE 1,
   3.647 -            fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
   3.648 -                             addDs [less_trans_Suc]) 1,
   3.649 -            atac 1]);
   3.650 -val leD = le_eq_less_Suc RS iffD1;
   3.651 -val not_lessD = nat_leI RS leD;
   3.652 -val not_leD = not_leE
   3.653 -val eqD1 = prove_goal Nat.thy  "!!n. m = n ==> m < Suc n"
   3.654 - (fn _ => [etac subst 1, rtac lessI 1]);
   3.655 -val eqD2 = sym RS eqD1;
   3.656 -
   3.657 -fun is_zero(t) =  t = Const("0",Type("nat",[]));
   3.658 -
   3.659 -fun nnb T = T = Type("fun",[Type("nat",[]),
   3.660 -                            Type("fun",[Type("nat",[]),
   3.661 -                                        Type("bool",[])])])
   3.662 -
   3.663 -fun decomp_Suc(Const("Suc",_)$t) = let val (a,i) = decomp_Suc t in (a,i+1) end
   3.664 -  | decomp_Suc t = (t,0);
   3.665 -
   3.666 -fun decomp2(rel,T,lhs,rhs) =
   3.667 -  if not(nnb T) then None else
   3.668 -  let val (x,i) = decomp_Suc lhs
   3.669 -      val (y,j) = decomp_Suc rhs
   3.670 -  in case rel of
   3.671 -       "op <"  => Some(x,i,"<",y,j)
   3.672 -     | "op <=" => Some(x,i,"<=",y,j)
   3.673 -     | "op ="  => Some(x,i,"=",y,j)
   3.674 -     | _       => None
   3.675 -  end;
   3.676 -
   3.677 -fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   3.678 -  | negate None = None;
   3.679 -
   3.680 -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   3.681 -  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
   3.682 -      negate(decomp2(rel,T,lhs,rhs))
   3.683 -  | decomp _ = None
   3.684 -
   3.685 -end;
   3.686 -
   3.687 -structure Trans_Tac = Trans_Tac_Fun(Less_Arith);
   3.688 -
   3.689 -open Trans_Tac;
   3.690 -
   3.691 -(*** eliminates ~= in premises, which trans_tac cannot deal with ***)
   3.692 -qed_goal "nat_neqE" Nat.thy
   3.693 -  "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
   3.694 -  (fn major::prems => [cut_facts_tac [less_linear] 1,
   3.695 -                       REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
   3.696 +Addsimps [min_0L,min_0R,min_Suc_Suc];
     4.1 --- a/src/HOL/Nat.thy	Wed Feb 12 15:43:50 1997 +0100
     4.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 18:53:59 1997 +0100
     4.3 @@ -1,82 +1,13 @@
     4.4  (*  Title:      HOL/Nat.thy
     4.5      ID:         $Id$
     4.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4.7 -    Copyright   1991  University of Cambridge
     4.8 +    Author:     Tobias Nipkow
     4.9 +    Copyright   1997 TU Muenchen
    4.10  
    4.11 -Definition of types ind and nat.
    4.12 -
    4.13 -Type nat is defined as a set Nat over type ind.
    4.14 +Nat is a partial order
    4.15  *)
    4.16  
    4.17 -Nat = WF +
    4.18 -
    4.19 -(** type ind **)
    4.20 -
    4.21 -types
    4.22 -  ind
    4.23 -
    4.24 -arities
    4.25 -  ind :: term
    4.26 -
    4.27 -consts
    4.28 -  Zero_Rep      :: ind
    4.29 -  Suc_Rep       :: ind => ind
    4.30 -
    4.31 -rules
    4.32 -  (*the axiom of infinity in 2 parts*)
    4.33 -  inj_Suc_Rep           "inj(Suc_Rep)"
    4.34 -  Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
    4.35 -
    4.36 -
    4.37 -
    4.38 -(** type nat **)
    4.39 -
    4.40 -(* type definition *)
    4.41 -
    4.42 -typedef (Nat)
    4.43 -  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    4.44 -
    4.45 -instance
    4.46 -  nat :: ord
    4.47 -
    4.48 -
    4.49 -(* abstract constants and syntax *)
    4.50 +Nat = NatDef +
    4.51  
    4.52 -consts
    4.53 -  "0"       :: nat                ("0")
    4.54 -  Suc       :: nat => nat
    4.55 -  nat_case  :: ['a, nat => 'a, nat] => 'a
    4.56 -  pred_nat  :: "(nat * nat) set"
    4.57 -  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
    4.58 -
    4.59 -  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
    4.60 -
    4.61 -syntax
    4.62 -  "1"       :: nat                ("1")
    4.63 -  "2"       :: nat                ("2")
    4.64 -
    4.65 -translations
    4.66 -   "1"  == "Suc 0"
    4.67 -   "2"  == "Suc 1"
    4.68 -  "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
    4.69 -
    4.70 -
    4.71 -defs
    4.72 -  Zero_def      "0 == Abs_Nat(Zero_Rep)"
    4.73 -  Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    4.74 -
    4.75 -  (*nat operations and recursion*)
    4.76 -  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    4.77 -                                        & (!x. n=Suc x --> z=f(x))"
    4.78 -  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
    4.79 -
    4.80 -  less_def      "m<n == (m,n):trancl(pred_nat)"
    4.81 -
    4.82 -  le_def        "m<=(n::nat) == ~(n<m)"
    4.83 -
    4.84 -  nat_rec_def   "nat_rec c d ==
    4.85 -                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    4.86 -  (*least number operator*)
    4.87 -  Least_def     "Least P == @k. P(k) & (ALL j. j<k --> ~P(j))"
    4.88 +instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    4.89  
    4.90  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/NatDef.ML	Wed Feb 12 18:53:59 1997 +0100
     5.3 @@ -0,0 +1,684 @@
     5.4 +(*  Title:      HOL/NatDef.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     5.7 +    Copyright   1991  University of Cambridge
     5.8 +*)
     5.9 +
    5.10 +goal thy "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";
    5.11 +by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    5.12 +qed "Nat_fun_mono";
    5.13 +
    5.14 +val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski);
    5.15 +
    5.16 +(* Zero is a natural number -- this also justifies the type definition*)
    5.17 +goal thy "Zero_Rep: Nat";
    5.18 +by (stac Nat_unfold 1);
    5.19 +by (rtac (singletonI RS UnI1) 1);
    5.20 +qed "Zero_RepI";
    5.21 +
    5.22 +val prems = goal thy "i: Nat ==> Suc_Rep(i) : Nat";
    5.23 +by (stac Nat_unfold 1);
    5.24 +by (rtac (imageI RS UnI2) 1);
    5.25 +by (resolve_tac prems 1);
    5.26 +qed "Suc_RepI";
    5.27 +
    5.28 +(*** Induction ***)
    5.29 +
    5.30 +val major::prems = goal thy
    5.31 +    "[| i: Nat;  P(Zero_Rep);   \
    5.32 +\       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
    5.33 +by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
    5.34 +by (fast_tac (!claset addIs prems) 1);
    5.35 +qed "Nat_induct";
    5.36 +
    5.37 +val prems = goalw thy [Zero_def,Suc_def]
    5.38 +    "[| P(0);   \
    5.39 +\       !!k. P(k) ==> P(Suc(k)) |]  ==> P(n)";
    5.40 +by (rtac (Rep_Nat_inverse RS subst) 1);   (*types force good instantiation*)
    5.41 +by (rtac (Rep_Nat RS Nat_induct) 1);
    5.42 +by (REPEAT (ares_tac prems 1
    5.43 +     ORELSE eresolve_tac [Abs_Nat_inverse RS subst] 1));
    5.44 +qed "nat_induct";
    5.45 +
    5.46 +(*Perform induction on n. *)
    5.47 +fun nat_ind_tac a i = 
    5.48 +    EVERY [res_inst_tac [("n",a)] nat_induct i,
    5.49 +           rename_last_tac a ["1"] (i+1)];
    5.50 +
    5.51 +(*A special form of induction for reasoning about m<n and m-n*)
    5.52 +val prems = goal thy
    5.53 +    "[| !!x. P x 0;  \
    5.54 +\       !!y. P 0 (Suc y);  \
    5.55 +\       !!x y. [| P x y |] ==> P (Suc x) (Suc y)  \
    5.56 +\    |] ==> P m n";
    5.57 +by (res_inst_tac [("x","m")] spec 1);
    5.58 +by (nat_ind_tac "n" 1);
    5.59 +by (rtac allI 2);
    5.60 +by (nat_ind_tac "x" 2);
    5.61 +by (REPEAT (ares_tac (prems@[allI]) 1 ORELSE etac spec 1));
    5.62 +qed "diff_induct";
    5.63 +
    5.64 +(*Case analysis on the natural numbers*)
    5.65 +val prems = goal thy 
    5.66 +    "[| n=0 ==> P;  !!x. n = Suc(x) ==> P |] ==> P";
    5.67 +by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1);
    5.68 +by (fast_tac (!claset addSEs prems) 1);
    5.69 +by (nat_ind_tac "n" 1);
    5.70 +by (rtac (refl RS disjI1) 1);
    5.71 +by (Fast_tac 1);
    5.72 +qed "natE";
    5.73 +
    5.74 +(*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    5.75 +
    5.76 +(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),
    5.77 +  since we assume the isomorphism equations will one day be given by Isabelle*)
    5.78 +
    5.79 +goal thy "inj(Rep_Nat)";
    5.80 +by (rtac inj_inverseI 1);
    5.81 +by (rtac Rep_Nat_inverse 1);
    5.82 +qed "inj_Rep_Nat";
    5.83 +
    5.84 +goal thy "inj_onto Abs_Nat Nat";
    5.85 +by (rtac inj_onto_inverseI 1);
    5.86 +by (etac Abs_Nat_inverse 1);
    5.87 +qed "inj_onto_Abs_Nat";
    5.88 +
    5.89 +(*** Distinctness of constructors ***)
    5.90 +
    5.91 +goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0";
    5.92 +by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
    5.93 +by (rtac Suc_Rep_not_Zero_Rep 1);
    5.94 +by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
    5.95 +qed "Suc_not_Zero";
    5.96 +
    5.97 +bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
    5.98 +
    5.99 +AddIffs [Suc_not_Zero,Zero_not_Suc];
   5.100 +
   5.101 +bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
   5.102 +val Zero_neq_Suc = sym RS Suc_neq_Zero;
   5.103 +
   5.104 +(** Injectiveness of Suc **)
   5.105 +
   5.106 +goalw thy [Suc_def] "inj(Suc)";
   5.107 +by (rtac injI 1);
   5.108 +by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1);
   5.109 +by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
   5.110 +by (dtac (inj_Suc_Rep RS injD) 1);
   5.111 +by (etac (inj_Rep_Nat RS injD) 1);
   5.112 +qed "inj_Suc";
   5.113 +
   5.114 +val Suc_inject = inj_Suc RS injD;
   5.115 +
   5.116 +goal thy "(Suc(m)=Suc(n)) = (m=n)";
   5.117 +by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
   5.118 +qed "Suc_Suc_eq";
   5.119 +
   5.120 +AddIffs [Suc_Suc_eq];
   5.121 +
   5.122 +goal thy "n ~= Suc(n)";
   5.123 +by (nat_ind_tac "n" 1);
   5.124 +by (ALLGOALS Asm_simp_tac);
   5.125 +qed "n_not_Suc_n";
   5.126 +
   5.127 +bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
   5.128 +
   5.129 +(*** nat_case -- the selection operator for nat ***)
   5.130 +
   5.131 +goalw thy [nat_case_def] "nat_case a f 0 = a";
   5.132 +by (fast_tac (!claset addIs [select_equality]) 1);
   5.133 +qed "nat_case_0";
   5.134 +
   5.135 +goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
   5.136 +by (fast_tac (!claset addIs [select_equality]) 1);
   5.137 +qed "nat_case_Suc";
   5.138 +
   5.139 +(** Introduction rules for 'pred_nat' **)
   5.140 +
   5.141 +goalw thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
   5.142 +by (Fast_tac 1);
   5.143 +qed "pred_natI";
   5.144 +
   5.145 +val major::prems = goalw thy [pred_nat_def]
   5.146 +    "[| p : pred_nat;  !!x n. [| p = (n, Suc(n)) |] ==> R \
   5.147 +\    |] ==> R";
   5.148 +by (rtac (major RS CollectE) 1);
   5.149 +by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
   5.150 +qed "pred_natE";
   5.151 +
   5.152 +goalw thy [wf_def] "wf(pred_nat)";
   5.153 +by (strip_tac 1);
   5.154 +by (nat_ind_tac "x" 1);
   5.155 +by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
   5.156 +by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
   5.157 +qed "wf_pred_nat";
   5.158 +
   5.159 +
   5.160 +(*** nat_rec -- by wf recursion on pred_nat ***)
   5.161 +
   5.162 +(* The unrolling rule for nat_rec *)
   5.163 +goal thy
   5.164 +   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
   5.165 +  by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
   5.166 +bind_thm("nat_rec_unfold", wf_pred_nat RS 
   5.167 +                            ((result() RS eq_reflection) RS def_wfrec));
   5.168 +
   5.169 +(*---------------------------------------------------------------------------
   5.170 + * Old:
   5.171 + * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); 
   5.172 + *---------------------------------------------------------------------------*)
   5.173 +
   5.174 +(** conversion rules **)
   5.175 +
   5.176 +goal thy "nat_rec c h 0 = c";
   5.177 +by (rtac (nat_rec_unfold RS trans) 1);
   5.178 +by (simp_tac (!simpset addsimps [nat_case_0]) 1);
   5.179 +qed "nat_rec_0";
   5.180 +
   5.181 +goal thy "nat_rec c h (Suc n) = h n (nat_rec c h n)";
   5.182 +by (rtac (nat_rec_unfold RS trans) 1);
   5.183 +by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
   5.184 +qed "nat_rec_Suc";
   5.185 +
   5.186 +(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
   5.187 +val [rew] = goal thy
   5.188 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
   5.189 +by (rewtac rew);
   5.190 +by (rtac nat_rec_0 1);
   5.191 +qed "def_nat_rec_0";
   5.192 +
   5.193 +val [rew] = goal thy
   5.194 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
   5.195 +by (rewtac rew);
   5.196 +by (rtac nat_rec_Suc 1);
   5.197 +qed "def_nat_rec_Suc";
   5.198 +
   5.199 +fun nat_recs def =
   5.200 +      [standard (def RS def_nat_rec_0),
   5.201 +       standard (def RS def_nat_rec_Suc)];
   5.202 +
   5.203 +
   5.204 +(*** Basic properties of "less than" ***)
   5.205 +
   5.206 +(** Introduction properties **)
   5.207 +
   5.208 +val prems = goalw thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
   5.209 +by (rtac (trans_trancl RS transD) 1);
   5.210 +by (resolve_tac prems 1);
   5.211 +by (resolve_tac prems 1);
   5.212 +qed "less_trans";
   5.213 +
   5.214 +goalw thy [less_def] "n < Suc(n)";
   5.215 +by (rtac (pred_natI RS r_into_trancl) 1);
   5.216 +qed "lessI";
   5.217 +AddIffs [lessI];
   5.218 +
   5.219 +(* i<j ==> i<Suc(j) *)
   5.220 +bind_thm("less_SucI", lessI RSN (2, less_trans));
   5.221 +Addsimps [less_SucI];
   5.222 +
   5.223 +goal thy "0 < Suc(n)";
   5.224 +by (nat_ind_tac "n" 1);
   5.225 +by (rtac lessI 1);
   5.226 +by (etac less_trans 1);
   5.227 +by (rtac lessI 1);
   5.228 +qed "zero_less_Suc";
   5.229 +AddIffs [zero_less_Suc];
   5.230 +
   5.231 +(** Elimination properties **)
   5.232 +
   5.233 +val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
   5.234 +by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
   5.235 +qed "less_not_sym";
   5.236 +
   5.237 +(* [| n<m; m<n |] ==> R *)
   5.238 +bind_thm ("less_asym", (less_not_sym RS notE));
   5.239 +
   5.240 +goalw thy [less_def] "~ n<(n::nat)";
   5.241 +by (rtac notI 1);
   5.242 +by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
   5.243 +qed "less_not_refl";
   5.244 +
   5.245 +(* n<n ==> R *)
   5.246 +bind_thm ("less_irrefl", (less_not_refl RS notE));
   5.247 +
   5.248 +goal thy "!!m. n<m ==> m ~= (n::nat)";
   5.249 +by (fast_tac (!claset addEs [less_irrefl]) 1);
   5.250 +qed "less_not_refl2";
   5.251 +
   5.252 +
   5.253 +val major::prems = goalw thy [less_def]
   5.254 +    "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   5.255 +\    |] ==> P";
   5.256 +by (rtac (major RS tranclE) 1);
   5.257 +by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
   5.258 +                  eresolve_tac (prems@[pred_natE, Pair_inject])));
   5.259 +by (rtac refl 1);
   5.260 +qed "lessE";
   5.261 +
   5.262 +goal thy "~ n<0";
   5.263 +by (rtac notI 1);
   5.264 +by (etac lessE 1);
   5.265 +by (etac Zero_neq_Suc 1);
   5.266 +by (etac Zero_neq_Suc 1);
   5.267 +qed "not_less0";
   5.268 +
   5.269 +AddIffs [not_less0];
   5.270 +
   5.271 +(* n<0 ==> R *)
   5.272 +bind_thm ("less_zeroE", not_less0 RS notE);
   5.273 +
   5.274 +val [major,less,eq] = goal thy
   5.275 +    "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
   5.276 +by (rtac (major RS lessE) 1);
   5.277 +by (rtac eq 1);
   5.278 +by (Fast_tac 1);
   5.279 +by (rtac less 1);
   5.280 +by (Fast_tac 1);
   5.281 +qed "less_SucE";
   5.282 +
   5.283 +goal thy "(m < Suc(n)) = (m < n | m = n)";
   5.284 +by (fast_tac (!claset addSIs [lessI]
   5.285 +                      addEs  [less_trans, less_SucE]) 1);
   5.286 +qed "less_Suc_eq";
   5.287 +
   5.288 +val prems = goal thy "m<n ==> n ~= 0";
   5.289 +by (res_inst_tac [("n","n")] natE 1);
   5.290 +by (cut_facts_tac prems 1);
   5.291 +by (ALLGOALS Asm_full_simp_tac);
   5.292 +qed "gr_implies_not0";
   5.293 +Addsimps [gr_implies_not0];
   5.294 +
   5.295 +qed_goal "zero_less_eq" thy "0 < n = (n ~= 0)" (fn _ => [
   5.296 +        rtac iffI 1,
   5.297 +        etac gr_implies_not0 1,
   5.298 +        rtac natE 1,
   5.299 +        contr_tac 1,
   5.300 +        etac ssubst 1,
   5.301 +        rtac zero_less_Suc 1]);
   5.302 +
   5.303 +(** Inductive (?) properties **)
   5.304 +
   5.305 +val [prem] = goal thy "Suc(m) < n ==> m<n";
   5.306 +by (rtac (prem RS rev_mp) 1);
   5.307 +by (nat_ind_tac "n" 1);
   5.308 +by (ALLGOALS (fast_tac (!claset addSIs [lessI RS less_SucI]
   5.309 +                                addEs  [less_trans, lessE])));
   5.310 +qed "Suc_lessD";
   5.311 +
   5.312 +val [major,minor] = goal thy 
   5.313 +    "[| Suc(i)<k;  !!j. [| i<j;  k=Suc(j) |] ==> P \
   5.314 +\    |] ==> P";
   5.315 +by (rtac (major RS lessE) 1);
   5.316 +by (etac (lessI RS minor) 1);
   5.317 +by (etac (Suc_lessD RS minor) 1);
   5.318 +by (assume_tac 1);
   5.319 +qed "Suc_lessE";
   5.320 +
   5.321 +goal thy "!!m n. Suc(m) < Suc(n) ==> m<n";
   5.322 +by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
   5.323 +qed "Suc_less_SucD";
   5.324 +
   5.325 +goal thy "!!m n. m<n ==> Suc(m) < Suc(n)";
   5.326 +by (etac rev_mp 1);
   5.327 +by (nat_ind_tac "n" 1);
   5.328 +by (ALLGOALS (fast_tac (!claset addSIs [lessI]
   5.329 +                                addEs  [less_trans, lessE])));
   5.330 +qed "Suc_mono";
   5.331 +
   5.332 +
   5.333 +goal thy "(Suc(m) < Suc(n)) = (m<n)";
   5.334 +by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
   5.335 +qed "Suc_less_eq";
   5.336 +Addsimps [Suc_less_eq];
   5.337 +
   5.338 +goal thy "~(Suc(n) < n)";
   5.339 +by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
   5.340 +qed "not_Suc_n_less_n";
   5.341 +Addsimps [not_Suc_n_less_n];
   5.342 +
   5.343 +goal thy "!!i. i<j ==> j<k --> Suc i < k";
   5.344 +by (nat_ind_tac "k" 1);
   5.345 +by (ALLGOALS (asm_simp_tac (!simpset)));
   5.346 +by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.347 +by (fast_tac (!claset addDs [Suc_lessD]) 1);
   5.348 +qed_spec_mp "less_trans_Suc";
   5.349 +
   5.350 +(*"Less than" is a linear ordering*)
   5.351 +goal thy "m<n | m=n | n<(m::nat)";
   5.352 +by (nat_ind_tac "m" 1);
   5.353 +by (nat_ind_tac "n" 1);
   5.354 +by (rtac (refl RS disjI1 RS disjI2) 1);
   5.355 +by (rtac (zero_less_Suc RS disjI1) 1);
   5.356 +by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
   5.357 +qed "less_linear";
   5.358 +
   5.359 +qed_goal "nat_less_cases" thy 
   5.360 +   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
   5.361 +( fn prems =>
   5.362 +        [
   5.363 +        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
   5.364 +        (etac disjE 2),
   5.365 +        (etac (hd (tl (tl prems))) 1),
   5.366 +        (etac (sym RS hd (tl prems)) 1),
   5.367 +        (etac (hd prems) 1)
   5.368 +        ]);
   5.369 +
   5.370 +(*Can be used with less_Suc_eq to get n=m | n<m *)
   5.371 +goal thy "(~ m < n) = (n < Suc(m))";
   5.372 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   5.373 +by (ALLGOALS Asm_simp_tac);
   5.374 +qed "not_less_eq";
   5.375 +
   5.376 +(*Complete induction, aka course-of-values induction*)
   5.377 +val prems = goalw thy [less_def]
   5.378 +    "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
   5.379 +by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
   5.380 +by (eresolve_tac prems 1);
   5.381 +qed "less_induct";
   5.382 +
   5.383 +qed_goal "nat_induct2" thy 
   5.384 +"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
   5.385 +	cut_facts_tac prems 1,
   5.386 +	rtac less_induct 1,
   5.387 +	res_inst_tac [("n","n")] natE 1,
   5.388 +	 hyp_subst_tac 1,
   5.389 +	 atac 1,
   5.390 +	hyp_subst_tac 1,
   5.391 +	res_inst_tac [("n","x")] natE 1,
   5.392 +	 hyp_subst_tac 1,
   5.393 +	 atac 1,
   5.394 +	hyp_subst_tac 1,
   5.395 +	resolve_tac prems 1,
   5.396 +	dtac spec 1,
   5.397 +	etac mp 1,
   5.398 +	rtac (lessI RS less_trans) 1,
   5.399 +	rtac (lessI RS Suc_mono) 1]);
   5.400 +
   5.401 +(*** Properties of <= ***)
   5.402 +
   5.403 +goalw thy [le_def] "(m <= n) = (m < Suc n)";
   5.404 +by (rtac not_less_eq 1);
   5.405 +qed "le_eq_less_Suc";
   5.406 +
   5.407 +goalw thy [le_def] "0 <= n";
   5.408 +by (rtac not_less0 1);
   5.409 +qed "le0";
   5.410 +
   5.411 +goalw thy [le_def] "~ Suc n <= n";
   5.412 +by (Simp_tac 1);
   5.413 +qed "Suc_n_not_le_n";
   5.414 +
   5.415 +goalw thy [le_def] "(i <= 0) = (i = 0)";
   5.416 +by (nat_ind_tac "i" 1);
   5.417 +by (ALLGOALS Asm_simp_tac);
   5.418 +qed "le_0_eq";
   5.419 +
   5.420 +Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
   5.421 +          Suc_n_not_le_n,
   5.422 +          n_not_Suc_n, Suc_n_not_n,
   5.423 +          nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   5.424 +
   5.425 +(*
   5.426 +goal thy "(Suc m < n | Suc m = n) = (m < n)";
   5.427 +by (stac (less_Suc_eq RS sym) 1);
   5.428 +by (rtac Suc_less_eq 1);
   5.429 +qed "Suc_le_eq";
   5.430 +
   5.431 +this could make the simpset (with less_Suc_eq added again) more confluent,
   5.432 +but less_Suc_eq makes additional problems with terms of the form 0 < Suc (...)
   5.433 +*)
   5.434 +
   5.435 +(*Prevents simplification of f and g: much faster*)
   5.436 +qed_goal "nat_case_weak_cong" thy
   5.437 +  "m=n ==> nat_case a f m = nat_case a f n"
   5.438 +  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   5.439 +
   5.440 +qed_goal "nat_rec_weak_cong" thy
   5.441 +  "m=n ==> nat_rec a f m = nat_rec a f n"
   5.442 +  (fn [prem] => [rtac (prem RS arg_cong) 1]);
   5.443 +
   5.444 +qed_goal "expand_nat_case" thy
   5.445 +  "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
   5.446 +  (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
   5.447 +
   5.448 +val prems = goalw thy [le_def] "~n<m ==> m<=(n::nat)";
   5.449 +by (resolve_tac prems 1);
   5.450 +qed "leI";
   5.451 +
   5.452 +val prems = goalw thy [le_def] "m<=n ==> ~ n < (m::nat)";
   5.453 +by (resolve_tac prems 1);
   5.454 +qed "leD";
   5.455 +
   5.456 +val leE = make_elim leD;
   5.457 +
   5.458 +goal thy "(~n<m) = (m<=(n::nat))";
   5.459 +by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
   5.460 +qed "not_less_iff_le";
   5.461 +
   5.462 +goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   5.463 +by (Fast_tac 1);
   5.464 +qed "not_leE";
   5.465 +
   5.466 +goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   5.467 +by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.468 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.469 +qed "lessD";
   5.470 +
   5.471 +goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
   5.472 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.473 +qed "Suc_leD";
   5.474 +
   5.475 +(* stronger version of Suc_leD *)
   5.476 +goalw thy [le_def] 
   5.477 +        "!!m. Suc m <= n ==> m < n";
   5.478 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.479 +by (cut_facts_tac [less_linear] 1);
   5.480 +by (Fast_tac 1);
   5.481 +qed "Suc_le_lessD";
   5.482 +
   5.483 +goal thy "(Suc m <= n) = (m < n)";
   5.484 +by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   5.485 +qed "Suc_le_eq";
   5.486 +
   5.487 +goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
   5.488 +by (fast_tac (!claset addDs [Suc_lessD]) 1);
   5.489 +qed "le_SucI";
   5.490 +Addsimps[le_SucI];
   5.491 +
   5.492 +bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
   5.493 +
   5.494 +goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)";
   5.495 +by (fast_tac (!claset addEs [less_asym]) 1);
   5.496 +qed "less_imp_le";
   5.497 +
   5.498 +goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
   5.499 +by (cut_facts_tac [less_linear] 1);
   5.500 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.501 +qed "le_imp_less_or_eq";
   5.502 +
   5.503 +goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
   5.504 +by (cut_facts_tac [less_linear] 1);
   5.505 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.506 +by (flexflex_tac);
   5.507 +qed "less_or_eq_imp_le";
   5.508 +
   5.509 +goal thy "(x <= (y::nat)) = (x < y | x=y)";
   5.510 +by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
   5.511 +qed "le_eq_less_or_eq";
   5.512 +
   5.513 +goal thy "n <= (n::nat)";
   5.514 +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   5.515 +qed "le_refl";
   5.516 +
   5.517 +val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
   5.518 +by (dtac le_imp_less_or_eq 1);
   5.519 +by (fast_tac (!claset addIs [less_trans]) 1);
   5.520 +qed "le_less_trans";
   5.521 +
   5.522 +goal thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
   5.523 +by (dtac le_imp_less_or_eq 1);
   5.524 +by (fast_tac (!claset addIs [less_trans]) 1);
   5.525 +qed "less_le_trans";
   5.526 +
   5.527 +goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
   5.528 +by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   5.529 +          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
   5.530 +qed "le_trans";
   5.531 +
   5.532 +val prems = goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
   5.533 +by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   5.534 +          fast_tac (!claset addEs [less_irrefl,less_asym])]);
   5.535 +qed "le_anti_sym";
   5.536 +
   5.537 +goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
   5.538 +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   5.539 +qed "Suc_le_mono";
   5.540 +
   5.541 +AddIffs [Suc_le_mono];
   5.542 +
   5.543 +(* Axiom 'order_le_less' of class 'order': *)
   5.544 +goal thy "(m::nat) < n = (m <= n & m ~= n)";
   5.545 +br iffI 1;
   5.546 + br conjI 1;
   5.547 +  be less_imp_le 1;
   5.548 + be (less_not_refl2 RS not_sym) 1;
   5.549 +by(fast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
   5.550 +qed "nat_less_le";
   5.551 +
   5.552 +(** LEAST -- the least number operator **)
   5.553 +
   5.554 +val [prem1,prem2] = goalw thy [Least_def]
   5.555 +    "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
   5.556 +by (rtac select_equality 1);
   5.557 +by (fast_tac (!claset addSIs [prem1,prem2]) 1);
   5.558 +by (cut_facts_tac [less_linear] 1);
   5.559 +by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
   5.560 +qed "Least_equality";
   5.561 +
   5.562 +val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
   5.563 +by (rtac (prem RS rev_mp) 1);
   5.564 +by (res_inst_tac [("n","k")] less_induct 1);
   5.565 +by (rtac impI 1);
   5.566 +by (rtac classical 1);
   5.567 +by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   5.568 +by (assume_tac 1);
   5.569 +by (assume_tac 2);
   5.570 +by (Fast_tac 1);
   5.571 +qed "LeastI";
   5.572 +
   5.573 +(*Proof is almost identical to the one above!*)
   5.574 +val [prem] = goal thy "P(k::nat) ==> (LEAST x.P(x)) <= k";
   5.575 +by (rtac (prem RS rev_mp) 1);
   5.576 +by (res_inst_tac [("n","k")] less_induct 1);
   5.577 +by (rtac impI 1);
   5.578 +by (rtac classical 1);
   5.579 +by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   5.580 +by (assume_tac 1);
   5.581 +by (rtac le_refl 2);
   5.582 +by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
   5.583 +qed "Least_le";
   5.584 +
   5.585 +val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
   5.586 +by (rtac notI 1);
   5.587 +by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
   5.588 +by (rtac prem 1);
   5.589 +qed "not_less_Least";
   5.590 +
   5.591 +qed_goalw "Least_Suc" thy [Least_def]
   5.592 + "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   5.593 + (fn _ => [
   5.594 +        rtac select_equality 1,
   5.595 +        fold_goals_tac [Least_def],
   5.596 +        safe_tac (!claset addSEs [LeastI]),
   5.597 +        rename_tac "j" 1,
   5.598 +        res_inst_tac [("n","j")] natE 1,
   5.599 +        Fast_tac 1,
   5.600 +        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   5.601 +        rename_tac "k n" 1,
   5.602 +        res_inst_tac [("n","k")] natE 1,
   5.603 +        Fast_tac 1,
   5.604 +        hyp_subst_tac 1,
   5.605 +        rewtac Least_def,
   5.606 +        rtac (select_equality RS arg_cong RS sym) 1,
   5.607 +        safe_tac (!claset),
   5.608 +        dtac Suc_mono 1,
   5.609 +        Fast_tac 1,
   5.610 +        cut_facts_tac [less_linear] 1,
   5.611 +        safe_tac (!claset),
   5.612 +        atac 2,
   5.613 +        Fast_tac 2,
   5.614 +        dtac Suc_mono 1,
   5.615 +        Fast_tac 1]);
   5.616 +
   5.617 +
   5.618 +(*** Instantiation of transitivity prover ***)
   5.619 +
   5.620 +structure Less_Arith =
   5.621 +struct
   5.622 +val nat_leI = leI;
   5.623 +val nat_leD = leD;
   5.624 +val lessI = lessI;
   5.625 +val zero_less_Suc = zero_less_Suc;
   5.626 +val less_reflE = less_irrefl;
   5.627 +val less_zeroE = less_zeroE;
   5.628 +val less_incr = Suc_mono;
   5.629 +val less_decr = Suc_less_SucD;
   5.630 +val less_incr_rhs = Suc_mono RS Suc_lessD;
   5.631 +val less_decr_lhs = Suc_lessD;
   5.632 +val less_trans_Suc = less_trans_Suc;
   5.633 +val leI = lessD RS (Suc_le_mono RS iffD1);
   5.634 +val not_lessI = leI RS leD
   5.635 +val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
   5.636 +  (fn _ => [etac swap2 1, etac leD 1]);
   5.637 +val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
   5.638 +  (fn _ => [etac less_SucE 1,
   5.639 +            fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
   5.640 +                             addDs [less_trans_Suc]) 1,
   5.641 +            atac 1]);
   5.642 +val leD = le_eq_less_Suc RS iffD1;
   5.643 +val not_lessD = nat_leI RS leD;
   5.644 +val not_leD = not_leE
   5.645 +val eqD1 = prove_goal thy  "!!n. m = n ==> m < Suc n"
   5.646 + (fn _ => [etac subst 1, rtac lessI 1]);
   5.647 +val eqD2 = sym RS eqD1;
   5.648 +
   5.649 +fun is_zero(t) =  t = Const("0",Type("nat",[]));
   5.650 +
   5.651 +fun nnb T = T = Type("fun",[Type("nat",[]),
   5.652 +                            Type("fun",[Type("nat",[]),
   5.653 +                                        Type("bool",[])])])
   5.654 +
   5.655 +fun decomp_Suc(Const("Suc",_)$t) = let val (a,i) = decomp_Suc t in (a,i+1) end
   5.656 +  | decomp_Suc t = (t,0);
   5.657 +
   5.658 +fun decomp2(rel,T,lhs,rhs) =
   5.659 +  if not(nnb T) then None else
   5.660 +  let val (x,i) = decomp_Suc lhs
   5.661 +      val (y,j) = decomp_Suc rhs
   5.662 +  in case rel of
   5.663 +       "op <"  => Some(x,i,"<",y,j)
   5.664 +     | "op <=" => Some(x,i,"<=",y,j)
   5.665 +     | "op ="  => Some(x,i,"=",y,j)
   5.666 +     | _       => None
   5.667 +  end;
   5.668 +
   5.669 +fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   5.670 +  | negate None = None;
   5.671 +
   5.672 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   5.673 +  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
   5.674 +      negate(decomp2(rel,T,lhs,rhs))
   5.675 +  | decomp _ = None
   5.676 +
   5.677 +end;
   5.678 +
   5.679 +structure Trans_Tac = Trans_Tac_Fun(Less_Arith);
   5.680 +
   5.681 +open Trans_Tac;
   5.682 +
   5.683 +(*** eliminates ~= in premises, which trans_tac cannot deal with ***)
   5.684 +qed_goal "nat_neqE" thy
   5.685 +  "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
   5.686 +  (fn major::prems => [cut_facts_tac [less_linear] 1,
   5.687 +                       REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/NatDef.thy	Wed Feb 12 18:53:59 1997 +0100
     6.3 @@ -0,0 +1,77 @@
     6.4 +(*  Title:      HOL/NatDef.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     6.7 +    Copyright   1991  University of Cambridge
     6.8 +
     6.9 +Definition of types ind and nat.
    6.10 +
    6.11 +Type nat is defined as a set Nat over type ind.
    6.12 +*)
    6.13 +
    6.14 +NatDef = WF +
    6.15 +
    6.16 +(** type ind **)
    6.17 +
    6.18 +types
    6.19 +  ind
    6.20 +
    6.21 +arities
    6.22 +  ind :: term
    6.23 +
    6.24 +consts
    6.25 +  Zero_Rep      :: ind
    6.26 +  Suc_Rep       :: ind => ind
    6.27 +
    6.28 +rules
    6.29 +  (*the axiom of infinity in 2 parts*)
    6.30 +  inj_Suc_Rep           "inj(Suc_Rep)"
    6.31 +  Suc_Rep_not_Zero_Rep  "Suc_Rep(x) ~= Zero_Rep"
    6.32 +
    6.33 +
    6.34 +
    6.35 +(** type nat **)
    6.36 +
    6.37 +(* type definition *)
    6.38 +
    6.39 +typedef (Nat)
    6.40 +  nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    6.41 +
    6.42 +instance
    6.43 +  nat :: ord
    6.44 +
    6.45 +
    6.46 +(* abstract constants and syntax *)
    6.47 +
    6.48 +consts
    6.49 +  "0"       :: nat                ("0")
    6.50 +  Suc       :: nat => nat
    6.51 +  nat_case  :: ['a, nat => 'a, nat] => 'a
    6.52 +  pred_nat  :: "(nat * nat) set"
    6.53 +  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
    6.54 +
    6.55 +syntax
    6.56 +  "1"       :: nat                ("1")
    6.57 +  "2"       :: nat                ("2")
    6.58 +
    6.59 +translations
    6.60 +   "1"  == "Suc 0"
    6.61 +   "2"  == "Suc 1"
    6.62 +  "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
    6.63 +
    6.64 +
    6.65 +defs
    6.66 +  Zero_def      "0 == Abs_Nat(Zero_Rep)"
    6.67 +  Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
    6.68 +
    6.69 +  (*nat operations and recursion*)
    6.70 +  nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  
    6.71 +                                        & (!x. n=Suc x --> z=f(x))"
    6.72 +  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc n)}"
    6.73 +
    6.74 +  less_def      "m<n == (m,n):trancl(pred_nat)"
    6.75 +
    6.76 +  le_def        "m<=(n::nat) == ~(n<m)"
    6.77 +
    6.78 +  nat_rec_def   "nat_rec c d ==
    6.79 +                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
    6.80 +end
     7.1 --- a/src/HOL/Ord.ML	Wed Feb 12 15:43:50 1997 +0100
     7.2 +++ b/src/HOL/Ord.ML	Wed Feb 12 18:53:59 1997 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  The type class for ordered types
     7.5  *)
     7.6  
     7.7 -open Ord;
     7.8 +(** mono **)
     7.9  
    7.10  val [prem] = goalw Ord.thy [mono_def]
    7.11      "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
    7.12 @@ -19,3 +19,32 @@
    7.13  by (rtac minor 1);
    7.14  qed "monoD";
    7.15  
    7.16 +
    7.17 +section "Orders";
    7.18 +
    7.19 +AddIffs [order_refl];
    7.20 +
    7.21 +goal Ord.thy "~ x < (x::'a::order)";
    7.22 +by(simp_tac (!simpset addsimps [order_less_le]) 1);
    7.23 +qed "order_less_irrefl";
    7.24 +AddIffs [order_less_irrefl];
    7.25 +
    7.26 +goal thy "(x::'a::order) <= y = (x < y | x = y)";
    7.27 +by(simp_tac (!simpset addsimps [order_less_le]) 1);
    7.28 +by(Fast_tac 1);
    7.29 +qed "order_le_less";
    7.30 +
    7.31 +(** min **)
    7.32 +
    7.33 +goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    7.34 +by(split_tac [expand_if] 1);
    7.35 +by(Asm_simp_tac 1);
    7.36 +qed "min_leastL";
    7.37 +
    7.38 +val prems = goalw thy [min_def]
    7.39 + "(!!x::'a::order. least <= x) ==> min x least = least";
    7.40 +by(cut_facts_tac prems 1);
    7.41 +by(split_tac [expand_if] 1);
    7.42 +by(Asm_simp_tac 1);
    7.43 +by(fast_tac (!claset addEs [order_antisym]) 1);
    7.44 +qed "min_leastR";
     8.1 --- a/src/HOL/Ord.thy	Wed Feb 12 15:43:50 1997 +0100
     8.2 +++ b/src/HOL/Ord.thy	Wed Feb 12 18:53:59 1997 +0100
     8.3 @@ -17,6 +17,8 @@
     8.4    mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
     8.5    min, max      :: ['a::ord, 'a] => 'a
     8.6  
     8.7 +  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
     8.8 +
     8.9  syntax
    8.10    "op <"        :: ['a::ord, 'a] => bool             ("op <")
    8.11    "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    8.12 @@ -29,5 +31,13 @@
    8.13    mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    8.14    min_def       "min a b == (if a <= b then a else b)"
    8.15    max_def       "max a b == (if a <= b then b else a)"
    8.16 +  Least_def     "Least P == @x. P(x) & (ALL y. y<x --> ~P(y))"
    8.17 +
    8.18 +
    8.19 +axclass order < ord
    8.20 +  order_refl    "x <= x"
    8.21 +  order_trans   "[| x <= y; y <= z |] ==> x <= z"
    8.22 +  order_antisym "[| x <= y; y <= x |] ==> x = y"
    8.23 +  order_less_le "x < y = (x <= y & x ~= y)"
    8.24  
    8.25  end
     9.1 --- a/src/HOL/Set.ML	Wed Feb 12 15:43:50 1997 +0100
     9.2 +++ b/src/HOL/Set.ML	Wed Feb 12 18:53:59 1997 +0100
     9.3 @@ -341,6 +341,18 @@
     9.4  qed "bex_empty";
     9.5  Addsimps [ball_empty, bex_empty];
     9.6  
     9.7 +goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
     9.8 +by(Fast_tac 1);
     9.9 +qed "ball_False";
    9.10 +Addsimps [ball_False];
    9.11 +
    9.12 +(* The dual is probably not helpful:
    9.13 +goal Set.thy "(? x:A.True) = (A ~= {})";
    9.14 +by(Fast_tac 1);
    9.15 +qed "bex_True";
    9.16 +Addsimps [bex_True];
    9.17 +*)
    9.18 +
    9.19  
    9.20  section "Augmenting a set -- insert";
    9.21