src/HOL/Real/Hyperreal/HyperOrd.ML
changeset 10045 c76b73e16711
child 10607 352f6f209775
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperOrd.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,791 @@
     1.4 +(*  Title:	 Real/Hyperreal/HyperOrd.ML
     1.5 +    Author:      Jacques D. Fleuriot
     1.6 +    Copyright:   1998 University of Cambridge
     1.7 +                 2000 University of Edinburgh
     1.8 +    Description: Type "hypreal" is a linear order and also 
     1.9 +                 satisfies plus_ac0: + is an AC-operator with zero
    1.10 +*)
    1.11 +
    1.12 +(**** The simproc abel_cancel ****)
    1.13 +
    1.14 +(*** Two lemmas needed for the simprocs ***)
    1.15 +
    1.16 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
    1.17 +Goal "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)";
    1.18 +by (stac hypreal_add_left_commute 1);
    1.19 +by (rtac hypreal_add_left_cancel 1);
    1.20 +qed "hypreal_add_cancel_21";
    1.21 +
    1.22 +(*A further rule to deal with the case that
    1.23 +  everything gets cancelled on the right.*)
    1.24 +Goal "((x::hypreal) + (y + z) = y) = (x = -z)";
    1.25 +by (stac hypreal_add_left_commute 1);
    1.26 +by (res_inst_tac [("t", "y")] (hypreal_add_zero_right RS subst) 1
    1.27 +    THEN stac hypreal_add_left_cancel 1);
    1.28 +by (simp_tac (simpset() addsimps [hypreal_eq_diff_eq RS sym]) 1);
    1.29 +qed "hypreal_add_cancel_end";
    1.30 +
    1.31 +
    1.32 +structure Hyperreal_Cancel_Data =
    1.33 +struct
    1.34 +  val ss		= HOL_ss
    1.35 +  val eq_reflection	= eq_reflection
    1.36 +
    1.37 +  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
    1.38 +  val T			= Type("HyperDef.hypreal",[])
    1.39 +  val zero		= Const ("0", T)
    1.40 +  val restrict_to_left  = restrict_to_left
    1.41 +  val add_cancel_21	= hypreal_add_cancel_21
    1.42 +  val add_cancel_end	= hypreal_add_cancel_end
    1.43 +  val add_left_cancel	= hypreal_add_left_cancel
    1.44 +  val add_assoc		= hypreal_add_assoc
    1.45 +  val add_commute	= hypreal_add_commute
    1.46 +  val add_left_commute	= hypreal_add_left_commute
    1.47 +  val add_0		= hypreal_add_zero_left
    1.48 +  val add_0_right	= hypreal_add_zero_right
    1.49 +
    1.50 +  val eq_diff_eq	= hypreal_eq_diff_eq
    1.51 +  val eqI_rules		= [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
    1.52 +  fun dest_eqI th = 
    1.53 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    1.54 +	      (HOLogic.dest_Trueprop (concl_of th)))
    1.55 +
    1.56 +  val diff_def		= hypreal_diff_def
    1.57 +  val minus_add_distrib	= hypreal_minus_add_distrib
    1.58 +  val minus_minus	= hypreal_minus_minus
    1.59 +  val minus_0		= hypreal_minus_zero
    1.60 +  val add_inverses	= [hypreal_add_minus, hypreal_add_minus_left];
    1.61 +  val cancel_simps	= [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
    1.62 +end;
    1.63 +
    1.64 +structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
    1.65 +
    1.66 +Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
    1.67 +
    1.68 +Goal "- (z - y) = y - (z::hypreal)";
    1.69 +by (Simp_tac 1);
    1.70 +qed "hypreal_minus_diff_eq";
    1.71 +Addsimps [hypreal_minus_diff_eq];
    1.72 +
    1.73 +
    1.74 +Goal "((x::hypreal) < y) = (-y < -x)";
    1.75 +by (stac hypreal_less_minus_iff 1);
    1.76 +by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
    1.77 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
    1.78 +qed "hypreal_less_swap_iff";
    1.79 +
    1.80 +Goalw [hypreal_zero_def] 
    1.81 +      "((0::hypreal) < x) = (-x < x)";
    1.82 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.83 +by (auto_tac (claset(),simpset() addsimps [hypreal_less,
    1.84 +    hypreal_minus]));
    1.85 +by (ALLGOALS(Ultra_tac));
    1.86 +qed "hypreal_gt_zero_iff";
    1.87 +
    1.88 +Goal "(A::hypreal) < B ==> A + C < B + C";
    1.89 +by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
    1.90 +by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
    1.91 +by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
    1.92 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
    1.93 +    [hypreal_less_def,hypreal_add]));
    1.94 +by (Ultra_tac 1);
    1.95 +qed "hypreal_add_less_mono1";
    1.96 +
    1.97 +Goal "!!(A::hypreal). A < B ==> C + A < C + B";
    1.98 +by (auto_tac (claset() addIs [hypreal_add_less_mono1],
    1.99 +    simpset() addsimps [hypreal_add_commute]));
   1.100 +qed "hypreal_add_less_mono2";
   1.101 +
   1.102 +Goal "(x < (0::hypreal)) = (x < -x)";
   1.103 +by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
   1.104 +by (stac hypreal_gt_zero_iff 1);
   1.105 +by (Full_simp_tac 1);
   1.106 +qed "hypreal_lt_zero_iff";
   1.107 +
   1.108 +Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
   1.109 +by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
   1.110 +qed "hypreal_ge_zero_iff";
   1.111 +
   1.112 +Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
   1.113 +by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
   1.114 +qed "hypreal_le_zero_iff";
   1.115 +
   1.116 +Goalw [hypreal_zero_def] 
   1.117 +      "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
   1.118 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.119 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.120 +by (auto_tac (claset(),simpset() addsimps
   1.121 +    [hypreal_less_def,hypreal_add]));
   1.122 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
   1.123 +    [hypreal_less_def,hypreal_add]));
   1.124 +by (ultra_tac (claset() addIs [real_add_order],simpset()) 1);
   1.125 +qed "hypreal_add_order";
   1.126 +
   1.127 +Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
   1.128 +by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
   1.129 +              addIs [hypreal_add_order],simpset()));
   1.130 +qed "hypreal_add_order_le";            
   1.131 +
   1.132 +Goalw [hypreal_zero_def] 
   1.133 +          "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
   1.134 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.135 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.136 +by (auto_tac (claset() addSIs [exI],simpset() addsimps
   1.137 +    [hypreal_less_def,hypreal_mult]));
   1.138 +by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
   1.139 +	       simpset()) 1);
   1.140 +qed "hypreal_mult_order";
   1.141 +
   1.142 +Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
   1.143 +by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
   1.144 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.145 +by (Asm_full_simp_tac 1);
   1.146 +qed "hypreal_mult_less_zero1";
   1.147 +
   1.148 +Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
   1.149 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.150 +by (auto_tac (claset() addIs [hypreal_mult_order,
   1.151 +    hypreal_less_imp_le],simpset()));
   1.152 +qed "hypreal_le_mult_order";
   1.153 +
   1.154 +
   1.155 +Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
   1.156 +by (rtac hypreal_less_or_eq_imp_le 1);
   1.157 +by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.158 +by Auto_tac;
   1.159 +by (dtac hypreal_le_imp_less_or_eq 1);
   1.160 +by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
   1.161 +qed "hypreal_mult_le_zero1";
   1.162 +
   1.163 +Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
   1.164 +by (rtac hypreal_less_or_eq_imp_le 1);
   1.165 +by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.166 +by Auto_tac;
   1.167 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.168 +by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
   1.169 +by (blast_tac (claset() addDs [hypreal_mult_order] 
   1.170 +    addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
   1.171 +qed "hypreal_mult_le_zero";
   1.172 +
   1.173 +Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
   1.174 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.175 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.176 +by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.177 +by (Asm_full_simp_tac 1);
   1.178 +qed "hypreal_mult_less_zero";
   1.179 +
   1.180 +Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
   1.181 +by (res_inst_tac [("x","%n. #0")] exI 1);
   1.182 +by (res_inst_tac [("x","%n. #1")] exI 1);
   1.183 +by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
   1.184 +    FreeUltrafilterNat_Nat_set]));
   1.185 +qed "hypreal_zero_less_one";
   1.186 +
   1.187 +Goal "1hr < 1hr + 1hr";
   1.188 +by (rtac (hypreal_less_minus_iff RS iffD2) 1);
   1.189 +by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
   1.190 +    hypreal_add_assoc]) 1);
   1.191 +qed "hypreal_one_less_two";
   1.192 +
   1.193 +Goal "0 < 1hr + 1hr";
   1.194 +by (rtac ([hypreal_zero_less_one,
   1.195 +          hypreal_one_less_two] MRS hypreal_less_trans) 1);
   1.196 +qed "hypreal_zero_less_two";
   1.197 +
   1.198 +Goal "1hr + 1hr ~= 0";
   1.199 +by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
   1.200 +qed "hypreal_two_not_zero";
   1.201 +Addsimps [hypreal_two_not_zero];
   1.202 +
   1.203 +Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
   1.204 +by (stac hypreal_add_self 1);
   1.205 +by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc,
   1.206 +    hypreal_two_not_zero RS hypreal_mult_hrinv_left]) 1);
   1.207 +qed "hypreal_sum_of_halves";
   1.208 +
   1.209 +Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
   1.210 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.211 +by (auto_tac (claset() addIs [hypreal_add_order,
   1.212 +    hypreal_less_imp_le],simpset()));
   1.213 +qed "hypreal_le_add_order";
   1.214 +
   1.215 +(*** Monotonicity results ***)
   1.216 +
   1.217 +Goal "(v+z < w+z) = (v < (w::hypreal))";
   1.218 +by (Simp_tac 1);
   1.219 +qed "hypreal_add_right_cancel_less";
   1.220 +
   1.221 +Goal "(z+v < z+w) = (v < (w::hypreal))";
   1.222 +by (Simp_tac 1);
   1.223 +qed "hypreal_add_left_cancel_less";
   1.224 +
   1.225 +Addsimps [hypreal_add_right_cancel_less, 
   1.226 +          hypreal_add_left_cancel_less];
   1.227 +
   1.228 +Goal "(v+z <= w+z) = (v <= (w::hypreal))";
   1.229 +by (Simp_tac 1);
   1.230 +qed "hypreal_add_right_cancel_le";
   1.231 +
   1.232 +Goal "(z+v <= z+w) = (v <= (w::hypreal))";
   1.233 +by (Simp_tac 1);
   1.234 +qed "hypreal_add_left_cancel_le";
   1.235 +
   1.236 +Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le];
   1.237 +
   1.238 +Goal  "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
   1.239 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.240 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.241 +by (dtac hypreal_add_order 1 THEN assume_tac 1);
   1.242 +by (thin_tac "0 < y2 + - z2" 1);
   1.243 +by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   1.244 +by (auto_tac (claset(),simpset() addsimps 
   1.245 +    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
   1.246 +    delsimps [hypreal_minus_add_distrib]));
   1.247 +qed "hypreal_add_less_mono";
   1.248 +
   1.249 +Goal "(q1::hypreal) <= q2  ==> x + q1 <= x + q2";
   1.250 +by (dtac hypreal_le_imp_less_or_eq 1);
   1.251 +by (Step_tac 1);
   1.252 +by (auto_tac (claset() addSIs [hypreal_le_refl,
   1.253 +    hypreal_less_imp_le,hypreal_add_less_mono1],
   1.254 +    simpset() addsimps [hypreal_add_commute]));
   1.255 +qed "hypreal_add_left_le_mono1";
   1.256 +
   1.257 +Goal "(q1::hypreal) <= q2  ==> q1 + x <= q2 + x";
   1.258 +by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
   1.259 +    simpset() addsimps [hypreal_add_commute]));
   1.260 +qed "hypreal_add_le_mono1";
   1.261 +
   1.262 +Goal "[|(i::hypreal)<=j;  k<=l |] ==> i + k <= j + l";
   1.263 +by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
   1.264 +by (Simp_tac 1);
   1.265 +qed "hypreal_add_le_mono";
   1.266 +
   1.267 +Goal "[|(i::hypreal)<j;  k<=l |] ==> i + k < j + l";
   1.268 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.269 +    addIs [hypreal_add_less_mono1,hypreal_add_less_mono],
   1.270 +    simpset()));
   1.271 +qed "hypreal_add_less_le_mono";
   1.272 +
   1.273 +Goal "[|(i::hypreal)<=j;  k<l |] ==> i + k < j + l";
   1.274 +by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.275 +    addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
   1.276 +qed "hypreal_add_le_less_mono";
   1.277 +
   1.278 +Goal "(A::hypreal) + C < B + C ==> A < B";
   1.279 +by (Full_simp_tac 1);
   1.280 +qed "hypreal_less_add_right_cancel";
   1.281 +
   1.282 +Goal "(C::hypreal) + A < C + B ==> A < B";
   1.283 +by (Full_simp_tac 1);
   1.284 +qed "hypreal_less_add_left_cancel";
   1.285 +
   1.286 +Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y";
   1.287 +by (auto_tac (claset() addDs [hypreal_add_less_le_mono],
   1.288 +    simpset()));
   1.289 +qed "hypreal_add_zero_less_le_mono";
   1.290 +
   1.291 +Goal "!!(A::hypreal). A + C <= B + C ==> A <= B";
   1.292 +by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1);
   1.293 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   1.294 +qed "hypreal_le_add_right_cancel";
   1.295 +
   1.296 +Goal "!!(A::hypreal). C + A <= C + B ==> A <= B";
   1.297 +by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1);
   1.298 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   1.299 +qed "hypreal_le_add_left_cancel";
   1.300 +
   1.301 +Goal "(0::hypreal) <= x*x";
   1.302 +by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
   1.303 +by (auto_tac (claset() addIs [hypreal_mult_order,
   1.304 +    hypreal_mult_less_zero1,hypreal_less_imp_le],
   1.305 +    simpset()));
   1.306 +qed "hypreal_le_square";
   1.307 +Addsimps [hypreal_le_square];
   1.308 +
   1.309 +Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
   1.310 +by (auto_tac (claset() addSDs [(hypreal_le_square RS 
   1.311 +    hypreal_le_less_trans)],simpset() addsimps 
   1.312 +    [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
   1.313 +qed "hypreal_less_minus_square";
   1.314 +Addsimps [hypreal_less_minus_square];
   1.315 +
   1.316 +Goal "(0*x<r)=((0::hypreal)<r)";
   1.317 +by (Simp_tac 1);
   1.318 +qed "hypreal_mult_0_less";
   1.319 +
   1.320 +Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";       
   1.321 +by (rotate_tac 1 1);
   1.322 +by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.323 +by (rtac (hypreal_less_minus_iff RS iffD2) 1);
   1.324 +by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.325 +by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
   1.326 +					   hypreal_mult_commute ]) 1);
   1.327 +qed "hypreal_mult_less_mono1";
   1.328 +
   1.329 +Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";       
   1.330 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
   1.331 +qed "hypreal_mult_less_mono2";
   1.332 +
   1.333 +Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
   1.334 +by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
   1.335 +by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
   1.336 +qed "hypreal_mult_le_less_mono1";
   1.337 +
   1.338 +Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
   1.339 +by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
   1.340 +				      hypreal_mult_le_less_mono1]) 1);
   1.341 +qed "hypreal_mult_le_less_mono2";
   1.342 +
   1.343 +Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y";
   1.344 +by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.345 +by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
   1.346 +qed "hypreal_mult_le_le_mono1";
   1.347 +
   1.348 +val prem1::prem2::prem3::rest = goal thy
   1.349 +     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
   1.350 +by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
   1.351 +qed "hypreal_mult_less_trans";
   1.352 +
   1.353 +Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
   1.354 +by (dtac hypreal_le_imp_less_or_eq 1);
   1.355 +by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
   1.356 +qed "hypreal_mult_le_less_trans";
   1.357 +
   1.358 +Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
   1.359 +by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.360 +by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
   1.361 +qed "hypreal_mult_le_le_trans";
   1.362 +
   1.363 +Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \
   1.364 +\                     ==> r1 * x < r2 * y";
   1.365 +by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
   1.366 +by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2);
   1.367 +by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
   1.368 +by Auto_tac;
   1.369 +by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
   1.370 +qed "hypreal_mult_less_mono";
   1.371 +
   1.372 +Goal "[| 0 < r1; r1 <r2; 0 < y|] \
   1.373 +\                           ==> (0::hypreal) < r2 * y";
   1.374 +by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1);
   1.375 +by (assume_tac 1);
   1.376 +by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
   1.377 +qed "hypreal_mult_order_trans";
   1.378 +
   1.379 +Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \
   1.380 +\                  ==> r1 * x <= r2 * y";
   1.381 +by (rtac hypreal_less_or_eq_imp_le 1);
   1.382 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.383 +by (auto_tac (claset() addIs [hypreal_mult_less_mono,
   1.384 +    hypreal_mult_less_mono1,hypreal_mult_less_mono2,
   1.385 +    hypreal_mult_order_trans,hypreal_mult_order],simpset()));
   1.386 +qed "hypreal_mult_le_mono";
   1.387 +
   1.388 +Goal "0 < x ==> 0 < hrinv x";
   1.389 +by (EVERY1[rtac ccontr, dtac hypreal_leI]);
   1.390 +by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
   1.391 +by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
   1.392 +by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
   1.393 +by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
   1.394 +by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
   1.395 +by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
   1.396 +    simpset() addsimps [hypreal_minus_zero_less_iff]));
   1.397 +qed "hypreal_hrinv_gt_zero";
   1.398 +
   1.399 +Goal "x < 0 ==> hrinv x < 0";
   1.400 +by (ftac hypreal_not_refl2 1);
   1.401 +by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.402 +by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.403 +by (dtac (hypreal_minus_hrinv RS sym) 1);
   1.404 +by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
   1.405 +    simpset()));
   1.406 +qed "hypreal_hrinv_less_zero";
   1.407 +
   1.408 +(* check why this does not work without 2nd substitution anymore! *)
   1.409 +Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
   1.410 +by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
   1.411 +by (dtac (hypreal_add_self RS subst) 1);
   1.412 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
   1.413 +          hypreal_mult_less_mono1) 1);
   1.414 +by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
   1.415 +          (hypreal_mult_hrinv RS subst)],simpset() 
   1.416 +          addsimps [hypreal_mult_assoc]));
   1.417 +qed "hypreal_less_half_sum";
   1.418 +
   1.419 +(* check why this does not work without 2nd substitution anymore! *)
   1.420 +Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
   1.421 +by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
   1.422 +by (dtac (hypreal_add_self RS subst) 1);
   1.423 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
   1.424 +          hypreal_mult_less_mono1) 1);
   1.425 +by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
   1.426 +          (hypreal_mult_hrinv RS subst)],simpset() 
   1.427 +          addsimps [hypreal_mult_assoc]));
   1.428 +qed "hypreal_gt_half_sum";
   1.429 +
   1.430 +Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
   1.431 +by (blast_tac (claset() addSIs [hypreal_less_half_sum,
   1.432 +    hypreal_gt_half_sum]) 1);
   1.433 +qed "hypreal_dense";
   1.434 +
   1.435 +
   1.436 +Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
   1.437 +by Auto_tac;
   1.438 +by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
   1.439 +by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
   1.440 +by (ALLGOALS(rtac ccontr));
   1.441 +by (ALLGOALS(dtac hypreal_mult_self_not_zero));
   1.442 +by (cut_inst_tac [("x1","x")] (hypreal_le_square 
   1.443 +        RS hypreal_le_imp_less_or_eq) 1);
   1.444 +by (cut_inst_tac [("x1","y")] (hypreal_le_square 
   1.445 +        RS hypreal_le_imp_less_or_eq) 2);
   1.446 +by (auto_tac (claset() addDs [sym],simpset()));
   1.447 +by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
   1.448 +    RS hypreal_le_less_trans) 1);
   1.449 +by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
   1.450 +    RS hypreal_le_less_trans) 2);
   1.451 +by (auto_tac (claset(),simpset() addsimps 
   1.452 +       [hypreal_less_not_refl]));
   1.453 +qed "hypreal_squares_add_zero_iff";
   1.454 +Addsimps [hypreal_squares_add_zero_iff];
   1.455 +
   1.456 +Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
   1.457 +by (cut_inst_tac [("x1","x")] (hypreal_le_square 
   1.458 +        RS hypreal_le_imp_less_or_eq) 1);
   1.459 +by (auto_tac (claset() addSIs 
   1.460 +              [hypreal_add_order_le],simpset()));
   1.461 +qed "hypreal_sum_squares3_gt_zero";
   1.462 +
   1.463 +Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
   1.464 +by (dtac hypreal_sum_squares3_gt_zero 1);
   1.465 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.466 +qed "hypreal_sum_squares3_gt_zero2";
   1.467 +
   1.468 +Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
   1.469 +by (dtac hypreal_sum_squares3_gt_zero 1);
   1.470 +by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.471 +qed "hypreal_sum_squares3_gt_zero3";
   1.472 +
   1.473 +
   1.474 +Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
   1.475 +by Auto_tac;
   1.476 +by (ALLGOALS(rtac ccontr));
   1.477 +by (ALLGOALS(dtac hypreal_mult_self_not_zero));
   1.478 +by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
   1.479 +   hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
   1.480 +   hypreal_sum_squares3_gt_zero2],simpset() delsimps
   1.481 +   [hypreal_mult_self_eq_zero_iff]));
   1.482 +qed "hypreal_three_squares_add_zero_iff";
   1.483 +Addsimps [hypreal_three_squares_add_zero_iff];
   1.484 +
   1.485 +Addsimps [rename_numerals real_le_square];
   1.486 +Goal "(x::hypreal)*x <= x*x + y*y";
   1.487 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.488 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.489 +by (auto_tac (claset(),simpset() addsimps 
   1.490 +    [hypreal_mult,hypreal_add,hypreal_le]));
   1.491 +qed "hypreal_self_le_add_pos";
   1.492 +Addsimps [hypreal_self_le_add_pos];
   1.493 +
   1.494 +Goal "(x::hypreal)*x <= x*x + y*y + z*z";
   1.495 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.496 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.497 +by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   1.498 +by (auto_tac (claset(),
   1.499 +	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
   1.500 +				  rename_numerals real_le_add_order]));
   1.501 +qed "hypreal_self_le_add_pos2";
   1.502 +Addsimps [hypreal_self_le_add_pos2];
   1.503 +
   1.504 +
   1.505 +(*---------------------------------------------------------------------------------
   1.506 +             Embedding of the naturals in the hyperreals
   1.507 + ---------------------------------------------------------------------------------*)
   1.508 +Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
   1.509 +by (full_simp_tac (simpset() addsimps 
   1.510 +    [pnat_one_iff RS sym,real_of_preal_def]) 1);
   1.511 +by (fold_tac [real_one_def]);
   1.512 +by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
   1.513 +qed "hypreal_of_posnat_one";
   1.514 +
   1.515 +Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
   1.516 +by (full_simp_tac (simpset() addsimps 
   1.517 +		   [real_of_preal_def,
   1.518 +		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
   1.519 +		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
   1.520 +		    hypreal_one_def, real_add,
   1.521 +		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
   1.522 +		    pnat_add_ac) 1);
   1.523 +qed "hypreal_of_posnat_two";
   1.524 +
   1.525 +Goalw [hypreal_of_posnat_def]
   1.526 +          "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
   1.527 +\          hypreal_of_posnat (n1 + n2) + 1hr";
   1.528 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
   1.529 +    hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
   1.530 +    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
   1.531 +qed "hypreal_of_posnat_add";
   1.532 +
   1.533 +Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
   1.534 +by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
   1.535 +by (rtac (hypreal_of_posnat_add RS subst) 1);
   1.536 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
   1.537 +qed "hypreal_of_posnat_add_one";
   1.538 +
   1.539 +Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
   1.540 +      "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
   1.541 +by (rtac refl 1);
   1.542 +qed "hypreal_of_real_of_posnat";
   1.543 +
   1.544 +Goalw [hypreal_of_posnat_def] 
   1.545 +      "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
   1.546 +by Auto_tac;
   1.547 +qed "hypreal_of_posnat_less_iff";
   1.548 +
   1.549 +Addsimps [hypreal_of_posnat_less_iff RS sym];
   1.550 +(*---------------------------------------------------------------------------------
   1.551 +               Existence of infinite hyperreal number
   1.552 + ---------------------------------------------------------------------------------*)
   1.553 +
   1.554 +Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
   1.555 +by Auto_tac;
   1.556 +qed "hypreal_omega";
   1.557 +
   1.558 +Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
   1.559 +by (rtac Rep_hypreal 1);
   1.560 +qed "Rep_hypreal_omega";
   1.561 +
   1.562 +(* existence of infinite number not corresponding to any real number *)
   1.563 +(* use assumption that member FreeUltrafilterNat is not finite       *)
   1.564 +(* a few lemmas first *)
   1.565 +
   1.566 +Goal "{n::nat. x = real_of_posnat n} = {} | \
   1.567 +\     (EX y. {n::nat. x = real_of_posnat n} = {y})";
   1.568 +by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
   1.569 +qed "lemma_omega_empty_singleton_disj";
   1.570 +
   1.571 +Goal "finite {n::nat. x = real_of_posnat n}";
   1.572 +by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
   1.573 +by Auto_tac;
   1.574 +qed "lemma_finite_omega_set";
   1.575 +
   1.576 +Goalw [omega_def,hypreal_of_real_def] 
   1.577 +      "~ (EX x. hypreal_of_real x = whr)";
   1.578 +by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
   1.579 +    RS FreeUltrafilterNat_finite]));
   1.580 +qed "not_ex_hypreal_of_real_eq_omega";
   1.581 +
   1.582 +Goal "hypreal_of_real x ~= whr";
   1.583 +by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
   1.584 +by Auto_tac;
   1.585 +qed "hypreal_of_real_not_eq_omega";
   1.586 +
   1.587 +(* existence of infinitesimal number also not *)
   1.588 +(* corresponding to any real number *)
   1.589 +
   1.590 +Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
   1.591 +\     (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
   1.592 +by (Step_tac 1 THEN Step_tac 1);
   1.593 +by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
   1.594 +qed "lemma_epsilon_empty_singleton_disj";
   1.595 +
   1.596 +Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
   1.597 +by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
   1.598 +by Auto_tac;
   1.599 +qed "lemma_finite_epsilon_set";
   1.600 +
   1.601 +Goalw [epsilon_def,hypreal_of_real_def] 
   1.602 +      "~ (EX x. hypreal_of_real x = ehr)";
   1.603 +by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
   1.604 +    RS FreeUltrafilterNat_finite]));
   1.605 +qed "not_ex_hypreal_of_real_eq_epsilon";
   1.606 +
   1.607 +Goal "hypreal_of_real x ~= ehr";
   1.608 +by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
   1.609 +by Auto_tac;
   1.610 +qed "hypreal_of_real_not_eq_epsilon";
   1.611 +
   1.612 +Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
   1.613 +by (auto_tac (claset(),
   1.614 +     simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero]));
   1.615 +qed "hypreal_epsilon_not_zero";
   1.616 +
   1.617 +Addsimps [rename_numerals real_of_posnat_not_eq_zero];
   1.618 +Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
   1.619 +by (Simp_tac 1);
   1.620 +qed "hypreal_omega_not_zero";
   1.621 +
   1.622 +Goal "ehr = hrinv(whr)";
   1.623 +by (asm_full_simp_tac (simpset() addsimps 
   1.624 +    [hypreal_hrinv,omega_def,epsilon_def]) 1);
   1.625 +qed "hypreal_epsilon_hrinv_omega";
   1.626 +
   1.627 +(*----------------------------------------------------------------
   1.628 +     Another embedding of the naturals in the 
   1.629 +    hyperreals (see hypreal_of_posnat)
   1.630 + ----------------------------------------------------------------*)
   1.631 +Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
   1.632 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
   1.633 +qed "hypreal_of_nat_zero";
   1.634 +
   1.635 +Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
   1.636 +by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
   1.637 +    hypreal_add_assoc]) 1);
   1.638 +qed "hypreal_of_nat_one";
   1.639 +
   1.640 +Goalw [hypreal_of_nat_def]
   1.641 +      "hypreal_of_nat n1 + hypreal_of_nat n2 = \
   1.642 +\      hypreal_of_nat (n1 + n2)";
   1.643 +by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
   1.644 +by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
   1.645 +    hypreal_add_assoc RS sym]) 1);
   1.646 +qed "hypreal_of_nat_add";
   1.647 +
   1.648 +Goal "hypreal_of_nat 2 = 1hr + 1hr";
   1.649 +by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
   1.650 +    RS sym,hypreal_of_nat_add]) 1);
   1.651 +qed "hypreal_of_nat_two";
   1.652 +
   1.653 +Goalw [hypreal_of_nat_def] 
   1.654 +      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
   1.655 +by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
   1.656 +qed "hypreal_of_nat_less_iff";
   1.657 +Addsimps [hypreal_of_nat_less_iff RS sym];
   1.658 +
   1.659 +(*------------------------------------------------------------*)
   1.660 +(* naturals embedded in hyperreals                            *)
   1.661 +(* is a hyperreal c.f. NS extension                           *)
   1.662 +(*------------------------------------------------------------*)
   1.663 +
   1.664 +Goalw [hypreal_of_nat_def,real_of_nat_def] 
   1.665 +      "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
   1.666 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
   1.667 +    hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
   1.668 +qed "hypreal_of_nat_iff";
   1.669 +
   1.670 +Goal "inj hypreal_of_nat";
   1.671 +by (rtac injI 1);
   1.672 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
   1.673 +        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
   1.674 +        real_add_right_cancel,inj_real_of_nat RS injD]));
   1.675 +qed "inj_hypreal_of_nat";
   1.676 +
   1.677 +Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
   1.678 +       real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
   1.679 +       "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
   1.680 +by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
   1.681 +qed "hypreal_of_nat_real_of_nat";
   1.682 +
   1.683 +Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr";
   1.684 +by (stac (hypreal_of_posnat_add_one RS sym) 1);
   1.685 +by (Simp_tac 1);
   1.686 +qed "hypreal_of_posnat_Suc";
   1.687 +
   1.688 +Goalw [hypreal_of_nat_def] 
   1.689 +      "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr";
   1.690 +by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1);
   1.691 +qed "hypreal_of_nat_Suc";
   1.692 +
   1.693 +Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
   1.694 +by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
   1.695 +          RS hypreal_mult_less_mono1) 1);
   1.696 +by Auto_tac;
   1.697 +qed "hypreal_half_gt_zero";
   1.698 +
   1.699 +(* this proof is so much simpler than one for reals!! *)
   1.700 +Goal "[| 0 < r; r < x |] ==> hrinv x < hrinv r";
   1.701 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.702 +by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   1.703 +by (auto_tac (claset(),simpset() addsimps [hypreal_hrinv,
   1.704 +    hypreal_less,hypreal_zero_def]));
   1.705 +by (ultra_tac (claset() addIs [real_rinv_less_swap],simpset()) 1);
   1.706 +qed "hypreal_hrinv_less_swap";
   1.707 +
   1.708 +Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
   1.709 +by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
   1.710 +by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
   1.711 +by (etac (hypreal_not_refl2 RS not_sym) 1);
   1.712 +by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
   1.713 +by (etac (hypreal_not_refl2 RS not_sym) 1);
   1.714 +by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
   1.715 +    simpset() addsimps [hypreal_hrinv_gt_zero]));
   1.716 +qed "hypreal_hrinv_less_iff";
   1.717 +
   1.718 +Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
   1.719 +by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
   1.720 +    hypreal_hrinv_gt_zero]) 1);
   1.721 +qed "hypreal_mult_hrinv_less_mono1";
   1.722 +
   1.723 +Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
   1.724 +by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
   1.725 +    hypreal_hrinv_gt_zero]) 1);
   1.726 +qed "hypreal_mult_hrinv_less_mono2";
   1.727 +
   1.728 +Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
   1.729 +by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
   1.730 +by (dtac (hypreal_not_refl2 RS not_sym) 2);
   1.731 +by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
   1.732 +              simpset() addsimps hypreal_mult_ac));
   1.733 +qed "hypreal_less_mult_right_cancel";
   1.734 +
   1.735 +Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
   1.736 +by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
   1.737 +    simpset() addsimps [hypreal_mult_commute]));
   1.738 +qed "hypreal_less_mult_left_cancel";
   1.739 +
   1.740 +Goal "[| 0 < r; (0::hypreal) < ra; \
   1.741 +\                 r < x; ra < y |] \
   1.742 +\              ==> r*ra < x*y";
   1.743 +by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
   1.744 +by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
   1.745 +by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
   1.746 +by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
   1.747 +qed "hypreal_mult_less_gt_zero"; 
   1.748 +
   1.749 +Goal "[| 0 < r; (0::hypreal) < ra; \
   1.750 +\                 r <= x; ra <= y |] \
   1.751 +\              ==> r*ra <= x*y";
   1.752 +by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.753 +by (rtac hypreal_less_or_eq_imp_le 1);
   1.754 +by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
   1.755 +    hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
   1.756 +    simpset()));
   1.757 +qed "hypreal_mult_le_ge_zero"; 
   1.758 +
   1.759 +(*----------------------------------------------------------------------------
   1.760 +     Some convenient biconditionals for products of signs 
   1.761 + ----------------------------------------------------------------------------*)
   1.762 +
   1.763 +Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
   1.764 + by (auto_tac (claset(), simpset() addsimps [order_le_less, 
   1.765 +    linorder_not_less, hypreal_mult_order, hypreal_mult_less_zero1]));
   1.766 +by (ALLGOALS (rtac ccontr)); 
   1.767 +by (auto_tac (claset(), simpset() addsimps 
   1.768 +    [order_le_less, linorder_not_less]));
   1.769 +by (ALLGOALS (etac rev_mp)); 
   1.770 +by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
   1.771 +by (auto_tac (claset() addDs [order_less_not_sym], 
   1.772 +              simpset() addsimps [hypreal_mult_commute]));  
   1.773 +qed "hypreal_zero_less_mult_iff";
   1.774 +
   1.775 +Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
   1.776 +by (auto_tac (claset() addDs [sym RS hypreal_mult_zero_disj],
   1.777 +    simpset() addsimps [order_le_less,
   1.778 +    linorder_not_less,hypreal_zero_less_mult_iff]));
   1.779 +qed "hypreal_zero_le_mult_iff";
   1.780 +
   1.781 +Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
   1.782 +by (auto_tac (claset(), 
   1.783 +              simpset() addsimps [hypreal_zero_le_mult_iff, 
   1.784 +                                  linorder_not_le RS sym]));
   1.785 +by (auto_tac (claset() addDs [order_less_not_sym],  
   1.786 +              simpset() addsimps [linorder_not_le]));
   1.787 +qed "hypreal_mult_less_zero_iff";
   1.788 +
   1.789 +Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
   1.790 +by (auto_tac (claset() addDs [order_less_not_sym], 
   1.791 +              simpset() addsimps [hypreal_zero_less_mult_iff, 
   1.792 +                                  linorder_not_less RS sym]));
   1.793 +qed "hypreal_mult_le_zero_iff";
   1.794 +