replacing 0hr by (0::hypreal)
authorpaulson
Wed Jun 07 17:14:58 2000 +0200 (2000-06-07)
changeset 9055f020e00c6304
parent 9054 0e48e7d4d4f9
child 9056 8f78b2aea39e
replacing 0hr by (0::hypreal)
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/HyperDef.thy
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 17:14:19 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 17:14:58 2000 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4   ------------------------------------------------------------------------*)
     1.5  
     1.6  (*** based on James' proof that the set of naturals is not finite ***)
     1.7 -Goal "finite (A::nat set) --> (? n. !m. Suc (n + m) ~: A)";
     1.8 +Goal "finite (A::nat set) --> (EX n. ALL m. Suc (n + m) ~: A)";
     1.9  by (rtac impI 1);
    1.10  by (eres_inst_tac [("F","A")] finite_induct 1);
    1.11  by (Blast_tac 1 THEN etac exE 1);
    1.12 @@ -22,7 +22,7 @@
    1.13  				  less_add_Suc2 RS less_not_refl2]));
    1.14  qed_spec_mp "finite_exhausts";
    1.15  
    1.16 -Goal "finite (A :: nat set) --> (? n. n ~:A)";
    1.17 +Goal "finite (A :: nat set) --> (EX n. n ~:A)";
    1.18  by (rtac impI 1 THEN dtac finite_exhausts 1);
    1.19  by (Blast_tac 1);
    1.20  qed_spec_mp "finite_not_covers";
    1.21 @@ -311,13 +311,13 @@
    1.22  by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
    1.23  qed "inj_hypreal_minus";
    1.24  
    1.25 -Goalw [hypreal_zero_def] "-0hr = 0hr";
    1.26 +Goalw [hypreal_zero_def] "-0 = (0::hypreal)";
    1.27  by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
    1.28  qed "hypreal_minus_zero";
    1.29  
    1.30  Addsimps [hypreal_minus_zero];
    1.31  
    1.32 -Goal "(-x = 0hr) = (x = 0hr)"; 
    1.33 +Goal "(-x = 0) = (x = (0::hypreal))"; 
    1.34  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.35  by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
    1.36      hypreal_minus] @ real_add_ac));
    1.37 @@ -342,7 +342,7 @@
    1.38     [hyprel_in_hypreal RS Abs_hypreal_inverse,hypreal_hrinv_ize UN_equiv_class]) 1);
    1.39  qed "hypreal_hrinv";
    1.40  
    1.41 -Goal "z ~= 0hr ==> hrinv (hrinv z) = z";
    1.42 +Goal "z ~= 0 ==> hrinv (hrinv z) = z";
    1.43  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
    1.44  by (rotate_tac 1 1);
    1.45  by (asm_full_simp_tac (simpset() addsimps 
    1.46 @@ -402,24 +402,24 @@
    1.47  val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
    1.48                        hypreal_add_left_commute];
    1.49  
    1.50 -Goalw [hypreal_zero_def] "0hr + z = z";
    1.51 +Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
    1.52  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
    1.53  by (asm_full_simp_tac (simpset() addsimps 
    1.54      [hypreal_add]) 1);
    1.55  qed "hypreal_add_zero_left";
    1.56  
    1.57 -Goal "z + 0hr = z";
    1.58 +Goal "z + (0::hypreal) = z";
    1.59  by (simp_tac (simpset() addsimps 
    1.60      [hypreal_add_zero_left,hypreal_add_commute]) 1);
    1.61  qed "hypreal_add_zero_right";
    1.62  
    1.63 -Goalw [hypreal_zero_def] "z + -z = 0hr";
    1.64 +Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
    1.65  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
    1.66  by (asm_full_simp_tac (simpset() addsimps [hypreal_minus,
    1.67          hypreal_add]) 1);
    1.68  qed "hypreal_add_minus";
    1.69  
    1.70 -Goal "-z + z = 0hr";
    1.71 +Goal "-z + z = (0::hypreal)";
    1.72  by (simp_tac (simpset() addsimps 
    1.73      [hypreal_add_commute,hypreal_add_minus]) 1);
    1.74  qed "hypreal_add_minus_left";
    1.75 @@ -427,31 +427,31 @@
    1.76  Addsimps [hypreal_add_minus,hypreal_add_minus_left,
    1.77            hypreal_add_zero_left,hypreal_add_zero_right];
    1.78  
    1.79 -Goal "? y. (x::hypreal) + y = 0hr";
    1.80 +Goal "EX y. (x::hypreal) + y = 0";
    1.81  by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
    1.82  qed "hypreal_minus_ex";
    1.83  
    1.84 -Goal "?! y. (x::hypreal) + y = 0hr";
    1.85 +Goal "EX! y. (x::hypreal) + y = 0";
    1.86  by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
    1.87  by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
    1.88  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
    1.89  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
    1.90  qed "hypreal_minus_ex1";
    1.91  
    1.92 -Goal "?! y. y + (x::hypreal) = 0hr";
    1.93 +Goal "EX! y. y + (x::hypreal) = 0";
    1.94  by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
    1.95  by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
    1.96  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
    1.97  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
    1.98  qed "hypreal_minus_left_ex1";
    1.99  
   1.100 -Goal "x + y = 0hr ==> x = -y";
   1.101 +Goal "x + y = (0::hypreal) ==> x = -y";
   1.102  by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   1.103  by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   1.104  by (Blast_tac 1);
   1.105  qed "hypreal_add_minus_eq_minus";
   1.106  
   1.107 -Goal "? y::hypreal. x = -y";
   1.108 +Goal "EX y::hypreal. x = -y";
   1.109  by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   1.110  by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   1.111  by (Fast_tac 1);
   1.112 @@ -572,12 +572,12 @@
   1.113      hypreal_mult_1]) 1);
   1.114  qed "hypreal_mult_1_right";
   1.115  
   1.116 -Goalw [hypreal_zero_def] "0hr * z = 0hr";
   1.117 +Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
   1.118  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   1.119  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult,real_mult_0]) 1);
   1.120  qed "hypreal_mult_0";
   1.121  
   1.122 -Goal "z * 0hr = 0hr";
   1.123 +Goal "z * 0 = (0::hypreal)";
   1.124  by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   1.125      hypreal_mult_0]) 1);
   1.126  qed "hypreal_mult_0_right";
   1.127 @@ -600,16 +600,11 @@
   1.128                                             @ real_mult_ac @ real_add_ac));
   1.129  qed "hypreal_minus_mult_eq2";
   1.130  
   1.131 -Goal "-x*-y = x*(y::hypreal)";
   1.132 -by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   1.133 -				       hypreal_minus_mult_eq1 RS sym]) 1);
   1.134 -qed "hypreal_minus_mult_cancel";
   1.135 -
   1.136 -Addsimps [hypreal_minus_mult_cancel];
   1.137 +(*Pull negations out*)
   1.138 +Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
   1.139  
   1.140  Goal "-x*y = (x::hypreal)*-y";
   1.141 -by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
   1.142 -				       hypreal_minus_mult_eq1 RS sym]) 1);
   1.143 +by Auto_tac;
   1.144  qed "hypreal_minus_mult_commute";
   1.145  
   1.146  
   1.147 @@ -642,13 +637,13 @@
   1.148  Addsimps hypreal_mult_simps;
   1.149  
   1.150  (*** one and zero are distinct ***)
   1.151 -Goalw [hypreal_zero_def,hypreal_one_def] "0hr ~= 1hr";
   1.152 +Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
   1.153  by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   1.154  qed "hypreal_zero_not_eq_one";
   1.155  
   1.156  (*** existence of inverse ***)
   1.157  Goalw [hypreal_one_def,hypreal_zero_def] 
   1.158 -          "x ~= 0hr ==> x*hrinv(x) = 1hr";
   1.159 +          "x ~= 0 ==> x*hrinv(x) = 1hr";
   1.160  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.161  by (rotate_tac 1 1);
   1.162  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   1.163 @@ -658,41 +653,41 @@
   1.164      FreeUltrafilterNat_subset]) 1);
   1.165  qed "hypreal_mult_hrinv";
   1.166  
   1.167 -Goal "x ~= 0hr ==> hrinv(x)*x = 1hr";
   1.168 +Goal "x ~= 0 ==> hrinv(x)*x = 1hr";
   1.169  by (asm_simp_tac (simpset() addsimps [hypreal_mult_hrinv,
   1.170 -    hypreal_mult_commute]) 1);
   1.171 +				      hypreal_mult_commute]) 1);
   1.172  qed "hypreal_mult_hrinv_left";
   1.173  
   1.174 -Goal "x ~= 0hr ==> ? y. (x::hypreal) * y = 1hr";
   1.175 +Goal "x ~= 0 ==> EX y. x * y = 1hr";
   1.176  by (fast_tac (claset() addDs [hypreal_mult_hrinv]) 1);
   1.177  qed "hypreal_hrinv_ex";
   1.178  
   1.179 -Goal "x ~= 0hr ==> ? y. y * (x::hypreal) = 1hr";
   1.180 +Goal "x ~= 0 ==> EX y. y * x = 1hr";
   1.181  by (fast_tac (claset() addDs [hypreal_mult_hrinv_left]) 1);
   1.182  qed "hypreal_hrinv_left_ex";
   1.183  
   1.184 -Goal "x ~= 0hr ==> ?! y. (x::hypreal) * y = 1hr";
   1.185 +Goal "x ~= 0 ==> EX! y. x * y = 1hr";
   1.186  by (auto_tac (claset() addIs [hypreal_mult_hrinv],simpset()));
   1.187  by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
   1.188  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   1.189  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   1.190  qed "hypreal_hrinv_ex1";
   1.191  
   1.192 -Goal "x ~= 0hr ==> ?! y. y * (x::hypreal) = 1hr";
   1.193 +Goal "x ~= 0 ==> EX! y. y * x = 1hr";
   1.194  by (auto_tac (claset() addIs [hypreal_mult_hrinv_left],simpset()));
   1.195  by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
   1.196  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   1.197  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   1.198  qed "hypreal_hrinv_left_ex1";
   1.199  
   1.200 -Goal "[| y~= 0hr; x * y = 1hr |]  ==> x = hrinv y";
   1.201 +Goal "[| y~= 0; x * y = 1hr |]  ==> x = hrinv y";
   1.202  by (forw_inst_tac [("x","y")] hypreal_mult_hrinv_left 1);
   1.203  by (res_inst_tac [("x1","y")] (hypreal_hrinv_left_ex1 RS ex1E) 1);
   1.204  by (assume_tac 1);
   1.205  by (Blast_tac 1);
   1.206  qed "hypreal_mult_inv_hrinv";
   1.207  
   1.208 -Goal "x ~= 0hr ==> ? y. x = hrinv y";
   1.209 +Goal "x ~= 0 ==> EX y. x = hrinv y";
   1.210  by (forw_inst_tac [("x","x")] hypreal_hrinv_left_ex 1);
   1.211  by (etac exE 1 THEN 
   1.212      forw_inst_tac [("x","y")] hypreal_mult_inv_hrinv 1);
   1.213 @@ -700,19 +695,19 @@
   1.214  by Auto_tac;
   1.215  qed "hypreal_as_inverse_ex";
   1.216  
   1.217 -Goal "(c::hypreal) ~= 0hr ==> (c*a=c*b) = (a=b)";
   1.218 +Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
   1.219  by Auto_tac;
   1.220  by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   1.221  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   1.222  qed "hypreal_mult_left_cancel";
   1.223      
   1.224 -Goal "(c::hypreal) ~= 0hr ==> (a*c=b*c) = (a=b)";
   1.225 +Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)";
   1.226  by (Step_tac 1);
   1.227  by (dres_inst_tac [("f","%x. x*hrinv c")] arg_cong 1);
   1.228  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_hrinv] @ hypreal_mult_ac)  1);
   1.229  qed "hypreal_mult_right_cancel";
   1.230  
   1.231 -Goalw [hypreal_zero_def] "x ~= 0hr ==> hrinv(x) ~= 0hr";
   1.232 +Goalw [hypreal_zero_def] "x ~= 0 ==> hrinv(x) ~= 0";
   1.233  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.234  by (rotate_tac 1 1);
   1.235  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
   1.236 @@ -724,7 +719,7 @@
   1.237  
   1.238  Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
   1.239  
   1.240 -Goal "[| x ~= 0hr; y ~= 0hr |] ==> x * y ~= 0hr";
   1.241 +Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";
   1.242  by (Step_tac 1);
   1.243  by (dres_inst_tac [("f","%z. hrinv x*z")] arg_cong 1);
   1.244  by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   1.245 @@ -732,11 +727,11 @@
   1.246  
   1.247  bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   1.248  
   1.249 -Goal "x ~= 0hr ==> x * x ~= 0hr";
   1.250 +Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
   1.251  by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   1.252  qed "hypreal_mult_self_not_zero";
   1.253  
   1.254 -Goal "[| x ~= 0hr; y ~= 0hr |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   1.255 +Goal "[| x ~= 0; y ~= 0 |] ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   1.256  by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   1.257  by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
   1.258      hypreal_mult_not_0]));
   1.259 @@ -745,12 +740,13 @@
   1.260  by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
   1.261  qed "hrinv_mult_eq";
   1.262  
   1.263 -Goal "x ~= 0hr ==> hrinv(-x) = -hrinv(x)";
   1.264 -by (res_inst_tac [("c1","-x")] (hypreal_mult_right_cancel RS iffD1) 1);
   1.265 +Goal "x ~= 0 ==> hrinv(-x) = -hrinv(x)";
   1.266 +by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
   1.267 +by (stac hypreal_mult_hrinv_left 2);
   1.268  by Auto_tac;
   1.269  qed "hypreal_minus_hrinv";
   1.270  
   1.271 -Goal "[| x ~= 0hr; y ~= 0hr |] \
   1.272 +Goal "[| x ~= 0; y ~= 0 |] \
   1.273  \     ==> hrinv(x*y) = hrinv(x)*hrinv(y)";
   1.274  by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   1.275  by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   1.276 @@ -844,7 +840,7 @@
   1.277  (*** sum order ***)
   1.278  
   1.279  Goalw [hypreal_zero_def] 
   1.280 -      "[| 0hr < x; 0hr < y |] ==> 0hr < x + y";
   1.281 +      "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
   1.282  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.283  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.284  by (auto_tac (claset(),simpset() addsimps
   1.285 @@ -857,7 +853,7 @@
   1.286  (*** mult order ***)
   1.287  
   1.288  Goalw [hypreal_zero_def] 
   1.289 -          "[| 0hr < x; 0hr < y |] ==> 0hr < x * y";
   1.290 +          "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
   1.291  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.292  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.293  by (auto_tac (claset() addSIs [exI],simpset() addsimps
   1.294 @@ -870,13 +866,13 @@
   1.295                           Trichotomy of the hyperreals
   1.296    --------------------------------------------------------------------------------*)
   1.297  
   1.298 -Goalw [hyprel_def] "? x. x: hyprel ^^ {%n. #0}";
   1.299 +Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}";
   1.300  by (res_inst_tac [("x","%n. #0")] exI 1);
   1.301  by (Step_tac 1);
   1.302  by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
   1.303  qed "lemma_hyprel_0r_mem";
   1.304  
   1.305 -Goalw [hypreal_zero_def]"0hr <  x | x = 0hr | x < 0hr";
   1.306 +Goalw [hypreal_zero_def]"0 <  x | x = 0 | x < (0::hypreal)";
   1.307  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.308  by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   1.309  by (cut_facts_tac [lemma_hyprel_0r_mem] 1 THEN etac exE 1);
   1.310 @@ -891,9 +887,9 @@
   1.311  by (auto_tac (claset() addIs [real_linear_less2],simpset()));
   1.312  qed "hypreal_trichotomy";
   1.313  
   1.314 -val prems = Goal "[| 0hr < x ==> P; \
   1.315 -\                 x = 0hr ==> P; \
   1.316 -\                 x < 0hr ==> P |] ==> P";
   1.317 +val prems = Goal "[| (0::hypreal) < x ==> P; \
   1.318 +\                 x = 0 ==> P; \
   1.319 +\                 x < 0 ==> P |] ==> P";
   1.320  by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
   1.321  by (REPEAT (eresolve_tac (disjE::prems) 1));
   1.322  qed "hypreal_trichotomyE";
   1.323 @@ -915,14 +911,14 @@
   1.324      simpset() addsimps [hypreal_add_commute]));
   1.325  qed "hypreal_add_less_mono2";
   1.326  
   1.327 -Goal "((x::hypreal) < y) = (0hr < y + -x)";
   1.328 +Goal "((x::hypreal) < y) = (0 < y + -x)";
   1.329  by (Step_tac 1);
   1.330  by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
   1.331  by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
   1.332  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.333  qed "hypreal_less_minus_iff"; 
   1.334  
   1.335 -Goal "((x::hypreal) < y) = (x + -y< 0hr)";
   1.336 +Goal "((x::hypreal) < y) = (x + -y< 0)";
   1.337  by (Step_tac 1);
   1.338  by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
   1.339  by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
   1.340 @@ -933,19 +929,19 @@
   1.341  by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.342  by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.343  by (dtac hypreal_add_order 1 THEN assume_tac 1);
   1.344 -by (thin_tac "0hr < y2 + - z2" 1);
   1.345 +by (thin_tac "0 < y2 + - z2" 1);
   1.346  by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   1.347  by (auto_tac (claset(),simpset() addsimps 
   1.348      [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
   1.349  qed "hypreal_add_less_mono";
   1.350  
   1.351 -Goal "((x::hypreal) = y) = (0hr = x + - y)";
   1.352 +Goal "((x::hypreal) = y) = (0 = x + - y)";
   1.353  by Auto_tac;
   1.354  by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   1.355  by Auto_tac;
   1.356  qed "hypreal_eq_minus_iff"; 
   1.357  
   1.358 -Goal "((x::hypreal) = y) = (0hr = y + - x)";
   1.359 +Goal "((x::hypreal) = y) = (0 = y + - x)";
   1.360  by Auto_tac;
   1.361  by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
   1.362  by Auto_tac;
   1.363 @@ -959,7 +955,7 @@
   1.364  by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.365  qed "hypreal_eq_minus_iff4";
   1.366  
   1.367 -Goal "(x ~= a) = (x + -a ~= 0hr)";
   1.368 +Goal "(x ~= a) = (x + -a ~= (0::hypreal))";
   1.369  by (auto_tac (claset() addDs [sym RS 
   1.370      (hypreal_eq_minus_iff RS iffD2)],simpset())); 
   1.371  qed "hypreal_not_eq_minus_iff";
   1.372 @@ -1057,7 +1053,7 @@
   1.373              fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
   1.374  qed "hypreal_le_anti_sym";
   1.375  
   1.376 -Goal "[| 0hr < x; 0hr <= y |] ==> 0hr < x + y";
   1.377 +Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
   1.378  by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
   1.379                addIs [hypreal_add_order],simpset()));
   1.380  qed "hypreal_add_order_le";            
   1.381 @@ -1070,14 +1066,14 @@
   1.382  by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
   1.383  qed "not_less_not_eq_hypreal_less";
   1.384  
   1.385 -Goal "(0hr < -R) = (R < 0hr)";
   1.386 +Goal "(0 < -R) = (R < (0::hypreal))";
   1.387  by (Step_tac 1);
   1.388  by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
   1.389  by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
   1.390  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.391  qed "hypreal_minus_zero_less_iff";
   1.392  
   1.393 -Goal "(-R < 0hr) = (0hr < R)";
   1.394 +Goal "(-R < 0) = ((0::hypreal) < R)";
   1.395  by (Step_tac 1);
   1.396  by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
   1.397  by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
   1.398 @@ -1090,7 +1086,7 @@
   1.399  by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.400  qed "hypreal_less_swap_iff";
   1.401  
   1.402 -Goal "(0hr < x) = (-x < x)";
   1.403 +Goal "((0::hypreal) < x) = (-x < x)";
   1.404  by (Step_tac 1);
   1.405  by (rtac ccontr 2 THEN forward_tac 
   1.406      [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
   1.407 @@ -1103,33 +1099,33 @@
   1.408  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.409  qed "hypreal_gt_zero_iff";
   1.410  
   1.411 -Goal "(x < 0hr) = (x < -x)";
   1.412 +Goal "(x < (0::hypreal)) = (x < -x)";
   1.413  by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
   1.414  by (stac hypreal_gt_zero_iff 1);
   1.415  by (Full_simp_tac 1);
   1.416  qed "hypreal_lt_zero_iff";
   1.417  
   1.418 -Goalw [hypreal_le_def] "(0hr <= x) = (-x <= x)";
   1.419 +Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
   1.420  by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
   1.421  qed "hypreal_ge_zero_iff";
   1.422  
   1.423 -Goalw [hypreal_le_def] "(x <= 0hr) = (x <= -x)";
   1.424 +Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
   1.425  by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
   1.426  qed "hypreal_le_zero_iff";
   1.427  
   1.428 -Goal "[| x < 0hr; y < 0hr |] ==> 0hr < x * y";
   1.429 +Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
   1.430  by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
   1.431  by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.432  by (Asm_full_simp_tac 1);
   1.433  qed "hypreal_mult_less_zero1";
   1.434  
   1.435 -Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x * y";
   1.436 +Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
   1.437  by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.438  by (auto_tac (claset() addIs [hypreal_mult_order,
   1.439      hypreal_less_imp_le],simpset()));
   1.440  qed "hypreal_le_mult_order";
   1.441  
   1.442 -Goal "[| x <= 0hr; y <= 0hr |] ==> 0hr <= x * y";
   1.443 +Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
   1.444  by (rtac hypreal_less_or_eq_imp_le 1);
   1.445  by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.446  by Auto_tac;
   1.447 @@ -1137,7 +1133,7 @@
   1.448  by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
   1.449  qed "real_mult_le_zero1";
   1.450  
   1.451 -Goal "[| 0hr <= x; y < 0hr |] ==> x * y <= 0hr";
   1.452 +Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
   1.453  by (rtac hypreal_less_or_eq_imp_le 1);
   1.454  by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.455  by Auto_tac;
   1.456 @@ -1147,21 +1143,21 @@
   1.457      addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
   1.458  qed "hypreal_mult_le_zero";
   1.459  
   1.460 -Goal "[| 0hr < x; y < 0hr |] ==> x*y < 0hr";
   1.461 +Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
   1.462  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.463  by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.464  by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.465 -by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2]) 1);
   1.466 +by (Asm_full_simp_tac 1);
   1.467  qed "hypreal_mult_less_zero";
   1.468  
   1.469 -Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0hr < 1hr";
   1.470 +Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
   1.471  by (res_inst_tac [("x","%n. #0")] exI 1);
   1.472  by (res_inst_tac [("x","%n. #1")] exI 1);
   1.473  by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
   1.474      FreeUltrafilterNat_Nat_set]));
   1.475  qed "hypreal_zero_less_one";
   1.476  
   1.477 -Goal "[| 0hr <= x; 0hr <= y |] ==> 0hr <= x + y";
   1.478 +Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
   1.479  by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.480  by (auto_tac (claset() addIs [hypreal_add_order,
   1.481      hypreal_less_imp_le],simpset()));
   1.482 @@ -1197,70 +1193,70 @@
   1.483      addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
   1.484  qed "hypreal_add_le_less_mono";
   1.485  
   1.486 -Goal "(0hr*x<r)=(0hr<r)";
   1.487 +Goal "(0*x<r)=((0::hypreal)<r)";
   1.488  by (Simp_tac 1);
   1.489  qed "hypreal_mult_0_less";
   1.490  
   1.491 -Goal "[| 0hr < z; x < y |] ==> x*z < y*z";       
   1.492 +Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";       
   1.493  by (rotate_tac 1 1);
   1.494  by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.495  by (rtac (hypreal_less_minus_iff RS iffD2) 1);
   1.496  by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.497  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
   1.498 -    hypreal_minus_mult_eq2 RS sym, hypreal_mult_commute ]) 1);
   1.499 +					   hypreal_mult_commute ]) 1);
   1.500  qed "hypreal_mult_less_mono1";
   1.501  
   1.502 -Goal "[| 0hr<z; x<y |] ==> z*x<z*y";       
   1.503 +Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";       
   1.504  by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
   1.505  qed "hypreal_mult_less_mono2";
   1.506  
   1.507 -Goal "[| 0hr<=z; x<y |] ==> x*z<=y*z";
   1.508 +Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
   1.509  by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
   1.510  by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
   1.511  qed "hypreal_mult_le_less_mono1";
   1.512  
   1.513 -Goal "[| 0hr<=z; x<y |] ==> z*x<=z*y";
   1.514 +Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
   1.515  by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
   1.516  				      hypreal_mult_le_less_mono1]) 1);
   1.517  qed "hypreal_mult_le_less_mono2";
   1.518  
   1.519 -Goal "[| 0hr<=z; x<=y |] ==> z*x<=z*y";
   1.520 +Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y";
   1.521  by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.522  by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
   1.523  qed "hypreal_mult_le_le_mono1";
   1.524  
   1.525  val prem1::prem2::prem3::rest = goal thy
   1.526 -     "[| 0hr<y; x<r; y*r<t*s |] ==> y*x<t*s";
   1.527 +     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
   1.528  by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
   1.529  qed "hypreal_mult_less_trans";
   1.530  
   1.531 -Goal "[| 0hr<=y; x<r; y*r<t*s; 0hr<t*s|] ==> y*x<t*s";
   1.532 +Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
   1.533  by (dtac hypreal_le_imp_less_or_eq 1);
   1.534  by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
   1.535  qed "hypreal_mult_le_less_trans";
   1.536  
   1.537 -Goal "[| 0hr <= y; x <= r; y*r < t*s; 0hr < t*s|] ==> y*x < t*s";
   1.538 +Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
   1.539  by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.540  by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
   1.541  qed "hypreal_mult_le_le_trans";
   1.542  
   1.543 -Goal "[| 0hr < r1; r1 <r2; 0hr < x; x < y|] \
   1.544 +Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \
   1.545  \                     ==> r1 * x < r2 * y";
   1.546  by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
   1.547 -by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 2);
   1.548 +by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2);
   1.549  by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
   1.550  by Auto_tac;
   1.551  by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
   1.552  qed "hypreal_mult_less_mono";
   1.553  
   1.554 -Goal "[| 0hr < r1; r1 <r2; 0hr < y|] \
   1.555 -\                           ==> 0hr < r2 * y";
   1.556 -by (dres_inst_tac [("R1.0","0hr")] hypreal_less_trans 1);
   1.557 +Goal "[| 0 < r1; r1 <r2; 0 < y|] \
   1.558 +\                           ==> (0::hypreal) < r2 * y";
   1.559 +by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1);
   1.560  by (assume_tac 1);
   1.561  by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
   1.562  qed "hypreal_mult_order_trans";
   1.563  
   1.564 -Goal "[| 0hr < r1; r1 <= r2; 0hr <= x; x <= y |] \
   1.565 +Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \
   1.566  \                  ==> r1 * x <= r2 * y";
   1.567  by (rtac hypreal_less_or_eq_imp_le 1);
   1.568  by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.569 @@ -1307,7 +1303,7 @@
   1.570  by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
   1.571  qed "hypreal_of_real_minus";
   1.572  
   1.573 -Goal "0hr < x ==> 0hr < hrinv x";
   1.574 +Goal "0 < x ==> 0 < hrinv x";
   1.575  by (EVERY1[rtac ccontr, dtac hypreal_leI]);
   1.576  by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
   1.577  by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
   1.578 @@ -1315,11 +1311,10 @@
   1.579  by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
   1.580  by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
   1.581  by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
   1.582 -    simpset() addsimps [hypreal_minus_mult_eq1 RS sym,
   1.583 -     hypreal_minus_zero_less_iff]));
   1.584 +    simpset() addsimps [hypreal_minus_zero_less_iff]));
   1.585  qed "hypreal_hrinv_gt_zero";
   1.586  
   1.587 -Goal "x < 0hr ==> hrinv x < 0hr";
   1.588 +Goal "x < 0 ==> hrinv x < 0";
   1.589  by (ftac hypreal_not_refl2 1);
   1.590  by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.591  by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.592 @@ -1332,17 +1327,17 @@
   1.593  by (Step_tac 1);
   1.594  qed "hypreal_of_real_one";
   1.595  
   1.596 -Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0hr";
   1.597 +Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real  #0 = 0";
   1.598  by (Step_tac 1);
   1.599  qed "hypreal_of_real_zero";
   1.600  
   1.601 -Goal "(hypreal_of_real  r = 0hr) = (r = #0)";
   1.602 +Goal "(hypreal_of_real  r = 0) = (r = #0)";
   1.603  by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
   1.604      simpset() addsimps [hypreal_of_real_def,
   1.605      hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
   1.606  qed "hypreal_of_real_zero_iff";
   1.607  
   1.608 -Goal "(hypreal_of_real  r ~= 0hr) = (r ~= #0)";
   1.609 +Goal "(hypreal_of_real  r ~= 0) = (r ~= #0)";
   1.610  by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
   1.611  qed "hypreal_of_real_not_zero_iff";
   1.612  
   1.613 @@ -1354,7 +1349,7 @@
   1.614  by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
   1.615  qed "hypreal_of_real_hrinv";
   1.616  
   1.617 -Goal "hypreal_of_real r ~= 0hr ==> hrinv (hypreal_of_real r) = \
   1.618 +Goal "hypreal_of_real r ~= 0 ==> hrinv (hypreal_of_real r) = \
   1.619  \          hypreal_of_real (rinv r)";
   1.620  by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_hrinv) 1);
   1.621  qed "hypreal_of_real_hrinv2";
   1.622 @@ -1369,12 +1364,12 @@
   1.623      hypreal_add_assoc]) 1);
   1.624  qed "hypreal_one_less_two";
   1.625  
   1.626 -Goal "0hr < 1hr + 1hr";
   1.627 +Goal "0 < 1hr + 1hr";
   1.628  by (rtac ([hypreal_zero_less_one,
   1.629            hypreal_one_less_two] MRS hypreal_less_trans) 1);
   1.630  qed "hypreal_zero_less_two";
   1.631  
   1.632 -Goal "1hr + 1hr ~= 0hr";
   1.633 +Goal "1hr + 1hr ~= 0";
   1.634  by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
   1.635  qed "hypreal_two_not_zero";
   1.636  Addsimps [hypreal_two_not_zero];
   1.637 @@ -1384,18 +1379,18 @@
   1.638  by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   1.639  qed "hypreal_sum_of_halves";
   1.640  
   1.641 -Goal "z ~= 0hr ==> x*y = (x*hrinv(z))*(z*y)";
   1.642 +Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)";
   1.643  by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
   1.644  qed "lemma_chain";
   1.645  
   1.646 -Goal "0hr < r ==> 0hr < r*hrinv(1hr+1hr)";
   1.647 +Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
   1.648  by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
   1.649            RS hypreal_mult_less_mono1) 1);
   1.650  by Auto_tac;
   1.651  qed "hypreal_half_gt_zero";
   1.652  
   1.653 -(* TODO: remove redundant  0hr < x *)
   1.654 -Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r";
   1.655 +(* TODO: remove redundant  0 < x *)
   1.656 +Goal "[| 0 < r; 0 < x; r < x |] ==> hrinv x < hrinv r";
   1.657  by (ftac hypreal_hrinv_gt_zero 1);
   1.658  by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
   1.659  by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
   1.660 @@ -1409,7 +1404,7 @@
   1.661           not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
   1.662  qed "hypreal_hrinv_less_swap";
   1.663  
   1.664 -Goal "[| 0hr < r; 0hr < x|] ==> (r < x) = (hrinv x < hrinv r)";
   1.665 +Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
   1.666  by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
   1.667  by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
   1.668  by (etac (hypreal_not_refl2 RS not_sym) 1);
   1.669 @@ -1419,29 +1414,29 @@
   1.670      simpset() addsimps [hypreal_hrinv_gt_zero]));
   1.671  qed "hypreal_hrinv_less_iff";
   1.672  
   1.673 -Goal "[| 0hr < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
   1.674 +Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
   1.675  by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
   1.676      hypreal_hrinv_gt_zero]) 1);
   1.677  qed "hypreal_mult_hrinv_less_mono1";
   1.678  
   1.679 -Goal "[| 0hr < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
   1.680 +Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
   1.681  by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
   1.682      hypreal_hrinv_gt_zero]) 1);
   1.683  qed "hypreal_mult_hrinv_less_mono2";
   1.684  
   1.685 -Goal "[| 0hr < z; x*z < y*z |] ==> x < y";
   1.686 +Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
   1.687  by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
   1.688  by (dtac (hypreal_not_refl2 RS not_sym) 2);
   1.689  by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
   1.690                simpset() addsimps hypreal_mult_ac));
   1.691  qed "hypreal_less_mult_right_cancel";
   1.692  
   1.693 -Goal "[| 0hr < z; z*x < z*y |] ==> x < y";
   1.694 +Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
   1.695  by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
   1.696      simpset() addsimps [hypreal_mult_commute]));
   1.697  qed "hypreal_less_mult_left_cancel";
   1.698  
   1.699 -Goal "[| 0hr < r; 0hr < ra; \
   1.700 +Goal "[| 0 < r; (0::hypreal) < ra; \
   1.701  \                 r < x; ra < y |] \
   1.702  \              ==> r*ra < x*y";
   1.703  by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
   1.704 @@ -1450,7 +1445,7 @@
   1.705  by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
   1.706  qed "hypreal_mult_less_gt_zero"; 
   1.707  
   1.708 -Goal "[| 0hr < r; 0hr < ra; \
   1.709 +Goal "[| 0 < r; (0::hypreal) < ra; \
   1.710  \                 r <= x; ra <= y |] \
   1.711  \              ==> r*ra <= x*y";
   1.712  by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.713 @@ -1460,7 +1455,7 @@
   1.714      simpset()));
   1.715  qed "hypreal_mult_le_ge_zero"; 
   1.716  
   1.717 -Goal "? (x::hypreal). x < y";
   1.718 +Goal "EX (x::hypreal). x < y";
   1.719  by (rtac (hypreal_add_zero_right RS subst) 1);
   1.720  by (res_inst_tac [("x","y + -1hr")] exI 1);
   1.721  by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
   1.722 @@ -1478,22 +1473,22 @@
   1.723  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   1.724  qed "hypreal_less_add_left_cancel";
   1.725  
   1.726 -Goal "0hr <= x*x";
   1.727 -by (res_inst_tac [("x","0hr"),("y","x")] hypreal_linear_less2 1);
   1.728 +Goal "(0::hypreal) <= x*x";
   1.729 +by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
   1.730  by (auto_tac (claset() addIs [hypreal_mult_order,
   1.731      hypreal_mult_less_zero1,hypreal_less_imp_le],
   1.732      simpset()));
   1.733  qed "hypreal_le_square";
   1.734  Addsimps [hypreal_le_square];
   1.735  
   1.736 -Goalw [hypreal_le_def] "- (x*x) <= 0hr";
   1.737 +Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
   1.738  by (auto_tac (claset() addSDs [(hypreal_le_square RS 
   1.739      hypreal_le_less_trans)],simpset() addsimps 
   1.740      [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
   1.741  qed "hypreal_less_minus_square";
   1.742  Addsimps [hypreal_less_minus_square];
   1.743  
   1.744 -Goal "[|x ~= 0hr; y ~= 0hr |] ==> \
   1.745 +Goal "[|x ~= 0; y ~= 0 |] ==> \
   1.746  \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
   1.747  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
   1.748               hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
   1.749 @@ -1502,7 +1497,7 @@
   1.750  by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.751  qed "hypreal_hrinv_add";
   1.752  
   1.753 -Goal "x = -x ==> x = 0hr";
   1.754 +Goal "x = -x ==> x = (0::hypreal)";
   1.755  by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
   1.756  by (Asm_full_simp_tac 1);
   1.757  by (dtac (hypreal_add_self RS subst) 1);
   1.758 @@ -1511,7 +1506,7 @@
   1.759                 (2,hypreal_mult_not_0)]) 1);
   1.760  qed "hypreal_self_eq_minus_self_zero";
   1.761  
   1.762 -Goal "(x + x = 0hr) = (x = 0hr)";
   1.763 +Goal "(x + x = 0) = (x = (0::hypreal))";
   1.764  by Auto_tac;
   1.765  by (dtac (hypreal_add_self RS subst) 1);
   1.766  by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
   1.767 @@ -1519,14 +1514,14 @@
   1.768  qed "hypreal_add_self_zero_cancel";
   1.769  Addsimps [hypreal_add_self_zero_cancel];
   1.770  
   1.771 -Goal "(x + x + y = y) = (x = 0hr)";
   1.772 +Goal "(x + x + y = y) = (x = (0::hypreal))";
   1.773  by Auto_tac;
   1.774  by (dtac (hypreal_eq_minus_iff RS iffD1) 1 THEN dtac sym 1);
   1.775  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.776  qed "hypreal_add_self_zero_cancel2";
   1.777  Addsimps [hypreal_add_self_zero_cancel2];
   1.778  
   1.779 -Goal "(x + (x + y) = y) = (x = 0hr)";
   1.780 +Goal "(x + (x + y) = y) = (x = (0::hypreal))";
   1.781  by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   1.782  qed "hypreal_add_self_zero_cancel2a";
   1.783  Addsimps [hypreal_add_self_zero_cancel2a];
   1.784 @@ -1607,18 +1602,18 @@
   1.785      hypreal_gt_half_sum]) 1);
   1.786  qed "hypreal_dense";
   1.787  
   1.788 -Goal "(x * x = 0hr) = (x = 0hr)";
   1.789 +Goal "(x * x = 0) = (x = (0::hypreal))";
   1.790  by Auto_tac;
   1.791  by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
   1.792  qed "hypreal_mult_self_eq_zero_iff";
   1.793  Addsimps [hypreal_mult_self_eq_zero_iff];
   1.794  
   1.795 -Goal "(0hr = x * x) = (x = 0hr)";
   1.796 +Goal "(0 = x * x) = (x = (0::hypreal))";
   1.797  by (auto_tac (claset() addDs [sym],simpset()));
   1.798  qed "hypreal_mult_self_eq_zero_iff2";
   1.799  Addsimps [hypreal_mult_self_eq_zero_iff2];
   1.800  
   1.801 -Goal "(x*x + y*y = 0hr) = (x = 0hr & y = 0hr)";
   1.802 +Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
   1.803  by Auto_tac;
   1.804  by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
   1.805  by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
   1.806 @@ -1638,25 +1633,24 @@
   1.807  qed "hypreal_squares_add_zero_iff";
   1.808  Addsimps [hypreal_squares_add_zero_iff];
   1.809  
   1.810 -Goal "x * x ~= 0hr ==> 0hr < x* x + y*y + z*z";
   1.811 +Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
   1.812  by (cut_inst_tac [("x1","x")] (hypreal_le_square 
   1.813          RS hypreal_le_imp_less_or_eq) 1);
   1.814  by (auto_tac (claset() addSIs 
   1.815                [hypreal_add_order_le],simpset()));
   1.816  qed "hypreal_sum_squares3_gt_zero";
   1.817  
   1.818 -Goal "x * x ~= 0hr ==> 0hr < y*y + x*x + z*z";
   1.819 +Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
   1.820  by (dtac hypreal_sum_squares3_gt_zero 1);
   1.821  by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.822  qed "hypreal_sum_squares3_gt_zero2";
   1.823  
   1.824 -Goal "x * x ~= 0hr ==> 0hr < y*y + z*z + x*x";
   1.825 +Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
   1.826  by (dtac hypreal_sum_squares3_gt_zero 1);
   1.827  by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.828  qed "hypreal_sum_squares3_gt_zero3";
   1.829  
   1.830 -Goal "(x*x + y*y + z*z = 0hr) = \ 
   1.831 -\               (x = 0hr & y = 0hr & z = 0hr)";
   1.832 +Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
   1.833  by Auto_tac;
   1.834  by (ALLGOALS(rtac ccontr));
   1.835  by (ALLGOALS(dtac hypreal_mult_self_not_zero));
   1.836 @@ -1746,7 +1740,7 @@
   1.837  (* a few lemmas first *)
   1.838  
   1.839  Goal "{n::nat. x = real_of_posnat n} = {} | \
   1.840 -\     (? y. {n::nat. x = real_of_posnat n} = {y})";
   1.841 +\     (EX y. {n::nat. x = real_of_posnat n} = {y})";
   1.842  by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
   1.843  qed "lemma_omega_empty_singleton_disj";
   1.844  
   1.845 @@ -1756,7 +1750,7 @@
   1.846  qed "lemma_finite_omega_set";
   1.847  
   1.848  Goalw [omega_def,hypreal_of_real_def] 
   1.849 -      "~ (? x. hypreal_of_real x = whr)";
   1.850 +      "~ (EX x. hypreal_of_real x = whr)";
   1.851  by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
   1.852      RS FreeUltrafilterNat_finite]));
   1.853  qed "not_ex_hypreal_of_real_eq_omega";
   1.854 @@ -1770,7 +1764,7 @@
   1.855  (* corresponding to any real number *)
   1.856  
   1.857  Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
   1.858 -\     (? y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
   1.859 +\     (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
   1.860  by (Step_tac 1 THEN Step_tac 1);
   1.861  by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
   1.862  qed "lemma_epsilon_empty_singleton_disj";
   1.863 @@ -1781,7 +1775,7 @@
   1.864  qed "lemma_finite_epsilon_set";
   1.865  
   1.866  Goalw [epsilon_def,hypreal_of_real_def] 
   1.867 -      "~ (? x. hypreal_of_real x = ehr)";
   1.868 +      "~ (EX x. hypreal_of_real x = ehr)";
   1.869  by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
   1.870      RS FreeUltrafilterNat_finite]));
   1.871  qed "not_ex_hypreal_of_real_eq_epsilon";
   1.872 @@ -1791,13 +1785,13 @@
   1.873  by Auto_tac;
   1.874  qed "hypreal_of_real_not_eq_epsilon";
   1.875  
   1.876 -Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0hr";
   1.877 +Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
   1.878  by (auto_tac (claset(),simpset() addsimps 
   1.879      [rename_numerals thy real_of_posnat_rinv_not_zero]));
   1.880  qed "hypreal_epsilon_not_zero";
   1.881  
   1.882  Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
   1.883 -Goalw [omega_def,hypreal_zero_def] "whr ~= 0hr";
   1.884 +Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
   1.885  by (Simp_tac 1);
   1.886  qed "hypreal_omega_not_zero";
   1.887  
   1.888 @@ -1811,7 +1805,7 @@
   1.889       Another embedding of the naturals in the 
   1.890      hyperreals (see hypreal_of_posnat)
   1.891   ----------------------------------------------------------------*)
   1.892 -Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0hr";
   1.893 +Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
   1.894  by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
   1.895  qed "hypreal_of_nat_zero";
   1.896  
     2.1 --- a/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jun 07 17:14:19 2000 +0200
     2.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy	Wed Jun 07 17:14:58 2000 +0200
     2.3 @@ -22,14 +22,13 @@
     2.4      "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
     2.5                     {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
     2.6  
     2.7 -typedef hypreal = "{x::nat=>real. True}/hyprel"              (Equiv.quotient_def)
     2.8 +typedef hypreal = "{x::nat=>real. True}/hyprel"   (Equiv.quotient_def)
     2.9  
    2.10  instance
    2.11 -   hypreal  :: {ord,plus,times,minus}
    2.12 +   hypreal  :: {ord, zero, plus, times, minus}
    2.13  
    2.14  consts 
    2.15  
    2.16 -  "0hr"       :: hypreal               ("0hr")   
    2.17    "1hr"       :: hypreal               ("1hr")  
    2.18    "whr"       :: hypreal               ("whr")  
    2.19    "ehr"       :: hypreal               ("ehr")  
    2.20 @@ -37,7 +36,7 @@
    2.21  
    2.22  defs
    2.23  
    2.24 -  hypreal_zero_def     "0hr == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
    2.25 +  hypreal_zero_def     "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})"
    2.26    hypreal_one_def      "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})"
    2.27  
    2.28    (* an infinite number = [<1,2,3,...>] *)
    2.29 @@ -47,7 +46,7 @@
    2.30    epsilon_def "ehr == Abs_hypreal(hyprel^^{%n::nat. rinv(real_of_posnat n)})"
    2.31  
    2.32    hypreal_minus_def
    2.33 -  "- P         == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    2.34 +  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})"
    2.35  
    2.36    hypreal_diff_def 
    2.37    "x - y == x + -(y::hypreal)"