src/HOL/Hyperreal/NSA.ML

new theorems

(*  Title       : NSA.ML
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Infinite numbers, Infinitesimals,
                  infinitely close relation  etc.
*) 

fun CLAIM_SIMP str thms =
               prove_goal (the_context()) str
               (fn prems => [cut_facts_tac prems 1,
                   auto_tac (claset(),simpset() addsimps thms)]);
fun CLAIM str = CLAIM_SIMP str [];

(*--------------------------------------------------------------------
     Closure laws for members of (embedded) set standard real Reals
 --------------------------------------------------------------------*)

Goalw [SReal_def] "[| (x::hypreal): Reals; y: Reals |] ==> x + y: Reals";
by (Step_tac 1);
by (res_inst_tac [("x","r + ra")] exI 1);
by (Simp_tac 1);
qed "SReal_add";

Goalw [SReal_def] "[| (x::hypreal): Reals; y: Reals |] ==> x * y: Reals";
by (Step_tac 1);
by (res_inst_tac [("x","r * ra")] exI 1);
by (simp_tac (simpset() addsimps [hypreal_of_real_mult]) 1);
qed "SReal_mult";

Goalw [SReal_def] "(x::hypreal): Reals ==> inverse x : Reals";
by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1); 
qed "SReal_inverse";

Goal "[| (x::hypreal): Reals;  y: Reals |] ==> x/y: Reals";
by (asm_simp_tac (simpset() addsimps [SReal_mult,SReal_inverse,
                                      hypreal_divide_def]) 1); 
qed "SReal_divide";

Goalw [SReal_def] "(x::hypreal): Reals ==> -x : Reals";
by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1); 
qed "SReal_minus";

Goal "(-x : Reals) = ((x::hypreal): Reals)";
by Auto_tac;  
by (etac SReal_minus 2); 
by (dtac SReal_minus 1); 
by Auto_tac;  
qed "SReal_minus_iff";
Addsimps [SReal_minus_iff]; 

Goal "[| (x::hypreal) + y : Reals; y: Reals |] ==> x: Reals";
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1);
by (assume_tac 1); 
by Auto_tac;  
qed "SReal_add_cancel";

Goalw [SReal_def] "(x::hypreal): Reals ==> abs x : Reals";
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_hrabs]));
qed "SReal_hrabs";

Goalw [SReal_def] "hypreal_of_real x: Reals";
by (Blast_tac 1);
qed "SReal_hypreal_of_real";
Addsimps [SReal_hypreal_of_real];

Goalw [hypreal_number_of_def] "(number_of w ::hypreal) : Reals";
by (rtac SReal_hypreal_of_real 1);
qed "SReal_number_of";
Addsimps [SReal_number_of];

(** As always with numerals, 0 and 1 are special cases **)

Goal "(0::hypreal) : Reals";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
by (rtac SReal_number_of 1); 
qed "Reals_0";
Addsimps [Reals_0];

Goal "(1::hypreal) : Reals";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
by (rtac SReal_number_of 1); 
qed "Reals_1";
Addsimps [Reals_1];

Goalw [hypreal_divide_def] "r : Reals ==> r/(number_of w::hypreal) : Reals";
by (blast_tac (claset() addSIs [SReal_number_of, SReal_mult, 
                                SReal_inverse]) 1);
qed "SReal_divide_number_of";

(* Infinitesimal epsilon not in Reals *)

Goalw [SReal_def] "epsilon ~: Reals";
by (auto_tac (claset(),
              simpset() addsimps [hypreal_of_real_not_eq_epsilon RS not_sym]));
qed "SReal_epsilon_not_mem";

Goalw [SReal_def] "omega ~: Reals";
by (auto_tac (claset(),
              simpset() addsimps [hypreal_of_real_not_eq_omega RS not_sym]));
qed "SReal_omega_not_mem";

Goalw [SReal_def] "{x. hypreal_of_real x : Reals} = (UNIV::real set)";
by Auto_tac;
qed "SReal_UNIV_real";

Goalw [SReal_def] "(x: Reals) = (EX y. x = hypreal_of_real y)";
by Auto_tac;
qed "SReal_iff";

Goalw [SReal_def] "hypreal_of_real `(UNIV::real set) = Reals";
by Auto_tac;
qed "hypreal_of_real_image";

Goalw [SReal_def] "inv hypreal_of_real `Reals = (UNIV::real set)";
by Auto_tac;
by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypreal_of_real_image";

Goalw [SReal_def] 
      "[| EX x. x: P; P <= Reals |] ==> EX Q. P = hypreal_of_real ` Q";
by (Best_tac 1); 
qed "SReal_hypreal_of_real_image";

Goal "[| (x::hypreal): Reals; y: Reals;  x<y |] ==> EX r: Reals. x<r & r<y";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
by (dtac real_dense 1 THEN Step_tac 1);
by (res_inst_tac [("x","hypreal_of_real r")] bexI 1);
by Auto_tac;
qed "SReal_dense";

(*------------------------------------------------------------------
                   Completeness of Reals
 ------------------------------------------------------------------*)
Goal "P <= Reals ==> ((EX x:P. y < x) = \ 
\     (EX X. hypreal_of_real X : P & y < hypreal_of_real X))";
by (blast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (flexflex_tac );
qed "SReal_sup_lemma";

Goal "[| P <= Reals; EX x. x: P; EX y : Reals. ALL x: P. x < y |] \
\     ==> (EX X. X: {w. hypreal_of_real w : P}) & \
\         (EX Y. ALL X: {w. hypreal_of_real w : P}. X < Y)";
by (rtac conjI 1);
by (fast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (Auto_tac THEN ftac subsetD 1 THEN assume_tac 1);
by (dtac (SReal_iff RS iffD1) 1);
by (Auto_tac THEN res_inst_tac [("x","ya")] exI 1);
by Auto_tac;
qed "SReal_sup_lemma2";

(*------------------------------------------------------
    lifting of ub and property of lub
 -------------------------------------------------------*)
Goalw [isUb_def,setle_def] 
      "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\      (isUb (UNIV :: real set) Q Y)";
by Auto_tac;
qed "hypreal_of_real_isUb_iff";

Goalw [isLub_def,leastP_def] 
     "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) \
\     ==> isLub (UNIV :: real set) Q Y";
by (auto_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2],
              simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
qed "hypreal_of_real_isLub1";

Goalw [isLub_def,leastP_def] 
      "isLub (UNIV :: real set) Q Y \
\      ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)";
by (auto_tac (claset(),
              simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
by (forw_inst_tac [("x2","x")] (isUbD2a RS (SReal_iff RS iffD1) RS exE) 1);
by (assume_tac 2);
by (dres_inst_tac [("x","xa")] spec 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_isUb_iff]));
qed "hypreal_of_real_isLub2";

Goal "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\     (isLub (UNIV :: real set) Q Y)";
by (blast_tac (claset() addIs [hypreal_of_real_isLub1,
                               hypreal_of_real_isLub2]) 1);
qed "hypreal_of_real_isLub_iff";

(* lemmas *)
Goalw [isUb_def] 
     "isUb Reals P Y ==> EX Yo. isUb Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isUb_hypreal_of_real";

Goalw [isLub_def,leastP_def,isUb_def] 
     "isLub Reals P Y ==> EX Yo. isLub Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isLub_hypreal_of_real";

Goalw [isLub_def,leastP_def,isUb_def] 
     "EX Yo. isLub Reals P (hypreal_of_real Yo) ==> EX Y. isLub Reals P Y";
by Auto_tac;
qed "lemma_isLub_hypreal_of_real2";

Goal "[| P <= Reals;  EX x. x: P;  EX Y. isUb Reals P Y |] \
\     ==> EX t::hypreal. isLub Reals P t";
by (ftac SReal_hypreal_of_real_image 1);
by (Auto_tac THEN dtac lemma_isUb_hypreal_of_real 1);
by (auto_tac (claset() addSIs [reals_complete, lemma_isLub_hypreal_of_real2], 
     simpset() addsimps [hypreal_of_real_isLub_iff,hypreal_of_real_isUb_iff]));
qed "SReal_complete";

(*--------------------------------------------------------------------
        Set of finite elements is a subring of the extended reals
 --------------------------------------------------------------------*)
Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> (x+y) : HFinite";
by (blast_tac (claset() addSIs [SReal_add,hrabs_add_less]) 1);
qed "HFinite_add";

Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> x*y : HFinite";
by (Asm_full_simp_tac 1); 
by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
qed "HFinite_mult";

Goalw [HFinite_def] "(-x : HFinite) = (x : HFinite)";
by (Simp_tac 1);
qed "HFinite_minus_iff";

Goalw [SReal_def,HFinite_def] "Reals <= HFinite";
by Auto_tac;
by (res_inst_tac [("x","1 + abs(hypreal_of_real r)")] exI 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_hrabs]));
by (res_inst_tac [("x","1 + abs r")] exI 1);
by (Simp_tac 1);
qed "SReal_subset_HFinite";

Goal "hypreal_of_real x : HFinite";
by (auto_tac (claset() addIs [(SReal_subset_HFinite RS subsetD)],
              simpset()));
qed "HFinite_hypreal_of_real";

Addsimps [HFinite_hypreal_of_real];

Goalw [HFinite_def] "x : HFinite ==> EX t: Reals. abs x < t";
by Auto_tac;
qed "HFiniteD";

Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)";
by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
qed "HFinite_hrabs_iff";
AddIffs [HFinite_hrabs_iff];

Goal "number_of w : HFinite";
by (rtac (SReal_number_of RS (SReal_subset_HFinite RS subsetD)) 1);
qed "HFinite_number_of";
Addsimps [HFinite_number_of];

(** As always with numerals, 0 and 1 are special cases **)

Goal "0 : HFinite";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
by (rtac HFinite_number_of 1); 
qed "HFinite_0";
Addsimps [HFinite_0];

Goal "1 : HFinite";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
by (rtac HFinite_number_of 1); 
qed "HFinite_1";
Addsimps [HFinite_1];

Goal "[|x : HFinite; y <= x; 0 <= y |] ==> y: HFinite";
by (case_tac "x <= 0" 1);
by (dres_inst_tac [("y","x")] order_trans 1);
by (dtac hypreal_le_anti_sym 2);
by (auto_tac (claset() addSDs [not_hypreal_leE], simpset()));
by (auto_tac (claset() addSIs [bexI] addIs [order_le_less_trans],
     simpset() addsimps [hrabs_eqI1,hrabs_eqI2,hrabs_minus_eqI1,HFinite_def]));
qed "HFinite_bounded"; 

(*------------------------------------------------------------------
       Set of infinitesimals is a subring of the hyperreals   
 ------------------------------------------------------------------*)
Goalw [Infinitesimal_def]
      "x : Infinitesimal ==> ALL r: Reals. 0 < r --> abs x < r";
by Auto_tac;
qed "InfinitesimalD";

Goalw [Infinitesimal_def] "0 : Infinitesimal";
by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
qed "Infinitesimal_zero";
AddIffs [Infinitesimal_zero];

Goal "x/(2::hypreal) + x/(2::hypreal) = x";
by Auto_tac;  
qed "hypreal_sum_of_halves";

Goal "0 < r ==> 0 < r/(2::hypreal)";
by Auto_tac;  
qed "hypreal_half_gt_zero";

Goalw [Infinitesimal_def] 
     "[| x : Infinitesimal; y : Infinitesimal |] ==> (x+y) : Infinitesimal";
by Auto_tac;
by (rtac (hypreal_sum_of_halves RS subst) 1);
by (dtac hypreal_half_gt_zero 1);
by (blast_tac (claset() addIs [hrabs_add_less, hrabs_add_less, 
                               SReal_divide_number_of]) 1); 
qed "Infinitesimal_add";

Goalw [Infinitesimal_def] "(-x:Infinitesimal) = (x:Infinitesimal)";
by (Full_simp_tac 1);
qed "Infinitesimal_minus_iff";
Addsimps [Infinitesimal_minus_iff];

