src/HOL/Hyperreal/NatStar.ML

generic of_nat and of_int functions, and generalization of iszero
and neg

(*  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];