1.1 --- a/src/HOL/Integ/nat_bin.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Integ/nat_bin.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -493,3 +493,62 @@
     1.4  	  [add_mult_distrib, add_mult_distrib2,
     1.5  	   diff_mult_distrib, diff_mult_distrib2]);
     1.6  
     1.7 +
     1.8 +(*** Literal arithmetic involving powers, type nat ***)
     1.9 +
    1.10 +Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
    1.11 +by (induct_tac "n" 1); 
    1.12 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
    1.13 +qed "nat_power_eq";
    1.14 +
    1.15 +Goal "(number_of v :: nat) ^ n = \
    1.16 +\      (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
    1.17 +by (simp_tac
    1.18 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
    1.19 +				  nat_power_eq]) 1);
    1.20 +qed "power_nat_number_of";
    1.21 +
    1.22 +Addsimps [inst "n" "number_of ?w" power_nat_number_of];
    1.23 +
    1.24 +
    1.25 +
    1.26 +(*** Literal arithmetic involving powers, type int ***)
    1.27 +
    1.28 +Goal "(z::int) ^ (2*a) = (z^a)^2";
    1.29 +by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1); 
    1.30 +qed "zpower_even";
    1.31 +
    1.32 +Goal "(p::int) ^ 2 = p*p"; 
    1.33 +by (simp_tac numeral_ss 1);
    1.34 +qed "zpower_two";  
    1.35 +
    1.36 +Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
    1.37 +by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); 
    1.38 +qed "zpower_odd";
    1.39 +
    1.40 +Goal "(z::int) ^ number_of (w BIT False) = \
    1.41 +\     (let w = z ^ (number_of w) in  w*w)";
    1.42 +by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
    1.43 +        number_of_BIT, Let_def]) 1);
    1.44 +by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
    1.45 +by (case_tac "(0::int) <= x" 1);
    1.46 +by (auto_tac (claset(), 
    1.47 +     simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); 
    1.48 +qed "zpower_number_of_even";
    1.49 +
    1.50 +Goal "(z::int) ^ number_of (w BIT True) = \
    1.51 +\         (if (0::int) <= number_of w                   \
    1.52 +\          then (let w = z ^ (number_of w) in  z*w*w)   \
    1.53 +\          else 1)";
    1.54 +by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
    1.55 +        number_of_BIT, Let_def]) 1);
    1.56 +by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
    1.57 +by (case_tac "(0::int) <= x" 1);
    1.58 +by (auto_tac (claset(), 
    1.59 +              simpset() addsimps [nat_add_distrib, nat_mult_distrib, 
    1.60 +                                  zpower_even, zpower_two])); 
    1.61 +qed "zpower_number_of_odd";
    1.62 +
    1.63 +Addsimps (map (inst "z" "number_of ?v")
    1.64 +              [zpower_number_of_even, zpower_number_of_odd]);
    1.65 +