Goal "[| x : Infinitesimal;  y : Infinitesimal |] ==> x-y : Infinitesimal";
by (asm_simp_tac
    (simpset() addsimps [hypreal_diff_def, Infinitesimal_add]) 1);
qed "Infinitesimal_diff";

Goalw [Infinitesimal_def] 
     "[| x : Infinitesimal; y : Infinitesimal |] ==> (x * y) : Infinitesimal";
by Auto_tac;
by (case_tac "y=0" 1);
by (cut_inst_tac [("u","abs x"),("v","1"),("x","abs y"),("y","r")] 
    hypreal_mult_less_mono 2);
by Auto_tac;
qed "Infinitesimal_mult";

Goal "[| x : Infinitesimal; y : HFinite |] ==> (x * y) : Infinitesimal";
by (auto_tac (claset() addSDs [HFiniteD],
              simpset() addsimps [Infinitesimal_def]));
by (ftac hrabs_less_gt_zero 1);
by (dres_inst_tac [("x","r/t")] bspec 1); 
by (blast_tac (claset() addIs [SReal_divide]) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1); 
by (case_tac "x=0 | y=0" 1);
by (cut_inst_tac [("u","abs x"),("v","r/t"),("x","abs y")] 
    hypreal_mult_less_mono 2);
by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_divide_iff]));  
qed "Infinitesimal_HFinite_mult";

Goal "[| x : Infinitesimal; y : HFinite |] ==> (y * x) : Infinitesimal";
by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
              simpset() addsimps [hypreal_mult_commute]));
qed "Infinitesimal_HFinite_mult2";

(*** rather long proof ***)
Goalw [HInfinite_def,Infinitesimal_def] 
     "x: HInfinite ==> inverse x: Infinitesimal";
by Auto_tac;
by (eres_inst_tac [("x","inverse r")] ballE 1);
by (stac hrabs_inverse 1);
by (forw_inst_tac [("x1","r"),("z","abs x")] 
    (hypreal_inverse_gt_0 RS order_less_trans) 1);
by (assume_tac 1);
by (dtac ((hypreal_inverse_inverse RS sym) RS subst) 1);
by (rtac (hypreal_inverse_less_iff RS iffD1) 1);
by (auto_tac (claset(), simpset() addsimps [SReal_inverse]));  
qed "HInfinite_inverse_Infinitesimal";



Goalw [HInfinite_def] "[|x: HInfinite;y: HInfinite|] ==> (x*y): HInfinite";
by Auto_tac;
by (eres_inst_tac [("x","1")] ballE 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (case_tac "y=0" 1); 
by (cut_inst_tac [("x","1"),("y","abs x"),
                  ("u","r"),("v","abs y")] hypreal_mult_less_mono 2);
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));  
qed "HInfinite_mult";

Goalw [HInfinite_def] 
      "[|x: HInfinite; 0 <= y; 0 <= x|] ==> (x + y): HInfinite";
by (auto_tac (claset() addSIs [hypreal_add_zero_less_le_mono],
              simpset() addsimps [hrabs_eqI1, hypreal_add_commute,
                                  hypreal_le_add_order]));
qed "HInfinite_add_ge_zero";

Goal "[|x: HInfinite; 0 <= y; 0 <= x|] ==> (y + x): HInfinite";
by (auto_tac (claset() addSIs [HInfinite_add_ge_zero],
              simpset() addsimps [hypreal_add_commute]));
qed "HInfinite_add_ge_zero2";

Goal "[|x: HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite";
by (blast_tac (claset() addIs [HInfinite_add_ge_zero,
                    order_less_imp_le]) 1);
qed "HInfinite_add_gt_zero";

Goalw [HInfinite_def] "(-x: HInfinite) = (x: HInfinite)";
by Auto_tac;
qed "HInfinite_minus_iff";

Goal "[|x: HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite";
by (dtac (HInfinite_minus_iff RS iffD2) 1);
by (rtac (HInfinite_minus_iff RS iffD1) 1);
by (auto_tac (claset() addIs [HInfinite_add_ge_zero],
              simpset() addsimps [hypreal_minus_zero_le_iff]));
qed "HInfinite_add_le_zero";

Goal "[|x: HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite";
by (blast_tac (claset() addIs [HInfinite_add_le_zero,
                               order_less_imp_le]) 1);
qed "HInfinite_add_lt_zero";

Goal "[|a: HFinite; b: HFinite; c: HFinite|] \ 
\     ==> a*a + b*b + c*c : HFinite";
by (auto_tac (claset() addIs [HFinite_mult,HFinite_add], simpset()));
qed "HFinite_sum_squares";

Goal "x ~: Infinitesimal ==> x ~= 0";
by Auto_tac;
qed "not_Infinitesimal_not_zero";

Goal "x: HFinite - Infinitesimal ==> x ~= 0";
by Auto_tac;
qed "not_Infinitesimal_not_zero2";

Goal "(abs x : Infinitesimal) = (x : Infinitesimal)";
by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
qed "Infinitesimal_hrabs_iff";
AddIffs [Infinitesimal_hrabs_iff];

Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal";
by (Blast_tac 1);
qed "HFinite_diff_Infinitesimal_hrabs";

Goalw [Infinitesimal_def] 
      "[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
by (auto_tac (claset() addSDs [bspec], simpset()));
by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
by (fast_tac (claset() addIs [order_less_trans]) 1);
qed "hrabs_less_Infinitesimal";

Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
by (blast_tac (claset() addDs [order_le_imp_less_or_eq] 
                        addIs [hrabs_less_Infinitesimal]) 1);
qed "hrabs_le_Infinitesimal";

Goalw [Infinitesimal_def] 
      "[| e : Infinitesimal; \
\         e' : Infinitesimal; \
\         e' < x ; x < e |] ==> x : Infinitesimal";
by (auto_tac (claset() addSDs [bspec], simpset()));
by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
by (dtac (hrabs_interval_iff RS iffD1) 1);
by (fast_tac(claset() addIs [order_less_trans,hrabs_interval_iff RS iffD2]) 1);
qed "Infinitesimal_interval";

Goal "[| e : Infinitesimal; e' : Infinitesimal; \
\        e' <= x ; x <= e |] ==> x : Infinitesimal";
by (auto_tac (claset() addIs [Infinitesimal_interval],
    simpset() addsimps [hypreal_le_eq_less_or_eq]));
qed "Infinitesimal_interval2";

Goalw [Infinitesimal_def] 
     "[| x ~: Infinitesimal;  y ~: Infinitesimal|] ==> (x*y) ~:Infinitesimal";
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); 
by (eres_inst_tac [("x","r*ra")] ballE 1);
by (fast_tac (claset() addIs [SReal_mult]) 2);
by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff]));
by (cut_inst_tac [("x","ra"),("y","abs y"),
                  ("u","r"),("v","abs x")] hypreal_mult_le_mono 1);
by Auto_tac;  
qed "not_Infinitesimal_mult";

Goal "x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
by (rtac ccontr 1);
by (dtac (de_Morgan_disj RS iffD1) 1);
by (fast_tac (claset() addDs [not_Infinitesimal_mult]) 1);
qed "Infinitesimal_mult_disj";

Goal "x: HFinite-Infinitesimal ==> x ~= 0";
by (Blast_tac 1);
qed "HFinite_Infinitesimal_not_zero";

Goal "[| x : HFinite - Infinitesimal; \
\                  y : HFinite - Infinitesimal \
\               |] ==> (x*y) : HFinite - Infinitesimal";
by (Clarify_tac 1);
by (blast_tac (claset() addDs [HFinite_mult,not_Infinitesimal_mult]) 1);
qed "HFinite_Infinitesimal_diff_mult";

Goalw [Infinitesimal_def,HFinite_def]  
      "Infinitesimal <= HFinite";
by Auto_tac;  
by (res_inst_tac [("x","1")] bexI 1); 
by Auto_tac;  
qed "Infinitesimal_subset_HFinite";

Goal "x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
by (etac (HFinite_hypreal_of_real RSN 
          (2,Infinitesimal_HFinite_mult)) 1);
qed "Infinitesimal_hypreal_of_real_mult";

Goal "x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
by (etac (HFinite_hypreal_of_real RSN 
          (2,Infinitesimal_HFinite_mult2)) 1);
qed "Infinitesimal_hypreal_of_real_mult2";

(*----------------------------------------------------------------------
                   Infinitely close relation @=
 ----------------------------------------------------------------------*)

Goalw [Infinitesimal_def,approx_def] 
        "(x:Infinitesimal) = (x @= 0)";
by (Simp_tac 1);
qed "mem_infmal_iff";

Goalw [approx_def]" (x @= y) = (x + -y @= 0)";
by (Simp_tac 1);
qed "approx_minus_iff";

Goalw [approx_def]" (x @= y) = (-y + x @= 0)";
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
qed "approx_minus_iff2";

Goalw [approx_def,Infinitesimal_def]  "x @= x";
by (Simp_tac 1);
qed "approx_refl";
AddIffs [approx_refl];

Goalw [approx_def]  "x @= y ==> y @= x";
by (rtac (hypreal_minus_distrib1 RS subst) 1);
by (etac (Infinitesimal_minus_iff RS iffD2) 1);
qed "approx_sym";

Goalw [approx_def]  "[| x @= y; y @= z |] ==> x @= z";
by (dtac Infinitesimal_add 1); 
by (assume_tac 1); 
by Auto_tac;  
qed "approx_trans";

Goal "[| r @= x; s @= x |] ==> r @= s";
by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1); 
qed "approx_trans2";

Goal "[| x @= r; x @= s|] ==> r @= s";
by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1); 
qed "approx_trans3";

Goal "(number_of w @= x) = (x @= number_of w)"; 
by (blast_tac (claset() addIs [approx_sym]) 1); 
qed "number_of_approx_reorient";

Goal "(0 @= x) = (x @= 0)"; 
by (blast_tac (claset() addIs [approx_sym]) 1); 
qed "zero_approx_reorient";

Goal "(1 @= x) = (x @= 1)"; 
by (blast_tac (claset() addIs [approx_sym]) 1); 
qed "one_approx_reorient";


(*** re-orientation, following HOL/Integ/Bin.ML 
     We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
 ***)

(*reorientation simprules using ==, for the following simproc*)
val meta_zero_approx_reorient = zero_approx_reorient RS eq_reflection;
val meta_one_approx_reorient = one_approx_reorient RS eq_reflection;
val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection;

(*reorientation simplification procedure: reorients (polymorphic) 
  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
  case u of
      Const("0", _) => None
    | Const("1", _) => None
    | Const("Numeral.number_of", _) $ _ => None
    | _ => Some (case t of
		Const("0", _) => meta_zero_approx_reorient
	      | Const("1", _) => meta_one_approx_reorient
	      | Const("Numeral.number_of", _) $ _ => 
                                 meta_number_of_approx_reorient);

val approx_reorient_simproc = 
    Bin_Simprocs.prep_simproc ("reorient_simproc",
		  Bin_Simprocs.prep_pats ["0@=x", "1@=x", "number_of w @= x"], 
		  reorient_proc);

Addsimprocs [approx_reorient_simproc];


Goal "(x-y : Infinitesimal) = (x @= y)";
by (auto_tac (claset(),
              simpset() addsimps [hypreal_diff_def, approx_minus_iff RS sym,
                                  mem_infmal_iff]));
qed "Infinitesimal_approx_minus";

Goalw [monad_def] "(x @= y) = (monad(x)=monad(y))";
by (auto_tac (claset() addDs [approx_sym] 
                       addSEs [approx_trans,equalityCE],
              simpset()));
qed "approx_monad_iff";

Goal "[| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
by (blast_tac (claset() addIs [approx_trans, approx_sym]) 1); 
qed "Infinitesimal_approx";

val prem1::prem2::rest = 
goalw thy [approx_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
by (stac hypreal_minus_add_distrib 1);
by (stac hypreal_add_assoc 1);
by (res_inst_tac [("y1","c")] (hypreal_add_left_commute RS subst) 1);
by (rtac (hypreal_add_assoc RS subst) 1);
by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1);
qed "approx_add";

Goal "a @= b ==> -a @= -b";
by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
by (dtac (approx_minus_iff RS iffD1) 1);
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
qed "approx_minus";

Goal "-a @= -b ==> a @= b";
by (auto_tac (claset() addDs [approx_minus], simpset()));
qed "approx_minus2";

Goal "(-a @= -b) = (a @= b)";
by (blast_tac (claset() addIs [approx_minus,approx_minus2]) 1);
qed "approx_minus_cancel";

Addsimps [approx_minus_cancel];

Goal "[| a @= b; c @= d |] ==> a + -c @= b + -d";
by (blast_tac (claset() addSIs [approx_add,approx_minus]) 1);
qed "approx_add_minus";

Goalw [approx_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c"; 
by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult,
    hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym] 
    delsimps [hypreal_minus_mult_eq1 RS sym]) 1);
