--- a/src/HOL/Hyperreal/HyperPow.thy Fri Sep 09 17:47:37 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Fri Sep 09 19:34:22 2005 +0200
@@ -10,22 +10,7 @@
imports HyperArith HyperNat
begin
-(* instance hypreal :: power .. *)
-
-consts hpowr :: "[hypreal,nat] => hypreal"
-(*
-primrec
- hpowr_0: "r ^ 0 = (1::hypreal)"
- hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
-
-instance hypreal :: recpower
-proof
- fix z :: hypreal
- fix n :: nat
- show "z^0 = 1" by simp
- show "z^(Suc n) = z * (z^n)" by simp
-qed
-*)
+(* consts hpowr :: "[hypreal,nat] => hypreal" *)
lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
by (rule power_0)
@@ -34,15 +19,13 @@
by (rule power_Suc)
consts
- "pow" :: "[hypreal,hypnat] => hypreal" (infixr 80)
+ "pow" :: "[hypreal,hypnat] => hypreal" (infixr "pow" 80)
defs
(* hypernatural powers of hyperreals *)
hyperpow_def:
- "(R::hypreal) pow (N::hypnat) ==
- Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_star(N).
- starrel``{%n::nat. (X n) ^ (Y n)})"
+ "(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
by simp
@@ -52,11 +35,11 @@
lemma hrealpow_two_le_add_order [simp]:
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
-by (simp only: hrealpow_two_le hypreal_le_add_order)
+by (simp only: hrealpow_two_le add_nonneg_nonneg)
lemma hrealpow_two_le_add_order2 [simp]:
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
-by (simp only: hrealpow_two_le hypreal_le_add_order)
+by (simp only: hrealpow_two_le add_nonneg_nonneg)
lemma hypreal_add_nonneg_eq_0_iff:
"[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
@@ -66,7 +49,7 @@
text{*FIXME: DELETE THESE*}
lemma hypreal_three_squares_add_zero_iff:
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
-apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
+apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
done
lemma hrealpow_three_squares_add_zero_iff [simp]:
@@ -90,9 +73,9 @@
done
lemma hrealpow:
- "Abs_star(starrel``{%n. X n}) ^ m = Abs_star(starrel``{%n. (X n::real) ^ m})"
+ "star_n X ^ m = star_n (%n. (X n::real) ^ m)"
apply (induct_tac "m")
-apply (auto simp add: hypreal_one_def hypreal_mult power_0)
+apply (auto simp add: star_n_one_num star_n_mult power_0)
done
lemma hrealpow_sum_square_expand:
@@ -103,14 +86,10 @@
subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
-lemma hypreal_of_real_power [simp]:
- "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
-by (induct_tac "n", simp_all add: nat_mult_distrib)
-
lemma power_hypreal_of_real_number_of:
"(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
-by (simp only: hypreal_number_of [symmetric] hypreal_of_real_power)
-
+by simp
+(* why is this a simp rule? - BH *)
declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite"
@@ -121,98 +100,50 @@
subsection{*Powers with Hypernatural Exponents*}
-lemma hyperpow_congruent: "(%X Y. starrel``{%n. (X n ^ Y n)}) respects starrel"
-by (auto simp add: congruent_def intro!: ext, fuf+)
-
-lemma hyperpow:
- "Abs_star(starrel``{%n. X n}) pow Abs_star(starrel``{%n. Y n}) =
- Abs_star(starrel``{%n. X n ^ Y n})"
-apply (unfold hyperpow_def)
-apply (rule_tac f = Abs_star in arg_cong)
-apply (auto intro!: lemma_starrel_refl bexI
- simp add: starrel_in_hypreal [THEN Abs_star_inverse] equiv_starrel
- hyperpow_congruent, fuf)
-done
+lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
+by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
-lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
-apply (unfold hypnat_one_def)
-apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_star)
-apply (auto simp add: hyperpow hypnat_add)
-done
-declare hyperpow_zero [simp]
+lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
+by (unfold hyperpow_def, transfer, simp)
-lemma hyperpow_not_zero [rule_format (no_asm)]:
- "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hyperpow)
-apply (drule FreeUltrafilterNat_Compl_mem, ultra)
-done
+lemma hyperpow_not_zero: "!!r n. r \<noteq> (0::hypreal) ==> r pow n \<noteq> 0"
+by (unfold hyperpow_def, transfer, simp)
lemma hyperpow_inverse:
- "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
-apply (rule FreeUltrafilterNat_subset)
-apply (auto dest: realpow_not_zero intro: power_inverse)
-done
+ "!!r n. r \<noteq> (0::hypreal) ==> inverse(r pow n) = (inverse r) pow n"
+by (unfold hyperpow_def, transfer, rule power_inverse)
+
+lemma hyperpow_hrabs: "!!r n. abs r pow n = abs (r pow n)"
+by (unfold hyperpow_def, transfer, rule power_abs [symmetric])
-lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
-done
+lemma hyperpow_add: "!!r n m. r pow (n + m) = (r pow n) * (r pow m)"
+by (unfold hyperpow_def, transfer, rule power_add)
-lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (rule_tac z=n in eq_Abs_star, rule_tac z=m in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
-done
-
-lemma hyperpow_one [simp]: "r pow (1::hypnat) = r"
-apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hyperpow)
-done
+lemma hyperpow_one [simp]: "!!r. r pow (1::hypnat) = r"
+by (unfold hyperpow_def, transfer, simp)
lemma hyperpow_two:
- "r pow ((1::hypnat) + (1::hypnat)) = r * r"
-apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hyperpow hypnat_add hypreal_mult)
-done
+ "!!r. r pow ((1::hypnat) + (1::hypnat)) = r * r"
+by (unfold hyperpow_def, transfer, simp)
-lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
- simp add: hyperpow hypreal_less hypreal_le)
-done
+lemma hyperpow_gt_zero: "!!r n. (0::hypreal) < r ==> 0 < r pow n"
+by (unfold hyperpow_def, transfer, rule zero_less_power)
-lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
- simp add: hyperpow hypreal_le)
-done
+lemma hyperpow_ge_zero: "!!r n. (0::hypreal) \<le> r ==> 0 \<le> r pow n"
+by (unfold hyperpow_def, transfer, rule zero_le_power)
-lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
-apply (auto simp add: hyperpow hypreal_le hypreal_less)
-apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
-apply (auto intro: power_mono)
-done
-
-lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)"
-apply (rule_tac z=n in eq_Abs_star)
-apply (auto simp add: hypreal_one_def hyperpow)
-done
+lemma hyperpow_le:
+ "!!x y n. [|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
+by (unfold hyperpow_def, transfer, rule power_mono [OF _ order_less_imp_le])
-lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)"
-apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
-apply simp
-apply (rule_tac z=n in eq_Abs_star)
-apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
-done
+lemma hyperpow_eq_one [simp]: "!!n. 1 pow n = (1::hypreal)"
+by (unfold hyperpow_def, transfer, simp)
-lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
-apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
-done
+lemma hrabs_hyperpow_minus_one [simp]: "!!n. abs(-1 pow n) = (1::hypreal)"
+by (unfold hyperpow_def, transfer, simp)
+
+lemma hyperpow_mult: "!!r s n. (r * s) pow n = (r pow n) * (s pow n)"
+by (unfold hyperpow_def, transfer, rule power_mult_distrib)
lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
by (auto simp add: hyperpow_two zero_le_mult_iff)
@@ -244,23 +175,12 @@
done
lemma hyperpow_minus_one2 [simp]:
- "-1 pow ((1 + 1)*n) = (1::hypreal)"
-apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
-apply simp
-apply (simp only: hypreal_one_def, rule_tac z=n in eq_Abs_star)
-apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
- hypnat_mult left_distrib)
-done
+ "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
+by (unfold hyperpow_def, transfer, simp)
lemma hyperpow_less_le:
- "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (rule_tac z=n in eq_Abs_star, rule_tac z=N in eq_Abs_star, rule_tac z=r in eq_Abs_star)
-apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
- hypreal_zero_def hypreal_one_def)
-apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
-apply (erule FreeUltrafilterNat_Int, assumption)
-apply (auto intro: power_decreasing)
-done
+ "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
+by (unfold hyperpow_def, transfer, rule power_decreasing [OF order_less_imp_le])
lemma hyperpow_SHNat_le:
"[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |]
@@ -269,11 +189,11 @@
lemma hyperpow_realpow:
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-by (simp add: hypreal_of_real_def star_of_def star_n_def hypnat_of_nat_eq hyperpow)
+by (simp add: star_of_def hypnat_of_nat_eq hyperpow)
lemma hyperpow_SReal [simp]:
"(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
-by (simp del: hypreal_of_real_power add: hyperpow_realpow SReal_def)
+by (simp del: star_of_power add: hyperpow_realpow SReal_def)
lemma hyperpow_zero_HNatInfinite [simp]:
@@ -307,16 +227,13 @@
lemma hrealpow_hyperpow_Infinitesimal_iff:
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (rule_tac z=x in eq_Abs_star)
+apply (cases x)
apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
done
lemma Infinitesimal_hrealpow:
"[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
-by (force intro!: Infinitesimal_hyperpow
- simp add: hrealpow_hyperpow_Infinitesimal_iff
- hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
- simp del: hypnat_of_nat_less_iff)
+by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
ML
{*
@@ -332,10 +249,8 @@
val two_hrealpow_gt = thm "two_hrealpow_gt";
val hrealpow = thm "hrealpow";
val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
-val hypreal_of_real_power = thm "hypreal_of_real_power";
val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
val hrealpow_HFinite = thm "hrealpow_HFinite";
-val hyperpow_congruent = thm "hyperpow_congruent";
val hyperpow = thm "hyperpow";
val hyperpow_zero = thm "hyperpow_zero";
val hyperpow_not_zero = thm "hyperpow_not_zero";