# HG changeset patch
# User huffman
# Date 1166297025 -3600
# Node ID 55cc354fd2d9e4816f3e317d5230c00df97882e2
# Parent  2ecfd8985982e02a086021a3a611d909c52d8aeb
moved several theorems; rearranged theory dependencies

diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -8,7 +8,8 @@
 header{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
-imports StarClasses "../Real/Real"
+imports HyperNat "../Real/Real"
+uses ("hypreal_arith.ML")
 begin
 
 types hypreal = "real star"
@@ -17,6 +18,10 @@
   hypreal_of_real :: "real => real star" where
   "hypreal_of_real == star_of"
 
+abbreviation
+  hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" where
+  "hypreal_of_hypnat \<equiv> of_hypnat"
+
 definition
   omega :: hypreal where
    -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
@@ -236,4 +241,269 @@
 lemma hypreal_epsilon_gt_zero: "0 < epsilon"
 by (simp add: hypreal_epsilon_inverse_omega)
 
+subsection{*Absolute Value Function for the Hyperreals*}
+
+lemma hrabs_add_less:
+     "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
+by (simp add: abs_if split: split_if_asm)
+
+lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
+by (blast intro!: order_le_less_trans abs_ge_zero)
+
+lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x"
+by (simp add: abs_if)
+
+lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
+by (simp add: abs_if split add: split_if_asm)
+
+
+subsection{*Embedding the Naturals into the Hyperreals*}
+
+abbreviation
+  hypreal_of_nat :: "nat => hypreal" where
+  "hypreal_of_nat == of_nat"
+
+lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
+by (simp add: Nats_def image_def)
+
+(*------------------------------------------------------------*)
+(* naturals embedded in hyperreals                            *)
+(* is a hyperreal c.f. NS extension                           *)
+(*------------------------------------------------------------*)
+
+lemma hypreal_of_nat_eq:
+     "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
+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 (simp add: real_of_nat_def)
+done
+
+(*
+FIXME: we should declare this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
+Addsimps [symmetric hypreal_diff_def]
+*)
+
+use "hypreal_arith.ML"
+
+setup hypreal_arith_setup
+
+
+subsection {* Exponentials on the Hyperreals *}
+
+lemma hpowr_0 [simp]:   "r ^ 0       = (1::hypreal)"
+by (rule power_0)
+
+lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
+by (rule power_Suc)
+
+lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
+by simp
+
+lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
+by (auto simp add: zero_le_mult_iff)
+
+lemma hrealpow_two_le_add_order [simp]:
+     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
+by (simp only: hrealpow_two_le add_nonneg_nonneg)
+
+lemma hrealpow_two_le_add_order2 [simp]:
+     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
+by (simp only: hrealpow_two_le add_nonneg_nonneg)
+
+lemma hypreal_add_nonneg_eq_0_iff:
+     "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
+by arith
+
+
+text{*FIXME: DELETE THESE*}
+lemma hypreal_three_squares_add_zero_iff:
+     "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
+apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
+done
+
+lemma hrealpow_three_squares_add_zero_iff [simp]:
+     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
+      (x = 0 & y = 0 & z = 0)"
+by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
+
+(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract
+  result proved in Ring_and_Field*)
+lemma hrabs_hrealpow_two [simp]:
+     "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
+by (simp add: abs_mult)
+
+lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
+by (insert power_increasing [of 0 n "2::hypreal"], simp)
+
+lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
+apply (induct_tac "n")
+apply (auto simp add: left_distrib)
+apply (cut_tac n = n in two_hrealpow_ge_one, arith)
+done
+
+lemma hrealpow:
+    "star_n X ^ m = star_n (%n. (X n::real) ^ m)"
+apply (induct_tac "m")
+apply (auto simp add: star_n_one_num star_n_mult power_0)
+done
+
+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)
+
+lemma power_hypreal_of_real_number_of:
+     "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
+by simp
+declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
+(*
+lemma hrealpow_HFinite:
+  fixes x :: "'a::{real_normed_algebra,recpower} star"
+  shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc intro: HFinite_mult)
+done
+*)
+
+subsection{*Powers with Hypernatural Exponents*}
+
+definition
+  (* hypernatural powers of hyperreals *)
+  pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+  hyperpow_def [transfer_unfold]:
+  "R pow N = ( *f2* op ^) R N"
+
+lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
+by (simp add: hyperpow_def starfun2_star_n)
+
+lemma hyperpow_zero [simp]:
+  "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0"
+by transfer simp
+
+lemma hyperpow_not_zero:
+  "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0"
+by transfer (rule field_power_not_zero)
+
+lemma hyperpow_inverse:
+  "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star)
+   \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
+by transfer (rule power_inverse)
+
+lemma hyperpow_hrabs:
+  "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)"
+by transfer (rule power_abs [symmetric])
+
+lemma hyperpow_add:
+  "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)"
+by transfer (rule power_add)
+
+lemma hyperpow_one [simp]:
+  "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
+by transfer (rule power_one_right)
+
+lemma hyperpow_two:
+  "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r"
+by transfer (simp add: power_Suc)
+
+lemma hyperpow_gt_zero:
+  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
+by transfer (rule zero_less_power)
+
+lemma hyperpow_ge_zero:
+  "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n"
+by transfer (rule zero_le_power)
+
+lemma hyperpow_le:
+  "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk>
+   \<Longrightarrow> x pow n \<le> y pow n"
+by transfer (rule power_mono [OF _ order_less_imp_le])
+
+lemma hyperpow_eq_one [simp]:
+  "\<And>n. 1 pow n = (1::'a::recpower star)"
+by transfer (rule power_one)
+
+lemma hrabs_hyperpow_minus_one [simp]:
+  "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)"
+by transfer (rule abs_power_minus_one)
+
+lemma hyperpow_mult:
+  "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n
+   = (r pow n) * (s pow n)"
+by transfer (rule power_mult_distrib)
+
+lemma hyperpow_two_le [simp]:
+  "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)"
+by (auto simp add: hyperpow_two zero_le_mult_iff)
+
+lemma hrabs_hyperpow_two [simp]:
+  "abs(x pow (1 + 1)) =
+   (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)"
+by (simp only: abs_of_nonneg hyperpow_two_le)
+
+lemma hyperpow_two_hrabs [simp]:
+  "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1)  = x pow (1 + 1)"
+by (simp add: hyperpow_hrabs)
+
+text{*The precondition could be weakened to @{term "0\<le>x"}*}
+lemma hypreal_mult_less_mono:
+     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
+ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
+
+lemma hyperpow_two_gt_one:
+  "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
+by transfer (simp add: power_gt1)
+
+lemma hyperpow_two_ge_one:
+  "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
+by transfer (simp add: one_le_power)
+
+lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
+apply (rule_tac y = "1 pow n" in order_trans)
+apply (rule_tac [2] hyperpow_le, auto)
+done
+
+lemma hyperpow_minus_one2 [simp]:
+     "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
+by transfer (subst power_mult, simp)
+
+lemma hyperpow_less_le:
+     "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
+by transfer (rule power_decreasing [OF order_less_imp_le])
+
+lemma hyperpow_SHNat_le:
+     "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
+      ==> ALL n: Nats. r pow N \<le> r pow n"
+by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
+
+lemma hyperpow_realpow:
+      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
+by transfer (rule refl)
+
+lemma hyperpow_SReal [simp]:
+     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
+by (simp add: hyperpow_def Reals_eq_Standard)
+
+lemma hyperpow_zero_HNatInfinite [simp]:
+     "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
+by (drule HNatInfinite_is_Suc, auto)
+
+lemma hyperpow_le_le:
+     "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
+apply (drule order_le_less [of n, THEN iffD1])
+apply (auto intro: hyperpow_less_le)
+done
+
+lemma hyperpow_Suc_le_self2:
+     "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
+apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
+apply auto
+done
+
+lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n"
+by transfer (rule refl)
+
 end
diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -8,7 +8,7 @@
 header{*Hypernatural numbers*}
 
 theory HyperNat
-imports Star
+imports StarClasses
 begin
 
 types hypnat = "nat star"
@@ -32,6 +32,9 @@
 lemma hSuc_hSuc_eq [iff]: "\<And>m n. (hSuc m = hSuc n) = (m = n)"
 by transfer (rule Suc_Suc_eq)
 
+lemma zero_less_hSuc [iff]: "\<And>n. 0 < hSuc n"
+by transfer (rule zero_less_Suc)
+
 lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"
 by transfer (rule diff_self_eq_0)
 
@@ -282,17 +285,6 @@
 lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
 by (simp add: HNatInfinite_def)
 
-text{* Example of an hypersequence (i.e. an extended standard sequence)
-   whose term with an hypernatural suffix is an infinitesimal i.e.
-   the whn'nth term of the hypersequence is a member of Infinitesimal*}
-
-lemma SEQ_Infinitesimal:
-      "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def starfun star_n_inverse)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
-done
-
 lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
 apply (insert finite_atMost [of m]) 
 apply (simp add: atMost_def)
@@ -358,12 +350,12 @@
      "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
 apply (auto simp add: HNatInfinite_iff SHNat_eq)
 apply (drule_tac x="star_of u" in spec, simp)
-apply (simp add: star_of_def star_n_less)
+apply (simp add: star_of_def star_less_def starP2_star_n)
 done
 
 lemma FreeUltrafilterNat_HNatInfinite:
      "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
-by (auto simp add: star_n_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
+by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:
      "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
@@ -376,10 +368,6 @@
   of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
   of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
 
-abbreviation
-  hypreal_of_hypnat :: "hypnat => hypreal" where
-  "hypreal_of_hypnat == of_hypnat"
-
 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
 by transfer (rule of_nat_0)
 
@@ -429,16 +417,6 @@
   "\<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: 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_of_hypnat_gt_zero:
   "N \<in> HNatInfinite \<Longrightarrow> (0::'a::ordered_semidom star) < of_hypnat N"
 by (rule ccontr, simp add: linorder_not_less)
diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -8,7 +8,7 @@
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
 theory NSA
-imports HyperArith "../Real/RComplete"
+imports HyperDef "../Real/RComplete"
 begin
 
 definition
@@ -174,13 +174,10 @@
 by (drule (1) Reals_diff, simp)
 
 lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
-apply (auto simp add: SReal_def)
-apply (rule_tac x="abs r" in exI)
-apply simp
-done
+by (simp add: Reals_eq_Standard)
 
 lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
-by (simp add: SReal_def)
+by (simp add: Reals_eq_Standard)
 
 lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
 by simp
@@ -197,13 +194,13 @@
 done
 
 lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
-by (simp add: SReal_def)
+by simp
 
 lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
 by (simp add: SReal_def)
 
 lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
-by (auto simp add: SReal_def)
+by (simp add: Reals_eq_Standard Standard_def)
 
 lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
 apply (auto simp add: SReal_def)
@@ -212,14 +209,12 @@
 
 lemma SReal_hypreal_of_real_image:
       "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
-apply (simp add: SReal_def, blast)
-done
+by (simp add: SReal_def image_def, blast)
 
 lemma SReal_dense:
      "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
-apply (auto simp add: SReal_iff)
-apply (drule dense, safe)
-apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
+apply (auto simp add: SReal_def)
+apply (drule dense, auto)
 done
 
 text{*Completeness of Reals, but both lemmas are unused.*}
@@ -295,6 +290,13 @@
 lemma HFinite_1 [simp]: "1 \<in> HFinite"
 unfolding star_one_def by (rule HFinite_star_of)
 
+lemma hrealpow_HFinite:
+  fixes x :: "'a::{real_normed_algebra,recpower} star"
+  shows "x \<in> HFinite ==> x ^ n \<in> HFinite"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc intro: HFinite_mult)
+done
+
 lemma HFinite_bounded:
   "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
 apply (case_tac "x \<le> 0")
@@ -522,6 +524,28 @@
          e' \<le> x ; x \<le> e |] ==> (x::hypreal) \<in> Infinitesimal"
 by (auto intro: Infinitesimal_interval simp add: order_le_less)
 
+
+lemma lemma_Infinitesimal_hyperpow:
+     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
+apply (unfold Infinitesimal_def)
+apply (auto intro!: hyperpow_Suc_le_self2 
+          simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
+done
+
+lemma Infinitesimal_hyperpow:
+     "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
+apply (rule hrabs_le_Infinitesimal)
+apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
+done
+
+lemma hrealpow_hyperpow_Infinitesimal_iff:
+     "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
+by (simp only: hyperpow_hypnat_of_nat)
+
+lemma Infinitesimal_hrealpow:
+     "[| (x::hypreal) \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
+by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
+
 lemma not_Infinitesimal_mult:
   fixes x y :: "'a::real_normed_div_algebra star"
   shows "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
@@ -2209,6 +2233,17 @@
 apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq)
 done
 
+text{* Example of an hypersequence (i.e. an extended standard sequence)
+   whose term with an hypernatural suffix is an infinitesimal i.e.
+   the whn'nth term of the hypersequence is a member of Infinitesimal*}
+
+lemma SEQ_Infinitesimal:
+      "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
+apply (simp add: hypnat_omega_def starfun_star_n star_n_inverse)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
+apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
+done
+
 text{* Example where we get a hyperreal from a real sequence
       for which a particular property holds. The theorem is
       used in proofs about equivalence of nonstandard and
diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -8,7 +8,7 @@
 header{*Star-transforms for the Hypernaturals*}
 
 theory NatStar
-imports HyperPow
+imports Star
 begin
 
 lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"
diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -7,7 +7,7 @@
 header{*Existence of Nth Root*}
 
 theory NthRoot
-imports SEQ
+imports SEQ Parity
 begin
 
 definition
diff -r 2ecfd8985982 -r 55cc354fd2d9 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Sat Dec 16 19:37:07 2006 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Sat Dec 16 20:23:45 2006 +0100
@@ -305,6 +305,16 @@
      hnorm_def star_of_nat_def starfun_star_n
      star_n_inverse star_n_less real_of_nat_def)
 
+lemma HNatInfinite_inverse_Infinitesimal [simp]:
+     "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
+apply (cases n)
+apply (auto simp add: of_hypnat_def starfun_star_n real_of_nat_def [symmetric] star_n_inverse real_norm_def
+      HNatInfinite_FreeUltrafilterNat_iff
+      Infinitesimal_FreeUltrafilterNat_iff2)
+apply (drule_tac x="Suc m" in spec)
+apply (erule ultra, simp)
+done
+
 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
       (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
 apply (subst approx_minus_iff)