qed "approx_mult1";

Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b"; 
by (asm_simp_tac (simpset() addsimps [approx_mult1,hypreal_mult_commute]) 1);
qed "approx_mult2";

Goal "[|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
by (fast_tac (claset() addIs [approx_mult2,approx_trans]) 1);
qed "approx_mult_subst";

Goal "[| u @= x*v; x @= y; v: HFinite |] ==> u @= y*v";
by (fast_tac (claset() addIs [approx_mult1,approx_trans]) 1);
qed "approx_mult_subst2";

Goal "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v";
by (auto_tac (claset() addIs [approx_mult_subst2], simpset()));
qed "approx_mult_subst_SReal";

Goalw [approx_def]  "a = b ==> a @= b";
by (Asm_simp_tac 1);
qed "approx_eq_imp";

Goal "x: Infinitesimal ==> -x @= x"; 
by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD2,
    mem_infmal_iff RS iffD1,approx_trans2]) 1);
qed "Infinitesimal_minus_approx";

Goalw [approx_def]  "(EX y: Infinitesimal. x + -z = y) = (x @= z)";
by (Blast_tac 1);
qed "bex_Infinitesimal_iff";

Goal "(EX y: Infinitesimal. x = z + y) = (x @= z)";
by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff RS sym]) 1);
by (Force_tac 1);
qed "bex_Infinitesimal_iff2";

Goal "[| y: Infinitesimal; x + y = z |] ==> x @= z";
by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib,
    hypreal_add_assoc RS sym]));
qed "Infinitesimal_add_approx";

Goal "y: Infinitesimal ==> x @= x + y";
by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib,
    hypreal_add_assoc RS sym]));
qed "Infinitesimal_add_approx_self";

Goal "y: Infinitesimal ==> x @= y + x";
by (auto_tac (claset() addDs [Infinitesimal_add_approx_self],
    simpset() addsimps [hypreal_add_commute]));
qed "Infinitesimal_add_approx_self2";

Goal "y: Infinitesimal ==> x @= x + -y";
by (blast_tac (claset() addSIs [Infinitesimal_add_approx_self,
                                Infinitesimal_minus_iff RS iffD2]) 1);
qed "Infinitesimal_add_minus_approx_self";

Goal "[| y: Infinitesimal; x+y @= z|] ==> x @= z";
by (dres_inst_tac [("x","x")] (Infinitesimal_add_approx_self RS approx_sym) 1);
by (etac (approx_trans3 RS approx_sym) 1);
by (assume_tac 1);
qed "Infinitesimal_add_cancel";

Goal "[| y: Infinitesimal; x @= z + y|] ==> x @= z";
by (dres_inst_tac [("x","z")] (Infinitesimal_add_approx_self2  RS approx_sym) 1);
by (etac (approx_trans3 RS approx_sym) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
by (etac approx_sym 1);
qed "Infinitesimal_add_right_cancel";

Goal "d + b  @= d + c ==> b @= c";
by (dtac (approx_minus_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps 
    [hypreal_minus_add_distrib,approx_minus_iff RS sym] 
    @ hypreal_add_ac) 1);
qed "approx_add_left_cancel";

Goal "b + d @= c + d ==> b @= c";
by (rtac approx_add_left_cancel 1);
by (asm_full_simp_tac (simpset() addsimps 
    [hypreal_add_commute]) 1);
qed "approx_add_right_cancel";

Goal "b @= c ==> d + b @= d + c";
by (rtac (approx_minus_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps 
    [hypreal_minus_add_distrib,approx_minus_iff RS sym] 
    @ hypreal_add_ac) 1);
qed "approx_add_mono1";

Goal "b @= c ==> b + a @= c + a";
by (asm_simp_tac (simpset() addsimps 
    [hypreal_add_commute,approx_add_mono1]) 1);
qed "approx_add_mono2";

Goal "(a + b @= a + c) = (b @= c)";
by (fast_tac (claset() addEs [approx_add_left_cancel,
    approx_add_mono1]) 1);
qed "approx_add_left_iff";

Addsimps [approx_add_left_iff];

Goal "(b + a @= c + a) = (b @= c)";
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
qed "approx_add_right_iff";

Addsimps [approx_add_right_iff];

Goal "[| x: HFinite; x @= y |] ==> y: HFinite";
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (Step_tac 1);
by (dtac (Infinitesimal_subset_HFinite RS subsetD 
          RS (HFinite_minus_iff RS iffD2)) 1);
by (dtac HFinite_add 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
qed "approx_HFinite";

Goal "x @= hypreal_of_real D ==> x: HFinite";
by (rtac (approx_sym RSN (2,approx_HFinite)) 1);
by Auto_tac;
qed "approx_hypreal_of_real_HFinite";

Goal "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d";
by (rtac approx_trans 1); 
by (rtac approx_mult2 2); 
by (rtac approx_mult1 1);
by (blast_tac (claset() addIs [approx_HFinite, approx_sym]) 2);  
by Auto_tac;  
qed "approx_mult_HFinite";

Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
\     ==> a*c @= hypreal_of_real b*hypreal_of_real d";
by (blast_tac (claset() addSIs [approx_mult_HFinite,
            approx_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
qed "approx_mult_hypreal_of_real";

Goal "[| a: Reals; a ~= 0; a*x @= 0 |] ==> x @= 0";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [approx_mult2],
    simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "approx_SReal_mult_cancel_zero";

(* REM comments: newly added *)
Goal "[| a: Reals; x @= 0 |] ==> x*a @= 0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
              approx_mult1], simpset()));
qed "approx_mult_SReal1";

Goal "[| a: Reals; x @= 0 |] ==> a*x @= 0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
              approx_mult2], simpset()));
qed "approx_mult_SReal2";

Goal "[|a : Reals; a ~= 0 |] ==> (a*x @= 0) = (x @= 0)";
by (blast_tac (claset() addIs [approx_SReal_mult_cancel_zero,
    approx_mult_SReal2]) 1);
qed "approx_mult_SReal_zero_cancel_iff";
Addsimps [approx_mult_SReal_zero_cancel_iff];

Goal "[| a: Reals; a ~= 0; a* w @= a*z |] ==> w @= z";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [approx_mult2],
    simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "approx_SReal_mult_cancel";

Goal "[| a: Reals; a ~= 0|] ==> (a* w @= a*z) = (w @= z)";
by (auto_tac (claset() addSIs [approx_mult2,SReal_subset_HFinite RS subsetD] 
    addIs [approx_SReal_mult_cancel], simpset()));
qed "approx_SReal_mult_cancel_iff1";
Addsimps [approx_SReal_mult_cancel_iff1];

Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff2 RS sym]) 1); 
by Auto_tac;  
by (res_inst_tac [("x","g+y-z")] bexI 1);
by (Simp_tac 1); 
by (rtac Infinitesimal_interval2 1); 
by (rtac Infinitesimal_zero 2); 
by Auto_tac;  
qed "approx_le_bound";

(*-----------------------------------------------------------------
    Zero is the only infinitesimal that is also a real
 -----------------------------------------------------------------*)

Goalw [Infinitesimal_def] 
     "[| x: Reals; y: Infinitesimal; 0 < x |] ==> y < x";
by (rtac (hrabs_ge_self RS order_le_less_trans) 1);
by Auto_tac;  
qed "Infinitesimal_less_SReal";

Goal "y: Infinitesimal ==> ALL r: Reals. 0 < r --> y < r";
by (blast_tac (claset() addIs [Infinitesimal_less_SReal]) 1);
qed "Infinitesimal_less_SReal2";

Goalw [Infinitesimal_def] 
     "[| 0 < y;  y: Reals|] ==> y ~: Infinitesimal";
by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
qed "SReal_not_Infinitesimal";

Goal "[| y < 0;  y : Reals |] ==> y ~: Infinitesimal";
by (stac (Infinitesimal_minus_iff RS sym) 1); 
by (rtac SReal_not_Infinitesimal 1); 
by Auto_tac;  
qed "SReal_minus_not_Infinitesimal";

Goal "Reals Int Infinitesimal = {0}";
by Auto_tac;
by (cut_inst_tac [("x","x"),("y","0")] hypreal_linear 1);
by (blast_tac (claset() addDs [SReal_not_Infinitesimal,
                               SReal_minus_not_Infinitesimal]) 1);
qed "SReal_Int_Infinitesimal_zero";

Goal "[| x: Reals; x: Infinitesimal|] ==> x = 0";
by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
by (Blast_tac 1);
qed "SReal_Infinitesimal_zero";

Goal "[| x : Reals; x ~= 0 |] ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
                              SReal_subset_HFinite RS subsetD], 
              simpset()));
qed "SReal_HFinite_diff_Infinitesimal";

Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
by (rtac SReal_HFinite_diff_Infinitesimal 1);
by Auto_tac;
qed "hypreal_of_real_HFinite_diff_Infinitesimal";

Goal "(hypreal_of_real x : Infinitesimal) = (x=0)";
by Auto_tac;  
by (rtac ccontr 1); 
by (rtac (hypreal_of_real_HFinite_diff_Infinitesimal RS DiffD2) 1); 
by Auto_tac;
qed "hypreal_of_real_Infinitesimal_iff_0";
AddIffs [hypreal_of_real_Infinitesimal_iff_0];

Goal "number_of w ~= (0::hypreal) ==> number_of w ~: Infinitesimal";
by (fast_tac (claset() addDs [SReal_number_of RS SReal_Infinitesimal_zero]) 1);
qed "number_of_not_Infinitesimal";
Addsimps [number_of_not_Infinitesimal];

(*again: 1 is a special case, but not 0 this time*)
Goal "1 ~: Infinitesimal";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
by (rtac number_of_not_Infinitesimal 1); 
by (Simp_tac 1); 
qed "one_not_Infinitesimal";
Addsimps [one_not_Infinitesimal];

Goal "[| y: Reals; x @= y; y~= 0 |] ==> x ~= 0";
by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
by (Asm_full_simp_tac 1); 
by (blast_tac (claset() addDs 
		[approx_sym RS (mem_infmal_iff RS iffD2),
		 SReal_not_Infinitesimal, SReal_minus_not_Infinitesimal]) 1);
qed "approx_SReal_not_zero";

Goal "[| x @= y; y : HFinite - Infinitesimal |] \
\     ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
              simpset() addsimps [mem_infmal_iff]));
by (dtac approx_trans3 1 THEN assume_tac 1);
by (blast_tac (claset() addDs [approx_sym]) 1);
qed "HFinite_diff_Infinitesimal_approx";

(*The premise y~=0 is essential; otherwise x/y =0 and we lose the 
  HFinite premise.*)
