src/HOL/Integ/nat_bin.ML
changeset 10574 8f98f0301d67
child 10693 9e4a0e84d0d6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/nat_bin.ML	Fri Dec 01 19:53:29 2000 +0100
     1.3 @@ -0,0 +1,548 @@
     1.4 +(*  Title:      HOL/nat_bin.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 +val nat_number_of_def = thm "nat_number_of_def";
    1.13 +
    1.14 +(** nat (coercion from int to nat) **)
    1.15 +
    1.16 +Goal "nat (number_of w) = number_of w";
    1.17 +by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    1.18 +qed "nat_number_of";
    1.19 +Addsimps [nat_number_of];
    1.20 +
    1.21 +(*These rewrites should one day be re-oriented...*)
    1.22 +
    1.23 +Goal "#0 = (0::nat)";
    1.24 +by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
    1.25 +qed "numeral_0_eq_0";
    1.26 +
    1.27 +Goal "#1 = (1::nat)";
    1.28 +by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
    1.29 +qed "numeral_1_eq_1";
    1.30 +
    1.31 +Goal "#2 = (2::nat)";
    1.32 +by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
    1.33 +qed "numeral_2_eq_2";
    1.34 +
    1.35 +bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
    1.36 +
    1.37 +(** int (coercion from nat to int) **)
    1.38 +
    1.39 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.40 +Goal "int (number_of v :: nat) = \
    1.41 +\        (if neg (number_of v) then #0 \
    1.42 +\         else (number_of v :: int))";
    1.43 +by (simp_tac
    1.44 +    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
    1.45 +				  not_neg_nat, int_0]) 1);
    1.46 +qed "int_nat_number_of";
    1.47 +Addsimps [int_nat_number_of];
    1.48 +
    1.49 +
    1.50 +val nat_bin_arith_setup =
    1.51 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    1.52 +   {add_mono_thms = add_mono_thms,
    1.53 +    inj_thms = inj_thms,
    1.54 +    lessD = lessD,
    1.55 +    simpset = simpset addsimps [int_nat_number_of,
    1.56 + not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})];
    1.57 +
    1.58 +(** Successor **)
    1.59 +
    1.60 +Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
    1.61 +by (rtac sym 1);
    1.62 +by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    1.63 +qed "Suc_nat_eq_nat_zadd1";
    1.64 +
    1.65 +Goal "Suc (number_of v) = \
    1.66 +\       (if neg (number_of v) then #1 else number_of (bin_succ v))";
    1.67 +by (simp_tac
    1.68 +    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    1.69 +				  nat_number_of_def, int_Suc, 
    1.70 +				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    1.71 +qed "Suc_nat_number_of";
    1.72 +Addsimps [Suc_nat_number_of];
    1.73 +
    1.74 +Goal "Suc (number_of v + n) = \
    1.75 +\       (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
    1.76 +by (Simp_tac 1);
    1.77 +qed "Suc_nat_number_of_add";
    1.78 +
    1.79 +Goal "Suc #0 = #1";
    1.80 +by (Simp_tac 1);
    1.81 +qed "Suc_numeral_0_eq_1";
    1.82 +
    1.83 +Goal "Suc #1 = #2";
    1.84 +by (Simp_tac 1);
    1.85 +qed "Suc_numeral_1_eq_2";
    1.86 +
    1.87 +(** Addition **)
    1.88 +
    1.89 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
    1.90 +by (rtac (inj_int RS injD) 1);
    1.91 +by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    1.92 +qed "nat_add_distrib";
    1.93 +
    1.94 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.95 +Goal "(number_of v :: nat) + number_of v' = \
    1.96 +\        (if neg (number_of v) then number_of v' \
    1.97 +\         else if neg (number_of v') then number_of v \
    1.98 +\         else number_of (bin_add v v'))";
    1.99 +by (simp_tac
   1.100 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.101 +				  nat_add_distrib RS sym, number_of_add]) 1);
   1.102 +qed "add_nat_number_of";
   1.103 +
   1.104 +Addsimps [add_nat_number_of];
   1.105 +
   1.106 +
   1.107 +(** Subtraction **)
   1.108 +
   1.109 +Goal "[| (#0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   1.110 +by (rtac (inj_int RS injD) 1);
   1.111 +by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   1.112 +qed "nat_diff_distrib";
   1.113 +
   1.114 +
   1.115 +Goal "nat z - nat z' = \
   1.116 +\       (if neg z' then nat z  \
   1.117 +\        else let d = z-z' in    \
   1.118 +\             if neg d then 0 else nat d)";
   1.119 +by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   1.120 +				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   1.121 +by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   1.122 +qed "diff_nat_eq_if";
   1.123 +
   1.124 +Goalw [nat_number_of_def]
   1.125 +     "(number_of v :: nat) - number_of v' = \
   1.126 +\       (if neg (number_of v') then number_of v \
   1.127 +\        else let d = number_of (bin_add v (bin_minus v')) in    \
   1.128 +\             if neg d then #0 else nat d)";
   1.129 +by (simp_tac
   1.130 +    (simpset_of Int.thy delcongs [if_weak_cong]
   1.131 +			addsimps [not_neg_eq_ge_0, nat_0,
   1.132 +				  diff_nat_eq_if, diff_number_of_eq]) 1);
   1.133 +qed "diff_nat_number_of";
   1.134 +
   1.135 +Addsimps [diff_nat_number_of];
   1.136 +
   1.137 +
   1.138 +(** Multiplication **)
   1.139 +
   1.140 +Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
   1.141 +by (case_tac "#0 <= z'" 1);
   1.142 +by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   1.143 +by (rtac (inj_int RS injD) 1);
   1.144 +by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   1.145 +				      int_0_le_mult_iff]) 1);
   1.146 +qed "nat_mult_distrib";
   1.147 +
   1.148 +Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   1.149 +by (rtac trans 1); 
   1.150 +by (rtac nat_mult_distrib 2); 
   1.151 +by Auto_tac;  
   1.152 +qed "nat_mult_distrib_neg";
   1.153 +
   1.154 +Goal "(number_of v :: nat) * number_of v' = \
   1.155 +\      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
   1.156 +by (simp_tac
   1.157 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.158 +				  nat_mult_distrib RS sym, number_of_mult, 
   1.159 +				  nat_0]) 1);
   1.160 +qed "mult_nat_number_of";
   1.161 +
   1.162 +Addsimps [mult_nat_number_of];
   1.163 +
   1.164 +
   1.165 +(** Quotient **)
   1.166 +
   1.167 +Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
   1.168 +by (case_tac "#0 <= z'" 1);
   1.169 +by (auto_tac (claset(), 
   1.170 +	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
   1.171 +by (zdiv_undefined_case_tac "z' = #0" 1);
   1.172 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   1.173 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.174 +by (rename_tac "m m'" 1);
   1.175 +by (subgoal_tac "#0 <= int m div int m'" 1);
   1.176 + by (asm_full_simp_tac 
   1.177 +     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
   1.178 +by (rtac (inj_int RS injD) 1);
   1.179 +by (Asm_simp_tac 1);
   1.180 +by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   1.181 + by (Force_tac 2);
   1.182 +by (asm_full_simp_tac 
   1.183 +    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   1.184 +	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
   1.185 +by (rtac (mod_div_equality RS sym RS trans) 1);
   1.186 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   1.187 +qed "nat_div_distrib";
   1.188 +
   1.189 +Goal "(number_of v :: nat)  div  number_of v' = \
   1.190 +\         (if neg (number_of v) then #0 \
   1.191 +\          else nat (number_of v div number_of v'))";
   1.192 +by (simp_tac
   1.193 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   1.194 +				  nat_div_distrib RS sym, nat_0]) 1);
   1.195 +qed "div_nat_number_of";
   1.196 +
   1.197 +Addsimps [div_nat_number_of];
   1.198 +
   1.199 +
   1.200 +(** Remainder **)
   1.201 +
   1.202 +(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   1.203 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
   1.204 +by (zdiv_undefined_case_tac "z' = #0" 1);
   1.205 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   1.206 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.207 +by (rename_tac "m m'" 1);
   1.208 +by (subgoal_tac "#0 <= int m mod int m'" 1);
   1.209 + by (asm_full_simp_tac 
   1.210 +     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
   1.211 +by (rtac (inj_int RS injD) 1);
   1.212 +by (Asm_simp_tac 1);
   1.213 +by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   1.214 + by (Force_tac 2);
   1.215 +by (asm_full_simp_tac 
   1.216 +     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   1.217 +		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
   1.218 +by (rtac (mod_div_equality RS sym RS trans) 1);
   1.219 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   1.220 +qed "nat_mod_distrib";
   1.221 +
   1.222 +Goal "(number_of v :: nat)  mod  number_of v' = \
   1.223 +\       (if neg (number_of v) then #0 \
   1.224 +\        else if neg (number_of v') then number_of v \
   1.225 +\        else nat (number_of v mod number_of v'))";
   1.226 +by (simp_tac
   1.227 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   1.228 +				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   1.229 +				  nat_mod_distrib RS sym]) 1);
   1.230 +qed "mod_nat_number_of";
   1.231 +
   1.232 +Addsimps [mod_nat_number_of];
   1.233 +
   1.234 +
   1.235 +(*** Comparisons ***)
   1.236 +
   1.237 +(** Equals (=) **)
   1.238 +
   1.239 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
   1.240 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   1.241 +qed "eq_nat_nat_iff";
   1.242 +
   1.243 +(*"neg" is used in rewrite rules for binary comparisons*)
   1.244 +Goal "((number_of v :: nat) = number_of v') = \
   1.245 +\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   1.246 +\      else if neg (number_of v') then iszero (number_of v) \
   1.247 +\      else iszero (number_of (bin_add v (bin_minus v'))))";
   1.248 +by (simp_tac
   1.249 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.250 +				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   1.251 +by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
   1.252 +					   iszero_def]) 1);
   1.253 +by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   1.254 +qed "eq_nat_number_of";
   1.255 +
   1.256 +Addsimps [eq_nat_number_of];
   1.257 +
   1.258 +(** Less-than (<) **)
   1.259 +
   1.260 +(*"neg" is used in rewrite rules for binary comparisons*)
   1.261 +Goal "((number_of v :: nat) < number_of v') = \
   1.262 +\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   1.263 +\         else neg (number_of (bin_add v (bin_minus v'))))";
   1.264 +by (simp_tac
   1.265 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   1.266 +				  nat_less_eq_zless, less_number_of_eq_neg,
   1.267 +				  nat_0]) 1);
   1.268 +by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
   1.269 +				number_of_minus, zless_nat_eq_int_zless]) 1);
   1.270 +qed "less_nat_number_of";
   1.271 +
   1.272 +Addsimps [less_nat_number_of];
   1.273 +
   1.274 +
   1.275 +(** Less-than-or-equals (<=) **)
   1.276 +
   1.277 +Goal "(number_of x <= (number_of y::nat)) = \
   1.278 +\     (~ number_of y < (number_of x::nat))";
   1.279 +by (rtac (linorder_not_less RS sym) 1);
   1.280 +qed "le_nat_number_of_eq_not_less"; 
   1.281 +
   1.282 +Addsimps [le_nat_number_of_eq_not_less];
   1.283 +
   1.284 +(*** New versions of existing theorems involving 0, 1, 2 ***)
   1.285 +
   1.286 +(*Maps n to #n for n = 0, 1, 2*)
   1.287 +val numeral_sym_ss = 
   1.288 +    HOL_ss addsimps [numeral_0_eq_0 RS sym, 
   1.289 +		     numeral_1_eq_1 RS sym, 
   1.290 +		     numeral_2_eq_2 RS sym,
   1.291 +		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
   1.292 +
   1.293 +fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
   1.294 +
   1.295 +(*Maps #n to n for n = 0, 1, 2*)
   1.296 +val numeral_ss = 
   1.297 +    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
   1.298 +
   1.299 +(** Nat **)
   1.300 +
   1.301 +Goal "#0 < n ==> n = Suc(n - #1)";
   1.302 +by (asm_full_simp_tac numeral_ss 1);
   1.303 +qed "Suc_pred'";
   1.304 +
   1.305 +(*Expresses a natural number constant as the Suc of another one.
   1.306 +  NOT suitable for rewriting because n recurs in the condition.*)
   1.307 +bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   1.308 +
   1.309 +(** NatDef & Nat **)
   1.310 +
   1.311 +Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
   1.312 +
   1.313 +AddIffs (map rename_numerals
   1.314 +	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
   1.315 +	  le0, le_0_eq, 
   1.316 +	  neq0_conv, zero_neq_conv, not_gr0]);
   1.317 +
   1.318 +(** Arith **)
   1.319 +
   1.320 +(*Identity laws for + - * *)	 
   1.321 +val basic_renamed_arith_simps =
   1.322 +    map rename_numerals
   1.323 +        [diff_0, diff_0_eq_0, add_0, add_0_right, 
   1.324 +	 mult_0, mult_0_right, mult_1, mult_1_right];
   1.325 +	 
   1.326 +(*Non-trivial simplifications*)	 
   1.327 +val other_renamed_arith_simps =
   1.328 +    map rename_numerals
   1.329 +	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
   1.330 +	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
   1.331 +
   1.332 +Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
   1.333 +
   1.334 +AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
   1.335 +
   1.336 +Goal "Suc n = n + #1";
   1.337 +by (asm_simp_tac numeral_ss 1);
   1.338 +qed "Suc_eq_add_numeral_1";
   1.339 +
   1.340 +(* These two can be useful when m = number_of... *)
   1.341 +
   1.342 +Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
   1.343 +by (case_tac "m" 1);
   1.344 +by (ALLGOALS (asm_simp_tac numeral_ss));
   1.345 +qed "add_eq_if";
   1.346 +
   1.347 +Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   1.348 +by (case_tac "m" 1);
   1.349 +by (ALLGOALS (asm_simp_tac numeral_ss));
   1.350 +qed "mult_eq_if";
   1.351 +
   1.352 +Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
   1.353 +by (case_tac "m" 1);
   1.354 +by (ALLGOALS (asm_simp_tac numeral_ss));
   1.355 +qed "power_eq_if";
   1.356 +
   1.357 +Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
   1.358 +by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   1.359 +qed "diff_less'";
   1.360 +
   1.361 +Addsimps [inst "n" "number_of ?v" diff_less'];
   1.362 +
   1.363 +(*various theorems that aren't in the default simpset*)
   1.364 +bind_thm ("add_is_one'", rename_numerals add_is_1);
   1.365 +bind_thm ("one_is_add'", rename_numerals one_is_add);
   1.366 +bind_thm ("zero_induct'", rename_numerals zero_induct);
   1.367 +bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
   1.368 +bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
   1.369 +bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
   1.370 +bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
   1.371 +
   1.372 +(** Divides **)
   1.373 +
   1.374 +Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
   1.375 +AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
   1.376 +
   1.377 +(*useful?*)
   1.378 +bind_thm ("mod_self'", rename_numerals mod_self);
   1.379 +bind_thm ("div_self'", rename_numerals div_self);
   1.380 +bind_thm ("div_less'", rename_numerals div_less);
   1.381 +bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
   1.382 +
   1.383 +(** Power **)
   1.384 +
   1.385 +Goal "(p::nat) ^ #0 = #1";
   1.386 +by (simp_tac numeral_ss 1);
   1.387 +qed "power_zero";
   1.388 +
   1.389 +Goal "(p::nat) ^ #1 = p";
   1.390 +by (simp_tac numeral_ss 1);
   1.391 +qed "power_one";
   1.392 +Addsimps [power_zero, power_one];
   1.393 +
   1.394 +Goal "(p::nat) ^ #2 = p*p";
   1.395 +by (simp_tac numeral_ss 1);
   1.396 +qed "power_two";
   1.397 +
   1.398 +Goal "#0 < (i::nat) ==> #0 < i^n";
   1.399 +by (asm_simp_tac numeral_ss 1);
   1.400 +qed "zero_less_power'";
   1.401 +Addsimps [zero_less_power'];
   1.402 +
   1.403 +bind_thm ("binomial_zero", rename_numerals binomial_0);
   1.404 +bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
   1.405 +bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
   1.406 +
   1.407 +(*binomial_0_Suc doesn't work well on numerals*)
   1.408 +Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
   1.409 +
   1.410 +Addsimps [rename_numerals card_Pow];
   1.411 +
   1.412 +(*** Comparisons involving (0::nat) ***)
   1.413 +
   1.414 +Goal "(number_of v = (0::nat)) = \
   1.415 +\     (if neg (number_of v) then True else iszero (number_of v))";
   1.416 +by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   1.417 +qed "eq_number_of_0";
   1.418 +
   1.419 +Goal "((0::nat) = number_of v) = \
   1.420 +\     (if neg (number_of v) then True else iszero (number_of v))";
   1.421 +by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   1.422 +qed "eq_0_number_of";
   1.423 +
   1.424 +Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   1.425 +by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   1.426 +qed "less_0_number_of";
   1.427 +
   1.428 +(*Simplification already handles n<0, n<=0 and 0<=n.*)
   1.429 +Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   1.430 +
   1.431 +Goal "neg (number_of v) ==> number_of v = (0::nat)";
   1.432 +by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   1.433 +qed "neg_imp_number_of_eq_0";
   1.434 +
   1.435 +
   1.436 +
   1.437 +(*** Comparisons involving Suc ***)
   1.438 +
   1.439 +Goal "(number_of v = Suc n) = \
   1.440 +\       (let pv = number_of (bin_pred v) in \
   1.441 +\        if neg pv then False else nat pv = n)";
   1.442 +by (simp_tac
   1.443 +    (simpset_of Int.thy addsimps
   1.444 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   1.445 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   1.446 +by (res_inst_tac [("x", "number_of v")] spec 1);
   1.447 +by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   1.448 +qed "eq_number_of_Suc";
   1.449 +
   1.450 +Goal "(Suc n = number_of v) = \
   1.451 +\       (let pv = number_of (bin_pred v) in \
   1.452 +\        if neg pv then False else nat pv = n)";
   1.453 +by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   1.454 +qed "Suc_eq_number_of";
   1.455 +
   1.456 +Goal "(number_of v < Suc n) = \
   1.457 +\       (let pv = number_of (bin_pred v) in \
   1.458 +\        if neg pv then True else nat pv < n)";
   1.459 +by (simp_tac
   1.460 +    (simpset_of Int.thy addsimps
   1.461 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   1.462 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   1.463 +by (res_inst_tac [("x", "number_of v")] spec 1);
   1.464 +by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   1.465 +qed "less_number_of_Suc";
   1.466 +
   1.467 +Goal "(Suc n < number_of v) = \
   1.468 +\       (let pv = number_of (bin_pred v) in \
   1.469 +\        if neg pv then False else n < nat pv)";
   1.470 +by (simp_tac
   1.471 +    (simpset_of Int.thy addsimps
   1.472 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   1.473 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   1.474 +by (res_inst_tac [("x", "number_of v")] spec 1);
   1.475 +by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   1.476 +qed "less_Suc_number_of";
   1.477 +
   1.478 +Goal "(number_of v <= Suc n) = \
   1.479 +\       (let pv = number_of (bin_pred v) in \
   1.480 +\        if neg pv then True else nat pv <= n)";
   1.481 +by (simp_tac
   1.482 +    (simpset () addsimps
   1.483 +      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   1.484 +qed "le_number_of_Suc";
   1.485 +
   1.486 +Goal "(Suc n <= number_of v) = \
   1.487 +\       (let pv = number_of (bin_pred v) in \
   1.488 +\        if neg pv then False else n <= nat pv)";
   1.489 +by (simp_tac
   1.490 +    (simpset () addsimps
   1.491 +      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   1.492 +qed "le_Suc_number_of";
   1.493 +
   1.494 +Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   1.495 +	  less_number_of_Suc, less_Suc_number_of, 
   1.496 +	  le_number_of_Suc, le_Suc_number_of];
   1.497 +
   1.498 +(* Push int(.) inwards: *)
   1.499 +Addsimps [int_Suc,zadd_int RS sym];
   1.500 +
   1.501 +Goal "(m+m = n+n) = (m = (n::int))";
   1.502 +by Auto_tac;
   1.503 +val lemma1 = result();
   1.504 +
   1.505 +Goal "m+m ~= int 1 + n + n";
   1.506 +by Auto_tac;
   1.507 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   1.508 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   1.509 +val lemma2 = result();
   1.510 +
   1.511 +Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   1.512 +\     (x=y & (((number_of v) ::int) = number_of w))"; 
   1.513 +by (simp_tac (simpset_of Int.thy addsimps
   1.514 +	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   1.515 +qed "eq_number_of_BIT_BIT"; 
   1.516 +
   1.517 +Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
   1.518 +\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
   1.519 +by (simp_tac (simpset_of Int.thy addsimps
   1.520 +	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   1.521 +by (res_inst_tac [("x", "number_of v")] spec 1);
   1.522 +by Safe_tac;
   1.523 +by (ALLGOALS Full_simp_tac);
   1.524 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   1.525 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   1.526 +qed "eq_number_of_BIT_Pls"; 
   1.527 +
   1.528 +Goal "((number_of (v BIT x) ::int) = number_of Min) = \
   1.529 +\     (x=True & (((number_of v) ::int) = number_of Min))"; 
   1.530 +by (simp_tac (simpset_of Int.thy addsimps
   1.531 +	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   1.532 +by (res_inst_tac [("x", "number_of v")] spec 1);
   1.533 +by Auto_tac;
   1.534 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   1.535 +by Auto_tac;
   1.536 +qed "eq_number_of_BIT_Min"; 
   1.537 +
   1.538 +Goal "(number_of Pls ::int) ~= number_of Min"; 
   1.539 +by Auto_tac;
   1.540 +qed "eq_number_of_Pls_Min"; 
   1.541 +
   1.542 +
   1.543 +(*** Further lemmas about "nat" ***)
   1.544 +
   1.545 +Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   1.546 +by (case_tac "z=#0 | w=#0" 1);
   1.547 +by Auto_tac;  
   1.548 +by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   1.549 +                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   1.550 +by (arith_tac 1);
   1.551 +qed "nat_abs_mult_distrib";