NatBin: binary arithmetic for the naturals
authorpaulson
Mon Jul 19 15:27:34 1999 +0200 (1999-07-19)
changeset 7032d6efb3b8e669
parent 7031 972b5f62f476
child 7033 c7479ae352b1
NatBin: binary arithmetic for the naturals
src/HOL/Integ/NatBin.ML
src/HOL/Integ/NatBin.thy
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/List.thy
src/HOL/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/NatBin.ML	Mon Jul 19 15:27:34 1999 +0200
     1.3 @@ -0,0 +1,356 @@
     1.4 +(*  Title:      HOL/NatBin.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Binary arithmetic for the natural numbers
    1.10 +*)
    1.11 +
    1.12 +(** nat (coercion from int to nat) **)
    1.13 +
    1.14 +Goal "nat (number_of w) = number_of w";
    1.15 +by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    1.16 +qed "nat_number_of";
    1.17 +Addsimps [nat_number_of];
    1.18 +
    1.19 +(*These rewrites should one day be re-oriented...*)
    1.20 +
    1.21 +Goal "#0 = 0";
    1.22 +by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1);
    1.23 +qed "numeral_0_eq_0";
    1.24 +
    1.25 +Goal "#1 = 1";
    1.26 +by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1);
    1.27 +qed "numeral_1_eq_1";
    1.28 +
    1.29 +Goal "#2 = 2";
    1.30 +by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1);
    1.31 +qed "numeral_2_eq_2";
    1.32 +
    1.33 +
    1.34 +(** int (coercion from nat to int) **)
    1.35 +
    1.36 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.37 +Goal "int (number_of v :: nat) = \
    1.38 +\        (if neg (number_of v) then #0 \
    1.39 +\         else (number_of v :: int))";
    1.40 +by (simp_tac
    1.41 +    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
    1.42 +				  not_neg_nat, int_0]) 1);
    1.43 +qed "int_nat_number_of";
    1.44 +Addsimps [int_nat_number_of];
    1.45 +
    1.46 +
    1.47 +(** Successor **)
    1.48 +
    1.49 +Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
    1.50 +br sym 1;
    1.51 +by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.52 +qed "Suc_nat_eq_nat_zadd1";
    1.53 +
    1.54 +Goal "Suc (number_of v) = \
    1.55 +\       (if neg (number_of v) then #1 else number_of (bin_succ v))";
    1.56 +by (simp_tac
    1.57 +    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    1.58 +				  nat_number_of_def, int_Suc, 
    1.59 +				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    1.60 +qed "Suc_nat_number_of";
    1.61 +
    1.62 +Goal "Suc #0 = #1";
    1.63 +by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
    1.64 +qed "Suc_numeral_0_eq_1";
    1.65 +
    1.66 +Goal "Suc #1 = #2";
    1.67 +by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
    1.68 +qed "Suc_numeral_1_eq_2";
    1.69 +
    1.70 +(** Addition **)
    1.71 +
    1.72 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat z + nat z' = nat (z+z')";
    1.73 +by (rtac (inj_int RS injD) 1);
    1.74 +by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    1.75 +qed "add_nat_eq_nat_zadd";
    1.76 +
    1.77 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.78 +Goal "(number_of v :: nat) + number_of v' = \
    1.79 +\        (if neg (number_of v) then number_of v' \
    1.80 +\         else if neg (number_of v') then number_of v \
    1.81 +\         else number_of (bin_add v v'))";
    1.82 +by (simp_tac
    1.83 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
    1.84 +				  add_nat_eq_nat_zadd, number_of_add]) 1);
    1.85 +qed "add_nat_number_of";
    1.86 +
    1.87 +Addsimps [add_nat_number_of];
    1.88 +
    1.89 +
    1.90 +(** Subtraction **)
    1.91 +
    1.92 +Goal "[| (#0::int) <= z';  z' <= z |] ==> nat z - nat z' = nat (z-z')";
    1.93 +by (rtac (inj_int RS injD) 1);
    1.94 +by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
    1.95 +qed "diff_nat_eq_nat_zdiff";
    1.96 +
    1.97 +
    1.98 +Goal "nat z - nat z' = \
    1.99 +\       (if neg z' then nat z  \
   1.100 +\        else let d = z-z' in    \
   1.101 +\             if neg d then 0 else nat d)";
   1.102 +by (simp_tac (simpset() addsimps [Let_def, diff_nat_eq_nat_zdiff,
   1.103 +				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   1.104 +by (simp_tac (simpset() addsimps zcompare_rls@
   1.105 +		                 [diff_is_0_eq, nat_le_eq_zle]) 1);
   1.106 +qed "diff_nat_eq_if";
   1.107 +
   1.108 +Goalw [nat_number_of_def]
   1.109 +     "(number_of v :: nat) - number_of v' = \
   1.110 +\       (if neg (number_of v') then number_of v \
   1.111 +\        else let d = number_of (bin_add v (bin_minus v')) in    \
   1.112 +\             if neg d then #0 else nat d)";
   1.113 +by (simp_tac
   1.114 +    (simpset_of Int.thy delcongs [if_weak_cong]
   1.115 +			addsimps [not_neg_eq_ge_0, nat_0,
   1.116 +				  diff_nat_eq_if, diff_number_of_eq]) 1);
   1.117 +qed "diff_nat_number_of";
   1.118 +
   1.119 +Addsimps [diff_nat_number_of];
   1.120 +
   1.121 +
   1.122 +(** Multiplication **)
   1.123 +
   1.124 +Goal "(#0::int) <= z ==> nat z * nat z' = nat (z*z')";
   1.125 +by (case_tac "#0 <= z'" 1);
   1.126 +by (subgoal_tac "z'*z <= #0" 2);
   1.127 +by (rtac (neg_imp_zmult_nonpos_iff RS iffD2) 3);
   1.128 +by Auto_tac;
   1.129 +by (subgoal_tac "#0 <= z*z'" 1);
   1.130 +by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
   1.131 +by (rtac (inj_int RS injD) 1);
   1.132 +by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
   1.133 +qed "mult_nat_eq_nat_zmult";
   1.134 +
   1.135 +Goal "(number_of v :: nat) * number_of v' = \
   1.136 +\      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
   1.137 +by (simp_tac
   1.138 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.139 +				  mult_nat_eq_nat_zmult, number_of_mult, 
   1.140 +				  nat_0]) 1);
   1.141 +qed "mult_nat_number_of";
   1.142 +
   1.143 +Addsimps [mult_nat_number_of];
   1.144 +
   1.145 +
   1.146 +(** Quotient **)
   1.147 +
   1.148 +Goal "(#0::int) <= z ==> nat z div nat z' = nat (z div z')";
   1.149 +by (case_tac "#0 <= z'" 1);
   1.150 +by (auto_tac (claset(), 
   1.151 +	      simpset() addsimps [div_nonneg_neg, DIVISION_BY_ZERO_DIV]));
   1.152 +by (zdiv_undefined_case_tac "z' = #0" 1);
   1.153 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   1.154 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.155 +by (rename_tac "m m'" 1);
   1.156 +by (subgoal_tac "#0 <= int m div int m'" 1);
   1.157 + by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
   1.158 +				       pos_imp_zdiv_nonneg_iff]) 2);
   1.159 +by (rtac (inj_int RS injD) 1);
   1.160 +by (Asm_simp_tac 1);
   1.161 +by (rtac sym 1);
   1.162 +by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   1.163 + by (Force_tac 2);
   1.164 +by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   1.165 +				      numeral_0_eq_0, zadd_int, zmult_int, 
   1.166 +				      mod_less_divisor]) 1);
   1.167 +by (rtac (mod_div_equality RS sym RS trans) 1);
   1.168 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   1.169 +qed "div_nat_eq_nat_zdiv";
   1.170 +
   1.171 +Goal "(number_of v :: nat)  div  number_of v' = \
   1.172 +\         (if neg (number_of v) then #0 \
   1.173 +\          else nat (number_of v div number_of v'))";
   1.174 +by (simp_tac
   1.175 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   1.176 +				  div_nat_eq_nat_zdiv, nat_0]) 1);
   1.177 +qed "div_nat_number_of";
   1.178 +
   1.179 +Addsimps [div_nat_number_of];
   1.180 +
   1.181 +
   1.182 +(** Remainder **)
   1.183 +
   1.184 +(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   1.185 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat z mod nat z' = nat (z mod z')";
   1.186 +by (zdiv_undefined_case_tac "z' = #0" 1);
   1.187 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   1.188 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.189 +by (rename_tac "m m'" 1);
   1.190 +by (subgoal_tac "#0 <= int m mod int m'" 1);
   1.191 + by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
   1.192 +				       pos_mod_sign]) 2);
   1.193 +by (rtac (inj_int RS injD) 1);
   1.194 +by (Asm_simp_tac 1);
   1.195 +by (rtac sym 1);
   1.196 +by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   1.197 + by (Force_tac 2);
   1.198 +by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   1.199 +				      numeral_0_eq_0, zadd_int, zmult_int, 
   1.200 +				      mod_less_divisor]) 1);
   1.201 +by (rtac (mod_div_equality RS sym RS trans) 1);
   1.202 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   1.203 +qed "mod_nat_eq_nat_zmod";
   1.204 +
   1.205 +Goal "(number_of v :: nat)  mod  number_of v' = \
   1.206 +\       (if neg (number_of v) then #0 \
   1.207 +\        else if neg (number_of v') then number_of v \
   1.208 +\        else nat (number_of v mod number_of v'))";
   1.209 +by (simp_tac
   1.210 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   1.211 +				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   1.212 +				  mod_nat_eq_nat_zmod]) 1);
   1.213 +qed "mod_nat_number_of";
   1.214 +
   1.215 +Addsimps [mod_nat_number_of];
   1.216 +
   1.217 +
   1.218 +(*** Comparisons ***)
   1.219 +
   1.220 +(** Equals (=) **)
   1.221 +
   1.222 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
   1.223 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.224 +qed "eq_nat_nat_iff";
   1.225 +
   1.226 +(*"neg" is used in rewrite rules for binary comparisons*)
   1.227 +Goal "((number_of v :: nat) = number_of v') = \
   1.228 +\        (if neg (number_of v) then ((#0::nat) = number_of v') \
   1.229 +\         else if neg (number_of v') then iszero (number_of v) \
   1.230 +\         else iszero (number_of (bin_add v (bin_minus v'))))";
   1.231 +by (simp_tac
   1.232 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.233 +				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   1.234 +by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, iszero_def]) 1);
   1.235 +qed "eq_nat_number_of";
   1.236 +
   1.237 +Addsimps [eq_nat_number_of];
   1.238 +
   1.239 +(** Less-than (<) **)
   1.240 +
   1.241 +(*"neg" is used in rewrite rules for binary comparisons*)
   1.242 +Goal "((number_of v :: nat) < number_of v') = \
   1.243 +\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   1.244 +\         else neg (number_of (bin_add v (bin_minus v'))))";
   1.245 +by (simp_tac
   1.246 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.247 +				  nat_less_eq_zless, less_number_of_eq_neg,
   1.248 +				  nat_0]) 1);
   1.249 +by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
   1.250 +				    number_of_minus, zless_zero_nat]) 1);
   1.251 +qed "less_nat_number_of";
   1.252 +
   1.253 +Addsimps [less_nat_number_of];
   1.254 +
   1.255 +
   1.256 +(** Less-than-or-equals (<=) **)
   1.257 +
   1.258 +Goal "(number_of x <= (number_of y::nat)) = \
   1.259 +\     (~ number_of y < (number_of x::nat))";
   1.260 +by (rtac (linorder_not_less RS sym) 1);
   1.261 +qed "le_nat_number_of_eq_not_less"; 
   1.262 +
   1.263 +Addsimps [le_nat_number_of_eq_not_less];
   1.264 +
   1.265 +
   1.266 +(*** New versions of existing theorems involving 0, 1, 2 ***)
   1.267 +
   1.268 +fun change_theory thy th = 
   1.269 +    [th, read_instantiate_sg (sign_of thy) [("t","dummyVar")] refl] 
   1.270 +    MRS (conjI RS conjunct1) |> standard;
   1.271 +
   1.272 +(*Maps n to #n for n = 0, 1, 2*)
   1.273 +val numeral_sym_ss = 
   1.274 +    HOL_ss addsimps [numeral_0_eq_0 RS sym, 
   1.275 +		     numeral_1_eq_1 RS sym, 
   1.276 +		     numeral_2_eq_2 RS sym,
   1.277 +		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
   1.278 +
   1.279 +fun rename_numerals thy th = simplify numeral_sym_ss (change_theory thy th);
   1.280 +
   1.281 +(*Maps #n to n for n = 0, 1, 2*)
   1.282 +val numeral_ss = 
   1.283 +    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
   1.284 +
   1.285 +(** Nat **)
   1.286 +
   1.287 +Goal "#0 < n ==> n = Suc(n - #1)";
   1.288 +by (asm_full_simp_tac numeral_ss 1);
   1.289 +qed "Suc_pred'";
   1.290 +
   1.291 +
   1.292 +fun inst x t = read_instantiate_sg (sign_of NatBin.thy) [(x,t)];
   1.293 +
   1.294 +(*Expresses a natural number constant as the Suc of another one.
   1.295 +  NOT suitable for rewriting because n recurs in the condition.*)
   1.296 +bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   1.297 +
   1.298 +(** Arith **)
   1.299 +
   1.300 +Addsimps (map (rename_numerals thy) 
   1.301 +	  [diff_0_eq_0, add_0, add_0_right, add_pred, 
   1.302 +	   diff_is_0_eq RS iffD2, zero_less_diff,
   1.303 +	   mult_0, mult_0_right, mult_1, mult_1_right, 
   1.304 +	   mult_is_0, zero_less_mult_iff,
   1.305 +	   mult_eq_1_iff]);
   1.306 +
   1.307 +AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
   1.308 +
   1.309 +(* These two can be useful when m = number_of... *)
   1.310 +
   1.311 +Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
   1.312 +by (exhaust_tac "m" 1);
   1.313 +by (ALLGOALS (asm_simp_tac numeral_ss));
   1.314 +qed "add_eq_if";
   1.315 +
   1.316 +Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   1.317 +by (exhaust_tac "m" 1);
   1.318 +by (ALLGOALS (asm_simp_tac numeral_ss));
   1.319 +qed "mult_eq_if";
   1.320 +
   1.321 +(*various theorems that aren't in the default simpset*)
   1.322 +val add_is_one' = rename_numerals thy add_is_1;
   1.323 +val one_is_add' = rename_numerals thy one_is_add;
   1.324 +val zero_induct' = rename_numerals thy zero_induct;
   1.325 +val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
   1.326 +val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
   1.327 +val le_pred_eq' = rename_numerals thy le_pred_eq;
   1.328 +val less_pred_eq' = rename_numerals thy less_pred_eq;
   1.329 +
   1.330 +(** Divides **)
   1.331 +
   1.332 +Addsimps (map (rename_numerals thy) 
   1.333 +	  [mod_1, mod_0, div_1, div_0, mod2_gr_0, mod2_add_self_eq_0,
   1.334 +	   mod2_add_self]);
   1.335 +
   1.336 +AddIffs (map (rename_numerals thy) 
   1.337 +	  [dvd_1_left, dvd_0_right]);
   1.338 +
   1.339 +(*useful?*)
   1.340 +val mod_self' = rename_numerals thy mod_self;
   1.341 +val div_self' = rename_numerals thy div_self;
   1.342 +val div_less' = rename_numerals thy div_less;
   1.343 +val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
   1.344 +
   1.345 +(** Power **)
   1.346 +
   1.347 +Goal "(p::nat) ^ #0 = #1";
   1.348 +by (simp_tac numeral_ss 1);
   1.349 +qed "power_zero";
   1.350 +Addsimps [power_zero];
   1.351 +
   1.352 +val binomial_zero = rename_numerals thy binomial_0;
   1.353 +val binomial_Suc' = rename_numerals thy binomial_Suc;
   1.354 +val binomial_n_n' = rename_numerals thy binomial_n_n;
   1.355 +
   1.356 +(*binomial_0_Suc doesn't work well on numerals*)
   1.357 +Addsimps (map (rename_numerals thy) 
   1.358 +	  [binomial_n_0, binomial_zero, binomial_1]);
   1.359 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Jul 19 15:27:34 1999 +0200
     2.3 @@ -0,0 +1,21 @@
     2.4 +(*  Title:      HOL/NatBin.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1999  University of Cambridge
     2.8 +
     2.9 +Binary arithmetic for the natural numbers
    2.10 +
    2.11 +This case is simply reduced to that for the non-negative integers
    2.12 +*)
    2.13 +
    2.14 +NatBin = IntDiv +
    2.15 +
    2.16 +instance
    2.17 +  nat :: number 
    2.18 +
    2.19 +defs
    2.20 +  nat_number_of_def
    2.21 +    "number_of v == nat (number_of v)"
    2.22 +     (*::bin=>nat        ::bin=>int*)
    2.23 +
    2.24 +end
     3.1 --- a/src/HOL/IsaMakefile	Mon Jul 19 15:24:35 1999 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Mon Jul 19 15:27:34 1999 +0200
     3.3 @@ -48,7 +48,8 @@
     3.4    Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
     3.5    Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy \
     3.6    Integ/Int.ML Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy \
     3.7 -  Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
     3.8 +  Integ/NatBin.ML Integ/NatBin.thy Integ/simproc.ML \
     3.9 +  Lfp.ML Lfp.thy List.ML List.thy \
    3.10    Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    3.11    Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    3.12    Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
     4.1 --- a/src/HOL/List.ML	Mon Jul 19 15:24:35 1999 +0200
     4.2 +++ b/src/HOL/List.ML	Mon Jul 19 15:27:34 1999 +0200
     4.3 @@ -411,10 +411,11 @@
     4.4  
     4.5  section "set";
     4.6  
     4.7 -qed_goal "finite_set" thy "finite (set xs)" 
     4.8 -	(K [induct_tac "xs" 1, Auto_tac]);
     4.9 -Addsimps[finite_set];
    4.10 -AddSIs[finite_set];
    4.11 +Goal "finite (set xs)";
    4.12 +by (induct_tac "xs" 1);
    4.13 +by Auto_tac;
    4.14 +qed "finite_set";
    4.15 +AddIffs [finite_set];
    4.16  
    4.17  Goal "set (xs@ys) = (set xs Un set ys)";
    4.18  by (induct_tac "xs" 1);
    4.19 @@ -1227,3 +1228,31 @@
    4.20  by (Blast_tac 1);
    4.21  qed "Cons_in_lex";
    4.22  AddIffs [Cons_in_lex];
    4.23 +
    4.24 +
    4.25 +(*** Versions of some theorems above using binary numerals ***)
    4.26 +
    4.27 +AddIffs (map (rename_numerals thy) 
    4.28 +	  [length_0_conv, zero_length_conv, length_greater_0_conv,
    4.29 +	   sum_eq_0_conv]);
    4.30 +
    4.31 +Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
    4.32 +by (exhaust_tac "n" 1);
    4.33 +by (ALLGOALS 
    4.34 +    (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
    4.35 +qed "take_Cons'";
    4.36 +
    4.37 +Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
    4.38 +by (exhaust_tac "n" 1);
    4.39 +by (ALLGOALS
    4.40 +    (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
    4.41 +qed "drop_Cons'";
    4.42 +
    4.43 +Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
    4.44 +by (exhaust_tac "n" 1);
    4.45 +by (ALLGOALS
    4.46 +    (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
    4.47 +qed "nth_Cons'";
    4.48 +
    4.49 +Addsimps (map (inst "n" "number_of ?v") [take_Cons', drop_Cons', nth_Cons']);
    4.50 +
     5.1 --- a/src/HOL/List.thy	Mon Jul 19 15:24:35 1999 +0200
     5.2 +++ b/src/HOL/List.thy	Mon Jul 19 15:27:34 1999 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  The datatype of finite lists.
     5.5  *)
     5.6  
     5.7 -List = Datatype + WF_Rel +
     5.8 +List = Datatype + WF_Rel + NatBin +
     5.9  
    5.10  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
    5.11  
     6.1 --- a/src/HOL/ROOT.ML	Mon Jul 19 15:24:35 1999 +0200
     6.2 +++ b/src/HOL/ROOT.ML	Mon Jul 19 15:27:34 1999 +0200
     6.3 @@ -69,7 +69,7 @@
     6.4  cd "Integ";
     6.5  use_thy "IntDef";
     6.6  use "simproc.ML";
     6.7 -use_thy "IntDiv";
     6.8 +use_thy "NatBin";
     6.9  cd "..";
    6.10  
    6.11  (*the all-in-one theory*)