Goal "[| y ~= 0;  y: Infinitesimal;  x/y : HFinite |] ==> x : Infinitesimal";
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
by (asm_full_simp_tac 
    (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
qed "Infinitesimal_ratio";

(*------------------------------------------------------------------
       Standard Part Theorem: Every finite x: R* is infinitely 
       close to a unique real number (i.e a member of Reals)
 ------------------------------------------------------------------*)
(*------------------------------------------------------------------
         Uniqueness: Two infinitely close reals are equal
 ------------------------------------------------------------------*)

Goal "[|x: Reals; y: Reals|] ==> (x @= y) = (x = y)"; 
by Auto_tac;
by (rewtac approx_def);
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1 THEN assume_tac 1);
by (dtac SReal_Infinitesimal_zero 1 THEN assume_tac 1);
by (dtac sym 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff RS sym]) 1);
qed "SReal_approx_iff";

Goal "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))";
by (rtac SReal_approx_iff 1); 
by Auto_tac;  
qed "number_of_approx_iff";
Addsimps [number_of_approx_iff];

(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
Addsimps
 (map (simplify (simpset()))
      [inst "v" "Pls" number_of_approx_iff, 
       inst "v" "Pls BIT True" number_of_approx_iff,
       inst "w" "Pls" number_of_approx_iff, 
       inst "w" "Pls BIT True" number_of_approx_iff]);


Goal "~ (0 @= 1)";
by (stac SReal_approx_iff 1); 
by Auto_tac;  
qed "not_0_approx_1";
Addsimps [not_0_approx_1];

Goal "~ (1 @= 0)";
by (stac SReal_approx_iff 1); 
by Auto_tac;  
qed "not_1_approx_0";
Addsimps [not_1_approx_0];

Goal "(hypreal_of_real k @= hypreal_of_real m) = (k = m)";
by Auto_tac;  
by (rtac (inj_hypreal_of_real RS injD) 1); 
by (rtac (SReal_approx_iff RS iffD1) 1); 
by Auto_tac;  
qed "hypreal_of_real_approx_iff";
Addsimps [hypreal_of_real_approx_iff];

Goal "(hypreal_of_real k @= number_of w) = (k = number_of w)";
by (stac (hypreal_of_real_approx_iff RS sym) 1); 
by Auto_tac;  
qed "hypreal_of_real_approx_number_of_iff";
Addsimps [hypreal_of_real_approx_number_of_iff];

(*And also for 0 and 1.*)
Addsimps
 (map (simplify (simpset()))
      [inst "w" "Pls" hypreal_of_real_approx_number_of_iff, 
       inst "w" "Pls BIT True" hypreal_of_real_approx_number_of_iff]);

Goal "[| r: Reals; s: Reals; r @= x; s @= x|] ==> r = s";
by (blast_tac (claset() addIs [(SReal_approx_iff RS iffD1),
               approx_trans2]) 1);
qed "approx_unique_real";

(*------------------------------------------------------------------
       Existence of unique real infinitely close
 ------------------------------------------------------------------*)
(* lemma about lubs *)
Goal "!!(x::hypreal). [| isLub R S x; isLub R S y |] ==> x = y";
by (ftac isLub_isUb 1);
by (forw_inst_tac [("x","y")] isLub_isUb 1);
by (blast_tac (claset() addSIs [hypreal_le_anti_sym]
                addSDs [isLub_le_isUb]) 1);
qed "hypreal_isLub_unique";

Goal "x: HFinite ==> EX u. isUb Reals {s. s: Reals & s < x} u";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
by (auto_tac (claset() addIs [order_less_imp_le,setleI,isUbI,
    order_less_trans], simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_ub";

Goal "x: HFinite ==> EX y. y: {s. s: Reals & s < x}";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (dtac SReal_minus 1);
by (res_inst_tac [("x","-t")] exI 1); 
by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_nonempty";

Goal "{s. s: Reals & s < x} <= Reals";
by Auto_tac;
qed "lemma_st_part_subset";

Goal "x: HFinite ==> EX t. isLub Reals {s. s: Reals & s < x} t";
by (blast_tac (claset() addSIs [SReal_complete,lemma_st_part_ub,
    lemma_st_part_nonempty, lemma_st_part_subset]) 1);
qed "lemma_st_part_lub";

Goal "((t::hypreal) + r <= t) = (r <= 0)";
by (Step_tac 1);
by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
by (dres_inst_tac [("x","t")] hypreal_add_left_le_mono1 2);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc RS sym]));
qed "lemma_hypreal_le_left_cancel";

Goal "[| x: HFinite;  isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals;  0 < r |] ==> x <= t + r";
by (ftac isLubD1a 1);
by (rtac ccontr 1 THEN dtac (linorder_not_le RS iffD2) 1);
by (dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1);
by (dres_inst_tac [("y","t + r")] (isLubD1 RS setleD) 1);
by Auto_tac;  
qed "lemma_st_part_le1";

Goalw [setle_def] "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y";
by (auto_tac (claset() addSDs [bspec,order_le_less_trans]
                       addIs [order_less_imp_le],
              simpset()));
qed "hypreal_setle_less_trans";

Goalw [isUb_def] 
     "!!x::hypreal. [| isUb R S x; x < y; y: R |] ==> isUb R S y";
by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
qed "hypreal_gt_isUb";

Goal "[| x: HFinite; x < y; y: Reals |] \
\              ==> isUb Reals {s. s: Reals & s < x} y";
by (auto_tac (claset() addDs [order_less_trans]
    addIs [order_less_imp_le] addSIs [isUbI,setleI], simpset()));
qed "lemma_st_part_gt_ub";

Goal "t <= t + -r ==> r <= (0::hypreal)";
by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc RS sym]));
qed "lemma_minus_le_zero";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals; 0 < r |] \
\     ==> t + -r <= x";
by (ftac isLubD1a 1);
by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")] 
    SReal_add 1 THEN assume_tac 1);
by (dtac lemma_st_part_gt_ub 1 THEN REPEAT(assume_tac 1));
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
by (dtac lemma_minus_le_zero 1);
by (auto_tac (claset() addDs [order_less_le_trans],  simpset()));
qed "lemma_st_part_le2";

Goal "((x::hypreal) <= t + r) = (x + -t <= r)";
by Auto_tac;  
qed "lemma_hypreal_le_swap";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals; 0 < r |] \
\     ==> x + -t <= r";
by (blast_tac (claset() addSIs [lemma_hypreal_le_swap RS iffD1,
                                lemma_st_part_le1]) 1);
qed "lemma_st_part1a";

Goal "(t + -r <= x) = (-(x + -t) <= (r::hypreal))";
by Auto_tac;  
qed "lemma_hypreal_le_swap2";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals;  0 < r |] \
\     ==> -(x + -t) <= r";
by (blast_tac (claset() addSIs [lemma_hypreal_le_swap2 RS iffD1,
                                lemma_st_part_le2]) 1);
qed "lemma_st_part2a";

Goal "(x::hypreal): Reals ==> isUb Reals {s. s: Reals & s < x} x";
by (auto_tac (claset() addIs [isUbI, setleI,order_less_imp_le], simpset()));
qed "lemma_SReal_ub";

Goal "(x::hypreal): Reals ==> isLub Reals {s. s: Reals & s < x} x";
by (auto_tac (claset() addSIs [isLubI2,lemma_SReal_ub,setgeI], simpset()));
by (ftac isUbD2a 1);
by (res_inst_tac [("x","x"),("y","y")] hypreal_linear_less2 1);
by (auto_tac (claset() addSIs [order_less_imp_le], simpset()));
by (EVERY1[dtac SReal_dense, assume_tac, assume_tac, Step_tac]);
by (dres_inst_tac [("y","r")] isUbD 1);
by (auto_tac (claset() addDs [order_less_le_trans], simpset()));
qed "lemma_SReal_lub";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals; 0 < r |] \
\     ==> x + -t ~= r";
by Auto_tac;
by (forward_tac [isLubD1a RS SReal_minus] 1);
by (dtac SReal_add_cancel 1 THEN assume_tac 1);
by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
by (dtac hypreal_isLub_unique 1 THEN assume_tac 1);
by Auto_tac;
qed "lemma_st_part_not_eq1";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals; 0 < r |] \
\     ==> -(x + -t) ~= r";
by (auto_tac (claset(), simpset() addsimps [hypreal_minus_add_distrib]));
by (ftac isLubD1a 1);
by (dtac SReal_add_cancel 1 THEN assume_tac 1);
by (dres_inst_tac [("x","-x")] SReal_minus 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("x","x")] lemma_SReal_lub 1);
by (dtac hypreal_isLub_unique 1 THEN assume_tac 1);
by Auto_tac;
qed "lemma_st_part_not_eq2";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t; \
\        r: Reals; 0 < r |] \
\     ==> abs (x + -t) < r";
by (ftac lemma_st_part1a 1);
by (ftac lemma_st_part2a 4);
by Auto_tac;
by (REPEAT(dtac order_le_imp_less_or_eq 1));
by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
    lemma_st_part_not_eq2], simpset() addsimps [hrabs_interval_iff2]));
qed "lemma_st_part_major";

Goal "[| x: HFinite; \
\        isLub Reals {s. s: Reals & s < x} t |] \
\     ==> ALL r: Reals. 0 < r --> abs (x + -t) < r";
by (blast_tac (claset() addSDs [lemma_st_part_major]) 1);
qed "lemma_st_part_major2";

(*----------------------------------------------
  Existence of real and Standard Part Theorem
 ----------------------------------------------*)
Goal "x: HFinite ==> \
\     EX t: Reals. ALL r: Reals. 0 < r --> abs (x + -t) < r";
by (ftac lemma_st_part_lub 1 THEN Step_tac 1);
by (ftac isLubD1a 1);
by (blast_tac (claset() addDs [lemma_st_part_major2]) 1);
qed "lemma_st_part_Ex";

Goalw [approx_def,Infinitesimal_def] 
     "x:HFinite ==> EX t: Reals. x @= t";
by (dtac lemma_st_part_Ex 1);
by Auto_tac;  
qed "st_part_Ex";

(*--------------------------------
  Unique real infinitely close
 -------------------------------*)
Goal "x:HFinite ==> EX! t. t: Reals & x @= t";
by (dtac st_part_Ex 1 THEN Step_tac 1);
by (dtac approx_sym 2 THEN dtac approx_sym 2 
    THEN dtac approx_sym 2);
by (auto_tac (claset() addSIs [approx_unique_real], simpset()));
qed "st_part_Ex1";

(*------------------------------------------------------------------
       Finite and Infinite --- more theorems
 ------------------------------------------------------------------*)

Goalw [HFinite_def,HInfinite_def] "HFinite Int HInfinite = {}";
by (auto_tac (claset() addIs [hypreal_less_irrefl] addDs [order_less_trans],
              simpset()));
qed "HFinite_Int_HInfinite_empty";
Addsimps [HFinite_Int_HInfinite_empty];

Goal "x: HFinite ==> x ~: HInfinite";
by (EVERY1[Step_tac, dtac IntI, assume_tac]);
by Auto_tac;
qed "HFinite_not_HInfinite";

Goalw [HInfinite_def, HFinite_def] "x~: HFinite ==> x: HInfinite";
by Auto_tac;  
by (dres_inst_tac [("x","r + 1")] bspec 1);
by (auto_tac (claset(), simpset() addsimps [SReal_add]));   
qed "not_HFinite_HInfinite";

Goal "x : HInfinite | x : HFinite";
by (blast_tac (claset() addIs [not_HFinite_HInfinite]) 1);
qed "HInfinite_HFinite_disj";

Goal "(x : HInfinite) = (x ~: HFinite)";
by (blast_tac (claset() addDs [HFinite_not_HInfinite,
               not_HFinite_HInfinite]) 1);
qed "HInfinite_HFinite_iff";

Goal "(x : HFinite) = (x ~: HInfinite)";
by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
qed "HFinite_HInfinite_iff";

(*------------------------------------------------------------------
       Finite, Infinite and Infinitesimal --- more theorems
 ------------------------------------------------------------------*)

