# HG changeset patch
# User huffman
# Date 1166120116 -3600
# Node ID b35faf14a89f152562eb56622592d61f6a2f1110
# Parent  59a68ed9f2f2ea52aebfd361526e5d3e45fc32a8
generalized type of hyperpow; removed hcpow

diff -r 59a68ed9f2f2 -r b35faf14a89f src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Thu Dec 14 18:10:38 2006 +0100
+++ b/src/HOL/Complex/CStar.thy	Thu Dec 14 19:15:16 2006 +0100
@@ -22,7 +22,7 @@
 
 subsection{*Theorems about Nonstandard Extensions of Functions*}
 
-lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
+lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
 by transfer (rule refl)
 
 lemma starfunCR_cmod: "*f* cmod = hcmod"
diff -r 59a68ed9f2f2 -r b35faf14a89f src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Dec 14 18:10:38 2006 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Thu Dec 14 19:15:16 2006 +0100
@@ -79,14 +79,14 @@
 definition
   HComplex :: "[hypreal,hypreal] => hcomplex" where
   "HComplex = *f2* Complex"
-
+(*
 definition
   hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80) where
   "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n"
-
+*)
 lemmas hcomplex_defs [transfer_unfold] =
   hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
-  hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def
+  hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def
 
 lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard"
 by (simp add: hcomplex_defs)
@@ -463,10 +463,10 @@
 subsection{*A Few Nonlinear Theorems*}
 
 lemma hcomplex_of_hypreal_hyperpow:
-     "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
+     "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) pow n"
 by transfer (rule complex_of_real_pow)
 
-lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n"
+lemma hcmod_hcpow: "!!x n. hcmod(x pow n) = hcmod(x) pow n"
 by transfer (rule complex_mod_complexpow)
 
 lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)"
@@ -498,25 +498,23 @@
 by transfer (rule norm_power)
 
 lemma hcpow_minus:
-     "!!x n. (-x::hcomplex) hcpow n =
-      (if ( *p* even) n then (x hcpow n) else -(x hcpow n))"
+     "!!x n. (-x::hcomplex) pow n =
+      (if ( *p* even) n then (x pow n) else -(x pow n))"
 by transfer (rule neg_power_if)
 
 lemma hcpow_mult:
-  "!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
+  "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
 by transfer (rule power_mult_distrib)
 
-lemma hcpow_zero [simp]: "!!n. 0 hcpow (n + 1) = 0"
-by transfer simp
-
-lemma hcpow_zero2 [simp]: "!!n. 0 hcpow (hSuc n) = 0"
+lemma hcpow_zero2 [simp]:
+  "\<And>n. 0 pow (hSuc n) = (0::'a::{recpower,semiring_0} star)"
 by transfer (rule power_0_Suc)
 
 lemma hcpow_not_zero [simp,intro]:
-  "!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
-by transfer (rule field_power_not_zero)
+  "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
+by (rule hyperpow_not_zero)
 
-lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
+lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
 by (blast intro: ccontr dest: hcpow_not_zero)
 
 subsection{*The Function @{term hsgn}*}
@@ -709,7 +707,7 @@
 by transfer (simp add: cis_real_of_nat_Suc_mult)
 
 lemma NSDeMoivre_ext:
-  "!!a n. (hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
+  "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
 by transfer (rule DeMoivre)
 
 lemma NSDeMoivre2:
@@ -720,7 +718,7 @@
 done
 
 lemma DeMoivre2_ext:
-  "!! a r n. (hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
+  "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
 by transfer (rule DeMoivre2)
 
 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
@@ -741,10 +739,10 @@
 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
 by (simp add: NSDeMoivre)
 
-lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
+lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
 by (simp add: NSDeMoivre_ext)
 
-lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
+lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
 by (simp add: NSDeMoivre_ext)
 
 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
diff -r 59a68ed9f2f2 -r b35faf14a89f src/HOL/Hyperreal/HyperPow.thy
--- 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"