# HG changeset patch
# User huffman
# Date 1159333759 -7200
# Node ID da903f59e9ba439bbea7decd61e705dd6f549ff0
# Parent  1b45c35c4e85cf2c2ae7fc3deb3a21a3dd78ce6a
hypreal_of_nat abbreviates of_nat

diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -690,14 +690,12 @@
 lemma hcis_hypreal_of_nat_Suc_mult:
    "!!a. hcis (hypreal_of_nat (Suc n) * a) =
      hcis a * hcis (hypreal_of_nat n * a)"
-apply (unfold hypreal_of_nat_def)
 apply transfer
 apply (fold real_of_nat_def)
 apply (rule cis_real_of_nat_Suc_mult)
 done
 
 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
-apply (unfold hypreal_of_nat_def)
 apply transfer
 apply (fold real_of_nat_def)
 apply (rule DeMoivre)
@@ -714,7 +712,6 @@
 
 lemma NSDeMoivre2:
   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
-apply (unfold hypreal_of_nat_def)
 apply transfer
 apply (fold real_of_nat_def)
 apply (rule DeMoivre2)
diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -33,26 +33,12 @@
 
 subsection{*Embedding the Naturals into the Hyperreals*}
 
-definition
+abbreviation
   hypreal_of_nat   :: "nat => hypreal"
-  "hypreal_of_nat m = of_nat m"
+  "hypreal_of_nat == of_nat"
 
 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
-by (force simp add: hypreal_of_nat_def Nats_def) 
-
-lemma hypreal_of_nat_add [simp]:
-     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
-by (simp add: hypreal_of_nat_def)
-
-lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
-by (simp add: hypreal_of_nat_def)
-declare hypreal_of_nat_mult [simp]
-
-lemma hypreal_of_nat_less_iff:
-      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
-apply (simp add: hypreal_of_nat_def)
-done
-declare hypreal_of_nat_less_iff [symmetric, simp]
+by (simp add: Nats_def image_def)
 
 (*------------------------------------------------------------*)
 (* naturals embedded in hyperreals                            *)
@@ -61,42 +47,14 @@
 
 lemma hypreal_of_nat_eq:
      "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
-apply (induct n) 
-apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
-done
+by (simp add: real_of_nat_def)
 
 lemma hypreal_of_nat:
      "hypreal_of_nat m = star_n (%n. real m)"
 apply (fold star_of_def)
-apply (induct m)
-apply (simp_all add: hypreal_of_nat_def real_of_nat_def star_n_add)
+apply (simp add: real_of_nat_def)
 done
 
-lemma hypreal_of_nat_Suc:
-     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
-by (simp add: hypreal_of_nat_def)
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-lemma hypreal_of_nat_number_of [simp]:
-     "hypreal_of_nat (number_of v :: nat) =
-         (if neg (number_of v :: int) then 0
-          else (number_of v :: hypreal))"
-by (simp add: hypreal_of_nat_eq)
-
-lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
-by (simp add: hypreal_of_nat_def) 
-
-lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
-by (simp add: hypreal_of_nat_def) 
-
-lemma hypreal_of_nat_le_iff [simp]:
-     "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
-by (simp add: hypreal_of_nat_def) 
-
-lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n"
-by (simp add: hypreal_of_nat_def) 
-
-
 (*
 FIXME: we should declare this, as for type int, but many proofs would break.
 It replaces x+-y by x-y.
diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -334,9 +334,6 @@
 
 declare hypreal_of_hypnat_def [transfer_unfold]
 
-lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
-by (simp add: hypreal_of_nat_def) 
-
 lemma hypreal_of_hypnat:
       "hypreal_of_hypnat (star_n X) = star_n (%n. real (X n))"
 by (simp add: hypreal_of_hypnat_def starfun)
diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -65,7 +65,7 @@
 
 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
 apply (induct_tac "n")
-apply (auto simp add: hypreal_of_nat_Suc left_distrib)
+apply (auto simp add: left_distrib)
 apply (cut_tac n = n in two_hrealpow_ge_one, arith)
 done
 
@@ -78,7 +78,7 @@
 lemma hrealpow_sum_square_expand:
      "(x + (y::hypreal)) ^ Suc (Suc 0) =
       x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
-by (simp add: right_distrib left_distrib hypreal_of_nat_Suc)
+by (simp add: right_distrib left_distrib)
 
 
 subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -2020,10 +2020,10 @@
 apply (simp (no_asm_use) add: SReal_inverse)
 apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
 prefer 2 apply assumption
-apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
+apply (simp add: real_of_nat_def)
 apply (auto dest!: reals_Archimedean simp add: SReal_iff)
 apply (drule star_of_less [THEN iffD2])
-apply (simp add: real_of_nat_Suc_gt_zero hypreal_of_nat_eq)
+apply (simp add: real_of_nat_def)
 apply (blast intro: order_less_trans)
 done
 
diff -r 1b45c35c4e85 -r da903f59e9ba src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Wed Sep 27 05:58:42 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Sep 27 07:09:19 2006 +0200
@@ -326,7 +326,7 @@
                 \<in>  FreeUltrafilterNat)"
 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
      hnorm_def star_of_nat_def starfun_star_n
-     star_n_inverse star_n_less hypreal_of_nat_eq)
+     star_n_inverse star_n_less real_of_nat_def)
 
 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
       (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"