Goal "x ~: Infinitesimal ==> x : HInfinite | x : HFinite - Infinitesimal";
by (fast_tac (claset() addIs [not_HFinite_HInfinite]) 1);
qed "HInfinite_diff_HFinite_Infinitesimal_disj";

Goal "[| x : HFinite; x ~: Infinitesimal |] ==> inverse x : HFinite";
by (cut_inst_tac [("x","inverse x")] HInfinite_HFinite_disj 1);
by (auto_tac (claset() addSDs [HInfinite_inverse_Infinitesimal], simpset()));
qed "HFinite_inverse";

Goal "x : HFinite - Infinitesimal ==> inverse x : HFinite";
by (blast_tac (claset() addIs [HFinite_inverse]) 1);
qed "HFinite_inverse2";

(* stronger statement possible in fact *)
Goal "x ~: Infinitesimal ==> inverse(x) : HFinite";
by (dtac HInfinite_diff_HFinite_Infinitesimal_disj 1);
by (blast_tac (claset() addIs [HFinite_inverse,
                 HInfinite_inverse_Infinitesimal,
                 Infinitesimal_subset_HFinite RS subsetD]) 1);
qed "Infinitesimal_inverse_HFinite";

Goal "x : HFinite - Infinitesimal ==> inverse x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [Infinitesimal_inverse_HFinite], simpset()));
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
by (asm_full_simp_tac
   (simpset() addsimps [not_Infinitesimal_not_zero, hypreal_mult_inverse]) 1); 
qed "HFinite_not_Infinitesimal_inverse";

Goal "[| x @= y; y :  HFinite - Infinitesimal |] \
\     ==> inverse x @= inverse y";
by (ftac HFinite_diff_Infinitesimal_approx 1);
by (assume_tac 1);
by (ftac not_Infinitesimal_not_zero2 1);
by (forw_inst_tac [("x","x")] not_Infinitesimal_not_zero2 1);
by (REPEAT(dtac HFinite_inverse2 1));
by (dtac approx_mult2 1 THEN assume_tac 1);
by Auto_tac;
by (dres_inst_tac [("c","inverse x")] approx_mult1 1 
    THEN assume_tac 1);
by (auto_tac (claset() addIs [approx_sym],
    simpset() addsimps [hypreal_mult_assoc]));
qed "approx_inverse";

(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
bind_thm ("hypreal_of_real_approx_inverse",
       hypreal_of_real_HFinite_diff_Infinitesimal RSN (2, approx_inverse));

Goal "[| x: HFinite - Infinitesimal; \
\        h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
by (auto_tac (claset() addIs [approx_inverse, approx_sym, 
                              Infinitesimal_add_approx_self], 
              simpset()));
qed "inverse_add_Infinitesimal_approx";

Goal "[| x: HFinite - Infinitesimal; \
\        h : Infinitesimal |] ==> inverse(h + x) @= inverse x";
by (rtac (hypreal_add_commute RS subst) 1);
by (blast_tac (claset() addIs [inverse_add_Infinitesimal_approx]) 1);
qed "inverse_add_Infinitesimal_approx2";

Goal "[| x : HFinite - Infinitesimal; \
\        h : Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"; 
by (rtac approx_trans2 1);
by (auto_tac (claset() addIs [inverse_add_Infinitesimal_approx],
              simpset() addsimps [mem_infmal_iff,
                                  approx_minus_iff RS sym]));
qed "inverse_add_Infinitesimal_approx_Infinitesimal";

Goal "(x : Infinitesimal) = (x*x : Infinitesimal)";
by (auto_tac (claset() addIs [Infinitesimal_mult], simpset()));
by (rtac ccontr 1 THEN ftac Infinitesimal_inverse_HFinite 1);
by (ftac not_Infinitesimal_not_zero 1);
by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult],
    simpset() addsimps [hypreal_mult_assoc]));
qed "Infinitesimal_square_iff";
Addsimps [Infinitesimal_square_iff RS sym];

Goal "(x*x : HFinite) = (x : HFinite)";
by (auto_tac (claset() addIs [HFinite_mult], simpset()));
by (auto_tac (claset() addDs [HInfinite_mult],
    simpset() addsimps [HFinite_HInfinite_iff]));
qed "HFinite_square_iff";
Addsimps [HFinite_square_iff];

Goal "(x*x : HInfinite) = (x : HInfinite)";
by (auto_tac (claset(), simpset() addsimps 
    [HInfinite_HFinite_iff]));
qed "HInfinite_square_iff";
Addsimps [HInfinite_square_iff];

Goal "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z";
by (Step_tac 1);
by (ftac HFinite_inverse 1 THEN assume_tac 1);
by (dtac not_Infinitesimal_not_zero 1);
by (auto_tac (claset() addDs [approx_mult2],
    simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "approx_HFinite_mult_cancel";

Goal "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)";
by (auto_tac (claset() addIs [approx_mult2,
    approx_HFinite_mult_cancel], simpset()));
qed "approx_HFinite_mult_cancel_iff1";

(*------------------------------------------------------------------
                  more about absolute value (hrabs)
 ------------------------------------------------------------------*)

Goal "abs x @= x | abs x @= -x";
by (cut_inst_tac [("x","x")] hrabs_disj 1);
by Auto_tac;
qed "approx_hrabs_disj";

(*------------------------------------------------------------------
                  Theorems about monads
 ------------------------------------------------------------------*)

Goal "monad (abs x) <= monad(x) Un monad(-x)";
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
by Auto_tac;
qed "monad_hrabs_Un_subset";

Goal "e : Infinitesimal ==> monad (x+e) = monad x";
by (fast_tac (claset() addSIs [Infinitesimal_add_approx_self RS approx_sym,
    approx_monad_iff RS iffD1]) 1);
qed "Infinitesimal_monad_eq";

Goalw [monad_def] "(u:monad x) = (-u:monad (-x))";
by Auto_tac;
qed "mem_monad_iff";

Goalw [monad_def] "(x:Infinitesimal) = (x:monad 0)";
by (auto_tac (claset() addIs [approx_sym],
    simpset() addsimps [mem_infmal_iff]));
qed "Infinitesimal_monad_zero_iff";

Goal "(x:monad 0) = (-x:monad 0)";
by (simp_tac (simpset() addsimps [Infinitesimal_monad_zero_iff RS sym]) 1);
qed "monad_zero_minus_iff";

Goal "(x:monad 0) = (abs x:monad 0)";
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
by (auto_tac (claset(), simpset() addsimps [monad_zero_minus_iff RS sym]));
qed "monad_zero_hrabs_iff";

Goalw [monad_def] "x:monad x";
by (Simp_tac 1);
qed "mem_monad_self";
Addsimps [mem_monad_self];

(*------------------------------------------------------------------
         Proof that x @= y ==> abs x @= abs y
 ------------------------------------------------------------------*)
Goal "x @= y ==> {x,y}<=monad x";
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps 
    [approx_monad_iff]) 1);
qed "approx_subset_monad";

Goal "x @= y ==> {x,y}<=monad y";
by (dtac approx_sym 1);
by (fast_tac (claset() addDs [approx_subset_monad]) 1);
qed "approx_subset_monad2";

Goalw [monad_def] "u:monad x ==> x @= u";
by (Fast_tac 1);
qed "mem_monad_approx";

Goalw [monad_def] "x @= u ==> u:monad x";
by (Fast_tac 1);
qed "approx_mem_monad";

Goalw [monad_def] "x @= u ==> x:monad u";
by (blast_tac (claset() addSIs [approx_sym]) 1);
qed "approx_mem_monad2";

Goal "[| x @= y;x:monad 0 |] ==> y:monad 0";
by (dtac mem_monad_approx 1);
by (fast_tac (claset() addIs [approx_mem_monad,approx_trans]) 1);
qed "approx_mem_monad_zero";

Goal "[| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
by (dtac (Infinitesimal_monad_zero_iff RS iffD1) 1); 
by (blast_tac (claset() addIs [approx_mem_monad_zero, 
     monad_zero_hrabs_iff RS iffD1, mem_monad_approx, approx_trans3]) 1);
qed "Infinitesimal_approx_hrabs";

Goal "[| 0 < x;  x ~:Infinitesimal;  e :Infinitesimal |] ==> e < x";
by (rtac ccontr 1);
by (auto_tac (claset()
               addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)] 
               addSDs [hypreal_leI, order_le_imp_less_or_eq],
              simpset()));
qed "less_Infinitesimal_less";

Goal "[| 0 < x;  x ~: Infinitesimal; u: monad x |] ==> 0 < u";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1);
by (dres_inst_tac [("e","-xa")] less_Infinitesimal_less 1);
by Auto_tac;  
qed "Ball_mem_monad_gt_zero";

Goal "[| x < 0; x ~: Infinitesimal; u: monad x |] ==> u < 0";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1);
by (cut_inst_tac [("x","-x"),("e","xa")] less_Infinitesimal_less 1);
by Auto_tac;  
qed "Ball_mem_monad_less_zero";

Goal "[|0 < x; x ~: Infinitesimal; x @= y|] ==> 0 < y";
by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero,
                               approx_subset_monad]) 1);
qed "lemma_approx_gt_zero";

Goal "[|x < 0; x ~: Infinitesimal; x @= y|] ==> y < 0";
by (blast_tac (claset() addDs [Ball_mem_monad_less_zero,
    approx_subset_monad]) 1);
qed "lemma_approx_less_zero";

Goal "[| x @= y; x < 0; x ~: Infinitesimal |] ==> abs x @= abs y";
by (ftac lemma_approx_less_zero 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_minus_eqI2 1));
by Auto_tac;
qed "approx_hrabs1";

Goal "[| x @= y; 0 < x; x ~: Infinitesimal |] ==> abs x @= abs y";
by (ftac lemma_approx_gt_zero 1);
by (REPEAT(assume_tac 1));
by (REPEAT(dtac hrabs_eqI2 1));
by Auto_tac;
qed "approx_hrabs2";

Goal "x @= y ==> abs x @= abs y";
by (res_inst_tac [("Q","x:Infinitesimal")] (excluded_middle RS disjE) 1);
by (res_inst_tac [("x1","x"),("y1","0")] (hypreal_linear RS disjE) 1);
by (auto_tac (claset() addIs [approx_hrabs1,approx_hrabs2,
    Infinitesimal_approx_hrabs], simpset()));
qed "approx_hrabs";

Goal "abs(x) @= 0 ==> x @= 0";
by (cut_inst_tac [("x","x")] hrabs_disj 1);
by (auto_tac (claset() addDs [approx_minus], simpset()));
qed "approx_hrabs_zero_cancel";

Goal "e: Infinitesimal ==> abs x @= abs(x+e)";
by (fast_tac (claset() addIs [approx_hrabs,
       Infinitesimal_add_approx_self]) 1);
qed "approx_hrabs_add_Infinitesimal";

Goal "e: Infinitesimal ==> abs x @= abs(x + -e)";
by (fast_tac (claset() addIs [approx_hrabs,
    Infinitesimal_add_minus_approx_self]) 1);
qed "approx_hrabs_add_minus_Infinitesimal";

Goal "[| e: Infinitesimal; e': Infinitesimal; \
\        abs(x+e) = abs(y+e')|] ==> abs x @= abs y";
by (dres_inst_tac [("x","x")] approx_hrabs_add_Infinitesimal 1);
by (dres_inst_tac [("x","y")] approx_hrabs_add_Infinitesimal 1);
by (auto_tac (claset() addIs [approx_trans2], simpset()));
qed "hrabs_add_Infinitesimal_cancel";

Goal "[| e: Infinitesimal; e': Infinitesimal; \
\        abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y";
by (dres_inst_tac [("x","x")] approx_hrabs_add_minus_Infinitesimal 1);
by (dres_inst_tac [("x","y")] approx_hrabs_add_minus_Infinitesimal 1);
by (auto_tac (claset() addIs [approx_trans2], simpset()));
qed "hrabs_add_minus_Infinitesimal_cancel";

