src/HOL/Integ/nat_bin.ML
author nipkow
Fri Dec 01 19:53:29 2000 +0100 (2000-12-01)
changeset 10574 8f98f0301d67
child 10693 9e4a0e84d0d6
permissions -rw-r--r--
Linear arithmetic now copes with mixed nat/int formulae.
     1 (*  Title:      HOL/nat_bin.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Binary arithmetic for the natural numbers
     7 *)
     8 
     9 val nat_number_of_def = thm "nat_number_of_def";
    10 
    11 (** nat (coercion from int to nat) **)
    12 
    13 Goal "nat (number_of w) = number_of w";
    14 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    15 qed "nat_number_of";
    16 Addsimps [nat_number_of];
    17 
    18 (*These rewrites should one day be re-oriented...*)
    19 
    20 Goal "#0 = (0::nat)";
    21 by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
    22 qed "numeral_0_eq_0";
    23 
    24 Goal "#1 = (1::nat)";
    25 by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
    26 qed "numeral_1_eq_1";
    27 
    28 Goal "#2 = (2::nat)";
    29 by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
    30 qed "numeral_2_eq_2";
    31 
    32 bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
    33 
    34 (** int (coercion from nat to int) **)
    35 
    36 (*"neg" is used in rewrite rules for binary comparisons*)
    37 Goal "int (number_of v :: nat) = \
    38 \        (if neg (number_of v) then #0 \
    39 \         else (number_of v :: int))";
    40 by (simp_tac
    41     (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
    42 				  not_neg_nat, int_0]) 1);
    43 qed "int_nat_number_of";
    44 Addsimps [int_nat_number_of];
    45 
    46 
    47 val nat_bin_arith_setup =
    48  [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    49    {add_mono_thms = add_mono_thms,
    50     inj_thms = inj_thms,
    51     lessD = lessD,
    52     simpset = simpset addsimps [int_nat_number_of,
    53  not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})];
    54 
    55 (** Successor **)
    56 
    57 Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
    58 by (rtac sym 1);
    59 by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    60 qed "Suc_nat_eq_nat_zadd1";
    61 
    62 Goal "Suc (number_of v) = \
    63 \       (if neg (number_of v) then #1 else number_of (bin_succ v))";
    64 by (simp_tac
    65     (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    66 				  nat_number_of_def, int_Suc, 
    67 				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    68 qed "Suc_nat_number_of";
    69 Addsimps [Suc_nat_number_of];
    70 
    71 Goal "Suc (number_of v + n) = \
    72 \       (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
    73 by (Simp_tac 1);
    74 qed "Suc_nat_number_of_add";
    75 
    76 Goal "Suc #0 = #1";
    77 by (Simp_tac 1);
    78 qed "Suc_numeral_0_eq_1";
    79 
    80 Goal "Suc #1 = #2";
    81 by (Simp_tac 1);
    82 qed "Suc_numeral_1_eq_2";
    83 
    84 (** Addition **)
    85 
    86 Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
    87 by (rtac (inj_int RS injD) 1);
    88 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    89 qed "nat_add_distrib";
    90 
    91 (*"neg" is used in rewrite rules for binary comparisons*)
    92 Goal "(number_of v :: nat) + number_of v' = \
    93 \        (if neg (number_of v) then number_of v' \
    94 \         else if neg (number_of v') then number_of v \
    95 \         else number_of (bin_add v v'))";
    96 by (simp_tac
    97     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
    98 				  nat_add_distrib RS sym, number_of_add]) 1);
    99 qed "add_nat_number_of";
   100 
   101 Addsimps [add_nat_number_of];
   102 
   103 
   104 (** Subtraction **)
   105 
   106 Goal "[| (#0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   107 by (rtac (inj_int RS injD) 1);
   108 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   109 qed "nat_diff_distrib";
   110 
   111 
   112 Goal "nat z - nat z' = \
   113 \       (if neg z' then nat z  \
   114 \        else let d = z-z' in    \
   115 \             if neg d then 0 else nat d)";
   116 by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   117 				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   118 by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   119 qed "diff_nat_eq_if";
   120 
   121 Goalw [nat_number_of_def]
   122      "(number_of v :: nat) - number_of v' = \
   123 \       (if neg (number_of v') then number_of v \
   124 \        else let d = number_of (bin_add v (bin_minus v')) in    \
   125 \             if neg d then #0 else nat d)";
   126 by (simp_tac
   127     (simpset_of Int.thy delcongs [if_weak_cong]
   128 			addsimps [not_neg_eq_ge_0, nat_0,
   129 				  diff_nat_eq_if, diff_number_of_eq]) 1);
   130 qed "diff_nat_number_of";
   131 
   132 Addsimps [diff_nat_number_of];
   133 
   134 
   135 (** Multiplication **)
   136 
   137 Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
   138 by (case_tac "#0 <= z'" 1);
   139 by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   140 by (rtac (inj_int RS injD) 1);
   141 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   142 				      int_0_le_mult_iff]) 1);
   143 qed "nat_mult_distrib";
   144 
   145 Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   146 by (rtac trans 1); 
   147 by (rtac nat_mult_distrib 2); 
   148 by Auto_tac;  
   149 qed "nat_mult_distrib_neg";
   150 
   151 Goal "(number_of v :: nat) * number_of v' = \
   152 \      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
   153 by (simp_tac
   154     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   155 				  nat_mult_distrib RS sym, number_of_mult, 
   156 				  nat_0]) 1);
   157 qed "mult_nat_number_of";
   158 
   159 Addsimps [mult_nat_number_of];
   160 
   161 
   162 (** Quotient **)
   163 
   164 Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
   165 by (case_tac "#0 <= z'" 1);
   166 by (auto_tac (claset(), 
   167 	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
   168 by (zdiv_undefined_case_tac "z' = #0" 1);
   169  by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   170 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   171 by (rename_tac "m m'" 1);
   172 by (subgoal_tac "#0 <= int m div int m'" 1);
   173  by (asm_full_simp_tac 
   174      (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
   175 by (rtac (inj_int RS injD) 1);
   176 by (Asm_simp_tac 1);
   177 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   178  by (Force_tac 2);
   179 by (asm_full_simp_tac 
   180     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   181 	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
   182 by (rtac (mod_div_equality RS sym RS trans) 1);
   183 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   184 qed "nat_div_distrib";
   185 
   186 Goal "(number_of v :: nat)  div  number_of v' = \
   187 \         (if neg (number_of v) then #0 \
   188 \          else nat (number_of v div number_of v'))";
   189 by (simp_tac
   190     (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   191 				  nat_div_distrib RS sym, nat_0]) 1);
   192 qed "div_nat_number_of";
   193 
   194 Addsimps [div_nat_number_of];
   195 
   196 
   197 (** Remainder **)
   198 
   199 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   200 Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
   201 by (zdiv_undefined_case_tac "z' = #0" 1);
   202  by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   203 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   204 by (rename_tac "m m'" 1);
   205 by (subgoal_tac "#0 <= int m mod int m'" 1);
   206  by (asm_full_simp_tac 
   207      (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
   208 by (rtac (inj_int RS injD) 1);
   209 by (Asm_simp_tac 1);
   210 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   211  by (Force_tac 2);
   212 by (asm_full_simp_tac 
   213      (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   214 		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
   215 by (rtac (mod_div_equality RS sym RS trans) 1);
   216 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   217 qed "nat_mod_distrib";
   218 
   219 Goal "(number_of v :: nat)  mod  number_of v' = \
   220 \       (if neg (number_of v) then #0 \
   221 \        else if neg (number_of v') then number_of v \
   222 \        else nat (number_of v mod number_of v'))";
   223 by (simp_tac
   224     (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   225 				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   226 				  nat_mod_distrib RS sym]) 1);
   227 qed "mod_nat_number_of";
   228 
   229 Addsimps [mod_nat_number_of];
   230 
   231 
   232 (*** Comparisons ***)
   233 
   234 (** Equals (=) **)
   235 
   236 Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
   237 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   238 qed "eq_nat_nat_iff";
   239 
   240 (*"neg" is used in rewrite rules for binary comparisons*)
   241 Goal "((number_of v :: nat) = number_of v') = \
   242 \     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   243 \      else if neg (number_of v') then iszero (number_of v) \
   244 \      else iszero (number_of (bin_add v (bin_minus v'))))";
   245 by (simp_tac
   246     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   247 				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   248 by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
   249 					   iszero_def]) 1);
   250 by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   251 qed "eq_nat_number_of";
   252 
   253 Addsimps [eq_nat_number_of];
   254 
   255 (** Less-than (<) **)
   256 
   257 (*"neg" is used in rewrite rules for binary comparisons*)
   258 Goal "((number_of v :: nat) < number_of v') = \
   259 \        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   260 \         else neg (number_of (bin_add v (bin_minus v'))))";
   261 by (simp_tac
   262     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   263 				  nat_less_eq_zless, less_number_of_eq_neg,
   264 				  nat_0]) 1);
   265 by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
   266 				number_of_minus, zless_nat_eq_int_zless]) 1);
   267 qed "less_nat_number_of";
   268 
   269 Addsimps [less_nat_number_of];
   270 
   271 
   272 (** Less-than-or-equals (<=) **)
   273 
   274 Goal "(number_of x <= (number_of y::nat)) = \
   275 \     (~ number_of y < (number_of x::nat))";
   276 by (rtac (linorder_not_less RS sym) 1);
   277 qed "le_nat_number_of_eq_not_less"; 
   278 
   279 Addsimps [le_nat_number_of_eq_not_less];
   280 
   281 (*** New versions of existing theorems involving 0, 1, 2 ***)
   282 
   283 (*Maps n to #n for n = 0, 1, 2*)
   284 val numeral_sym_ss = 
   285     HOL_ss addsimps [numeral_0_eq_0 RS sym, 
   286 		     numeral_1_eq_1 RS sym, 
   287 		     numeral_2_eq_2 RS sym,
   288 		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
   289 
   290 fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
   291 
   292 (*Maps #n to n for n = 0, 1, 2*)
   293 val numeral_ss = 
   294     simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
   295 
   296 (** Nat **)
   297 
   298 Goal "#0 < n ==> n = Suc(n - #1)";
   299 by (asm_full_simp_tac numeral_ss 1);
   300 qed "Suc_pred'";
   301 
   302 (*Expresses a natural number constant as the Suc of another one.
   303   NOT suitable for rewriting because n recurs in the condition.*)
   304 bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   305 
   306 (** NatDef & Nat **)
   307 
   308 Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
   309 
   310 AddIffs (map rename_numerals
   311 	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
   312 	  le0, le_0_eq, 
   313 	  neq0_conv, zero_neq_conv, not_gr0]);
   314 
   315 (** Arith **)
   316 
   317 (*Identity laws for + - * *)	 
   318 val basic_renamed_arith_simps =
   319     map rename_numerals
   320         [diff_0, diff_0_eq_0, add_0, add_0_right, 
   321 	 mult_0, mult_0_right, mult_1, mult_1_right];
   322 	 
   323 (*Non-trivial simplifications*)	 
   324 val other_renamed_arith_simps =
   325     map rename_numerals
   326 	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
   327 	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
   328 
   329 Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
   330 
   331 AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
   332 
   333 Goal "Suc n = n + #1";
   334 by (asm_simp_tac numeral_ss 1);
   335 qed "Suc_eq_add_numeral_1";
   336 
   337 (* These two can be useful when m = number_of... *)
   338 
   339 Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
   340 by (case_tac "m" 1);
   341 by (ALLGOALS (asm_simp_tac numeral_ss));
   342 qed "add_eq_if";
   343 
   344 Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   345 by (case_tac "m" 1);
   346 by (ALLGOALS (asm_simp_tac numeral_ss));
   347 qed "mult_eq_if";
   348 
   349 Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
   350 by (case_tac "m" 1);
   351 by (ALLGOALS (asm_simp_tac numeral_ss));
   352 qed "power_eq_if";
   353 
   354 Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
   355 by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   356 qed "diff_less'";
   357 
   358 Addsimps [inst "n" "number_of ?v" diff_less'];
   359 
   360 (*various theorems that aren't in the default simpset*)
   361 bind_thm ("add_is_one'", rename_numerals add_is_1);
   362 bind_thm ("one_is_add'", rename_numerals one_is_add);
   363 bind_thm ("zero_induct'", rename_numerals zero_induct);
   364 bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
   365 bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
   366 bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
   367 bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
   368 
   369 (** Divides **)
   370 
   371 Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
   372 AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
   373 
   374 (*useful?*)
   375 bind_thm ("mod_self'", rename_numerals mod_self);
   376 bind_thm ("div_self'", rename_numerals div_self);
   377 bind_thm ("div_less'", rename_numerals div_less);
   378 bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
   379 
   380 (** Power **)
   381 
   382 Goal "(p::nat) ^ #0 = #1";
   383 by (simp_tac numeral_ss 1);
   384 qed "power_zero";
   385 
   386 Goal "(p::nat) ^ #1 = p";
   387 by (simp_tac numeral_ss 1);
   388 qed "power_one";
   389 Addsimps [power_zero, power_one];
   390 
   391 Goal "(p::nat) ^ #2 = p*p";
   392 by (simp_tac numeral_ss 1);
   393 qed "power_two";
   394 
   395 Goal "#0 < (i::nat) ==> #0 < i^n";
   396 by (asm_simp_tac numeral_ss 1);
   397 qed "zero_less_power'";
   398 Addsimps [zero_less_power'];
   399 
   400 bind_thm ("binomial_zero", rename_numerals binomial_0);
   401 bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
   402 bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
   403 
   404 (*binomial_0_Suc doesn't work well on numerals*)
   405 Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
   406 
   407 Addsimps [rename_numerals card_Pow];
   408 
   409 (*** Comparisons involving (0::nat) ***)
   410 
   411 Goal "(number_of v = (0::nat)) = \
   412 \     (if neg (number_of v) then True else iszero (number_of v))";
   413 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   414 qed "eq_number_of_0";
   415 
   416 Goal "((0::nat) = number_of v) = \
   417 \     (if neg (number_of v) then True else iszero (number_of v))";
   418 by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   419 qed "eq_0_number_of";
   420 
   421 Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   422 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   423 qed "less_0_number_of";
   424 
   425 (*Simplification already handles n<0, n<=0 and 0<=n.*)
   426 Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   427 
   428 Goal "neg (number_of v) ==> number_of v = (0::nat)";
   429 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   430 qed "neg_imp_number_of_eq_0";
   431 
   432 
   433 
   434 (*** Comparisons involving Suc ***)
   435 
   436 Goal "(number_of v = Suc n) = \
   437 \       (let pv = number_of (bin_pred v) in \
   438 \        if neg pv then False else nat pv = n)";
   439 by (simp_tac
   440     (simpset_of Int.thy addsimps
   441       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   442        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   443 by (res_inst_tac [("x", "number_of v")] spec 1);
   444 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   445 qed "eq_number_of_Suc";
   446 
   447 Goal "(Suc n = number_of v) = \
   448 \       (let pv = number_of (bin_pred v) in \
   449 \        if neg pv then False else nat pv = n)";
   450 by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   451 qed "Suc_eq_number_of";
   452 
   453 Goal "(number_of v < Suc n) = \
   454 \       (let pv = number_of (bin_pred v) in \
   455 \        if neg pv then True else nat pv < n)";
   456 by (simp_tac
   457     (simpset_of Int.thy addsimps
   458       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   459        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   460 by (res_inst_tac [("x", "number_of v")] spec 1);
   461 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   462 qed "less_number_of_Suc";
   463 
   464 Goal "(Suc n < number_of v) = \
   465 \       (let pv = number_of (bin_pred v) in \
   466 \        if neg pv then False else n < nat pv)";
   467 by (simp_tac
   468     (simpset_of Int.thy addsimps
   469       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   470        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   471 by (res_inst_tac [("x", "number_of v")] spec 1);
   472 by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   473 qed "less_Suc_number_of";
   474 
   475 Goal "(number_of v <= Suc n) = \
   476 \       (let pv = number_of (bin_pred v) in \
   477 \        if neg pv then True else nat pv <= n)";
   478 by (simp_tac
   479     (simpset () addsimps
   480       [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   481 qed "le_number_of_Suc";
   482 
   483 Goal "(Suc n <= number_of v) = \
   484 \       (let pv = number_of (bin_pred v) in \
   485 \        if neg pv then False else n <= nat pv)";
   486 by (simp_tac
   487     (simpset () addsimps
   488       [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   489 qed "le_Suc_number_of";
   490 
   491 Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   492 	  less_number_of_Suc, less_Suc_number_of, 
   493 	  le_number_of_Suc, le_Suc_number_of];
   494 
   495 (* Push int(.) inwards: *)
   496 Addsimps [int_Suc,zadd_int RS sym];
   497 
   498 Goal "(m+m = n+n) = (m = (n::int))";
   499 by Auto_tac;
   500 val lemma1 = result();
   501 
   502 Goal "m+m ~= int 1 + n + n";
   503 by Auto_tac;
   504 by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   505 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   506 val lemma2 = result();
   507 
   508 Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   509 \     (x=y & (((number_of v) ::int) = number_of w))"; 
   510 by (simp_tac (simpset_of Int.thy addsimps
   511 	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   512 qed "eq_number_of_BIT_BIT"; 
   513 
   514 Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
   515 \     (x=False & (((number_of v) ::int) = number_of Pls))"; 
   516 by (simp_tac (simpset_of Int.thy addsimps
   517 	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   518 by (res_inst_tac [("x", "number_of v")] spec 1);
   519 by Safe_tac;
   520 by (ALLGOALS Full_simp_tac);
   521 by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   522 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   523 qed "eq_number_of_BIT_Pls"; 
   524 
   525 Goal "((number_of (v BIT x) ::int) = number_of Min) = \
   526 \     (x=True & (((number_of v) ::int) = number_of Min))"; 
   527 by (simp_tac (simpset_of Int.thy addsimps
   528 	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   529 by (res_inst_tac [("x", "number_of v")] spec 1);
   530 by Auto_tac;
   531 by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   532 by Auto_tac;
   533 qed "eq_number_of_BIT_Min"; 
   534 
   535 Goal "(number_of Pls ::int) ~= number_of Min"; 
   536 by Auto_tac;
   537 qed "eq_number_of_Pls_Min"; 
   538 
   539 
   540 (*** Further lemmas about "nat" ***)
   541 
   542 Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   543 by (case_tac "z=#0 | w=#0" 1);
   544 by Auto_tac;  
   545 by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   546                           nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   547 by (arith_tac 1);
   548 qed "nat_abs_mult_distrib";