--- 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)
--- 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.
--- 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)
--- 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}*}
--- 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
--- 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)"