src/HOL/Hyperreal/NatStar.ML
changeset 13810 c3fbfd472365
parent 12486 0ed8bdd883e0
child 14268 5cf13e80be0e
     1.1 --- a/src/HOL/Hyperreal/NatStar.ML	Fri Feb 07 15:36:54 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Fri Feb 07 16:40:23 2003 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4           simpset() addsimps [starsetNat_n_Int RS sym]));
     1.5  qed "InternalNatSets_Int";
     1.6  
     1.7 -Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
     1.8 +Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)";
     1.9  by (Auto_tac);
    1.10  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.11  by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    1.12 @@ -78,7 +78,7 @@
    1.13  by (TRYALL(Ultra_tac));
    1.14  qed "NatStar_Compl";
    1.15  
    1.16 -Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)";
    1.17 +Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)";
    1.18  by (Auto_tac);
    1.19  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.20  by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    1.21 @@ -148,7 +148,7 @@
    1.22  by Auto_tac;
    1.23  qed "starsetNat_starsetNat_n_eq";
    1.24  
    1.25 -Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
    1.26 +Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets";
    1.27  by (auto_tac (claset(),
    1.28           simpset() addsimps [starsetNat_starsetNat_n_eq]));
    1.29  qed "InternalNatSets_starsetNat_n";
    1.30 @@ -195,7 +195,7 @@
    1.31  
    1.32  (* f::nat=>real *)
    1.33  Goalw [starfunNat_def]
    1.34 -      "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    1.35 +      "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    1.36  \      Abs_hypreal(hyprel `` {%n. f (X n)})";
    1.37  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    1.38  by (simp_tac (simpset() addsimps 
    1.39 @@ -205,7 +205,7 @@
    1.40  
    1.41  (* f::nat=>nat *)
    1.42  Goalw [starfunNat2_def]
    1.43 -      "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    1.44 +      "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    1.45  \      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
    1.46  by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
    1.47  by (simp_tac (simpset() addsimps 
    1.48 @@ -216,12 +216,12 @@
    1.49  (*---------------------------------------------
    1.50    multiplication: ( *f ) x ( *g ) = *(f x g)  
    1.51   ---------------------------------------------*)
    1.52 -Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z";
    1.53 +Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z";
    1.54  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.55  by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
    1.56  qed "starfunNat_mult";
    1.57  
    1.58 -Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z";
    1.59 +Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z";
    1.60  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.61  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
    1.62  qed "starfunNat2_mult";
    1.63 @@ -229,17 +229,17 @@
    1.64  (*---------------------------------------
    1.65    addition: ( *f ) + ( *g ) = *(f + g)  
    1.66   ---------------------------------------*)
    1.67 -Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z";
    1.68 +Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z";
    1.69  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.70  by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
    1.71  qed "starfunNat_add";
    1.72  
    1.73 -Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z";
    1.74 +Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z";
    1.75  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.76  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
    1.77  qed "starfunNat2_add";
    1.78  
    1.79 -Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z";
    1.80 +Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z";
    1.81  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.82  by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
    1.83  qed "starfunNat2_minus";
    1.84 @@ -249,18 +249,18 @@
    1.85   ---------------------------------------*)
    1.86  (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
    1.87   
    1.88 -Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
    1.89 +Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))";
    1.90  by (rtac ext 1);
    1.91  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    1.92  by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
    1.93  qed "starfunNatNat2_o";
    1.94  
    1.95 -Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
    1.96 +Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))";
    1.97  by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
    1.98  qed "starfunNatNat2_o2";
    1.99  
   1.100  (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
   1.101 -Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
   1.102 +Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))";
   1.103  by (rtac ext 1);
   1.104  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.105  by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
   1.106 @@ -268,38 +268,38 @@
   1.107  
   1.108  (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
   1.109  
   1.110 -Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; 
   1.111 +Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; 
   1.112  by (rtac ext 1);
   1.113  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.114  by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
   1.115  qed "starfun_stafunNat_o";
   1.116  
   1.117 -Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; 
   1.118 +Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; 
   1.119  by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
   1.120  qed "starfun_stafunNat_o2";
   1.121  
   1.122  (*--------------------------------------
   1.123    NS extension of constant function
   1.124   --------------------------------------*)
   1.125 -Goal "(*fNat* (%x. k)) z = hypreal_of_real k";
   1.126 +Goal "( *fNat* (%x. k)) z = hypreal_of_real k";
   1.127  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.128  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
   1.129  qed "starfunNat_const_fun";
   1.130  Addsimps [starfunNat_const_fun];
   1.131  
   1.132 -Goal "(*fNat2* (%x. k)) z = hypnat_of_nat  k";
   1.133 +Goal "( *fNat2* (%x. k)) z = hypnat_of_nat  k";
   1.134  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.135  by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
   1.136  qed "starfunNat2_const_fun";
   1.137  
   1.138  Addsimps [starfunNat2_const_fun];
   1.139  
   1.140 -Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
   1.141 +Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x";
   1.142  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.143  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
   1.144  qed "starfunNat_minus";
   1.145  
   1.146 -Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
   1.147 +Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x";
   1.148  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.149  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
   1.150  qed "starfunNat_inverse";
   1.151 @@ -310,20 +310,20 @@
   1.152     for all natural arguments (c.f. Hoskins pg. 107- SEQ)
   1.153   -------------------------------------------------------*)
   1.154  
   1.155 -Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
   1.156 +Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
   1.157  by (auto_tac (claset(),
   1.158        simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
   1.159  qed "starfunNat_eq";
   1.160  
   1.161  Addsimps [starfunNat_eq];
   1.162  
   1.163 -Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
   1.164 +Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
   1.165  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
   1.166  qed "starfunNat2_eq";
   1.167  
   1.168  Addsimps [starfunNat2_eq];
   1.169  
   1.170 -Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
   1.171 +Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
   1.172  by (Auto_tac);
   1.173  qed "starfunNat_approx";
   1.174  
   1.175 @@ -333,7 +333,7 @@
   1.176      --- used for limit comparison of sequences
   1.177   ----------------------------------------------------------------*)
   1.178  Goal "ALL n. N <= n --> f n <= g n \
   1.179 -\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
   1.180 +\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n";
   1.181  by (Step_tac 1);
   1.182  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.183  by (auto_tac (claset(),
   1.184 @@ -345,7 +345,7 @@
   1.185  
   1.186  (*****----- and another -----*****) 
   1.187  Goal "ALL n. N <= n --> f n < g n \
   1.188 -\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
   1.189 +\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n";
   1.190  by (Step_tac 1);
   1.191  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.192  by (auto_tac (claset(),
   1.193 @@ -358,7 +358,7 @@
   1.194  (*----------------------------------------------------------------
   1.195              NS extension when we displace argument by one
   1.196   ---------------------------------------------------------------*)
   1.197 -Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))";
   1.198 +Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))";
   1.199  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.200  by (auto_tac (claset(),
   1.201           simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
   1.202 @@ -367,7 +367,7 @@
   1.203  (*----------------------------------------------------------------
   1.204                   NS extension with rabs    
   1.205   ---------------------------------------------------------------*)
   1.206 -Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
   1.207 +Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)";
   1.208  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.209  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
   1.210  qed "starfunNat_rabs";
   1.211 @@ -375,19 +375,19 @@
   1.212  (*----------------------------------------------------------------
   1.213         The hyperpow function as a NS extension of realpow
   1.214   ----------------------------------------------------------------*)
   1.215 -Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
   1.216 +Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
   1.217  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.218  by (auto_tac (claset(),
   1.219           simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
   1.220  qed "starfunNat_pow";
   1.221  
   1.222 -Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
   1.223 +Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
   1.224  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.225  by (auto_tac (claset(),
   1.226           simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
   1.227  qed "starfunNat_pow2";
   1.228  
   1.229 -Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   1.230 +Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   1.231  by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   1.232  by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
   1.233  qed "starfun_pow";
   1.234 @@ -395,14 +395,14 @@
   1.235  (*----------------------------------------------------- 
   1.236     hypreal_of_hypnat as NS extension of real (from "nat")! 
   1.237  -------------------------------------------------------*)
   1.238 -Goal "(*fNat* real) = hypreal_of_hypnat";
   1.239 +Goal "( *fNat* real) = hypreal_of_hypnat";
   1.240  by (rtac ext 1);
   1.241  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.242  by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
   1.243  qed "starfunNat_real_of_nat";
   1.244  
   1.245  Goal "N : HNatInfinite \
   1.246 -\  ==> (*fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
   1.247 +\  ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
   1.248  by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   1.249  by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   1.250  by (auto_tac (claset(), 
   1.251 @@ -419,7 +419,7 @@
   1.252  qed "starfunNat_n_congruent";
   1.253  
   1.254  Goalw [starfunNat_n_def]
   1.255 -     "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
   1.256 +     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
   1.257  \     Abs_hypreal(hyprel `` {%n. f n (X n)})";
   1.258  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   1.259  by Auto_tac;
   1.260 @@ -429,7 +429,7 @@
   1.261  (*-------------------------------------------------
   1.262    multiplication: ( *fn ) x ( *gn ) = *(fn x gn)  
   1.263   -------------------------------------------------*)
   1.264 -Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z";
   1.265 +Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z";
   1.266  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.267  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
   1.268  qed "starfunNat_n_mult";
   1.269 @@ -437,7 +437,7 @@
   1.270  (*-----------------------------------------------
   1.271    addition: ( *fn ) + ( *gn ) = *(fn + gn)  
   1.272   -----------------------------------------------*)
   1.273 -Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z";
   1.274 +Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z";
   1.275  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.276  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
   1.277  qed "starfunNat_n_add";
   1.278 @@ -445,7 +445,7 @@
   1.279  (*-------------------------------------------------
   1.280    subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)  
   1.281   -------------------------------------------------*)
   1.282 -Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z";
   1.283 +Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z";
   1.284  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.285  by (auto_tac (claset(), 
   1.286            simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
   1.287 @@ -455,7 +455,7 @@
   1.288    composition: ( *fn ) o ( *gn ) = *(fn o gn)  
   1.289   -------------------------------------------------*)
   1.290   
   1.291 -Goal "(*fNatn* (%i x. k)) z = hypreal_of_real  k";
   1.292 +Goal "( *fNatn* (%i x. k)) z = hypreal_of_real  k";
   1.293  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.294  by (auto_tac (claset(), 
   1.295         simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
   1.296 @@ -463,17 +463,17 @@
   1.297  
   1.298  Addsimps [starfunNat_n_const_fun];
   1.299  
   1.300 -Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
   1.301 +Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x";
   1.302  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.303  by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
   1.304  qed "starfunNat_n_minus";
   1.305  
   1.306 -Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
   1.307 +Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
   1.308  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
   1.309  qed "starfunNat_n_eq";
   1.310  Addsimps [starfunNat_n_eq];
   1.311  
   1.312 -Goal "((*fNat* f) = (*fNat* g)) = (f = g)";
   1.313 +Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)";
   1.314  by Auto_tac;
   1.315  by (rtac ext 1 THEN rtac ccontr 1);
   1.316  by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);