# HG changeset patch
# User huffman
# Date 1166116238 -3600
# Node ID 59a68ed9f2f2ea52aebfd361526e5d3e45fc32a8
# Parent  c898fdd6ff2dfdea3e17d8ae77843a137af3c7d2
redefine hSuc as *f* Suc, and move to HyperNat.thy

diff -r c898fdd6ff2d -r 59a68ed9f2f2 src/HOL/Complex/NSComplex.thy
--- 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)"
diff -r c898fdd6ff2d -r 59a68ed9f2f2 src/HOL/Hyperreal/HyperNat.thy
--- 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)
 
diff -r c898fdd6ff2d -r 59a68ed9f2f2 src/HOL/Hyperreal/NatStar.thy
--- 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: