--- a/src/HOL/Hyperreal/HyperPow.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Wed Jan 02 16:06:31 2002 +0100
@@ -207,6 +207,22 @@
hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
qed "hrealpow_sum_square_expand";
+
+(*** Literal arithmetic involving powers, type hypreal ***)
+
+Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
+qed "hypreal_of_real_power";
+Addsimps [hypreal_of_real_power];
+
+Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)";
+by (simp_tac (HOL_ss addsimps [hypreal_number_of_def,
+ hypreal_of_real_power]) 1);
+qed "power_hypreal_of_real_number_of";
+
+Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of];
+
(*---------------------------------------------------------------
we'll prove the following theorem by going down to the
level of the ultrafilter and relying on the analogous
@@ -465,9 +481,9 @@
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
qed "hyperpow_realpow";
-Goalw [SReal_def]
- "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
-by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
+Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
+by (simp_tac (simpset() delsimps [hypreal_of_real_power]
+ addsimps [hyperpow_realpow]) 1);
qed "hyperpow_SReal";
Addsimps [hyperpow_SReal];
--- a/src/HOL/Integ/Int.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Integ/Int.ML Wed Jan 02 16:06:31 2002 +0100
@@ -356,11 +356,17 @@
simpset() addsimps [neg_eq_less_0]));
qed "zless_nat_eq_int_zless";
+Goal "0 <= z ==> int (nat z) = z";
+by (asm_full_simp_tac
+ (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
+qed "nat_0_le";
+
Goal "z <= 0 ==> nat z = 0";
by (auto_tac (claset(),
simpset() addsimps [order_le_less, neg_eq_less_0,
zle_def, neg_nat]));
-qed "nat_le_int0";
+qed "nat_le_0";
+Addsimps [nat_0_le, nat_le_0];
(*An alternative condition is 0 <= w *)
Goal "0 < z ==> (nat w < nat z) = (w < z)";
@@ -375,8 +381,7 @@
Goal "(nat w < nat z) = (0 < z & w < z)";
by (case_tac "0 < z" 1);
-by (auto_tac (claset(),
- simpset() addsimps [lemma, nat_le_int0, linorder_not_less]));
+by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less]));
qed "zless_nat_conj";
--- a/src/HOL/Integ/int_arith2.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Integ/int_arith2.ML Wed Jan 02 16:06:31 2002 +0100
@@ -21,20 +21,6 @@
(* nat *)
-Goal "0 <= z ==> int (nat z) = z";
-by (asm_full_simp_tac
- (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
-qed "nat_0_le";
-
-Goal "z <= 0 ==> nat z = 0";
-by (case_tac "z = 0" 1);
-by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
-qed "nat_le_0";
-
-Addsimps [nat_0_le, nat_le_0];
-
val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P";
by (rtac (major RS nat_0_le RS sym RS minor) 1);
qed "nonneg_eq_int";
--- a/src/HOL/Integ/nat_bin.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Integ/nat_bin.ML Wed Jan 02 16:06:31 2002 +0100
@@ -493,3 +493,62 @@
[add_mult_distrib, add_mult_distrib2,
diff_mult_distrib, diff_mult_distrib2]);
+
+(*** Literal arithmetic involving powers, type nat ***)
+
+Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
+qed "nat_power_eq";
+
+Goal "(number_of v :: nat) ^ n = \
+\ (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
+by (simp_tac
+ (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
+ nat_power_eq]) 1);
+qed "power_nat_number_of";
+
+Addsimps [inst "n" "number_of ?w" power_nat_number_of];
+
+
+
+(*** Literal arithmetic involving powers, type int ***)
+
+Goal "(z::int) ^ (2*a) = (z^a)^2";
+by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1);
+qed "zpower_even";
+
+Goal "(p::int) ^ 2 = p*p";
+by (simp_tac numeral_ss 1);
+qed "zpower_two";
+
+Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
+by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1);
+qed "zpower_odd";
+
+Goal "(z::int) ^ number_of (w BIT False) = \
+\ (let w = z ^ (number_of w) in w*w)";
+by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
+ number_of_BIT, Let_def]) 1);
+by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
+by (case_tac "(0::int) <= x" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two]));
+qed "zpower_number_of_even";
+
+Goal "(z::int) ^ number_of (w BIT True) = \
+\ (if (0::int) <= number_of w \
+\ then (let w = z ^ (number_of w) in z*w*w) \
+\ else 1)";
+by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
+ number_of_BIT, Let_def]) 1);
+by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
+by (case_tac "(0::int) <= x" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [nat_add_distrib, nat_mult_distrib,
+ zpower_even, zpower_two]));
+qed "zpower_number_of_odd";
+
+Addsimps (map (inst "z" "number_of ?v")
+ [zpower_number_of_even, zpower_number_of_odd]);
+
--- a/src/HOL/Real/RealBin.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Real/RealBin.ML Wed Jan 02 16:06:31 2002 +0100
@@ -18,7 +18,8 @@
qed "real_numeral_0_eq_0";
Goalw [real_number_of_def] "Numeral1 = (1::real)";
-by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
+by (stac (real_of_one RS sym) 1);
+by (Simp_tac 1);
qed "real_numeral_1_eq_1";
(** Addition **)
--- a/src/HOL/Real/RealInt.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Real/RealInt.ML Wed Jan 02 16:06:31 2002 +0100
@@ -39,12 +39,13 @@
by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
qed "real_of_int_zero";
-Goalw [int_def,real_one_def] "real (int 1) = (1::real)";
+Goal "real (1::int) = (1::real)";
+by (stac (int_1 RS sym) 1);
by (auto_tac (claset(),
- simpset() addsimps [real_of_int,
- preal_of_prat_add RS sym,pnat_two_eq,
- prat_of_pnat_add RS sym,pnat_one_iff RS sym]));
-qed "real_of_int_one";
+ simpset() addsimps [int_def, real_one_def, real_of_int,
+ preal_of_prat_add RS sym,pnat_two_eq,
+ prat_of_pnat_add RS sym, pnat_one_iff RS sym]));
+qed "real_of_one";
Goal "real (x::int) + real y = real (x + y)";
by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
@@ -81,7 +82,7 @@
Addsimps [real_of_int_mult RS sym];
Goal "real (int (Suc n)) = real (int n) + (1::real)";
-by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @
+by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @
zadd_ac) 1);
qed "real_of_int_Suc";
@@ -133,3 +134,6 @@
by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_of_int_le_iff";
Addsimps [real_of_int_le_iff];
+
+Addsimps [real_of_one];
+
--- a/src/HOL/Real/RealPow.ML Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Real/RealPow.ML Wed Jan 02 16:06:31 2002 +0100
@@ -371,3 +371,18 @@
by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
qed "zero_le_realpow_abs";
Addsimps [zero_le_realpow_abs];
+
+
+(*** Literal arithmetic involving powers, type real ***)
+
+Goal "real (x::int) ^ n = real (x ^ n)";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
+qed "real_of_int_power";
+Addsimps [real_of_int_power RS sym];
+
+Goal "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)";
+by (simp_tac (HOL_ss addsimps [real_number_of_def, real_of_int_power]) 1);
+qed "power_real_number_of";
+
+Addsimps [inst "n" "number_of ?w" power_real_number_of];
--- a/src/HOL/Real/ex/BinEx.thy Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/Real/ex/BinEx.thy Wed Jan 02 16:06:31 2002 +0100
@@ -64,6 +64,24 @@
by simp
+text {* \medskip Powers *}
+
+lemma "2 ^ 15 = (32768::real)"
+ by simp
+
+lemma "-3 ^ 7 = (-2187::real)"
+ by simp
+
+lemma "13 ^ 7 = (62748517::real)"
+ by simp
+
+lemma "3 ^ 15 = (14348907::real)"
+ by simp
+
+lemma "-5 ^ 11 = (-48828125::real)"
+ by simp
+
+
text {* \medskip Tests *}
lemma "(x + y = x) = (y = (0::real))"
--- a/src/HOL/ex/BinEx.thy Mon Dec 31 14:13:07 2001 +0100
+++ b/src/HOL/ex/BinEx.thy Wed Jan 02 16:06:31 2002 +0100
@@ -135,6 +135,24 @@
by simp
+text {* \medskip Powers *}
+
+lemma "2 ^ 10 = (1024::int)"
+ by simp
+
+lemma "-3 ^ 7 = (-2187::int)"
+ by simp
+
+lemma "13 ^ 7 = (62748517::int)"
+ by simp
+
+lemma "3 ^ 15 = (14348907::int)"
+ by simp
+
+lemma "-5 ^ 11 = (-48828125::int)"
+ by simp
+
+
subsection {* The Natural Numbers *}
text {* Successor *}
@@ -201,6 +219,24 @@
by simp
+text {* \medskip Powers *}
+
+lemma "2 ^ 12 = (4096::nat)"
+ by simp
+
+lemma "3 ^ 10 = (59049::nat)"
+ by simp
+
+lemma "12 ^ 7 = (35831808::nat)"
+ by simp
+
+lemma "3 ^ 14 = (4782969::nat)"
+ by simp
+
+lemma "5 ^ 11 = (48828125::nat)"
+ by simp
+
+
text {* \medskip Testing the cancellation of complementary terms *}
lemma "y + (x + -x) = (0::int) + y"