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