src/HOL/Hyperreal/NatStar.ML

 \     ==> (X Int Y) : InternalNatSets";
 by (auto_tac (claset(),
          simpset() addsimps [starsetNat_n_Int RS sym]));
 qed "InternalNatSets_Int";
 
-Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
+Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)";
 by (Auto_tac);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
 by (REPEAT(Step_tac 1) THEN Auto_tac);
 by (TRYALL(Ultra_tac));
 qed "NatStar_Compl";
 
-Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)";
+Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)";
 by (Auto_tac);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
 by (REPEAT(Step_tac 1) THEN Auto_tac);
 by (TRYALL(Ultra_tac));

 
 Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)";
 by Auto_tac;
 qed "starsetNat_starsetNat_n_eq";
 
-Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
+Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets";
 by (auto_tac (claset(),
          simpset() addsimps [starsetNat_starsetNat_n_eq]));
 qed "InternalNatSets_starsetNat_n";
 Addsimps [InternalNatSets_starsetNat_n];
 

 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_congruent";
 
 (* f::nat=>real *)
 Goalw [starfunNat_def]
-      "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+      "( *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})) = \
+      "( *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,
     [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
 qed "starfunNat2";
 
 (*---------------------------------------------
   multiplication: ( *f ) x ( *g ) = *(f x g)  
  ---------------------------------------------*)
-Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z";
+Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
 qed "starfunNat_mult";
 
-Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z";
+Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
 qed "starfunNat2_mult";
 
 (*---------------------------------------
   addition: ( *f ) + ( *g ) = *(f + g)  
  ---------------------------------------*)
-Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z";
+Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
 qed "starfunNat_add";
 
-Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z";
+Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
 qed "starfunNat2_add";
 
-Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z";
+Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
 qed "starfunNat2_minus";
 
 (*--------------------------------------
   composition: ( *f ) o ( *g ) = *(f o g)  
  ---------------------------------------*)
 (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
  
-Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
+Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
 qed "starfunNatNat2_o";
 
-Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
+Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))";
 by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
 qed "starfunNatNat2_o2";
 
 (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
-Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
+Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
 qed "starfunNat2_o";
 
 (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
 
-Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; 
+Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; 
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
 qed "starfun_stafunNat_o";
 
-Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; 
+Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; 
 by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
 qed "starfun_stafunNat_o2";
 
 (*--------------------------------------
   NS extension of constant function
  --------------------------------------*)
-Goal "(*fNat* (%x. k)) z = hypreal_of_real k";
+Goal "( *fNat* (%x. k)) z = hypreal_of_real k";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
 qed "starfunNat_const_fun";
 Addsimps [starfunNat_const_fun];
 
-Goal "(*fNat2* (%x. k)) z = hypnat_of_nat  k";
+Goal "( *fNat2* (%x. k)) z = hypnat_of_nat  k";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
 qed "starfunNat2_const_fun";
 
 Addsimps [starfunNat2_const_fun];
 
-Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
+Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
 qed "starfunNat_minus";
 
-Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
+Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
 qed "starfunNat_inverse";
 
 (*--------------------------------------------------------
    extented function has same solution as its standard
    version for natural arguments. i.e they are the same
    for all natural arguments (c.f. Hoskins pg. 107- SEQ)
  -------------------------------------------------------*)
 
-Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
+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)";
+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)";
+Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
 by (Auto_tac);
 qed "starfunNat_approx";
 
 
 (*-----------------------------------------------------------------
     Example of transfer of a property from reals to hyperreals
     --- used for limit comparison of sequences
  ----------------------------------------------------------------*)
 Goal "ALL n. N <= n --> f n <= g n \
-\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
+\         ==> 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,
                              hypreal_less, hypnat_le,hypnat_less]));

 by Auto_tac;
 qed "starfun_le_mono";
 
 (*****----- and another -----*****) 
 Goal "ALL n. N <= n --> f n < g n \
-\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
+\         ==> 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,
                              hypreal_less, hypnat_le,hypnat_less]));

 qed "starfun_less_mono";
 
 (*----------------------------------------------------------------
             NS extension when we displace argument by one
  ---------------------------------------------------------------*)
-Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))";
+Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
 by (auto_tac (claset(),
          simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
 qed "starfunNat_shift_one";
 
 (*----------------------------------------------------------------
                  NS extension with rabs    
  ---------------------------------------------------------------*)
-Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
+Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)";
 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
 qed "starfunNat_rabs";
 
 (*----------------------------------------------------------------
        The hyperpow function as a NS extension of realpow
  ----------------------------------------------------------------*)
-Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
+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";
+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";
+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 (from "nat")! 
 -------------------------------------------------------*)
-Goal "(*fNat* real) = hypreal_of_hypnat";
+Goal "( *fNat* real) = hypreal_of_hypnat";
 by (rtac ext 1);
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
 qed "starfunNat_real_of_nat";
 
 Goal "N : HNatInfinite \
-\  ==> (*fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
+\  ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
 by (auto_tac (claset(), 
        simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse]));
 qed "starfunNat_inverse_real_of_nat_eq";

 by Safe_tac;
 by (ALLGOALS(Fuf_tac));
 qed "starfunNat_n_congruent";
 
 Goalw [starfunNat_n_def]
-     "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
+     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
 \     Abs_hypreal(hyprel `` {%n. f n (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 by Auto_tac;
 by (Ultra_tac 1);
 qed "starfunNat_n";
 
 (*-------------------------------------------------
   multiplication: ( *fn ) x ( *gn ) = *(fn x gn)  
  -------------------------------------------------*)
-Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z";
+Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
 qed "starfunNat_n_mult";
 
 (*-----------------------------------------------
   addition: ( *fn ) + ( *gn ) = *(fn + gn)  
  -----------------------------------------------*)
-Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z";
+Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
 qed "starfunNat_n_add";
 
 (*-------------------------------------------------
   subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)  
  -------------------------------------------------*)
-Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z";
+Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), 
           simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
 qed "starfunNat_n_add_minus";
 
 (*--------------------------------------------------
   composition: ( *fn ) o ( *gn ) = *(fn o gn)  
  -------------------------------------------------*)
  
-Goal "(*fNatn* (%i x. k)) z = hypreal_of_real  k";
+Goal "( *fNatn* (%i x. k)) z = hypreal_of_real  k";
 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), 
        simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
 qed "starfunNat_n_const_fun";
 
 Addsimps [starfunNat_n_const_fun];
 
-Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
+Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x";
 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
 qed "starfunNat_n_minus";
 
-Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
+Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
 qed "starfunNat_n_eq";
 Addsimps [starfunNat_n_eq];
 
-Goal "((*fNat* f) = (*fNat* g)) = (f = g)";
+Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)";
 by Auto_tac;
 by (rtac ext 1 THEN rtac ccontr 1);
 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
 qed "starfun_eq_iff";