src/HOL/Integ/nat_bin.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 13261 a0460a450cf9
child 13485 acf39e924091
permissions -rw-r--r--
sane interface for simprocs;
     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, nat_0, nat_1];
    17 
    18 Goal "Numeral0 = (0::nat)";
    19 by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); 
    20 qed "numeral_0_eq_0";
    21 
    22 Goal "Numeral1 = (1::nat)";
    23 by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); 
    24 qed "numeral_1_eq_1";
    25 
    26 Goal "Numeral1 = Suc 0";
    27 by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1); 
    28 qed "numeral_1_eq_Suc_0";
    29 
    30 Goalw [nat_number_of_def] "2 = Suc (Suc 0)";
    31 by (rtac nat_2 1); 
    32 qed "numeral_2_eq_2";
    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 (** Successor **)
    48 
    49 Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
    50 by (rtac sym 1);
    51 by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
    52 qed "Suc_nat_eq_nat_zadd1";
    53 
    54 Goal "Suc (number_of v + n) = \
    55 \       (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
    56 by (simp_tac
    57     (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    58 				  nat_number_of_def, int_Suc, 
    59 				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    60 qed "Suc_nat_number_of_add";
    61 
    62 Goal "Suc (number_of v) = \
    63 \       (if neg (number_of v) then 1 else number_of (bin_succ v))";
    64 by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);
    65 by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); 
    66 qed "Suc_nat_number_of";
    67 Addsimps [Suc_nat_number_of];
    68 
    69 val nat_bin_arith_setup =
    70  [Fast_Arith.map_data 
    71    (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    72      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    73       inj_thms = inj_thms,
    74       lessD = lessD,
    75       simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
    76                                   not_neg_number_of_Pls,
    77                                   neg_number_of_Min,neg_number_of_BIT]})];
    78 
    79 (** Addition **)
    80 
    81 Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z+z') = nat z + nat z'";
    82 by (rtac (inj_int RS injD) 1);
    83 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    84 qed "nat_add_distrib";
    85 
    86 (*"neg" is used in rewrite rules for binary comparisons*)
    87 Goal "(number_of v :: nat) + number_of v' = \
    88 \        (if neg (number_of v) then number_of v' \
    89 \         else if neg (number_of v') then number_of v \
    90 \         else number_of (bin_add v v'))";
    91 by (simp_tac
    92     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
    93 				  nat_add_distrib RS sym, number_of_add]) 1);
    94 qed "add_nat_number_of";
    95 
    96 Addsimps [add_nat_number_of];
    97 
    98 
    99 (** Subtraction **)
   100 
   101 Goal "[| (0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   102 by (rtac (inj_int RS injD) 1);
   103 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   104 qed "nat_diff_distrib";
   105 
   106 
   107 Goal "nat z - nat z' = \
   108 \       (if neg z' then nat z  \
   109 \        else let d = z-z' in    \
   110 \             if neg d then 0 else nat d)";
   111 by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   112 				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   113 by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   114 qed "diff_nat_eq_if";
   115 
   116 Goalw [nat_number_of_def]
   117      "(number_of v :: nat) - number_of v' = \
   118 \       (if neg (number_of v') then number_of v \
   119 \        else let d = number_of (bin_add v (bin_minus v')) in    \
   120 \             if neg d then 0 else nat d)";
   121 by (simp_tac
   122     (simpset_of Int.thy delcongs [if_weak_cong]
   123 			addsimps [not_neg_eq_ge_0, nat_0,
   124 				  diff_nat_eq_if, diff_number_of_eq]) 1);
   125 qed "diff_nat_number_of";
   126 
   127 Addsimps [diff_nat_number_of];
   128 
   129 
   130 (** Multiplication **)
   131 
   132 Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
   133 by (case_tac "0 <= z'" 1);
   134 by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   135 by (rtac (inj_int RS injD) 1);
   136 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   137 				      int_0_le_mult_iff]) 1);
   138 qed "nat_mult_distrib";
   139 
   140 Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   141 by (rtac trans 1); 
   142 by (rtac nat_mult_distrib 2); 
   143 by Auto_tac;  
   144 qed "nat_mult_distrib_neg";
   145 
   146 Goal "(number_of v :: nat) * number_of v' = \
   147 \      (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
   148 by (simp_tac
   149     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   150 				  nat_mult_distrib RS sym, number_of_mult, 
   151 				  nat_0]) 1);
   152 qed "mult_nat_number_of";
   153 
   154 Addsimps [mult_nat_number_of];
   155 
   156 
   157 (** Quotient **)
   158 
   159 Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
   160 by (case_tac "0 <= z'" 1);
   161 by (auto_tac (claset(), 
   162 	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
   163 by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
   164  by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   165 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   166 by (rename_tac "m m'" 1);
   167 by (subgoal_tac "0 <= int m div int m'" 1);
   168  by (asm_full_simp_tac 
   169      (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
   170 by (rtac (inj_int RS injD) 1);
   171 by (Asm_simp_tac 1);
   172 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   173  by (Force_tac 2);
   174 by (asm_full_simp_tac 
   175     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   176 	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
   177 by (rtac (mod_div_equality RS sym RS trans) 1);
   178 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   179 qed "nat_div_distrib";
   180 
   181 Goal "(number_of v :: nat)  div  number_of v' = \
   182 \         (if neg (number_of v) then 0 \
   183 \          else nat (number_of v div number_of v'))";
   184 by (simp_tac
   185     (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   186 				  nat_div_distrib RS sym, nat_0]) 1);
   187 qed "div_nat_number_of";
   188 
   189 Addsimps [div_nat_number_of];
   190 
   191 
   192 (** Remainder **)
   193 
   194 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   195 Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
   196 by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
   197  by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   198 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   199 by (rename_tac "m m'" 1);
   200 by (subgoal_tac "0 <= int m mod int m'" 1);
   201  by (asm_full_simp_tac 
   202      (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
   203 by (rtac (inj_int RS injD) 1);
   204 by (Asm_simp_tac 1);
   205 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   206  by (Force_tac 2);
   207 by (asm_full_simp_tac 
   208      (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   209 		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
   210 by (rtac (mod_div_equality RS sym RS trans) 1);
   211 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   212 qed "nat_mod_distrib";
   213 
   214 Goal "(number_of v :: nat)  mod  number_of v' = \
   215 \       (if neg (number_of v) then 0 \
   216 \        else if neg (number_of v') then number_of v \
   217 \        else nat (number_of v mod number_of v'))";
   218 by (simp_tac
   219     (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   220 				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   221 				  nat_mod_distrib RS sym]) 1);
   222 qed "mod_nat_number_of";
   223 
   224 Addsimps [mod_nat_number_of];
   225 
   226 structure NatAbstractNumeralsData =
   227   struct
   228   val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   229   val is_numeral	= Bin_Simprocs.is_numeral
   230   val numeral_0_eq_0    = numeral_0_eq_0
   231   val numeral_1_eq_1    = numeral_1_eq_Suc_0
   232   val prove_conv   = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals"
   233   fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   234   val simplify_meta_eq  = Bin_Simprocs.simplify_meta_eq 
   235   end
   236 
   237 structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData)
   238 
   239 val nat_eval_numerals = 
   240   map Bin_Simprocs.prep_simproc
   241    [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
   242     ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];
   243 
   244 Addsimprocs nat_eval_numerals;
   245 
   246 
   247 (*** Comparisons ***)
   248 
   249 (** Equals (=) **)
   250 
   251 Goal "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')";
   252 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   253 qed "eq_nat_nat_iff";
   254 
   255 (*"neg" is used in rewrite rules for binary comparisons*)
   256 Goal "((number_of v :: nat) = number_of v') = \
   257 \     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   258 \      else if neg (number_of v') then iszero (number_of v) \
   259 \      else iszero (number_of (bin_add v (bin_minus v'))))";
   260 by (simp_tac
   261     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   262 				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   263 by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
   264 					   iszero_def]) 1);
   265 by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   266 qed "eq_nat_number_of";
   267 
   268 Addsimps [eq_nat_number_of];
   269 
   270 (** Less-than (<) **)
   271 
   272 (*"neg" is used in rewrite rules for binary comparisons*)
   273 Goal "((number_of v :: nat) < number_of v') = \
   274 \        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   275 \         else neg (number_of (bin_add v (bin_minus v'))))";
   276 by (simp_tac
   277     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   278 				  nat_less_eq_zless, less_number_of_eq_neg,
   279 				  nat_0]) 1);
   280 by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless, 
   281 				number_of_minus, zless_nat_eq_int_zless]) 1);
   282 qed "less_nat_number_of";
   283 
   284 Addsimps [less_nat_number_of];
   285 
   286 
   287 (** Less-than-or-equals (<=) **)
   288 
   289 Goal "(number_of x <= (number_of y::nat)) = \
   290 \     (~ number_of y < (number_of x::nat))";
   291 by (rtac (linorder_not_less RS sym) 1);
   292 qed "le_nat_number_of_eq_not_less"; 
   293 
   294 Addsimps [le_nat_number_of_eq_not_less];
   295 
   296 
   297 (*Maps #n to n for n = 0, 1, 2*)
   298 bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
   299 val numeral_ss = simpset() addsimps numerals;
   300 
   301 (** Nat **)
   302 
   303 Goal "0 < n ==> n = Suc(n - 1)";
   304 by (asm_full_simp_tac numeral_ss 1);
   305 qed "Suc_pred'";
   306 
   307 (*Expresses a natural number constant as the Suc of another one.
   308   NOT suitable for rewriting because n recurs in the condition.*)
   309 bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   310 
   311 (** Arith **)
   312 
   313 Goal "Suc n = n + 1";
   314 by (asm_simp_tac numeral_ss 1);
   315 qed "Suc_eq_add_numeral_1";
   316 
   317 (* These two can be useful when m = number_of... *)
   318 
   319 Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))";
   320 by (case_tac "m" 1);
   321 by (ALLGOALS (asm_simp_tac numeral_ss));
   322 qed "add_eq_if";
   323 
   324 Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))";
   325 by (case_tac "m" 1);
   326 by (ALLGOALS (asm_simp_tac numeral_ss));
   327 qed "mult_eq_if";
   328 
   329 Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))";
   330 by (case_tac "m" 1);
   331 by (ALLGOALS (asm_simp_tac numeral_ss));
   332 qed "power_eq_if";
   333 
   334 Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)";
   335 by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   336 qed "diff_less'";
   337 
   338 Addsimps [inst "n" "number_of ?v" diff_less'];
   339 
   340 (** Power **)
   341 
   342 Goal "(p::nat) ^ 2 = p*p";
   343 by (simp_tac numeral_ss 1);
   344 qed "power_two";
   345 
   346 
   347 (*** Comparisons involving (0::nat) ***)
   348 
   349 Goal "(number_of v = (0::nat)) = \
   350 \     (if neg (number_of v) then True else iszero (number_of v))";
   351 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
   352 qed "eq_number_of_0"; 
   353 
   354 Goal "((0::nat) = number_of v) = \
   355 \     (if neg (number_of v) then True else iszero (number_of v))";
   356 by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   357 qed "eq_0_number_of";
   358 
   359 Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   360 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   361 qed "less_0_number_of";
   362 
   363 (*Simplification already handles n<0, n<=0 and 0<=n.*)
   364 Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   365 
   366 Goal "neg (number_of v) ==> number_of v = (0::nat)";
   367 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
   368 qed "neg_imp_number_of_eq_0";
   369 
   370 
   371 
   372 (*** Comparisons involving Suc ***)
   373 
   374 Goal "(number_of v = Suc n) = \
   375 \       (let pv = number_of (bin_pred v) in \
   376 \        if neg pv then False else nat pv = n)";
   377 by (simp_tac
   378     (simpset_of Int.thy addsimps
   379       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   380        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   381 by (res_inst_tac [("x", "number_of v")] spec 1);
   382 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   383 qed "eq_number_of_Suc";
   384 
   385 Goal "(Suc n = number_of v) = \
   386 \       (let pv = number_of (bin_pred v) in \
   387 \        if neg pv then False else nat pv = n)";
   388 by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   389 qed "Suc_eq_number_of";
   390 
   391 Goal "(number_of v < Suc n) = \
   392 \       (let pv = number_of (bin_pred v) in \
   393 \        if neg pv then True else nat pv < n)";
   394 by (simp_tac
   395     (simpset_of Int.thy addsimps
   396       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   397        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   398 by (res_inst_tac [("x", "number_of v")] spec 1);
   399 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   400 qed "less_number_of_Suc";
   401 
   402 Goal "(Suc n < number_of v) = \
   403 \       (let pv = number_of (bin_pred v) in \
   404 \        if neg pv then False else n < nat pv)";
   405 by (simp_tac
   406     (simpset_of Int.thy addsimps
   407       [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   408        nat_number_of_def, zadd_0] @ zadd_ac) 1);
   409 by (res_inst_tac [("x", "number_of v")] spec 1);
   410 by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   411 qed "less_Suc_number_of";
   412 
   413 Goal "(number_of v <= Suc n) = \
   414 \       (let pv = number_of (bin_pred v) in \
   415 \        if neg pv then True else nat pv <= n)";
   416 by (simp_tac
   417     (simpset () addsimps
   418       [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   419 qed "le_number_of_Suc";
   420 
   421 Goal "(Suc n <= number_of v) = \
   422 \       (let pv = number_of (bin_pred v) in \
   423 \        if neg pv then False else n <= nat pv)";
   424 by (simp_tac
   425     (simpset () addsimps
   426       [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   427 qed "le_Suc_number_of";
   428 
   429 Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   430 	  less_number_of_Suc, less_Suc_number_of, 
   431 	  le_number_of_Suc, le_Suc_number_of];
   432 
   433 (* Push int(.) inwards: *)
   434 Addsimps [zadd_int RS sym];
   435 
   436 Goal "(m+m = n+n) = (m = (n::int))";
   437 by Auto_tac;
   438 val lemma1 = result();
   439 
   440 Goal "m+m ~= (1::int) + n + n";
   441 by Auto_tac;
   442 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   443 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   444 val lemma2 = result();
   445 
   446 Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   447 \     (x=y & (((number_of v) ::int) = number_of w))"; 
   448 by (simp_tac (simpset_of Int.thy addsimps
   449 	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   450 qed "eq_number_of_BIT_BIT"; 
   451 
   452 Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
   453 \     (x=False & (((number_of v) ::int) = number_of Pls))"; 
   454 by (simp_tac (simpset_of Int.thy addsimps
   455 	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   456 by (res_inst_tac [("x", "number_of v")] spec 1);
   457 by Safe_tac;
   458 by (ALLGOALS Full_simp_tac);
   459 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   460 by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   461 qed "eq_number_of_BIT_Pls"; 
   462 
   463 Goal "((number_of (v BIT x) ::int) = number_of Min) = \
   464 \     (x=True & (((number_of v) ::int) = number_of Min))"; 
   465 by (simp_tac (simpset_of Int.thy addsimps
   466 	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   467 by (res_inst_tac [("x", "number_of v")] spec 1);
   468 by Auto_tac;
   469 by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   470 by Auto_tac;
   471 qed "eq_number_of_BIT_Min"; 
   472 
   473 Goal "(number_of Pls ::int) ~= number_of Min"; 
   474 by Auto_tac;
   475 qed "eq_number_of_Pls_Min"; 
   476 
   477 
   478 (*** Further lemmas about "nat" ***)
   479 
   480 Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   481 by (case_tac "z=0 | w=0" 1);
   482 by Auto_tac;  
   483 by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   484                           nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   485 by (arith_tac 1);
   486 qed "nat_abs_mult_distrib";
   487 
   488 (*Distributive laws for literals*)
   489 Addsimps (map (inst "k" "number_of ?v")
   490 	  [add_mult_distrib, add_mult_distrib2,
   491 	   diff_mult_distrib, diff_mult_distrib2]);
   492 
   493 
   494 (*** Literal arithmetic involving powers, type nat ***)
   495 
   496 Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
   497 by (induct_tac "n" 1); 
   498 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
   499 qed "nat_power_eq";
   500 
   501 Goal "(number_of v :: nat) ^ n = \
   502 \      (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
   503 by (simp_tac
   504     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   505 				  nat_power_eq]) 1);
   506 qed "power_nat_number_of";
   507 
   508 Addsimps [inst "n" "number_of ?w" power_nat_number_of];
   509 
   510 
   511 
   512 (*** Literal arithmetic involving powers, type int ***)
   513 
   514 Goal "(z::int) ^ (2*a) = (z^a)^2";
   515 by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1); 
   516 qed "zpower_even";
   517 
   518 Goal "(p::int) ^ 2 = p*p"; 
   519 by (simp_tac numeral_ss 1);
   520 qed "zpower_two";  
   521 
   522 Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
   523 by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); 
   524 qed "zpower_odd";
   525 
   526 Goal "(z::int) ^ number_of (w BIT False) = \
   527 \     (let w = z ^ (number_of w) in  w*w)";
   528 by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
   529         number_of_BIT, Let_def]) 1);
   530 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
   531 by (case_tac "(0::int) <= x" 1);
   532 by (auto_tac (claset(), 
   533      simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); 
   534 qed "zpower_number_of_even";
   535 
   536 Goal "(z::int) ^ number_of (w BIT True) = \
   537 \         (if (0::int) <= number_of w                   \
   538 \          then (let w = z ^ (number_of w) in  z*w*w)   \
   539 \          else 1)";
   540 by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
   541         number_of_BIT, Let_def]) 1);
   542 by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
   543 by (case_tac "(0::int) <= x" 1);
   544 by (auto_tac (claset(), 
   545               simpset() addsimps [nat_add_distrib, nat_mult_distrib, 
   546                                   zpower_even, zpower_two])); 
   547 qed "zpower_number_of_odd";
   548 
   549 Addsimps (map (inst "z" "number_of ?v")
   550               [zpower_number_of_even, zpower_number_of_odd]);
   551