--- a/src/HOL/Complex/NSComplex.thy Thu Dec 14 16:08:09 2006 +0100
+++ b/src/HOL/Complex/NSComplex.thy Thu Dec 14 18:10:38 2006 +0100
@@ -510,7 +510,7 @@
by transfer simp
lemma hcpow_zero2 [simp]: "!!n. 0 hcpow (hSuc n) = 0"
-by (simp add: hSuc_def)
+by transfer (rule power_0_Suc)
lemma hcpow_not_zero [simp,intro]:
"!!r n. r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
--- a/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 16:08:09 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 18:10:38 2006 +0100
@@ -17,8 +17,21 @@
hypnat_of_nat :: "nat => nat star" where
"hypnat_of_nat == star_of"
+definition
+ hSuc :: "hypnat => hypnat" where
+ hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
+
subsection{*Properties Transferred from Naturals*}
+lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
+by transfer (rule Suc_not_Zero)
+
+lemma zero_not_hSuc [iff]: "\<And>m. 0 \<noteq> hSuc m"
+by transfer (rule Zero_not_Suc)
+
+lemma hSuc_hSuc_eq [iff]: "\<And>m n. (hSuc m = hSuc n) = (m = n)"
+by transfer (rule Suc_Suc_eq)
+
lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"
by transfer (rule diff_self_eq_0)
--- a/src/HOL/Hyperreal/NatStar.thy Thu Dec 14 16:08:09 2006 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy Thu Dec 14 18:10:38 2006 +0100
@@ -185,13 +185,6 @@
subsection{*Nonstandard Characterization of Induction*}
-definition
- hSuc :: "hypnat => hypnat" where
- "hSuc n = n + 1"
-
-lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"
-by (rule starP_star_n)
-
lemma hypnat_induct_obj:
"!!n. (( *p* P) (0::hypnat) &
(\<forall>n. ( *p* P)(n) --> ( *p* P)(n + 1)))
@@ -204,26 +197,14 @@
==> ( *p* P)(n)"
by (transfer, induct_tac n, auto)
-lemma starP2:
-"(( *p2* P) (star_n X) (star_n Y)) =
- ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
-by (rule starP2_star_n)
-
lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
-by (transfer, rule refl)
+by transfer (rule refl)
lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
by (simp add: starP2_eq_iff)
-lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
-by (simp add: hSuc_def)
-
-lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]
-
-lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
-by (simp add: hSuc_def star_n_one_num)
-
-lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
+lemma nonempty_nat_set_Least_mem:
+ "c \<in> (S :: nat set) ==> (LEAST n. n \<in> S) \<in> S"
by (erule LeastI)
lemma nonempty_set_star_has_least: