# HG changeset patch
# User paulson
# Date 1077791496 -3600
# Node ID 60aa114e2dba782dd28deefb2c8a8f112894e48a
# Parent  3fd75e96145d9027f30f7ec3ef5265d8a9f42ecb
converted Hyperreal/NatStar to Isar script

diff -r 3fd75e96145d -r 60aa114e2dba src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Feb 26 01:04:39 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Feb 26 11:31:36 2004 +0100
@@ -1,6 +1,8 @@
 (*  Title       : HyperNat.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
+
+Converted to Isar and polished by lcp    
 *)
 
 header{*Construction of Hypernaturals using Ultrafilters*}
@@ -48,9 +50,8 @@
                 hypnatrel``{%n::nat. X n - Y n})"
 
   hypnat_le_def:
-  "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) &
-                               Y \<in> Rep_hypnat(Q) &
-                               {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
+  "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) & Y \<in> Rep_hypnat(Q) &
+                            {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
 
   hypnat_less_def: "(x < (y::hypnat)) == (x \<le> y & x \<noteq> y)"
 
@@ -720,7 +721,8 @@
               dest: Nats_add [of "x-y", OF _ y]) 
 qed
 
-lemma HNatInfinite_add_one: "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
+lemma HNatInfinite_add_one:
+     "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
 by (auto intro: HNatInfinite_SHNat_add)
 
 lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
@@ -883,6 +885,8 @@
 val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
 val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
 val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
+val hypnat_of_nat_eq = thm"hypnat_of_nat_eq"
+val SHNat_eq = thm"SHNat_eq"
 val hypnat_of_nat_one = thm "hypnat_of_nat_one";
 val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
 val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
diff -r 3fd75e96145d -r 60aa114e2dba src/HOL/Hyperreal/NatStar.ML
--- a/src/HOL/Hyperreal/NatStar.ML	Thu Feb 26 01:04:39 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,494 +0,0 @@
-(*  Title       : NatStar.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Description : *-transforms in NSA which extends 
-                  sets of reals, and nat=>real, 
-                  nat=>nat functions
-*) 
-
-val hypnat_of_nat_eq = thm"hypnat_of_nat_eq";
-val SHNat_eq = thm"SHNat_eq";
-
-Goalw [starsetNat_def] 
-      "*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
-by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
-qed "NatStar_real_set";
-
-Goalw [starsetNat_def] "*sNat* {} = {}";
-by (Step_tac 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (dres_inst_tac [("x","%n. xa n")] bspec 1);
-by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_empty]));
-qed "NatStar_empty_set";
-
-Addsimps [NatStar_empty_set];
-
-Goalw [starsetNat_def] 
-      "*sNat* (A Un B) = *sNat* A Un *sNat* B";
-by (Auto_tac);
-by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
-by (dtac FreeUltrafilterNat_Compl_mem 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (Auto_tac);
-by (Fuf_tac 1);
-qed "NatStar_Un";
-
-Goalw [starsetNat_n_def] 
-      "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B";
-by Auto_tac;
-by (dres_inst_tac [("x","Xa")] bspec 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (auto_tac (claset() addSDs [bspec], simpset()));
-by (TRYALL(Ultra_tac));
-qed "starsetNat_n_Un";
-
-Goalw [InternalNatSets_def]
-     "[| X : InternalNatSets; Y : InternalNatSets |] \
-\     ==> (X Un Y) : InternalNatSets";
-by (auto_tac (claset(),
-         simpset() addsimps [starsetNat_n_Un RS sym]));
-qed "InternalNatSets_Un";
-
-Goalw [starsetNat_def] "*sNat* (A Int B) = *sNat* A Int *sNat* B";
-by (Auto_tac);
-by (blast_tac (claset() addIs [FreeUltrafilterNat_Int,
-    FreeUltrafilterNat_subset]) 3);
-by (REPEAT(blast_tac (claset() addIs 
-    [FreeUltrafilterNat_subset]) 1));
-qed "NatStar_Int";
-
-Goalw [starsetNat_n_def] 
-      "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B";
-by (Auto_tac);
-by (auto_tac (claset() addSDs [bspec],
-         simpset()));
-by (TRYALL(Ultra_tac));
-qed "starsetNat_n_Int";
-
-Goalw [InternalNatSets_def]
-     "[| X : InternalNatSets; Y : InternalNatSets |] \
-\     ==> (X Int Y) : InternalNatSets";
-by (auto_tac (claset(),
-         simpset() addsimps [starsetNat_n_Int RS sym]));
-qed "InternalNatSets_Int";
-
-Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)";
-by (Auto_tac);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (REPEAT(Step_tac 1) THEN Auto_tac);
-by (TRYALL(Ultra_tac));
-qed "NatStar_Compl";
-
-Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)";
-by (Auto_tac);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (REPEAT(Step_tac 1) THEN Auto_tac);
-by (TRYALL(Ultra_tac));
-qed "starsetNat_n_Compl";
-
-Goalw [InternalNatSets_def]
-     "X :InternalNatSets ==> -X : InternalNatSets";
-by (auto_tac (claset(),
-         simpset() addsimps [starsetNat_n_Compl RS sym]));
-qed "InternalNatSets_Compl";
-
-Goalw [starsetNat_n_def] 
-      "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B";
-by (Auto_tac);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 3);
-by (auto_tac (claset() addSDs [bspec], simpset()));
-by (TRYALL(Ultra_tac));
-qed "starsetNat_n_diff";
-
-Goalw [InternalNatSets_def]
-     "[| X : InternalNatSets; Y : InternalNatSets |] \
-\     ==> (X - Y) : InternalNatSets";
-by (auto_tac (claset(), simpset() addsimps [starsetNat_n_diff RS sym]));
-qed "InternalNatSets_diff";
-
-Goalw [starsetNat_def] "A <= B ==> *sNat* A <= *sNat* B";
-by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
-qed "NatStar_subset";
-
-Goal "a : A ==> hypnat_of_nat a : *sNat* A";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
-         simpset() addsimps [starsetNat_def,hypnat_of_nat_eq]));
-qed "NatStar_mem";
-
-Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
-by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_eq]));
-by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
-qed "NatStar_hypreal_of_real_image_subset";
-
-Goal "Nats <= *sNat* (UNIV:: nat set)";
-by (auto_tac (claset(), simpset() addsimps [starsetNat_def,SHNat_eq,hypnat_of_nat_eq]));
-qed "NatStar_SHNat_subset";
-
-Goalw [starsetNat_def] 
-     "*sNat* X Int Nats = hypnat_of_nat ` X";
-by (auto_tac (claset(),
-         simpset() addsimps 
-           [hypnat_of_nat_eq,SHNat_eq]));
-by (simp_tac (simpset() addsimps [hypnat_of_nat_eq RS sym]) 1);
-by (rtac imageI 1 THEN rtac ccontr 1);
-by (dtac bspec 1);
-by (rtac lemma_hypnatrel_refl 1);
-by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
-by (Auto_tac);
-qed "NatStar_hypreal_of_real_Int";
-
-Goal "x ~: hypnat_of_nat ` A ==> ALL y: A. x ~= hypnat_of_nat y";
-by (Auto_tac);
-qed "lemma_not_hypnatA";
-
-Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)";
-by Auto_tac;
-qed "starsetNat_starsetNat_n_eq";
-
-Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets";
-by (auto_tac (claset(),
-         simpset() addsimps [starsetNat_starsetNat_n_eq]));
-qed "InternalNatSets_starsetNat_n";
-Addsimps [InternalNatSets_starsetNat_n];
-
-Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets";
-by (auto_tac (claset() addIs [InternalNatSets_Compl], simpset()));
-qed "InternalNatSets_UNIV_diff";
-
-(*------------------------------------------------------------------ 
-   Nonstandard extension of a set (defined using a constant 
-   sequence) as a special case of an internal set
- -----------------------------------------------------------------*)
-
-Goalw [starsetNat_n_def,starsetNat_def] 
-     "ALL n. (As n = A) ==> *sNatn* As = *sNat* A";
-by (Auto_tac);
-qed "starsetNat_n_starsetNat";
-
-(*------------------------------------------------------
-   Theorems about nonstandard extensions of functions
- ------------------------------------------------------*)
-
-(*------------------------------------------------------------------ 
-   Nonstandard extension of a function (defined using a constant 
-   sequence) as a special case of an internal function
- -----------------------------------------------------------------*)
-
-Goalw [starfunNat_n_def,starfunNat_def] 
-     "ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
-by (Auto_tac);
-qed "starfunNat_n_starfunNat";
-
-Goalw [starfunNat2_n_def,starfunNat2_def] 
-     "ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f";
-by (Auto_tac);
-qed "starfunNat2_n_starfunNat2";
-
-Goalw [congruent_def] 
-      "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})";
-by Safe_tac;
-by (ALLGOALS(Fuf_tac));
-qed "starfunNat_congruent";
-
-(* f::nat=>real *)
-Goalw [starfunNat_def]
-      "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
-\      Abs_hypreal(hyprel `` {%n. f (X n)})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (simp_tac (simpset() addsimps 
-   [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1);
-by (Auto_tac THEN Fuf_tac 1);
-qed "starfunNat";
-
-(* f::nat=>nat *)
-Goalw [starfunNat2_def]
-      "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
-\      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
-by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
-by (simp_tac (simpset() addsimps 
-   [hypnatrel_in_hypnat RS thm"Abs_hypnat_inverse",
-    [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
-qed "starfunNat2";
-
-(*---------------------------------------------
-  multiplication: ( *f ) x ( *g ) = *(f x g)  
- ---------------------------------------------*)
-Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
-qed "starfunNat_mult";
-
-Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
-qed "starfunNat2_mult";
-
-(*---------------------------------------
-  addition: ( *f ) + ( *g ) = *(f + g)  
- ---------------------------------------*)
-Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
-qed "starfunNat_add";
-
-Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
-qed "starfunNat2_add";
-
-Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
-qed "starfunNat2_minus";
-
-(*--------------------------------------
-  composition: ( *f ) o ( *g ) = *(f o g)  
- ---------------------------------------*)
-(***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
- 
-Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))";
-by (rtac ext 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
-qed "starfunNatNat2_o";
-
-Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))";
-by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
-qed "starfunNatNat2_o2";
-
-(***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
-Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))";
-by (rtac ext 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
-qed "starfunNat2_o";
-
-(***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
-
-Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; 
-by (rtac ext 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
-qed "starfun_stafunNat_o";
-
-Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; 
-by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
-qed "starfun_stafunNat_o2";
-
-(*--------------------------------------
-  NS extension of constant function
- --------------------------------------*)
-Goal "( *fNat* (%x. k)) z = hypreal_of_real k";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
-qed "starfunNat_const_fun";
-Addsimps [starfunNat_const_fun];
-
-Goal "( *fNat2* (%x. k)) z = hypnat_of_nat  k";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_eq]));
-qed "starfunNat2_const_fun";
-
-Addsimps [starfunNat2_const_fun];
-
-Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
-qed "starfunNat_minus";
-
-Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
-qed "starfunNat_inverse";
-
-(*--------------------------------------------------------
-   extented function has same solution as its standard
-   version for natural arguments. i.e they are the same
-   for all natural arguments (c.f. Hoskins pg. 107- SEQ)
- -------------------------------------------------------*)
-
-Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
-by (auto_tac (claset(),
-      simpset() addsimps [starfunNat,hypnat_of_nat_eq,hypreal_of_real_def]));
-qed "starfunNat_eq";
-
-Addsimps [starfunNat_eq];
-
-Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
-by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_eq]));
-qed "starfunNat2_eq";
-
-Addsimps [starfunNat2_eq];
-
-Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
-by (Auto_tac);
-qed "starfunNat_approx";
-
-
-(*-----------------------------------------------------------------
-    Example of transfer of a property from reals to hyperreals
-    --- used for limit comparison of sequences
- ----------------------------------------------------------------*)
-Goal "ALL n. N <= n --> f n <= g n \
-\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n";
-by (Step_tac 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-         simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
-                             hypreal_less, hypnat_le,hypnat_less]));
-by (Ultra_tac 1);
-by Auto_tac;
-qed "starfun_le_mono";
-
-(*****----- and another -----*****) 
-Goal "ALL n. N <= n --> f n < g n \
-\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n";
-by (Step_tac 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-         simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
-                             hypreal_less, hypnat_le,hypnat_less]));
-by (Ultra_tac 1);
-by Auto_tac;
-qed "starfun_less_mono";
-
-(*----------------------------------------------------------------
-            NS extension when we displace argument by one
- ---------------------------------------------------------------*)
-Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-         simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
-qed "starfunNat_shift_one";
-
-(*----------------------------------------------------------------
-                 NS extension with rabs    
- ---------------------------------------------------------------*)
-Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
-qed "starfunNat_rabs";
-
-(*----------------------------------------------------------------
-       The hyperpow function as a NS extension of realpow
- ----------------------------------------------------------------*)
-Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-         simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
-qed "starfunNat_pow";
-
-Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-         simpset() addsimps [hyperpow, hypnat_of_nat_eq,starfunNat]));
-qed "starfunNat_pow2";
-
-Goal "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
-by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun,hypnat_of_nat_eq]));
-qed "starfun_pow";
-
-(*----------------------------------------------------- 
-   hypreal_of_hypnat as NS extension of real (from "nat")! 
--------------------------------------------------------*)
-Goal "( *fNat* real) = hypreal_of_hypnat";
-by (rtac ext 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
-qed "starfunNat_real_of_nat";
-
-Goal "N : HNatInfinite \
-\  ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
-by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
-by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(), 
-       simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat, starfun_inverse_inverse]));
-qed "starfunNat_inverse_real_of_nat_eq";
-
-(*----------------------------------------------------------
-     Internal functions - some redundancy with *fNat* now
- ---------------------------------------------------------*)
-Goalw [congruent_def] 
-      "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})";
-by Safe_tac;
-by (ALLGOALS(Fuf_tac));
-qed "starfunNat_n_congruent";
-
-Goalw [starfunNat_n_def]
-     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
-\     Abs_hypreal(hyprel `` {%n. f n (X n)})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by Auto_tac;
-by (Ultra_tac 1);
-qed "starfunNat_n";
-
-(*-------------------------------------------------
-  multiplication: ( *fn ) x ( *gn ) = *(fn x gn)  
- -------------------------------------------------*)
-Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
-qed "starfunNat_n_mult";
-
-(*-----------------------------------------------
-  addition: ( *fn ) + ( *gn ) = *(fn + gn)  
- -----------------------------------------------*)
-Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
-qed "starfunNat_n_add";
-
-(*-------------------------------------------------
-  subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)  
- -------------------------------------------------*)
-Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), 
-          simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
-qed "starfunNat_n_add_minus";
-
-(*--------------------------------------------------
-  composition: ( *fn ) o ( *gn ) = *(fn o gn)  
- -------------------------------------------------*)
- 
-Goal "( *fNatn* (%i x. k)) z = hypreal_of_real  k";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), 
-       simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
-qed "starfunNat_n_const_fun";
-
-Addsimps [starfunNat_n_const_fun];
-
-Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
-qed "starfunNat_n_minus";
-
-Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
-by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_eq]));
-qed "starfunNat_n_eq";
-Addsimps [starfunNat_n_eq];
-
-Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)";
-by Auto_tac;
-by (rtac ext 1 THEN rtac ccontr 1);
-by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
-by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_eq]));
-qed "starfun_eq_iff";
-
-
-
-(*MOVE UP*)
-
-Goal "N : HNatInfinite \
-\     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
-by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
-by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(), simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat]));
-qed "starfunNat_inverse_real_of_nat_Infinitesimal";
-Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
diff -r 3fd75e96145d -r 60aa114e2dba src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Thu Feb 26 01:04:39 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy	Thu Feb 26 11:31:36 2004 +0100
@@ -1,46 +1,538 @@
 (*  Title       : NatStar.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : defining *-transforms in NSA which extends 
-                  sets of reals, and nat=>real, nat=>nat functions
-*) 
+
+Converted to Isar and polished by lcp
+*)
+
+header{*Star-transforms for the Hypernaturals*}
 
-NatStar = RealPow + HyperPow + 
+theory NatStar = RealPow + HyperPow:
+
+
+text{*Extends sets of nats, and functions from the nats to nats or reals*}
+
 
 constdefs
 
   (* internal sets and nonstandard extensions -- see Star.thy as well *)
 
-    starsetNat :: nat set => hypnat set          ("*sNat* _" [80] 80)
-    "*sNat* A  == {x. ALL X: Rep_hypnat(x). {n::nat. X n : A}: FreeUltrafilterNat}"
+    starsetNat :: "nat set => hypnat set"          ("*sNat* _" [80] 80)
+    "*sNat* A ==
+       {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
 
-    starsetNat_n :: (nat => nat set) => hypnat set        ("*sNatn* _" [80] 80)
-    "*sNatn* As  == {x. ALL X: Rep_hypnat(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"   
+   starsetNat_n :: "(nat => nat set) => hypnat set"      ("*sNatn* _" [80] 80)
+    "*sNatn* As ==
+       {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
 
-    InternalNatSets :: "hypnat set set"
-    "InternalNatSets == {X. EX As. X = *sNatn* As}"
+   InternalNatSets :: "hypnat set set"
+    "InternalNatSets == {X. \<exists>As. X = *sNatn* As}"
 
     (* star transform of functions f:Nat --> Real *)
 
-    starfunNat :: (nat => real) => hypnat => hypreal        ("*fNat* _" [80] 80)
-    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. f (X n)}))" 
+    starfunNat :: "(nat => real) => hypnat => hypreal"
+                  ("*fNat* _" [80] 80)
+    "*fNat* f  == (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. f (X n)}))"
 
-    starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal        ("*fNatn* _" [80] 80)
-    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))" 
+   starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
+                   ("*fNatn* _" [80] 80)
+    "*fNatn* F ==
+      (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))"
 
-    InternalNatFuns :: (hypnat => hypreal) set
-    "InternalNatFuns == {X. EX F. X = *fNatn* F}"
+   InternalNatFuns :: "(hypnat => hypreal) set"
+    "InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
 
     (* star transform of functions f:Nat --> Nat *)
 
-    starfunNat2 :: (nat => nat) => hypnat => hypnat        ("*fNat2* _" [80] 80)
-    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. f (X n)}))" 
+   starfunNat2 :: "(nat => nat) => hypnat => hypnat"
+                   ("*fNat2* _" [80] 80)
+    "*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})"
+
+   starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat"
+                     ("*fNat2n* _" [80] 80)
+    "*fNat2n* F == 
+        %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})"
+
+   InternalNatFuns2 :: "(hypnat => hypnat) set"
+    "InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}"
+
+
+lemma NatStar_real_set: "*sNat*(UNIV::nat set) = (UNIV::hypnat set)"
+by (simp add: starsetNat_def)
+
+lemma NatStar_empty_set [simp]: "*sNat* {} = {}"
+by (simp add: starsetNat_def)
+
+lemma NatStar_Un: "*sNat* (A Un B) = *sNat* A Un *sNat* B"
+apply (auto simp add: starsetNat_def)
+ prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
+ prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply (drule bspec, assumption)
+apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra)
+done
+
+lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B"
+apply (auto simp add: starsetNat_n_def)
+apply (drule_tac x = Xa in bspec)
+apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (auto dest!: bspec, ultra+)
+done
+
+lemma InternalNatSets_Un:
+     "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
+      ==> (X Un Y) \<in> InternalNatSets"
+by (auto simp add: InternalNatSets_def starsetNat_n_Un [symmetric])
+
+lemma NatStar_Int: "*sNat* (A Int B) = *sNat* A Int *sNat* B"
+apply (auto simp add: starsetNat_def)
+prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
+apply (blast intro: FreeUltrafilterNat_subset)+
+done
+
+lemma starsetNat_n_Int:
+      "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B"
+apply (auto simp add: starsetNat_n_def)
+apply (auto dest!: bspec, ultra+)
+done
+
+lemma InternalNatSets_Int:
+     "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
+      ==> (X Int Y) \<in> InternalNatSets"
+by (auto simp add: InternalNatSets_def starsetNat_n_Int [symmetric])
+
+lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)"
+apply (auto simp add: starsetNat_def)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (auto dest!: bspec, ultra+)
+done
+
+lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)"
+apply (auto simp add: starsetNat_n_def)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (auto dest!: bspec, ultra+)
+done
+
+lemma InternalNatSets_Compl: "X \<in> InternalNatSets ==> -X \<in> InternalNatSets"
+by (auto simp add: InternalNatSets_def starsetNat_n_Compl [symmetric])
+
+lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"
+apply (auto simp add: starsetNat_n_def)
+apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac [3] z = x in eq_Abs_hypnat)
+apply (auto dest!: bspec, ultra+)
+done
+
+lemma InternalNatSets_diff:
+     "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |]
+      ==> (X - Y) \<in> InternalNatSets"
+by (auto simp add: InternalNatSets_def starsetNat_n_diff [symmetric])
+
+lemma NatStar_subset: "A \<le> B ==> *sNat* A \<le> *sNat* B"
+apply (simp add: starsetNat_def)
+apply (blast intro: FreeUltrafilterNat_subset)
+done
+
+lemma NatStar_mem: "a \<in> A ==> hypnat_of_nat a \<in> *sNat* A"
+by (auto intro: FreeUltrafilterNat_subset 
+         simp add: starsetNat_def hypnat_of_nat_eq)
+
+lemma NatStar_hypreal_of_real_image_subset: "hypnat_of_nat ` A \<le> *sNat* A"
+apply (auto simp add: starsetNat_def hypnat_of_nat_eq)
+apply (blast intro: FreeUltrafilterNat_subset)
+done
+
+lemma NatStar_SHNat_subset: "Nats \<le> *sNat* (UNIV:: nat set)"
+by (simp add: starsetNat_def SHNat_eq hypnat_of_nat_eq)
+
+lemma NatStar_hypreal_of_real_Int:
+     "*sNat* X Int Nats = hypnat_of_nat ` X"
+apply (auto simp add: starsetNat_def hypnat_of_nat_eq SHNat_eq)
+apply (simp add: hypnat_of_nat_eq [symmetric])
+apply (rule imageI, rule ccontr)
+apply (drule bspec)
+apply (rule lemma_hypnatrel_refl)
+prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
+done
+
+lemma starsetNat_starsetNat_n_eq: "*sNat* X = *sNatn* (%n. X)"
+by (simp add: starsetNat_n_def starsetNat_def)
+
+lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets"
+by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq)
+
+lemma InternalNatSets_UNIV_diff:
+     "X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets"
+by (auto intro: InternalNatSets_Compl)
+
+text{*Nonstandard extension of a set (defined using a constant
+   sequence) as a special case of an internal set*}
+lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A"
+by (simp add: starsetNat_n_def starsetNat_def)
+
+
+subsection{*Nonstandard Extensions of Functions*}
+
+text{* Nonstandard extension of a function (defined using a constant
+   sequence) as a special case of an internal function*}
+
+lemma starfunNat_n_starfunNat: "\<forall>n. (F n = f) ==> *fNatn* F = *fNat* f"
+by (simp add: starfunNat_n_def starfunNat_def)
+
+lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
+by (simp add: starfunNat2_n_def starfunNat2_def)
+
+lemma starfunNat_congruent:
+      "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"
+apply (simp add: congruent_def, safe)
+apply (ultra+)
+done
+
+(* f::nat=>real *)
+lemma starfunNat:
+      "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+       Abs_hypreal(hyprel `` {%n. f (X n)})"
+apply (simp add: starfunNat_def)
+apply (rule arg_cong [where f = Abs_hypreal])
+apply (auto, ultra)
+done
+
+(* f::nat=>nat *)
+lemma starfunNat2:
+      "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+       Abs_hypnat(hypnatrel `` {%n. f (X n)})"
+apply (simp add: starfunNat2_def)
+apply (rule arg_cong [where f = Abs_hypnat])
+apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse]
+         UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent])
+done
+
+subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*}
+
+lemma starfunNat_mult:
+     "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat hypreal_mult)
+done
+
+lemma starfunNat2_mult:
+     "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat2 hypnat_mult)
+done
+
+subsubsection{*Addition: @{text "( *f) + ( *g) = *(f + g)"}*}
+
+lemma starfunNat_add:
+     "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat hypreal_add)
+done
+
+lemma starfunNat2_add:
+     "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat2 hypnat_add)
+done
+
+lemma starfunNat2_minus:
+     "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat2 hypnat_minus)
+done
+
+subsubsection{*Composition: @{text "( *f) o ( *g) = *(f o g)"}*}
+
+(***** ( *f::nat=>real) o ( *g::nat=>nat) = *(f o g) *****)
+
+lemma starfunNatNat2_o:
+     "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"
+apply (rule ext)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (simp add: starfunNat2 starfunNat)
+done
+
+lemma starfunNatNat2_o2:
+     "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))"
+apply (insert starfunNatNat2_o [of f g]) 
+apply (simp add: o_def) 
+done
+
+(***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****)
+lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"
+apply (rule ext)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (simp add: starfunNat2)
+done
+
+(***** ( *f::real=>real) o ( *g::nat=>real) = *(f o g) *****)
+
+lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"
+apply (rule ext)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (simp add: starfunNat starfun)
+done
+
+lemma starfun_stafunNat_o2:
+     "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"
+apply (insert starfun_stafunNat_o [of f g]) 
+apply (simp add: o_def) 
+done
+
+
+text{*NS extension of constant function*}
+
+lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat hypreal_of_real_def)
+done
 
-    starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat        ("*fNat2n* _" [80] 80)
-    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)}))" 
+lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat  k"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat2 hypnat_of_nat_eq)
+done
+
+lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
+apply (rule eq_Abs_hypnat [of x])
+apply (simp add: starfunNat hypreal_minus)
+done
+
+lemma starfunNat_inverse:
+     "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
+apply (rule eq_Abs_hypnat [of x])
+apply (simp add: starfunNat hypreal_inverse)
+done
+
+text{* Extended function has same solution as its standard
+   version for natural arguments. i.e they are the same
+   for all natural arguments (c.f. Hoskins pg. 107- SEQ)*}
+
+lemma starfunNat_eq [simp]:
+     "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"
+by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def)
+
+lemma starfunNat2_eq [simp]:
+     "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"
+by (simp add: starfunNat2 hypnat_of_nat_eq)
+
+lemma starfunNat_approx:
+     "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"
+by auto
+
+
+text{* Example of transfer of a property from reals to hyperreals
+    --- used for limit comparison of sequences*}
+
+lemma starfun_le_mono:
+     "\<forall>n. N \<le> n --> f n \<le> g n
+      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n"
+apply safe
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
+done
+
+(*****----- and another -----*****)
+lemma starfun_less_mono:
+     "\<forall>n. N \<le> n --> f n < g n
+      ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n"
+apply safe
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
+done
+
+text{*Nonstandard extension when we increment the argument by one*}
+
+lemma starfunNat_shift_one:
+     "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
+apply (rule eq_Abs_hypnat [of N])
+apply (simp add: starfunNat hypnat_one_def hypnat_add)
+done
+
+text{*Nonstandard extension with absolute value*}
+
+lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
+apply (rule eq_Abs_hypnat [of N])
+apply (simp add: starfunNat hypreal_hrabs)
+done
+
+text{*The hyperpow function as a nonstandard extension of realpow*}
+
+lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
+apply (rule eq_Abs_hypnat [of N])
+apply (simp add: hyperpow hypreal_of_real_def starfunNat)
+done
+
+lemma starfunNat_pow2:
+     "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
+apply (rule eq_Abs_hypnat [of N])
+apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
+done
+
+lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
+apply (rule_tac z = R in eq_Abs_hypreal)
+apply (simp add: hyperpow starfun hypnat_of_nat_eq)
+done
+
+text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
+  @{term real_of_nat} *}
+
+lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat"
+apply (rule ext)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (simp add: hypreal_of_hypnat starfunNat)
+done
+
+lemma starfunNat_inverse_real_of_nat_eq:
+     "N \<in> HNatInfinite
+   ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"
+apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
+apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
+apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat starfun_inverse_inverse)
+done
+
+text{*Internal functions - some redundancy with *fNat* now*}
+
+lemma starfunNat_n_congruent:
+      "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"
+apply (simp add: congruent_def, safe)
+apply (ultra+)
+done
+
+lemma starfunNat_n:
+     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+      Abs_hypreal(hyprel `` {%n. f n (X n)})"
+apply (simp add: starfunNat_n_def)
+apply (rule_tac f = Abs_hypreal in arg_cong, auto, ultra)
+done
+
+text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
 
-    InternalNatFuns2 :: (hypnat => hypnat) set
-    "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}"
+lemma starfunNat_n_mult:
+     "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat_n hypreal_mult)
+done
+
+text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
+
+lemma starfunNat_n_add:
+     "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat_n hypreal_add)
+done
+
+text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
+
+lemma starfunNat_n_add_minus:
+     "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat_n hypreal_minus hypreal_add)
+done
+
+
+text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
+
+lemma starfunNat_n_const_fun [simp]:
+     "( *fNatn* (%i x. k)) z = hypreal_of_real  k"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: starfunNat_n hypreal_of_real_def)
+done
+
+lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
+apply (rule eq_Abs_hypnat [of x])
+apply (simp add: starfunNat_n hypreal_minus)
+done
+
+lemma starfunNat_n_eq [simp]:
+     "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"
+by (simp add: starfunNat_n hypnat_of_nat_eq)
+
+lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)"
+apply auto
+apply (rule ext, rule ccontr)
+apply (drule_tac x = "hypnat_of_nat (x) " in fun_cong)
+apply (simp add: starfunNat hypnat_of_nat_eq)
+done
+
+
+lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]:
+     "N \<in> HNatInfinite ==> ( *fNat* (%x. inverse (real x))) N \<in> Infinitesimal"
+apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
+apply (subgoal_tac "hypreal_of_hypnat N ~= 0")
+apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat)
+done
+
+ML
+{*
+val starsetNat_def = thm "starsetNat_def";
+
+val NatStar_real_set = thm "NatStar_real_set";
+val NatStar_empty_set = thm "NatStar_empty_set";
+val NatStar_Un = thm "NatStar_Un";
+val starsetNat_n_Un = thm "starsetNat_n_Un";
+val InternalNatSets_Un = thm "InternalNatSets_Un";
+val NatStar_Int = thm "NatStar_Int";
+val starsetNat_n_Int = thm "starsetNat_n_Int";
+val InternalNatSets_Int = thm "InternalNatSets_Int";
+val NatStar_Compl = thm "NatStar_Compl";
+val starsetNat_n_Compl = thm "starsetNat_n_Compl";
+val InternalNatSets_Compl = thm "InternalNatSets_Compl";
+val starsetNat_n_diff = thm "starsetNat_n_diff";
+val InternalNatSets_diff = thm "InternalNatSets_diff";
+val NatStar_subset = thm "NatStar_subset";
+val NatStar_mem = thm "NatStar_mem";
+val NatStar_hypreal_of_real_image_subset = thm "NatStar_hypreal_of_real_image_subset";
+val NatStar_SHNat_subset = thm "NatStar_SHNat_subset";
+val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int";
+val starsetNat_starsetNat_n_eq = thm "starsetNat_starsetNat_n_eq";
+val InternalNatSets_starsetNat_n = thm "InternalNatSets_starsetNat_n";
+val InternalNatSets_UNIV_diff = thm "InternalNatSets_UNIV_diff";
+val starsetNat_n_starsetNat = thm "starsetNat_n_starsetNat";
+val starfunNat_n_starfunNat = thm "starfunNat_n_starfunNat";
+val starfunNat2_n_starfunNat2 = thm "starfunNat2_n_starfunNat2";
+val starfunNat_congruent = thm "starfunNat_congruent";
+val starfunNat = thm "starfunNat";
+val starfunNat2 = thm "starfunNat2";
+val starfunNat_mult = thm "starfunNat_mult";
+val starfunNat2_mult = thm "starfunNat2_mult";
+val starfunNat_add = thm "starfunNat_add";
+val starfunNat2_add = thm "starfunNat2_add";
+val starfunNat2_minus = thm "starfunNat2_minus";
+val starfunNatNat2_o = thm "starfunNatNat2_o";
+val starfunNatNat2_o2 = thm "starfunNatNat2_o2";
+val starfunNat2_o = thm "starfunNat2_o";
+val starfun_stafunNat_o = thm "starfun_stafunNat_o";
+val starfun_stafunNat_o2 = thm "starfun_stafunNat_o2";
+val starfunNat_const_fun = thm "starfunNat_const_fun";
+val starfunNat2_const_fun = thm "starfunNat2_const_fun";
+val starfunNat_minus = thm "starfunNat_minus";
+val starfunNat_inverse = thm "starfunNat_inverse";
+val starfunNat_eq = thm "starfunNat_eq";
+val starfunNat2_eq = thm "starfunNat2_eq";
+val starfunNat_approx = thm "starfunNat_approx";
+val starfun_le_mono = thm "starfun_le_mono";
+val starfun_less_mono = thm "starfun_less_mono";
+val starfunNat_shift_one = thm "starfunNat_shift_one";
+val starfunNat_rabs = thm "starfunNat_rabs";
+val starfunNat_pow = thm "starfunNat_pow";
+val starfunNat_pow2 = thm "starfunNat_pow2";
+val starfun_pow = thm "starfun_pow";
+val starfunNat_real_of_nat = thm "starfunNat_real_of_nat";
+val starfunNat_inverse_real_of_nat_eq = thm "starfunNat_inverse_real_of_nat_eq";
+val starfunNat_n_congruent = thm "starfunNat_n_congruent";
+val starfunNat_n = thm "starfunNat_n";
+val starfunNat_n_mult = thm "starfunNat_n_mult";
+val starfunNat_n_add = thm "starfunNat_n_add";
+val starfunNat_n_add_minus = thm "starfunNat_n_add_minus";
+val starfunNat_n_const_fun = thm "starfunNat_n_const_fun";
+val starfunNat_n_minus = thm "starfunNat_n_minus";
+val starfunNat_n_eq = thm "starfunNat_n_eq";
+val starfun_eq_iff = thm "starfun_eq_iff";
+val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
+*}
+
 end
 
 
diff -r 3fd75e96145d -r 60aa114e2dba src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 26 01:04:39 2004 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 26 11:31:36 2004 +0100
@@ -150,8 +150,7 @@
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
   Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.thy\
-  Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
-  Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
+  Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy\
   Hyperreal/Poly.ML Hyperreal/Poly.thy\
   Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\