(* interesting slightly counterintuitive theorem: necessary 
   for proving that an open interval is an NS open set 
*)
Goalw [Infinitesimal_def] 
     "[| x < y;  u: Infinitesimal |] \
\     ==> hypreal_of_real x + u < hypreal_of_real y";
by (dtac (hypreal_of_real_less_iff RS iffD2) 1); 
by (dtac (hypreal_less_minus_iff RS iffD1) 1 THEN Step_tac 1);
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
by (auto_tac (claset(),
              simpset() addsimps [hypreal_add_commute, 
                                  hrabs_interval_iff,
                                  SReal_add, SReal_minus]));
qed "Infinitesimal_add_hypreal_of_real_less";

Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
\     ==> abs (hypreal_of_real r + x) < hypreal_of_real y";
by (dres_inst_tac [("x","hypreal_of_real r")] 
    approx_hrabs_add_Infinitesimal 1);
by (dtac (approx_sym RS (bex_Infinitesimal_iff2 RS iffD2)) 1);
by (auto_tac (claset() addSIs [Infinitesimal_add_hypreal_of_real_less],
              simpset() addsimps [hypreal_of_real_hrabs]));
qed "Infinitesimal_add_hrabs_hypreal_of_real_less";

Goal "[| x: Infinitesimal;  abs(hypreal_of_real r) < hypreal_of_real y |] \
\     ==> abs (x + hypreal_of_real r) < hypreal_of_real y";
by (rtac (hypreal_add_commute RS subst) 1);
by (etac Infinitesimal_add_hrabs_hypreal_of_real_less 1);
by (assume_tac 1);
qed "Infinitesimal_add_hrabs_hypreal_of_real_less2";

Goalw [hypreal_le_def]
     "[| u: Infinitesimal; hypreal_of_real x + u <= hypreal_of_real y |] \
\     ==> hypreal_of_real x <= hypreal_of_real y";
by (EVERY1 [rtac notI, rtac contrapos_np, assume_tac]);
by (res_inst_tac [("C","-u")] hypreal_less_add_right_cancel 1);
by (Asm_full_simp_tac 1); 
by (dtac (Infinitesimal_minus_iff RS iffD2) 1); 
by (dtac Infinitesimal_add_hypreal_of_real_less 1); 
by (assume_tac 1); 
by Auto_tac;  
qed "Infinitesimal_add_cancel_hypreal_of_real_le";

Goal "[| u: Infinitesimal;  hypreal_of_real x + u <= hypreal_of_real y |] \
\     ==> x <= y";
by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD1,
               Infinitesimal_add_cancel_hypreal_of_real_le]) 1);
qed "Infinitesimal_add_cancel_real_le";

Goal "[| u: Infinitesimal; v: Infinitesimal; \
\        hypreal_of_real x + u <= hypreal_of_real y + v |] \
\     ==> hypreal_of_real x <= hypreal_of_real y";
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
by Auto_tac;  
by (dres_inst_tac [("u","v-u")] Infinitesimal_add_hypreal_of_real_less 1);
by (auto_tac (claset(), simpset() addsimps [Infinitesimal_diff]));   
qed "hypreal_of_real_le_add_Infininitesimal_cancel";

Goal "[| u: Infinitesimal; v: Infinitesimal; \
\        hypreal_of_real x + u <= hypreal_of_real y + v |] \
\     ==> x <= y";
by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD1,
                          hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
qed "hypreal_of_real_le_add_Infininitesimal_cancel2";

Goal "[| hypreal_of_real x < e; e: Infinitesimal |] ==> hypreal_of_real x <= 0";
by (rtac hypreal_leI 1 THEN Step_tac 1);
by (dtac Infinitesimal_interval 1);
by (dtac (SReal_hypreal_of_real RS SReal_Infinitesimal_zero) 4);
by Auto_tac;
qed "hypreal_of_real_less_Infinitesimal_le_zero";

(*used once, in NSDERIV_inverse*)
Goal "[| h: Infinitesimal; x ~= 0 |] ==> hypreal_of_real x + h ~= 0";
by Auto_tac;  
qed "Infinitesimal_add_not_zero";

Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
by (rtac Infinitesimal_interval2 1); 
by (rtac hypreal_le_square 3); 
by (rtac hypreal_self_le_add_pos 3); 
by Auto_tac;  
qed "Infinitesimal_square_cancel";
Addsimps [Infinitesimal_square_cancel];

Goal "x*x + y*y : HFinite ==> x*x : HFinite";
by (rtac HFinite_bounded 1); 
by (rtac hypreal_self_le_add_pos 2); 
by (rtac (hypreal_le_square) 2); 
by (assume_tac 1); 
qed "HFinite_square_cancel";
Addsimps [HFinite_square_cancel];

Goal "x*x + y*y : Infinitesimal ==> y*y : Infinitesimal";
by (rtac Infinitesimal_square_cancel 1);
by (rtac (hypreal_add_commute RS subst) 1);
by (Simp_tac 1);
qed "Infinitesimal_square_cancel2";
Addsimps [Infinitesimal_square_cancel2];

Goal "x*x + y*y : HFinite ==> y*y : HFinite";
by (rtac HFinite_square_cancel 1);
by (rtac (hypreal_add_commute RS subst) 1);
by (Simp_tac 1);
qed "HFinite_square_cancel2";
Addsimps [HFinite_square_cancel2];

Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal";
by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
    Infinitesimal_interval2, hypreal_le_square]) 1);
qed "Infinitesimal_sum_square_cancel";
Addsimps [Infinitesimal_sum_square_cancel];

Goal "x*x + y*y + z*z : HFinite ==> x*x : HFinite";
by (blast_tac (claset() addIs [hypreal_self_le_add_pos2, HFinite_bounded, 
                               hypreal_le_square,
		               HFinite_number_of]) 1);
qed "HFinite_sum_square_cancel";
Addsimps [HFinite_sum_square_cancel];

Goal "y*y + x*x + z*z : Infinitesimal ==> x*x : Infinitesimal";
by (rtac Infinitesimal_sum_square_cancel 1);
by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
qed "Infinitesimal_sum_square_cancel2";
Addsimps [Infinitesimal_sum_square_cancel2];

Goal "y*y + x*x + z*z : HFinite ==> x*x : HFinite";
by (rtac HFinite_sum_square_cancel 1);
by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
qed "HFinite_sum_square_cancel2";
Addsimps [HFinite_sum_square_cancel2];

Goal "z*z + y*y + x*x : Infinitesimal ==> x*x : Infinitesimal";
by (rtac Infinitesimal_sum_square_cancel 1);
by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
qed "Infinitesimal_sum_square_cancel3";
Addsimps [Infinitesimal_sum_square_cancel3];

Goal "z*z + y*y + x*x : HFinite ==> x*x : HFinite";
by (rtac HFinite_sum_square_cancel 1);
by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
qed "HFinite_sum_square_cancel3";
Addsimps [HFinite_sum_square_cancel3];

Goal "[| y: monad x; 0 < hypreal_of_real e |] \
\     ==> abs (y + -x) < hypreal_of_real e";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (dtac (bex_Infinitesimal_iff RS iffD2) 1);
by (auto_tac (claset() addSDs [InfinitesimalD], simpset()));
qed "monad_hrabs_less";

Goal "x: monad (hypreal_of_real  a) ==> x: HFinite";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (step_tac (claset() addSDs 
       [Infinitesimal_subset_HFinite RS subsetD]) 1);
by (etac (SReal_hypreal_of_real RS (SReal_subset_HFinite 
         RS subsetD) RS HFinite_add) 1);
qed "mem_monad_SReal_HFinite";

(*------------------------------------------------------------------
              Theorems about standard part
 ------------------------------------------------------------------*)

Goalw [st_def] "x: HFinite ==> st x @= x";
by (ftac st_part_Ex 1 THEN Step_tac 1);
by (rtac someI2 1);
by (auto_tac (claset() addIs [approx_sym], simpset()));
qed "st_approx_self";

Goalw [st_def] "x: HFinite ==> st x: Reals";
by (ftac st_part_Ex 1 THEN Step_tac 1);
by (rtac someI2 1);
by (auto_tac (claset() addIs [approx_sym], simpset()));
qed "st_SReal";

Goal "x: HFinite ==> st x: HFinite";
by (etac (st_SReal RS (SReal_subset_HFinite RS subsetD)) 1);
qed "st_HFinite";

Goalw [st_def] "x: Reals ==> st x = x";
by (rtac some_equality 1);
by (fast_tac (claset() addIs [(SReal_subset_HFinite RS subsetD)]) 1);
by (blast_tac (claset() addDs [SReal_approx_iff RS iffD1]) 1);
qed "st_SReal_eq";

(* should be added to simpset *)
Goal "st (hypreal_of_real x) = hypreal_of_real x";
by (rtac (SReal_hypreal_of_real RS st_SReal_eq) 1);
qed "st_hypreal_of_real";

Goal "[| x: HFinite; y: HFinite; st x = st y |] ==> x @= y";
by (auto_tac (claset() addSDs [st_approx_self] 
              addSEs [approx_trans3], simpset()));
qed "st_eq_approx";

Goal "[| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
by (EVERY1 [ftac st_approx_self ,
    forw_inst_tac [("x","y")] st_approx_self,
    dtac st_SReal,dtac st_SReal]);
by (fast_tac (claset() addEs [approx_trans,
    approx_trans2,SReal_approx_iff RS iffD1]) 1);
qed "approx_st_eq";

Goal "[| x: HFinite; y: HFinite|] \
\                  ==> (x @= y) = (st x = st y)";
by (blast_tac (claset() addIs [approx_st_eq,
               st_eq_approx]) 1);
qed "st_eq_approx_iff";

Goal "[| x: Reals; e: Infinitesimal |] ==> st(x + e) = x";
by (forward_tac [st_SReal_eq RS subst] 1);
by (assume_tac 2);
by (forward_tac [SReal_subset_HFinite RS subsetD] 1);
by (forward_tac [Infinitesimal_subset_HFinite RS subsetD] 1);
by (dtac st_SReal_eq 1);
by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs  [HFinite_add],
    simpset() addsimps [Infinitesimal_add_approx_self 
    RS approx_sym]));
qed "st_Infinitesimal_add_SReal";

Goal "[| x: Reals; e: Infinitesimal |] \
\     ==> st(e + x) = x";
by (rtac (hypreal_add_commute RS subst) 1);
by (blast_tac (claset() addSIs [st_Infinitesimal_add_SReal]) 1);
qed "st_Infinitesimal_add_SReal2";

Goal "x: HFinite ==> \
\     EX e: Infinitesimal. x = st(x) + e";
by (blast_tac (claset() addSDs [(st_approx_self RS 
    approx_sym),bex_Infinitesimal_iff2 RS iffD2]) 1);
qed "HFinite_st_Infinitesimal_add";

Goal "[| x: HFinite; y: HFinite |] ==> st (x + y) = st(x) + st(y)";
by (ftac HFinite_st_Infinitesimal_add 1);
by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
by (Step_tac 1);
by (subgoal_tac "st (x + y) = st ((st x + e) + (st y + ea))" 1);
by (dtac sym 2 THEN dtac sym 2);
by (Asm_full_simp_tac 2);
by (asm_simp_tac (simpset() addsimps hypreal_add_ac) 1);
by (REPEAT(dtac st_SReal 1));
by (dtac SReal_add 1 THEN assume_tac 1);
by (dtac Infinitesimal_add 1 THEN assume_tac 1);
by (rtac (hypreal_add_assoc RS subst) 1);
by (blast_tac (claset() addSIs [st_Infinitesimal_add_SReal2]) 1);
qed "st_add";

Goal "st (number_of w) = number_of w";
by (rtac (SReal_number_of RS st_SReal_eq) 1);
qed "st_number_of";
Addsimps [st_number_of];

