# HG changeset patch # User paulson # Date 1009983991 -3600 # Node ID 279facb4253ae237dac05f04638698293e0411ed # Parent 2a64142500f6e090d58bacc1371edb5db202e3c2 Literal arithmetic: raising numbers to powers (nat, int, real, hypreal) diff -r 2a64142500f6 -r 279facb4253a src/HOL/Hyperreal/HyperPow.ML --- 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]; diff -r 2a64142500f6 -r 279facb4253a src/HOL/Integ/Int.ML --- 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"; diff -r 2a64142500f6 -r 279facb4253a src/HOL/Integ/int_arith2.ML --- 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"; diff -r 2a64142500f6 -r 279facb4253a src/HOL/Integ/nat_bin.ML --- 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]); + diff -r 2a64142500f6 -r 279facb4253a src/HOL/Real/RealBin.ML --- 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 **) diff -r 2a64142500f6 -r 279facb4253a src/HOL/Real/RealInt.ML --- 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]; + diff -r 2a64142500f6 -r 279facb4253a src/HOL/Real/RealPow.ML --- 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]; diff -r 2a64142500f6 -r 279facb4253a src/HOL/Real/ex/BinEx.thy --- 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))" diff -r 2a64142500f6 -r 279facb4253a src/HOL/ex/BinEx.thy --- 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"