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.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.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.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.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.58 +  val minus_minus	= hypreal_minus_minus
1.59 +  val minus_0		= hypreal_minus_zero
1.62 +end;
1.63 +
1.64 +structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
1.65 +
1.67 +
1.68 +Goal "- (z - y) = y - (z::hypreal)";
1.69 +by (Simp_tac 1);
1.70 +qed "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.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.94 +by (Ultra_tac 1);
1.96 +
1.97 +Goal "!!(A::hypreal). A < B ==> C + A < C + B";
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.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.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.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.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.202 +
1.203 +Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
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.212 +    hypreal_less_imp_le],simpset()));
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.220 +
1.221 +Goal "(z+v < z+w) = (v < (w::hypreal))";
1.222 +by (Simp_tac 1);
1.224 +
1.227 +
1.228 +Goal "(v+z <= w+z) = (v <= (w::hypreal))";
1.229 +by (Simp_tac 1);
1.231 +
1.232 +Goal "(z+v <= z+w) = (v <= (w::hypreal))";
1.233 +by (Simp_tac 1);
1.235 +
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.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.256 +
1.257 +Goal "(q1::hypreal) <= q2  ==> q1 + x <= q2 + x";
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.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.270 +    simpset()));
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.277 +
1.278 +Goal "(A::hypreal) + C < B + C ==> A < B";
1.279 +by (Full_simp_tac 1);
1.281 +
1.282 +Goal "(C::hypreal) + A < C + B ==> A < B";
1.283 +by (Full_simp_tac 1);
1.285 +
1.286 +Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y";
1.288 +    simpset()));
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.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.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.308 +
1.309 +Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
1.310 +by (auto_tac (claset() addSDs [(hypreal_le_square RS
1.312 +    [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
1.313 +qed "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.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.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.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.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.452 +       [hypreal_less_not_refl]));
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.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.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.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.484 +
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.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.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.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.517 +		   [real_of_preal_def,
1.518 +		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
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.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.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.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.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.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.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.645 +    hypreal_add_assoc RS sym]) 1);
1.647 +
1.648 +Goal "hypreal_of_nat 2 = 1hr + 1hr";
1.649 +by (simp_tac (simpset() addsimps [hypreal_of_nat_one
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.656 +qed "hypreal_of_nat_less_iff";
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.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.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.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.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.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.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.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.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.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(),