(*the theorem above for the special cases of zero and one*)
Addsimps
  (map (simplify (simpset()))
   [inst "w" "Pls" st_number_of, inst "w" "Pls BIT True" st_number_of]);

Goal "y: HFinite ==> st(-y) = -st(y)";
by (forward_tac [HFinite_minus_iff RS iffD2] 1);
by (rtac hypreal_add_minus_eq_minus 1);
by (dtac (st_add RS sym) 1 THEN assume_tac 1);
by Auto_tac;  
qed "st_minus";

Goalw [hypreal_diff_def]
     "[| x: HFinite; y: HFinite |] ==> st (x-y) = st(x) - st(y)";
by (forw_inst_tac [("y1","y")] (st_minus RS sym) 1);
by (dres_inst_tac [("x1","y")] (HFinite_minus_iff RS iffD2) 1);
by (asm_simp_tac (simpset() addsimps [st_add]) 1);
qed "st_diff";

(* lemma *)
Goal "[| x: HFinite; y: HFinite; \
\        e: Infinitesimal;       \
\        ea : Infinitesimal |]   \
\      ==> e*y + x*ea + e*ea: Infinitesimal";
by (forw_inst_tac [("x","e"),("y","y")] Infinitesimal_HFinite_mult 1);
by (forw_inst_tac [("x","ea"),("y","x")] Infinitesimal_HFinite_mult 2);
by (dtac Infinitesimal_mult 3);
by (auto_tac (claset() addIs [Infinitesimal_add],
              simpset() addsimps hypreal_add_ac @ hypreal_mult_ac));
qed "lemma_st_mult";

Goal "[| x: HFinite; y: HFinite |] \
\              ==> st (x * y) = st(x) * st(y)";
by (ftac HFinite_st_Infinitesimal_add 1);
by (forw_inst_tac [("x","y")] HFinite_st_Infinitesimal_add 1);
by (Step_tac 1);
by (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))" 1);
by (dtac sym 2 THEN dtac sym 2);
by (Asm_full_simp_tac 2);
by (thin_tac "x = st x + e" 1);
by (thin_tac "y = st y + ea" 1);
by (asm_full_simp_tac (simpset() addsimps 
    [hypreal_add_mult_distrib,hypreal_add_mult_distrib2]) 1);
by (REPEAT(dtac st_SReal 1));
by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
by (rtac st_Infinitesimal_add_SReal 1);
by (blast_tac (claset() addSIs [SReal_mult]) 1);
by (REPEAT(dtac (SReal_subset_HFinite RS subsetD) 1));
by (rtac (hypreal_add_assoc RS subst) 1);
by (blast_tac (claset() addSIs [lemma_st_mult]) 1);
qed "st_mult";

Goal "x: Infinitesimal ==> st x = 0";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1); 
by (rtac (st_number_of RS subst) 1);
by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
              simpset() addsimps [mem_infmal_iff RS sym]));
qed "st_Infinitesimal";

Goal "st(x) ~= 0 ==> x ~: Infinitesimal";
by (fast_tac (claset() addIs [st_Infinitesimal]) 1);
qed "st_not_Infinitesimal";

Goal "[| x: HFinite; st x ~= 0 |] \
\     ==> st(inverse x) = inverse (st x)";
by (res_inst_tac [("c1","st x")] (hypreal_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),
       simpset() addsimps [st_mult RS sym, st_not_Infinitesimal,
                           HFinite_inverse]));
by (stac hypreal_mult_inverse 1); 
by Auto_tac;  
qed "st_inverse";

Goal "[| x: HFinite; y: HFinite; st y ~= 0 |] \
\     ==> st(x/y) = (st x) / (st y)";
by (auto_tac (claset(),
      simpset() addsimps [hypreal_divide_def, st_mult, st_not_Infinitesimal, 
                          HFinite_inverse, st_inverse]));
qed "st_divide";
Addsimps [st_divide];

Goal "x: HFinite ==> st(st(x)) = st(x)";
by (blast_tac (claset() addIs [st_HFinite, st_approx_self,
                               approx_st_eq]) 1);
qed "st_idempotent";
Addsimps [st_idempotent];

(*** lemmas ***)
Goal "[| x: HFinite; y: HFinite; \
\        u: Infinitesimal; st x < st y \
\     |] ==> st x + u < st y";
by (REPEAT(dtac st_SReal 1));
by (auto_tac (claset() addSIs [Infinitesimal_add_hypreal_of_real_less],
              simpset() addsimps [SReal_iff]));
qed "Infinitesimal_add_st_less";

Goalw [hypreal_le_def]
     "[| x: HFinite; y: HFinite; \
\        u: Infinitesimal; st x <= st y + u\
\     |] ==> st x <= st y";
by (auto_tac (claset() addDs [Infinitesimal_add_st_less],
              simpset()));
qed "Infinitesimal_add_st_le_cancel";

Goal "[| x: HFinite; y: HFinite; x <= y |] ==> st(x) <= st(y)";
by (ftac HFinite_st_Infinitesimal_add 1);
by (rotate_tac 1 1);
by (ftac HFinite_st_Infinitesimal_add 1);
by (Step_tac 1);
by (rtac Infinitesimal_add_st_le_cancel 1);
by (res_inst_tac [("x","ea"),("y","e")] 
             Infinitesimal_diff 3);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc RS sym]));
qed "st_le";

Goal "[| 0 <= x;  x: HFinite |] ==> 0 <= st x";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1); 
by (rtac (st_number_of RS subst) 1);
by (rtac st_le 1); 
by Auto_tac; 
qed "st_zero_le";

Goal "[| x <= 0;  x: HFinite |] ==> st x <= 0";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1); 
by (rtac (st_number_of RS subst) 1);
by (rtac st_le 1); 
by Auto_tac; 
qed "st_zero_ge";

Goal "x: HFinite ==> abs(st x) = st(abs x)";
by (case_tac "0 <= x" 1);
by (auto_tac (claset() addSDs [not_hypreal_leE, order_less_imp_le],
              simpset() addsimps [st_zero_le,hrabs_eqI1, hrabs_minus_eqI1,
                                  st_zero_ge,st_minus]));
qed "st_hrabs";

(*--------------------------------------------------------------------
   Alternative definitions for HFinite using Free ultrafilter
 --------------------------------------------------------------------*)

Goal "[| X: Rep_hypreal x; Y: Rep_hypreal x |] \
\     ==> {n. X n = Y n} : FreeUltrafilterNat";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by Auto_tac;
by (Ultra_tac 1);
qed "FreeUltrafilterNat_Rep_hypreal";

Goal "{n. Yb n < Y n} Int {n. -y = Yb n} <= {n. -y < Y n}";
by Auto_tac;
qed "lemma_free1";

Goal "{n. Xa n < Yc n} Int {n. y = Yc n} <= {n. Xa n < y}";
by Auto_tac;
qed "lemma_free2";

Goalw [HFinite_def] 
    "x : HFinite ==> EX X: Rep_hypreal x. \
\    EX u. {n. abs (X n) < u}:  FreeUltrafilterNat";
by (auto_tac (claset(), simpset() addsimps 
    [hrabs_interval_iff]));
by (auto_tac (claset(), simpset() addsimps 
    [hypreal_less_def,SReal_iff,hypreal_minus,
     hypreal_of_real_def]));
by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
by (res_inst_tac [("x","Y")] bexI 1 THEN assume_tac 2);
by (res_inst_tac [("x","y")] exI 1);
by (Ultra_tac 1 THEN arith_tac 1);
qed "HFinite_FreeUltrafilterNat";

Goalw [HFinite_def] 
     "EX X: Rep_hypreal x. \
\      EX u. {n. abs (X n) < u}: FreeUltrafilterNat\
\      ==>  x : HFinite";
by (auto_tac (claset(), simpset() addsimps 
    [hrabs_interval_iff]));
by (res_inst_tac [("x","hypreal_of_real u")] bexI 1);
by (auto_tac (claset() addSIs [exI], simpset() addsimps 
    [hypreal_less_def,SReal_iff,hypreal_minus,
     hypreal_of_real_def]));
by (ALLGOALS(Ultra_tac THEN' arith_tac));
qed "FreeUltrafilterNat_HFinite";

Goal "(x : HFinite) = (EX X: Rep_hypreal x. \
\          EX u. {n. abs (X n) < u}:  FreeUltrafilterNat)";
by (blast_tac (claset() addSIs [HFinite_FreeUltrafilterNat,
               FreeUltrafilterNat_HFinite]) 1);
qed "HFinite_FreeUltrafilterNat_iff";

(*--------------------------------------------------------------------
   Alternative definitions for HInfinite using Free ultrafilter
 --------------------------------------------------------------------*)
Goal "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) <= u}";
by Auto_tac;
qed "lemma_Compl_eq";

Goal "- {n. abs (xa n) < (u::real)} = {n. u <= abs (xa n)}";
by Auto_tac;
qed "lemma_Compl_eq2";

Goal "{n. abs (xa n) <= (u::real)} Int {n. u <= abs (xa n)} \
\         = {n. abs(xa n) = u}";
by Auto_tac;
qed "lemma_Int_eq1";

Goal "{n. abs (xa n) = u} <= {n. abs (xa n) < u + (1::real)}";
by Auto_tac;
qed "lemma_FreeUltrafilterNat_one";

(*-------------------------------------
  Exclude this type of sets from free 
  ultrafilter for Infinite numbers!
 -------------------------------------*)
Goal "[| xa: Rep_hypreal x; \
\                 {n. abs (xa n) = u} : FreeUltrafilterNat \
\              |] ==> x: HFinite";
by (rtac FreeUltrafilterNat_HFinite 1);
by (res_inst_tac [("x","xa")] bexI 1);
by (res_inst_tac [("x","u + 1")] exI 1);
by (Ultra_tac 1 THEN assume_tac 1);
qed "FreeUltrafilterNat_const_Finite";

val [prem] = goal thy "x : HInfinite ==> EX X: Rep_hypreal x. \
\          ALL u. {n. u < abs (X n)}:  FreeUltrafilterNat";
by (cut_facts_tac [(prem RS (HInfinite_HFinite_iff RS iffD1))] 1);
by (cut_inst_tac [("x","x")] Rep_hypreal_nonempty 1);
by (auto_tac (claset(), simpset() delsimps [Rep_hypreal_nonempty] 
    addsimps [HFinite_FreeUltrafilterNat_iff,Bex_def]));
by (REPEAT(dtac spec 1));
by Auto_tac;
by (dres_inst_tac [("x","u")] spec 1 THEN 
    REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);


by (asm_full_simp_tac (simpset() addsimps [lemma_Compl_eq,
    lemma_Compl_eq2,lemma_Int_eq1]) 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_const_Finite],
    simpset() addsimps [(prem RS (HInfinite_HFinite_iff RS iffD1))]));
qed "HInfinite_FreeUltrafilterNat";

(* yet more lemmas! *)
Goal "{n. abs (Xa n) < u} Int {n. X n = Xa n} \
\         <= {n. abs (X n) < (u::real)}";
by Auto_tac;
qed "lemma_Int_HI";

Goal "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}";
by (auto_tac (claset() addIs [real_less_asym], simpset()));
qed "lemma_Int_HIa";

Goal "EX X: Rep_hypreal x. ALL u. \
\              {n. u < abs (X n)}: FreeUltrafilterNat\
\              ==>  x : HInfinite";
by (rtac (HInfinite_HFinite_iff RS iffD2) 1);
by (Step_tac 1 THEN dtac HFinite_FreeUltrafilterNat 1);
by Auto_tac;
by (dres_inst_tac [("x","u")] spec 1);
by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
by (dres_inst_tac [("Y","{n. X n = Xa n}")] FreeUltrafilterNat_Int 1);
by (dtac (lemma_Int_HI RSN (2,FreeUltrafilterNat_subset)) 2);
by (dres_inst_tac [("Y","{n. abs (X n) < u}")] FreeUltrafilterNat_Int 2);
by (auto_tac (claset(), simpset() addsimps [lemma_Int_HIa,
              FreeUltrafilterNat_empty]));
