(*  Title       : NatStar.ML
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : *-transforms for sets of nats, 
                  nat=>real, and nat=>nat functions
*) 

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_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_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 (Fuf_empty_tac 1);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (Fuf_tac 1);
qed "NatStar_Compl";

Goalw [starsetNat_def] "!!A. A <= B ==> *sNat* A <= *sNat* B";
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
qed "NatStar_subset";

Goalw [starsetNat_def,hypnat_of_nat_def] 
          "!!A. a : A ==> hypnat_of_nat a : *sNat* A";
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
qed "NatStar_mem";

Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";

Goal "SHNat <= *sNat* (UNIV:: nat set)";
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
    NatStar_hypreal_of_real_image_subset]) 1);
qed "NatStar_SHNat_subset";

Goalw [starsetNat_def] 
      "*sNat* X Int SHNat = hypnat_of_nat `` X";
by (auto_tac (claset(),simpset() addsimps 
           [hypnat_of_nat_def,SHNat_def]));
by (fold_tac [hypnat_of_nat_def]);
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. x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
by (Auto_tac);
qed "lemma_not_hypnatA";

(*----------------------------------------------------------- 
   Nonstandard extension of a set (defined using a constant 
   sequence) as a special case of an internal set
 -----------------------------------------------------------*)

Goalw [starsetNat_n_def,starsetNat_def] 
     "!!A. 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] 
     "!!A. ALL n. (F n = f) ==> *fNatn* F = *fNat* f";
by (Auto_tac);
qed "starfunNat_n_starfunNat";

Goalw [starfunNat2_n_def,starfunNat2_def] 
     "!!A. 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 (claset()));
by (ALLGOALS(Fuf_tac));
qed "starfunNat_congruent";

(*Resolve th against the corresponding facts for starfunNat*)
val starfunNat_ize = RSLIST [equiv_hypnatrel, 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 Abs_hypnat_inverse,
    starfunNat_ize UN_equiv_class]) 1);
qed "starfunNat2";

(*---------------------------------------------
  multiplication: ( *f ) x ( *g ) = *(f x g)  
 ---------------------------------------------*)
Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps 
    [starfunNat,hypreal_mult]));
qed "starfunNat_mult";

Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps 
    [starfunNat2,hypnat_mult]));
qed "starfunNat2_mult";

(*---------------------------------------
  addition: ( *f ) + ( *g ) = *(f + g)  
 ---------------------------------------*)
Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps 
    [starfunNat,hypreal_add]));
qed "starfunNat_add";

Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps 
    [starfunNat2,hypnat_add]));
qed "starfunNat2_add";

(*--------------------------------------------
  subtraction: ( *f ) + -( *g ) = *(f + -g)  
 --------------------------------------------*)
Goal "(*fNat* f) xa + -(*fNat* g) xa = (*fNat* (%x. f x + -g x)) xa";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
    hypreal_minus,hypreal_add]));
qed "starfunNat_add_minus";

Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa";
by (res_inst_tac [("z","xa")] 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";

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

(*--------------------------------------
  NS extension of constant function
 --------------------------------------*)
Goal "(*fNat* (%x. k)) xa = hypreal_of_real k";
by (res_inst_tac [("z","xa")] 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)) xa = hypnat_of_nat  k";
by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat2,
    hypnat_of_nat_def]));
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 
     "!!f. ALL x. f x ~= 0r ==> \
\     hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
              hypreal_hrinv]));
qed "starfunNat_hrinv";

(*-------------------------------------------------------
   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_def,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_def]));
qed "starfunNat2_eq";

Addsimps [starfunNat2_eq];

Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
by (Auto_tac);
qed "starfunNat_inf_close";

Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m; \
\                 l: HFinite; m: HFinite  \
\              |] ==>  (*fNat* (%x. f x * g x)) xa @= l * m";
by (dtac inf_close_mult_HFinite 1);
by (REPEAT(assume_tac 1));
by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
              simpset() addsimps [starfunNat_mult]));
qed "starfunNat_mult_HFinite_inf_close";

Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m \
\              |] ==>  (*fNat* (%x. f x + g x)) xa @= l + m";
by (auto_tac (claset() addIs [inf_close_add],
              simpset() addsimps [starfunNat_add RS sym]));
qed "starfunNat_add_inf_close";

(*------------------------------------------------------------------
  A few more theorems involving NS extensions of real sequences
  See analogous theorems for starfun- NS extension of f::real=>real
 ------------------------------------------------------------------*)
Goal 
     "!!f. (*fNat* f) x ~= 0hr ==> \
\     hrinv ((*fNat* f) x) = (*fNat* (%x. rinv (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
    addSDs [FreeUltrafilterNat_Compl_mem],
    simpset() addsimps [starfunNat,hypreal_hrinv,
    hypreal_zero_def]));
qed "starfunNat_hrinv2";

(*----------------------------------------------------------------
    Example of transfer of a property from reals to hyperreals
    --- used for limit comparison of sequences
 ----------------------------------------------------------------*)
Goal "!!f. 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_def,hypreal_le_def,hypreal_less_def,
        hypnat_le_def,hypnat_less_def]));
by (dres_inst_tac [("x","x")] spec 1);
by (Step_tac 1);
by (dres_inst_tac [("x","%n. N")] spec 2);
by (Auto_tac);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (Fuf_empty_tac 1);
by (rtac ccontr 1 THEN dtac leI 1);
by (REPEAT(Step_tac 1));
by (auto_tac (claset() addDs [real_less_asym],
    simpset() addsimps [real_le_less]));
qed "starfun_le_mono";

(*****----- and another -----*****) 
goal NatStar.thy 
     "!!f. 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_def,hypreal_le_def,hypreal_less_def,
        hypnat_le_def,hypnat_less_def]));
by (dres_inst_tac [("x","x")] spec 1);
by (Step_tac 1);
by (dres_inst_tac [("x","%n. N")] spec 2);
by (Auto_tac);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (REPEAT(rtac exI 1 THEN Auto_tac));
by (Ultra_tac 1 THEN rtac ccontr 1 THEN dtac leI 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 + 1hn)";
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. rabs (f n))) N = hrabs((*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_def,starfunNat]));
qed "starfunNat_pow2";

Goalw [hypnat_of_nat_def] "(*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]));
qed "starfun_pow";

(*------------------------------------------------------ 
   hypreal_of_hypnat as NS extension of real_of_nat! 
-------------------------------------------------------*)
Goal "(*fNat* real_of_nat) = 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";