--- 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)
--- 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
--- 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
--- 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