qed "FreeUltrafilterNat_HInfinite";

Goal "(x : HInfinite) = (EX X: Rep_hypreal x. \
\          ALL u. {n. u < abs (X n)}:  FreeUltrafilterNat)";
by (blast_tac (claset() addSIs [HInfinite_FreeUltrafilterNat,
               FreeUltrafilterNat_HInfinite]) 1);
qed "HInfinite_FreeUltrafilterNat_iff";

(*--------------------------------------------------------------------
   Alternative definitions for Infinitesimal using Free ultrafilter
 --------------------------------------------------------------------*)

Goal "{n. - u < Yd n} Int {n. xa n = Yd n} <= {n. -u < xa n}";
by Auto_tac;
qed "lemma_free4";

Goal "{n. Yb n < u} Int {n. xa n = Yb n} <= {n. xa n < u}";
by Auto_tac;
qed "lemma_free5";

Goalw [Infinitesimal_def] 
          "x : Infinitesimal ==> EX X: Rep_hypreal x. \
\          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat";
by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (EVERY[Auto_tac, rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
by (dres_inst_tac [("x","hypreal_of_real u")] bspec 1);
by Auto_tac;
by (auto_tac (claset(), 
              simpset() addsimps [hypreal_less_def, hypreal_minus,
                                  hypreal_of_real_def]));
by (Ultra_tac 1 THEN arith_tac 1);
qed "Infinitesimal_FreeUltrafilterNat";

Goalw [Infinitesimal_def] 
     "EX X: Rep_hypreal x. \
\           ALL u. 0 < u --> {n. abs (X n) < u} : FreeUltrafilterNat \
\     ==> x : Infinitesimal";
by (auto_tac (claset(),
              simpset() addsimps [hrabs_interval_iff,abs_interval_iff]));
by (auto_tac (claset(),
              simpset() addsimps [SReal_iff]));
by (auto_tac (claset() addSIs [exI] 
                               addIs [FreeUltrafilterNat_subset],
    simpset() addsimps [hypreal_less_def, hypreal_minus,hypreal_of_real_def]));
qed "FreeUltrafilterNat_Infinitesimal";

Goal "(x : Infinitesimal) = (EX X: Rep_hypreal x. \
\          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat)";
by (blast_tac (claset() addSIs [Infinitesimal_FreeUltrafilterNat,
               FreeUltrafilterNat_Infinitesimal]) 1);
qed "Infinitesimal_FreeUltrafilterNat_iff";

(*------------------------------------------------------------------------
         Infinitesimals as smaller than 1/n for all n::nat (> 0)
 ------------------------------------------------------------------------*)

Goal "(ALL r. 0 < r --> x < r) = (ALL n. x < inverse(real (Suc n)))";
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc_gt_zero]));
by (blast_tac (claset() addSDs [reals_Archimedean] 
                        addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal";

Goal "(ALL r: Reals. 0 < r --> x < r) = \
\     (ALL n. x < inverse(hypreal_of_nat (Suc n)))";
by (Step_tac 1);
by (dres_inst_tac [("x","inverse (hypreal_of_real(real (Suc n)))")] 
    bspec 1);
by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1); 
by (rtac (real_of_nat_Suc_gt_zero RS real_inverse_gt_0 RS 
          (hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1);
by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps 
       [real_of_nat_Suc_gt_zero, hypreal_of_nat_def]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
              simpset() addsimps [SReal_iff]));
by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps 
         [real_of_nat_Suc_gt_zero, hypreal_of_nat_def])1);
by (blast_tac (claset() addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal2";

Goalw [Infinitesimal_def] 
     "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_nat (Suc n))}";
by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
qed "Infinitesimal_hypreal_of_nat_iff";


(*-------------------------------------------------------------------------
       Proof that omega is an infinite number and 
       hence that epsilon is an infinitesimal number.
 -------------------------------------------------------------------------*)
Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}";
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
qed "Suc_Un_eq";

(*-------------------------------------------
  Prove that any segment is finite and 
  hence cannot belong to FreeUltrafilterNat
 -------------------------------------------*)
Goal "finite {n::nat. n < m}";
by (induct_tac "m" 1);
by (auto_tac (claset(), simpset() addsimps [Suc_Un_eq]));
qed "finite_nat_segment";

Goal "finite {n::nat. real n < real (m::nat)}";
by (auto_tac (claset() addIs [finite_nat_segment], simpset()));
qed "finite_real_of_nat_segment";

Goal "finite {n::nat. real n < u}";
by (cut_inst_tac [("x","u")] reals_Archimedean2 1);
by (Step_tac 1);
by (rtac (finite_real_of_nat_segment RSN (2,finite_subset)) 1);
by (auto_tac (claset() addDs [order_less_trans], simpset()));
qed "finite_real_of_nat_less_real";

Goal "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}";
by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
              simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq";

Goal "finite {n::nat. real n <= u}";
by (auto_tac (claset(), 
              simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set, 
                                  finite_real_of_nat_less_real]));
qed "finite_real_of_nat_le_real";

Goal "finite {n::nat. abs(real n) <= u}";
by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero,
                                  finite_real_of_nat_le_real]) 1);
qed "finite_rabs_real_of_nat_le_real";

Goal "{n. abs(real n) <= u} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
                                finite_rabs_real_of_nat_le_real]) 1);
qed "rabs_real_of_nat_le_real_FreeUltrafilterNat";

Goal "{n. u < real n} : FreeUltrafilterNat";
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
by (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}" 1);
by (Force_tac 2); 
by (asm_full_simp_tac (simpset() addsimps
        [finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1); 
qed "FreeUltrafilterNat_nat_gt_real";

(*--------------------------------------------------------------
 The complement of {n. abs(real n) <= u} = 
 {n. u < abs (real n)} is in FreeUltrafilterNat 
 by property of (free) ultrafilters
 --------------------------------------------------------------*)
Goal "- {n::nat. real n <= u} = {n. u < real n}";
by (auto_tac (claset() addSDs [order_le_less_trans],
              simpset() addsimps [not_real_leE]));
val lemma = result();

(*-----------------------------------------------
       Omega is a member of HInfinite
 -----------------------------------------------*)

Goal "hyprel``{%n::nat. real (Suc n)} : hypreal";
by Auto_tac;
qed "hypreal_omega";

Goal "{n. u < real n} : FreeUltrafilterNat";
by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
              simpset() addsimps [lemma]));
qed "FreeUltrafilterNat_omega";

Goalw [omega_def] "omega: HInfinite";
by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite], 
              simpset()));
by (rtac bexI 1); 
by (rtac lemma_hyprel_refl 2); 
by Auto_tac;  
by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym, 
                                  FreeUltrafilterNat_omega]) 1); 
qed "HInfinite_omega";

(*-----------------------------------------------
       Epsilon is a member of Infinitesimal
 -----------------------------------------------*)

Goal "epsilon : Infinitesimal";
by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,HInfinite_omega],
    simpset() addsimps [hypreal_epsilon_inverse_omega]));
qed "Infinitesimal_epsilon";
Addsimps [Infinitesimal_epsilon];

Goal "epsilon : HFinite";
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
    simpset()));
qed "HFinite_epsilon";
Addsimps [HFinite_epsilon];

Goal "epsilon @= 0";
by (simp_tac (simpset() addsimps [mem_infmal_iff RS sym]) 1);
qed "epsilon_approx_zero";
Addsimps [epsilon_approx_zero];

(*------------------------------------------------------------------------
  Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given 
  that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
 -----------------------------------------------------------------------*)

Goal "0 < u  ==> \
\     (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)";
by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
by (stac pos_real_less_divide_eq 1); 
by (assume_tac 1); 
by (stac pos_real_less_divide_eq 1); 
by (simp_tac (simpset() addsimps [real_mult_commute]) 2); 
by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); 
qed "real_of_nat_less_inverse_iff";

Goal "0 < u ==> finite {n. u < inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1);
by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc, 
                         real_less_diff_eq RS sym]) 1); 
by (rtac finite_real_of_nat_less_real 1);
qed "finite_inverse_real_of_posnat_gt_real";

Goal "{n. u <= inverse(real(Suc n))} = \
\    {n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}";
by (auto_tac (claset() addDs [order_le_imp_less_or_eq],
              simpset() addsimps [order_less_imp_le]));
qed "lemma_real_le_Un_eq2";

Goal "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))";
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
by (stac pos_real_less_divide_eq 1); 
by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); 
by (simp_tac (simpset() addsimps [real_mult_commute]) 1); 
qed "real_of_nat_inverse_le_iff";

Goal "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)";
by (auto_tac (claset(),
      simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero, 
			  real_not_refl2 RS not_sym]));
qed "real_of_nat_inverse_eq_iff";

Goal "finite {n::nat. u = inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1);
by (cut_inst_tac [("x","inverse u - 1")] lemma_finite_omega_set 1);
by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, 
                         real_diff_eq_eq RS sym, eq_commute]) 1); 
qed "lemma_finite_omega_set2";

Goal "0 < u ==> finite {n. u <= inverse(real(Suc n))}";
by (auto_tac (claset(), 
      simpset() addsimps [lemma_real_le_Un_eq2,lemma_finite_omega_set2,
                          finite_inverse_real_of_posnat_gt_real]));
qed "finite_inverse_real_of_posnat_ge_real";

Goal "0 < u ==> \
\      {n. u <= inverse(real(Suc n))} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
                                finite_inverse_real_of_posnat_ge_real]) 1);
qed "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";

(*--------------------------------------------------------------
    The complement of  {n. u <= inverse(real(Suc n))} =
    {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat 
    by property of (free) ultrafilters
 --------------------------------------------------------------*)
Goal "- {n. u <= inverse(real(Suc n))} = \
\     {n. inverse(real(Suc n)) < u}";
by (auto_tac (claset() addSDs [order_le_less_trans],
              simpset() addsimps [not_real_leE]));
val lemma = result();

Goal "0 < u ==> \
\     {n. inverse(real(Suc n)) < u} : FreeUltrafilterNat";
by (cut_inst_tac [("u","u")]  inverse_real_of_posnat_ge_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
    simpset() addsimps [lemma]));
qed "FreeUltrafilterNat_inverse_real_of_posnat";

(*--------------------------------------------------------------
      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
      standard neighbourhoods. Also used for equivalence of
      nonstandard ans standard definitions of pointwise 
      limit (the theorem was previously in REALTOPOS.thy).
 -------------------------------------------------------------*)
(*-----------------------------------------------------
    |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal 
 -----------------------------------------------------*)
Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \ 
\    ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x : Infinitesimal";
by (auto_tac (claset() addSIs [bexI] 
           addDs [FreeUltrafilterNat_inverse_real_of_posnat,
                  FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
           addIs [order_less_trans, FreeUltrafilterNat_subset],
      simpset() addsimps [hypreal_minus, 
                          hypreal_of_real_def,hypreal_add,
                      Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal";

Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \ 
\     ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
by (stac approx_minus_iff 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (etac real_seq_to_hypreal_Infinitesimal 1);
qed "real_seq_to_hypreal_approx";

Goal "ALL n. abs(x + -X n) < inverse(real(Suc n)) \ 
\              ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
        real_seq_to_hypreal_approx]) 1);
qed "real_seq_to_hypreal_approx2";

Goal "ALL n. abs(X n + -Y n) < inverse(real(Suc n)) \ 
\     ==> Abs_hypreal(hyprel``{X}) + \
\         -Abs_hypreal(hyprel``{Y}) : Infinitesimal";
by (auto_tac (claset() addSIs [bexI] 
                  addDs [FreeUltrafilterNat_inverse_real_of_posnat,
                         FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
        addIs [order_less_trans, FreeUltrafilterNat_subset],
     simpset() addsimps 
            [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add, 
             hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal2";