# HG changeset patch
# User huffman
# Date 1166294227 -3600
# Node ID 2ecfd8985982e02a086021a3a611d909c52d8aeb
# Parent  2cfc838297ff8b848978bf3d5fe242becc0f627f
hypreal_of_hypnat abbreviates more general of_hypnat

diff -r 2cfc838297ff -r 2ecfd8985982 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Fri Dec 15 17:51:07 2006 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Sat Dec 16 19:37:07 2006 +0100
@@ -704,22 +704,19 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (simp add: cis_real_of_nat_Suc_mult)
+by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
 
 lemma NSDeMoivre_ext:
   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
-by transfer (rule DeMoivre)
+by transfer (fold real_of_nat_def, rule DeMoivre)
 
 lemma NSDeMoivre2:
   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
-apply transfer
-apply (fold real_of_nat_def)
-apply (rule DeMoivre2)
-done
+by transfer (fold real_of_nat_def, rule DeMoivre2)
 
 lemma DeMoivre2_ext:
   "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
-by transfer (rule DeMoivre2)
+by transfer (fold real_of_nat_def, rule DeMoivre2)
 
 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
 by transfer (rule cis_inverse)
diff -r 2cfc838297ff -r 2ecfd8985982 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Fri Dec 15 17:51:07 2006 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Sat Dec 16 19:37:07 2006 +0100
@@ -107,7 +107,7 @@
 (* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
 (* maybe define omega = hypreal_of_hypnat whn + 1 *)
 apply (unfold star_class_defs omega_def hypnat_omega_def
-              hypreal_of_hypnat_def star_of_def)
+              of_hypnat_def star_of_def)
 apply (simp add: starfun_star_n starfun2_star_n real_of_nat_def)
 done
 
diff -r 2cfc838297ff -r 2ecfd8985982 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Fri Dec 15 17:51:07 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sat Dec 16 19:37:07 2006 +0100
@@ -370,62 +370,77 @@
 by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
                  FreeUltrafilterNat_HNatInfinite])
 
-subsection{*Embedding of the Hypernaturals into the Hyperreals*}
-text{*Obtained using the nonstandard extension of the naturals*}
+subsection {* Embedding of the Hypernaturals into other types *}
 
 definition
-  hypreal_of_hypnat :: "hypnat => hypreal" where
-  "hypreal_of_hypnat = *f* real"
+  of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
+  of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
 
-declare hypreal_of_hypnat_def [transfer_unfold]
+abbreviation
+  hypreal_of_hypnat :: "hypnat => hypreal" where
+  "hypreal_of_hypnat == of_hypnat"
 
-lemma hypreal_of_hypnat:
-      "hypreal_of_hypnat (star_n X) = star_n (%n. real (X n))"
-by (simp add: hypreal_of_hypnat_def starfun)
+lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
+by transfer (rule of_nat_0)
+
+lemma of_hypnat_1 [simp]: "of_hypnat 1 = 1"
+by transfer (rule of_nat_1)
 
-lemma hypreal_of_hypnat_inject [simp]:
-     "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-by transfer (rule real_of_nat_inject)
+lemma of_hypnat_hSuc: "\<And>m. of_hypnat (hSuc m) = of_hypnat m + 1"
+by transfer (rule of_nat_Suc)
+
+lemma of_hypnat_add [simp]:
+  "\<And>m n. of_hypnat (m + n) = of_hypnat m + of_hypnat n"
+by transfer (rule of_nat_add)
 
-lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
-by transfer (rule real_of_nat_zero)
+lemma of_hypnat_mult [simp]:
+  "\<And>m n. of_hypnat (m * n) = of_hypnat m * of_hypnat n"
+by transfer (rule of_nat_mult)
 
-lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
-by transfer simp
+lemma of_hypnat_less_iff [simp]:
+  "\<And>m n. (of_hypnat m < (of_hypnat n::'a::ordered_semidom star)) = (m < n)"
+by transfer (rule of_nat_less_iff)
 
-lemma hypreal_of_hypnat_add [simp]:
-     "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-by transfer (rule real_of_nat_add)
+lemma of_hypnat_0_less_iff [simp]:
+  "\<And>n. (0 < (of_hypnat n::'a::ordered_semidom star)) = (0 < n)"
+by transfer (rule of_nat_0_less_iff)
 
-lemma hypreal_of_hypnat_mult [simp]:
-     "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-by transfer (rule real_of_nat_mult)
+lemma of_hypnat_less_0_iff [simp]:
+  "\<And>m. \<not> (of_hypnat m::'a::ordered_semidom star) < 0"
+by transfer (rule of_nat_less_0_iff)
+
+lemma of_hypnat_le_iff [simp]:
+  "\<And>m n. (of_hypnat m \<le> (of_hypnat n::'a::ordered_semidom star)) = (m \<le> n)"
+by transfer (rule of_nat_le_iff)
 
-lemma hypreal_of_hypnat_less_iff [simp]:
-     "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-by transfer (rule real_of_nat_less_iff)
+lemma of_hypnat_0_le_iff [simp]:
+  "\<And>n. 0 \<le> (of_hypnat n::'a::ordered_semidom star)"
+by transfer (rule of_nat_0_le_iff)
+
+lemma of_hypnat_le_0_iff [simp]:
+  "\<And>m. ((of_hypnat m::'a::ordered_semidom star) \<le> 0) = (m = 0)"
+by transfer (rule of_nat_le_0_iff)
 
-lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
-by (simp add: hypreal_of_hypnat_zero [symmetric])
-declare hypreal_of_hypnat_eq_zero_iff [simp]
+lemma of_hypnat_eq_iff [simp]:
+  "\<And>m n. (of_hypnat m = (of_hypnat n::'a::ordered_semidom star)) = (m = n)"
+by transfer (rule of_nat_eq_iff)
 
-lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n"
-by transfer (rule real_of_nat_ge_zero)
+lemma of_hypnat_eq_0_iff [simp]:
+  "\<And>m. ((of_hypnat m::'a::ordered_semidom star) = 0) = (m = 0)"
+by transfer (rule of_nat_eq_0_iff)
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
 apply (cases n)
-apply (auto simp add: hypreal_of_hypnat star_n_inverse real_norm_def
+apply (auto simp add: of_hypnat_def starfun_star_n real_of_nat_def [symmetric] star_n_inverse
       HNatInfinite_FreeUltrafilterNat_iff
       Infinitesimal_FreeUltrafilterNat_iff2)
 apply (drule_tac x="Suc m" in spec)
 apply (erule ultra, simp)
 done
 
-lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
-     "N \<in> HNatInfinite ==> 0 < hypreal_of_hypnat N"
-apply (rule ccontr)
-apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
-done
+lemma HNatInfinite_of_hypnat_gt_zero:
+  "N \<in> HNatInfinite \<Longrightarrow> (0::'a::ordered_semidom star) < of_hypnat N"
+by (rule ccontr, simp add: linorder_not_less)
 
 end
diff -r 2cfc838297ff -r 2ecfd8985982 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Fri Dec 15 17:51:07 2006 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Sat Dec 16 19:37:07 2006 +0100
@@ -115,7 +115,7 @@
   @{term real_of_nat} *}
 
 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
-by (transfer, rule refl)
+by transfer (simp add: expand_fun_eq real_of_nat_def)
 
 lemma starfun_inverse_real_of_nat_eq:
      "N \<in> HNatInfinite