--- a/src/HOL/Hyperreal/HyperPow.thy Thu Dec 14 18:10:38 2006 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Thu Dec 14 19:15:16 2006 +0100
@@ -20,9 +20,9 @@
definition
(* hypernatural powers of hyperreals *)
- pow :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80) where
+ pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
hyperpow_def [transfer_unfold]:
- "(R::hypreal) pow (N::hypnat) = ( *f2* op ^) R N"
+ "R pow N = ( *f2* op ^) R N"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
by simp
@@ -101,55 +101,72 @@
lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
by (simp add: hyperpow_def starfun2_star_n)
-lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
-by (transfer, simp)
+lemma hyperpow_zero [simp]:
+ "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
+by transfer simp
-lemma hyperpow_not_zero: "!!r n. r \<noteq> (0::hypreal) ==> r pow n \<noteq> 0"
-by (transfer, simp)
+lemma hyperpow_not_zero:
+ "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
+by transfer (rule field_power_not_zero)
lemma hyperpow_inverse:
- "!!r n. r \<noteq> (0::hypreal) ==> inverse(r pow n) = (inverse r) pow n"
-by (transfer, rule power_inverse)
+ "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
+ \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
+by transfer (rule power_inverse)
-lemma hyperpow_hrabs: "!!r n. abs r pow n = abs (r pow n)"
-by (transfer, rule power_abs [symmetric])
+lemma hyperpow_hrabs:
+ "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
+by transfer (rule power_abs [symmetric])
-lemma hyperpow_add: "!!r n m. r pow (n + m) = (r pow n) * (r pow m)"
-by (transfer, rule power_add)
+lemma hyperpow_add:
+ "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
+by transfer (rule power_add)
-lemma hyperpow_one [simp]: "!!r. r pow (1::hypnat) = r"
-by (transfer, simp)
+lemma hyperpow_one [simp]:
+ "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
+by transfer (rule power_one_right)
lemma hyperpow_two:
- "!!r. r pow ((1::hypnat) + (1::hypnat)) = r * r"
-by (transfer, simp)
+ "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
+by transfer (simp add: power_Suc)
-lemma hyperpow_gt_zero: "!!r n. (0::hypreal) < r ==> 0 < r pow n"
-by (transfer, rule zero_less_power)
+lemma hyperpow_gt_zero:
+ "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
+by transfer (rule zero_less_power)
-lemma hyperpow_ge_zero: "!!r n. (0::hypreal) \<le> r ==> 0 \<le> r pow n"
-by (transfer, rule zero_le_power)
+lemma hyperpow_ge_zero:
+ "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
+by transfer (rule zero_le_power)
lemma hyperpow_le:
- "!!x y n. [|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-by (transfer, rule power_mono [OF _ order_less_imp_le])
+ "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
+ \<Longrightarrow> x pow n \<le> y pow n"
+by transfer (rule power_mono [OF _ order_less_imp_le])
-lemma hyperpow_eq_one [simp]: "!!n. 1 pow n = (1::hypreal)"
-by (transfer, simp)
+lemma hyperpow_eq_one [simp]:
+ "\<And>n. 1 pow n = (1::'a::recpower star)"
+by transfer (rule power_one)
-lemma hrabs_hyperpow_minus_one [simp]: "!!n. abs(-1 pow n) = (1::hypreal)"
-by (transfer, simp)
+lemma hrabs_hyperpow_minus_one [simp]:
+ "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
+by transfer (rule abs_power_minus_one)
-lemma hyperpow_mult: "!!r s n. (r * s) pow n = (r pow n) * (s pow n)"
-by (transfer, rule power_mult_distrib)
+lemma hyperpow_mult:
+ "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
+ = (r pow n) * (s pow n)"
+by transfer (rule power_mult_distrib)
-lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
+lemma hyperpow_two_le [simp]:
+ "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
by (auto simp add: hyperpow_two zero_le_mult_iff)
-lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
-by (simp add: abs_if hyperpow_two_le linorder_not_less)
+lemma hrabs_hyperpow_two [simp]:
+ "abs(x pow (1 + 1)) =
+ (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
+by (simp only: abs_of_nonneg hyperpow_two_le)
-lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)"
+lemma hyperpow_two_hrabs [simp]:
+ "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
by (simp add: hyperpow_hrabs)
text{*The precondition could be weakened to @{term "0\<le>x"}*}
@@ -157,15 +174,13 @@
"[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
-lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)"
-apply (auto simp add: hyperpow_two)
-apply (rule_tac y = "1*1" in order_le_less_trans)
-apply (rule_tac [2] hypreal_mult_less_mono, auto)
-done
+lemma hyperpow_two_gt_one:
+ "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
+by transfer (simp add: power_gt1)
lemma hyperpow_two_ge_one:
- "1 \<le> r ==> 1 \<le> r pow (1 + 1)"
-by (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
+ "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
+by transfer (simp add: one_le_power)
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
apply (rule_tac y = "1 pow n" in order_trans)
@@ -174,11 +189,11 @@
lemma hyperpow_minus_one2 [simp]:
"!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
-by (transfer, simp)
+by transfer (simp)
lemma hyperpow_less_le:
"!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-by (transfer, rule power_decreasing [OF order_less_imp_le])
+by transfer (rule power_decreasing [OF order_less_imp_le])
lemma hyperpow_SHNat_le:
"[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |]
@@ -211,23 +226,24 @@
done
lemma lemma_Infinitesimal_hyperpow:
- "[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
+ "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
apply (unfold Infinitesimal_def)
apply (auto intro!: hyperpow_Suc_le_self2
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
done
lemma Infinitesimal_hyperpow:
- "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
+ "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
apply (rule hrabs_le_Infinitesimal)
apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
done
+lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
+by transfer (rule refl)
+
lemma hrealpow_hyperpow_Infinitesimal_iff:
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (cases x)
-apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
-done
+by (simp only: hyperpow_hypnat_of_nat)
lemma Infinitesimal_hrealpow:
"[| (x::hypreal) \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"