1.1 --- a/src/HOL/Hyperreal/HyperPow.ML Mon Dec 31 14:13:07 2001 +0100
1.2 +++ b/src/HOL/Hyperreal/HyperPow.ML Wed Jan 02 16:06:31 2002 +0100
1.3 @@ -207,6 +207,22 @@
1.4 hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
1.5 qed "hrealpow_sum_square_expand";
1.6
1.7 +
1.8 +(*** Literal arithmetic involving powers, type hypreal ***)
1.9 +
1.10 +Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n";
1.11 +by (induct_tac "n" 1);
1.12 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
1.13 +qed "hypreal_of_real_power";
1.14 +Addsimps [hypreal_of_real_power];
1.15 +
1.16 +Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)";
1.17 +by (simp_tac (HOL_ss addsimps [hypreal_number_of_def,
1.18 + hypreal_of_real_power]) 1);
1.19 +qed "power_hypreal_of_real_number_of";
1.20 +
1.21 +Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of];
1.22 +
1.23 (*---------------------------------------------------------------
1.24 we'll prove the following theorem by going down to the
1.25 level of the ultrafilter and relying on the analogous
1.26 @@ -465,9 +481,9 @@
1.27 by (auto_tac (claset(), simpset() addsimps [hyperpow]));
1.28 qed "hyperpow_realpow";
1.29
1.30 -Goalw [SReal_def]
1.31 - "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
1.32 -by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
1.33 +Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
1.34 +by (simp_tac (simpset() delsimps [hypreal_of_real_power]
1.35 + addsimps [hyperpow_realpow]) 1);
1.36 qed "hyperpow_SReal";
1.37 Addsimps [hyperpow_SReal];
1.38
2.1 --- a/src/HOL/Integ/Int.ML Mon Dec 31 14:13:07 2001 +0100
2.2 +++ b/src/HOL/Integ/Int.ML Wed Jan 02 16:06:31 2002 +0100
2.3 @@ -356,11 +356,17 @@
2.4 simpset() addsimps [neg_eq_less_0]));
2.5 qed "zless_nat_eq_int_zless";
2.6
2.7 +Goal "0 <= z ==> int (nat z) = z";
2.8 +by (asm_full_simp_tac
2.9 + (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
2.10 +qed "nat_0_le";
2.11 +
2.12 Goal "z <= 0 ==> nat z = 0";
2.13 by (auto_tac (claset(),
2.14 simpset() addsimps [order_le_less, neg_eq_less_0,
2.15 zle_def, neg_nat]));
2.16 -qed "nat_le_int0";
2.17 +qed "nat_le_0";
2.18 +Addsimps [nat_0_le, nat_le_0];
2.19
2.20 (*An alternative condition is 0 <= w *)
2.21 Goal "0 < z ==> (nat w < nat z) = (w < z)";
2.22 @@ -375,8 +381,7 @@
2.23
2.24 Goal "(nat w < nat z) = (0 < z & w < z)";
2.25 by (case_tac "0 < z" 1);
2.26 -by (auto_tac (claset(),
2.27 - simpset() addsimps [lemma, nat_le_int0, linorder_not_less]));
2.28 +by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less]));
2.29 qed "zless_nat_conj";
2.30
2.31
3.1 --- a/src/HOL/Integ/int_arith2.ML Mon Dec 31 14:13:07 2001 +0100
3.2 +++ b/src/HOL/Integ/int_arith2.ML Wed Jan 02 16:06:31 2002 +0100
3.3 @@ -21,20 +21,6 @@
3.4
3.5 (* nat *)
3.6
3.7 -Goal "0 <= z ==> int (nat z) = z";
3.8 -by (asm_full_simp_tac
3.9 - (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1);
3.10 -qed "nat_0_le";
3.11 -
3.12 -Goal "z <= 0 ==> nat z = 0";
3.13 -by (case_tac "z = 0" 1);
3.14 -by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1);
3.15 -by (asm_full_simp_tac
3.16 - (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
3.17 -qed "nat_le_0";
3.18 -
3.19 -Addsimps [nat_0_le, nat_le_0];
3.20 -
3.21 val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P";
3.22 by (rtac (major RS nat_0_le RS sym RS minor) 1);
3.23 qed "nonneg_eq_int";
4.1 --- a/src/HOL/Integ/nat_bin.ML Mon Dec 31 14:13:07 2001 +0100
4.2 +++ b/src/HOL/Integ/nat_bin.ML Wed Jan 02 16:06:31 2002 +0100
4.3 @@ -493,3 +493,62 @@
4.4 [add_mult_distrib, add_mult_distrib2,
4.5 diff_mult_distrib, diff_mult_distrib2]);
4.6
4.7 +
4.8 +(*** Literal arithmetic involving powers, type nat ***)
4.9 +
4.10 +Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
4.11 +by (induct_tac "n" 1);
4.12 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
4.13 +qed "nat_power_eq";
4.14 +
4.15 +Goal "(number_of v :: nat) ^ n = \
4.16 +\ (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
4.17 +by (simp_tac
4.18 + (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
4.19 + nat_power_eq]) 1);
4.20 +qed "power_nat_number_of";
4.21 +
4.22 +Addsimps [inst "n" "number_of ?w" power_nat_number_of];
4.23 +
4.24 +
4.25 +
4.26 +(*** Literal arithmetic involving powers, type int ***)
4.27 +
4.28 +Goal "(z::int) ^ (2*a) = (z^a)^2";
4.29 +by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1);
4.30 +qed "zpower_even";
4.31 +
4.32 +Goal "(p::int) ^ 2 = p*p";
4.33 +by (simp_tac numeral_ss 1);
4.34 +qed "zpower_two";
4.35 +
4.36 +Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
4.37 +by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1);
4.38 +qed "zpower_odd";
4.39 +
4.40 +Goal "(z::int) ^ number_of (w BIT False) = \
4.41 +\ (let w = z ^ (number_of w) in w*w)";
4.42 +by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
4.43 + number_of_BIT, Let_def]) 1);
4.44 +by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
4.45 +by (case_tac "(0::int) <= x" 1);
4.46 +by (auto_tac (claset(),
4.47 + simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two]));
4.48 +qed "zpower_number_of_even";
4.49 +
4.50 +Goal "(z::int) ^ number_of (w BIT True) = \
4.51 +\ (if (0::int) <= number_of w \
4.52 +\ then (let w = z ^ (number_of w) in z*w*w) \
4.53 +\ else 1)";
4.54 +by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
4.55 + number_of_BIT, Let_def]) 1);
4.56 +by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
4.57 +by (case_tac "(0::int) <= x" 1);
4.58 +by (auto_tac (claset(),
4.59 + simpset() addsimps [nat_add_distrib, nat_mult_distrib,
4.60 + zpower_even, zpower_two]));
4.61 +qed "zpower_number_of_odd";
4.62 +
4.63 +Addsimps (map (inst "z" "number_of ?v")
4.64 + [zpower_number_of_even, zpower_number_of_odd]);
4.65 +
5.1 --- a/src/HOL/Real/RealBin.ML Mon Dec 31 14:13:07 2001 +0100
5.2 +++ b/src/HOL/Real/RealBin.ML Wed Jan 02 16:06:31 2002 +0100
5.3 @@ -18,7 +18,8 @@
5.4 qed "real_numeral_0_eq_0";
5.5
5.6 Goalw [real_number_of_def] "Numeral1 = (1::real)";
5.7 -by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
5.8 +by (stac (real_of_one RS sym) 1);
5.9 +by (Simp_tac 1);
5.10 qed "real_numeral_1_eq_1";
5.11
5.12 (** Addition **)
6.1 --- a/src/HOL/Real/RealInt.ML Mon Dec 31 14:13:07 2001 +0100
6.2 +++ b/src/HOL/Real/RealInt.ML Wed Jan 02 16:06:31 2002 +0100
6.3 @@ -39,12 +39,13 @@
6.4 by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
6.5 qed "real_of_int_zero";
6.6
6.7 -Goalw [int_def,real_one_def] "real (int 1) = (1::real)";
6.8 +Goal "real (1::int) = (1::real)";
6.9 +by (stac (int_1 RS sym) 1);
6.10 by (auto_tac (claset(),
6.11 - simpset() addsimps [real_of_int,
6.12 - preal_of_prat_add RS sym,pnat_two_eq,
6.13 - prat_of_pnat_add RS sym,pnat_one_iff RS sym]));
6.14 -qed "real_of_int_one";
6.15 + simpset() addsimps [int_def, real_one_def, real_of_int,
6.16 + preal_of_prat_add RS sym,pnat_two_eq,
6.17 + prat_of_pnat_add RS sym, pnat_one_iff RS sym]));
6.18 +qed "real_of_one";
6.19
6.20 Goal "real (x::int) + real y = real (x + y)";
6.21 by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
6.22 @@ -81,7 +82,7 @@
6.23 Addsimps [real_of_int_mult RS sym];
6.24
6.25 Goal "real (int (Suc n)) = real (int n) + (1::real)";
6.26 -by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @
6.27 +by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @
6.28 zadd_ac) 1);
6.29 qed "real_of_int_Suc";
6.30
6.31 @@ -133,3 +134,6 @@
6.32 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
6.33 qed "real_of_int_le_iff";
6.34 Addsimps [real_of_int_le_iff];
6.35 +
6.36 +Addsimps [real_of_one];
6.37 +
7.1 --- a/src/HOL/Real/RealPow.ML Mon Dec 31 14:13:07 2001 +0100
7.2 +++ b/src/HOL/Real/RealPow.ML Wed Jan 02 16:06:31 2002 +0100
7.3 @@ -371,3 +371,18 @@
7.4 by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
7.5 qed "zero_le_realpow_abs";
7.6 Addsimps [zero_le_realpow_abs];
7.7 +
7.8 +
7.9 +(*** Literal arithmetic involving powers, type real ***)
7.10 +
7.11 +Goal "real (x::int) ^ n = real (x ^ n)";
7.12 +by (induct_tac "n" 1);
7.13 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
7.14 +qed "real_of_int_power";
7.15 +Addsimps [real_of_int_power RS sym];
7.16 +
7.17 +Goal "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)";
7.18 +by (simp_tac (HOL_ss addsimps [real_number_of_def, real_of_int_power]) 1);
7.19 +qed "power_real_number_of";
7.20 +
7.21 +Addsimps [inst "n" "number_of ?w" power_real_number_of];
8.1 --- a/src/HOL/Real/ex/BinEx.thy Mon Dec 31 14:13:07 2001 +0100
8.2 +++ b/src/HOL/Real/ex/BinEx.thy Wed Jan 02 16:06:31 2002 +0100
8.3 @@ -64,6 +64,24 @@
8.4 by simp
8.5
8.6
8.7 +text {* \medskip Powers *}
8.8 +
8.9 +lemma "2 ^ 15 = (32768::real)"
8.10 + by simp
8.11 +
8.12 +lemma "-3 ^ 7 = (-2187::real)"
8.13 + by simp
8.14 +
8.15 +lemma "13 ^ 7 = (62748517::real)"
8.16 + by simp
8.17 +
8.18 +lemma "3 ^ 15 = (14348907::real)"
8.19 + by simp
8.20 +
8.21 +lemma "-5 ^ 11 = (-48828125::real)"
8.22 + by simp
8.23 +
8.24 +
8.25 text {* \medskip Tests *}
8.26
8.27 lemma "(x + y = x) = (y = (0::real))"
9.1 --- a/src/HOL/ex/BinEx.thy Mon Dec 31 14:13:07 2001 +0100
9.2 +++ b/src/HOL/ex/BinEx.thy Wed Jan 02 16:06:31 2002 +0100
9.3 @@ -135,6 +135,24 @@
9.4 by simp
9.5
9.6
9.7 +text {* \medskip Powers *}
9.8 +
9.9 +lemma "2 ^ 10 = (1024::int)"
9.10 + by simp
9.11 +
9.12 +lemma "-3 ^ 7 = (-2187::int)"
9.13 + by simp
9.14 +
9.15 +lemma "13 ^ 7 = (62748517::int)"
9.16 + by simp
9.17 +
9.18 +lemma "3 ^ 15 = (14348907::int)"
9.19 + by simp
9.20 +
9.21 +lemma "-5 ^ 11 = (-48828125::int)"
9.22 + by simp
9.23 +
9.24 +
9.25 subsection {* The Natural Numbers *}
9.26
9.27 text {* Successor *}
9.28 @@ -201,6 +219,24 @@
9.29 by simp
9.30
9.31
9.32 +text {* \medskip Powers *}
9.33 +
9.34 +lemma "2 ^ 12 = (4096::nat)"
9.35 + by simp
9.36 +
9.37 +lemma "3 ^ 10 = (59049::nat)"
9.38 + by simp
9.39 +
9.40 +lemma "12 ^ 7 = (35831808::nat)"
9.41 + by simp
9.42 +
9.43 +lemma "3 ^ 14 = (4782969::nat)"
9.44 + by simp
9.45 +
9.46 +lemma "5 ^ 11 = (48828125::nat)"
9.47 + by simp
9.48 +
9.49 +
9.50 text {* \medskip Testing the cancellation of complementary terms *}
9.51
9.52 lemma "y + (x + -x) = (0::int) + y"