1.1 --- a/src/HOL/Hyperreal/HyperOrd.ML Mon Dec 15 17:08:41 2003 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,529 +0,0 @@
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, hypreal_minus]));
1.84 -by (ALLGOALS(Ultra_tac));
1.85 -qed "hypreal_gt_zero_iff";
1.86 -
1.87 -Goal "(A::hypreal) < B ==> A + C < B + C";
1.88 -by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
1.89 -by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
1.90 -by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
1.91 -by (auto_tac (claset() addSIs [exI],
1.92 - simpset() addsimps [hypreal_less_def,hypreal_add]));
1.93 -by (Ultra_tac 1);
1.94 -qed "hypreal_add_less_mono1";
1.95 -
1.96 -Goal "!!(A::hypreal). A < B ==> C + A < C + B";
1.97 -by (auto_tac (claset() addIs [hypreal_add_less_mono1],
1.98 - simpset() addsimps [hypreal_add_commute]));
1.99 -qed "hypreal_add_less_mono2";
1.100 -
1.101 -Goal "(x < (0::hypreal)) = (x < -x)";
1.102 -by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
1.103 -by (stac hypreal_gt_zero_iff 1);
1.104 -by (Full_simp_tac 1);
1.105 -qed "hypreal_lt_zero_iff";
1.106 -
1.107 -Goalw [hypreal_zero_def] "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
1.108 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
1.109 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
1.110 -by (auto_tac (claset(),
1.111 - simpset() addsimps [hypreal_less_def,hypreal_add]));
1.112 -by (auto_tac (claset() addSIs [exI],
1.113 - simpset() addsimps [hypreal_less_def,hypreal_add]));
1.114 -by (ultra_tac (claset() addIs [real_add_order], simpset()) 1);
1.115 -qed "hypreal_add_order";
1.116 -
1.117 -Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
1.118 -by (auto_tac (claset() addDs [sym, order_le_imp_less_or_eq]
1.119 - addIs [hypreal_add_order],
1.120 - simpset()));
1.121 -qed "hypreal_add_order_le";
1.122 -
1.123 -Goalw [hypreal_zero_def] "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
1.124 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
1.125 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
1.126 -by (auto_tac (claset() addSIs [exI],
1.127 - simpset() addsimps [hypreal_less_def,hypreal_mult]));
1.128 -by (ultra_tac (claset() addIs [real_mult_order], simpset()) 1);
1.129 -qed "hypreal_mult_order";
1.130 -
1.131 -Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
1.132 -by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
1.133 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
1.134 -by (Asm_full_simp_tac 1);
1.135 -qed "hypreal_mult_less_zero1";
1.136 -
1.137 -Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
1.138 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
1.139 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
1.140 -by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
1.141 -by (Asm_full_simp_tac 1);
1.142 -qed "hypreal_mult_less_zero";
1.143 -
1.144 -Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < (1::hypreal)";
1.145 -by (res_inst_tac [("x","%n. 0")] exI 1);
1.146 -by (res_inst_tac [("x","%n. 1")] exI 1);
1.147 -by (auto_tac (claset(),
1.148 - simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
1.149 -qed "hypreal_zero_less_one";
1.150 -
1.151 -Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
1.152 -by (REPEAT(dtac order_le_imp_less_or_eq 1));
1.153 -by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le],
1.154 - simpset()));
1.155 -qed "hypreal_le_add_order";
1.156 -
1.157 -(*** Monotonicity results ***)
1.158 -
1.159 -Goal "(v+z < w+z) = (v < (w::hypreal))";
1.160 -by (Simp_tac 1);
1.161 -qed "hypreal_add_right_cancel_less";
1.162 -
1.163 -Goal "(z+v < z+w) = (v < (w::hypreal))";
1.164 -by (Simp_tac 1);
1.165 -qed "hypreal_add_left_cancel_less";
1.166 -
1.167 -Addsimps [hypreal_add_right_cancel_less,
1.168 - hypreal_add_left_cancel_less];
1.169 -
1.170 -Goal "(v+z <= w+z) = (v <= (w::hypreal))";
1.171 -by (Simp_tac 1);
1.172 -qed "hypreal_add_right_cancel_le";
1.173 -
1.174 -Goal "(z+v <= z+w) = (v <= (w::hypreal))";
1.175 -by (Simp_tac 1);
1.176 -qed "hypreal_add_left_cancel_le";
1.177 -
1.178 -Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le];
1.179 -
1.180 -Goal "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
1.181 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
1.182 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
1.183 -by (dtac hypreal_add_order 1 THEN assume_tac 1);
1.184 -by (thin_tac "0 < y2 + - z2" 1);
1.185 -by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
1.186 -by (auto_tac (claset(),
1.187 - simpset() addsimps [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
1.188 - delsimps [hypreal_minus_add_distrib]));
1.189 -qed "hypreal_add_less_mono";
1.190 -
1.191 -Goal "(q1::hypreal) <= q2 ==> x + q1 <= x + q2";
1.192 -by (dtac order_le_imp_less_or_eq 1);
1.193 -by (Step_tac 1);
1.194 -by (auto_tac (claset() addSIs [order_less_imp_le,hypreal_add_less_mono1],
1.195 - simpset() addsimps [hypreal_add_commute]));
1.196 -qed "hypreal_add_left_le_mono1";
1.197 -
1.198 -Goal "(q1::hypreal) <= q2 ==> q1 + x <= q2 + x";
1.199 -by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
1.200 - simpset() addsimps [hypreal_add_commute]));
1.201 -qed "hypreal_add_le_mono1";
1.202 -
1.203 -Goal "[|(i::hypreal)<=j; k<=l |] ==> i + k <= j + l";
1.204 -by (etac (hypreal_add_le_mono1 RS order_trans) 1);
1.205 -by (Simp_tac 1);
1.206 -qed "hypreal_add_le_mono";
1.207 -
1.208 -Goal "[|(i::hypreal)<j; k<=l |] ==> i + k < j + l";
1.209 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
1.210 - addIs [hypreal_add_less_mono1,hypreal_add_less_mono],
1.211 - simpset()));
1.212 -qed "hypreal_add_less_le_mono";
1.213 -
1.214 -Goal "[|(i::hypreal)<=j; k<l |] ==> i + k < j + l";
1.215 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
1.216 - addIs [hypreal_add_less_mono2,hypreal_add_less_mono],
1.217 - simpset()));
1.218 -qed "hypreal_add_le_less_mono";
1.219 -
1.220 -Goal "(A::hypreal) + C < B + C ==> A < B";
1.221 -by (Full_simp_tac 1);
1.222 -qed "hypreal_less_add_right_cancel";
1.223 -
1.224 -Goal "(C::hypreal) + A < C + B ==> A < B";
1.225 -by (Full_simp_tac 1);
1.226 -qed "hypreal_less_add_left_cancel";
1.227 -
1.228 -Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y";
1.229 -by (auto_tac (claset() addDs [hypreal_add_less_le_mono],
1.230 - simpset()));
1.231 -qed "hypreal_add_zero_less_le_mono";
1.232 -
1.233 -Goal "!!(A::hypreal). A + C <= B + C ==> A <= B";
1.234 -by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1);
1.235 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
1.236 -qed "hypreal_le_add_right_cancel";
1.237 -
1.238 -Goal "!!(A::hypreal). C + A <= C + B ==> A <= B";
1.239 -by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1);
1.240 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
1.241 -qed "hypreal_le_add_left_cancel";
1.242 -
1.243 -Goal "(0::hypreal) <= x*x";
1.244 -by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
1.245 -by (auto_tac (claset() addIs [hypreal_mult_order,
1.246 - hypreal_mult_less_zero1,order_less_imp_le],
1.247 - simpset()));
1.248 -qed "hypreal_le_square";
1.249 -Addsimps [hypreal_le_square];
1.250 -
1.251 -Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
1.252 -by (auto_tac (claset() addSDs [hypreal_le_square RS order_le_less_trans],
1.253 - simpset() addsimps [hypreal_minus_zero_less_iff]));
1.254 -qed "hypreal_less_minus_square";
1.255 -Addsimps [hypreal_less_minus_square];
1.256 -
1.257 -Goal "(0*x<r)=((0::hypreal)<r)";
1.258 -by (Simp_tac 1);
1.259 -qed "hypreal_mult_0_less";
1.260 -
1.261 -Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";
1.262 -by (rotate_tac 1 1);
1.263 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
1.264 -by (rtac (hypreal_less_minus_iff RS iffD2) 1);
1.265 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
1.266 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
1.267 - hypreal_mult_commute ]) 1);
1.268 -qed "hypreal_mult_less_mono1";
1.269 -
1.270 -Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";
1.271 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
1.272 -qed "hypreal_mult_less_mono2";
1.273 -
1.274 -Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
1.275 -by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
1.276 -by (auto_tac (claset() addIs [hypreal_mult_less_mono1], simpset()));
1.277 -qed "hypreal_mult_le_less_mono1";
1.278 -
1.279 -Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
1.280 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
1.281 - hypreal_mult_le_less_mono1]) 1);
1.282 -qed "hypreal_mult_le_less_mono2";
1.283 -
1.284 -val prem1::prem2::prem3::rest = goal thy
1.285 - "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
1.286 -by (rtac ([[prem1,prem2] MRS hypreal_mult_less_mono2, prem3]
1.287 - MRS order_less_trans) 1);
1.288 -qed "hypreal_mult_less_trans";
1.289 -
1.290 -Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
1.291 -by (dtac order_le_imp_less_or_eq 1);
1.292 -by (fast_tac (HOL_cs addEs [hypreal_mult_0_less RS iffD2,
1.293 - hypreal_mult_less_trans]) 1);
1.294 -qed "hypreal_mult_le_less_trans";
1.295 -
1.296 -Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
1.297 -by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
1.298 -by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
1.299 -qed "hypreal_mult_le_le_trans";
1.300 -
1.301 -Goal "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y";
1.302 -by (etac (hypreal_mult_less_mono1 RS order_less_trans) 1);
1.303 -by (assume_tac 1);
1.304 -by (etac hypreal_mult_less_mono2 1);
1.305 -by (assume_tac 1);
1.306 -qed "hypreal_mult_less_mono";
1.307 -
1.308 -(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
1.309 -Goal "[| x < y; r1 < r2; (0::hypreal) <= r1; 0 <= x|] ==> r1 * x < r2 * y";
1.310 -by (subgoal_tac "0<r2" 1);
1.311 -by (blast_tac (claset() addIs [order_le_less_trans]) 2);
1.312 -by (case_tac "x=0" 1);
1.313 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
1.314 - addIs [hypreal_mult_less_mono, hypreal_mult_order],
1.315 - simpset()));
1.316 -qed "hypreal_mult_less_mono'";
1.317 -
1.318 -Goal "0 < x ==> 0 < inverse (x::hypreal)";
1.319 -by (EVERY1[rtac ccontr, dtac hypreal_leI]);
1.320 -by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
1.321 -by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
1.322 -by (dtac (hypreal_not_refl2 RS not_sym RS hypreal_inverse_not_zero) 1);
1.323 -by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]);
1.324 -by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
1.325 -by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
1.326 - simpset() addsimps [hypreal_minus_zero_less_iff]));
1.327 -qed "hypreal_inverse_gt_0";
1.328 -
1.329 -Goal "x < 0 ==> inverse (x::hypreal) < 0";
1.330 -by (ftac hypreal_not_refl2 1);
1.331 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
1.332 -by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
1.333 -by (stac (hypreal_minus_inverse RS sym) 1);
1.334 -by (auto_tac (claset() addIs [hypreal_inverse_gt_0], simpset()));
1.335 -qed "hypreal_inverse_less_0";
1.336 -
1.337 -Goal "(x::hypreal)*x <= x*x + y*y";
1.338 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
1.339 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
1.340 -by (auto_tac (claset(),
1.341 - simpset() addsimps [hypreal_mult,hypreal_add,hypreal_le]));
1.342 -qed "hypreal_self_le_add_pos";
1.343 -Addsimps [hypreal_self_le_add_pos];
1.344 -
1.345 -(*lcp: new lemma unfortunately needed...*)
1.346 -Goal "-(x*x) <= (y*y::real)";
1.347 -by (rtac order_trans 1);
1.348 -by (rtac real_le_square 2);
1.349 -by Auto_tac;
1.350 -qed "minus_square_le_square";
1.351 -
1.352 -Goal "(x::hypreal)*x <= x*x + y*y + z*z";
1.353 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
1.354 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
1.355 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
1.356 -by (auto_tac (claset(),
1.357 - simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
1.358 - minus_square_le_square]));
1.359 -qed "hypreal_self_le_add_pos2";
1.360 -Addsimps [hypreal_self_le_add_pos2];
1.361 -
1.362 -
1.363 -(*----------------------------------------------------------------------------
1.364 - Existence of infinite hyperreal number
1.365 - ----------------------------------------------------------------------------*)
1.366 -
1.367 -Goalw [omega_def] "Rep_hypreal(omega) : hypreal";
1.368 -by (rtac Rep_hypreal 1);
1.369 -qed "Rep_hypreal_omega";
1.370 -
1.371 -(* existence of infinite number not corresponding to any real number *)
1.372 -(* use assumption that member FreeUltrafilterNat is not finite *)
1.373 -(* a few lemmas first *)
1.374 -
1.375 -Goal "{n::nat. x = real n} = {} | \
1.376 -\ (EX y. {n::nat. x = real n} = {y})";
1.377 -by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
1.378 -qed "lemma_omega_empty_singleton_disj";
1.379 -
1.380 -Goal "finite {n::nat. x = real n}";
1.381 -by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
1.382 -by Auto_tac;
1.383 -qed "lemma_finite_omega_set";
1.384 -
1.385 -Goalw [omega_def,hypreal_of_real_def]
1.386 - "~ (EX x. hypreal_of_real x = omega)";
1.387 -by (auto_tac (claset(),
1.388 - simpset() addsimps [real_of_nat_Suc, diff_eq_eq RS sym,
1.389 - lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
1.390 -qed "not_ex_hypreal_of_real_eq_omega";
1.391 -
1.392 -Goal "hypreal_of_real x ~= omega";
1.393 -by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
1.394 -by Auto_tac;
1.395 -qed "hypreal_of_real_not_eq_omega";
1.396 -
1.397 -(* existence of infinitesimal number also not *)
1.398 -(* corresponding to any real number *)
1.399 -
1.400 -Goal "inverse (real (x::nat)) = inverse (real y) ==> x = y";
1.401 -by (rtac (inj_real_of_nat RS injD) 1);
1.402 -by (Asm_full_simp_tac 1);
1.403 -qed "real_of_nat_inverse_inj";
1.404 -
1.405 -Goal "{n::nat. x = inverse(real(Suc n))} = {} | \
1.406 -\ (EX y. {n::nat. x = inverse(real(Suc n))} = {y})";
1.407 -by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq]));
1.408 -qed "lemma_epsilon_empty_singleton_disj";
1.409 -
1.410 -Goal "finite {n. x = inverse(real(Suc n))}";
1.411 -by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
1.412 -by Auto_tac;
1.413 -qed "lemma_finite_epsilon_set";
1.414 -
1.415 -Goalw [epsilon_def,hypreal_of_real_def]
1.416 - "~ (EX x. hypreal_of_real x = epsilon)";
1.417 -by (auto_tac (claset(),
1.418 - simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite]));
1.419 -qed "not_ex_hypreal_of_real_eq_epsilon";
1.420 -
1.421 -Goal "hypreal_of_real x ~= epsilon";
1.422 -by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
1.423 -by Auto_tac;
1.424 -qed "hypreal_of_real_not_eq_epsilon";
1.425 -
1.426 -Goalw [epsilon_def,hypreal_zero_def] "epsilon ~= 0";
1.427 -by Auto_tac;
1.428 -by (auto_tac (claset(),
1.429 - simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
1.430 -qed "hypreal_epsilon_not_zero";
1.431 -
1.432 -Goal "epsilon = inverse(omega)";
1.433 -by (asm_full_simp_tac (simpset() addsimps
1.434 - [hypreal_inverse, omega_def, epsilon_def]) 1);
1.435 -qed "hypreal_epsilon_inverse_omega";
1.436 -
1.437 -
1.438 -(* this proof is so much simpler than one for reals!! *)
1.439 -Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
1.440 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
1.441 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
1.442 -by (auto_tac (claset(),
1.443 - simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def]));
1.444 -by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1);
1.445 -qed "hypreal_inverse_less_swap";
1.446 -
1.447 -Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
1.448 -by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
1.449 -by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
1.450 -by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
1.451 -by (rtac hypreal_inverse_less_swap 1);
1.452 -by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_gt_0]));
1.453 -qed "hypreal_inverse_less_iff";
1.454 -
1.455 -Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)";
1.456 -by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
1.457 - hypreal_inverse_gt_0]) 1);
1.458 -qed "hypreal_mult_inverse_less_mono1";
1.459 -
1.460 -Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y";
1.461 -by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
1.462 - hypreal_inverse_gt_0]) 1);
1.463 -qed "hypreal_mult_inverse_less_mono2";
1.464 -
1.465 -Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
1.466 -by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1);
1.467 -by (dtac (hypreal_not_refl2 RS not_sym) 2);
1.468 -by (auto_tac (claset() addSDs [hypreal_mult_inverse],
1.469 - simpset() addsimps hypreal_mult_ac));
1.470 -qed "hypreal_less_mult_right_cancel";
1.471 -
1.472 -Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
1.473 -by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
1.474 - simpset() addsimps [hypreal_mult_commute]));
1.475 -qed "hypreal_less_mult_left_cancel";
1.476 -
1.477 -Goal "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y";
1.478 -by (forw_inst_tac [("y","r")] order_less_trans 1);
1.479 -by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
1.480 -by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
1.481 -by (auto_tac (claset() addIs [order_less_trans], simpset()));
1.482 -qed "hypreal_mult_less_gt_zero";
1.483 -
1.484 -Goal "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y";
1.485 -by (REPEAT(dtac order_le_imp_less_or_eq 1));
1.486 -by (rtac hypreal_less_or_eq_imp_le 1);
1.487 -by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
1.488 - hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
1.489 - simpset()));
1.490 -qed "hypreal_mult_le_ge_zero";
1.491 -
1.492 -(*----------------------------------------------------------------------------
1.493 - Some convenient biconditionals for products of signs
1.494 - ----------------------------------------------------------------------------*)
1.495 -
1.496 -Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
1.497 - by (auto_tac (claset(),
1.498 - simpset() addsimps [order_le_less, linorder_not_less,
1.499 - hypreal_mult_order, hypreal_mult_less_zero1]));
1.500 -by (ALLGOALS (rtac ccontr));
1.501 -by (auto_tac (claset(),
1.502 - simpset() addsimps [order_le_less, linorder_not_less]));
1.503 -by (ALLGOALS (etac rev_mp));
1.504 -by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
1.505 -by (auto_tac (claset() addDs [order_less_not_sym],
1.506 - simpset() addsimps [hypreal_mult_commute]));
1.507 -qed "hypreal_0_less_mult_iff";
1.508 -
1.509 -Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
1.510 -by (auto_tac (claset() addDs [hypreal_mult_zero_disj],
1.511 - simpset() addsimps [order_le_less, linorder_not_less,
1.512 - hypreal_0_less_mult_iff]));
1.513 -qed "hypreal_0_le_mult_iff";
1.514 -
1.515 -Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
1.516 -by (auto_tac (claset(),
1.517 - simpset() addsimps [hypreal_0_le_mult_iff,
1.518 - linorder_not_le RS sym]));
1.519 -by (auto_tac (claset() addDs [order_less_not_sym],
1.520 - simpset() addsimps [linorder_not_le]));
1.521 -qed "hypreal_mult_less_0_iff";
1.522 -
1.523 -Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
1.524 -by (auto_tac (claset() addDs [order_less_not_sym],
1.525 - simpset() addsimps [hypreal_0_less_mult_iff,
1.526 - linorder_not_less RS sym]));
1.527 -qed "hypreal_mult_le_0_iff";
1.528 -
1.529 -Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
1.530 -by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
1.531 - hypreal_mult_less_zero]));
1.532 -qed "hypreal_mult_less_zero2";
2.1 --- a/src/HOL/Hyperreal/HyperOrd.thy Mon Dec 15 17:08:41 2003 +0100
2.2 +++ b/src/HOL/Hyperreal/HyperOrd.thy Tue Dec 16 15:38:09 2003 +0100
2.3 @@ -5,11 +5,543 @@
2.4 satisfies plus_ac0: + is an AC-operator with zero
2.5 *)
2.6
2.7 -HyperOrd = HyperDef +
2.8 +theory HyperOrd = HyperDef:
2.9
2.10 -instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
2.11 -instance hypreal :: linorder (hypreal_le_linear)
2.12
2.13 -instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)
2.14 +method_setup fuf = {*
2.15 + Method.ctxt_args (fn ctxt =>
2.16 + Method.METHOD (fn facts =>
2.17 + fuf_tac (Classical.get_local_claset ctxt,
2.18 + Simplifier.get_local_simpset ctxt) 1)) *}
2.19 + "free ultrafilter tactic"
2.20 +
2.21 +method_setup ultra = {*
2.22 + Method.ctxt_args (fn ctxt =>
2.23 + Method.METHOD (fn facts =>
2.24 + ultra_tac (Classical.get_local_claset ctxt,
2.25 + Simplifier.get_local_simpset ctxt) 1)) *}
2.26 + "ultrafilter tactic"
2.27 +
2.28 +
2.29 +instance hypreal :: order
2.30 + by (intro_classes,
2.31 + (assumption |
2.32 + rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym
2.33 + hypreal_less_le)+)
2.34 +
2.35 +instance hypreal :: linorder
2.36 + by (intro_classes, rule hypreal_le_linear)
2.37 +
2.38 +instance hypreal :: plus_ac0
2.39 + by (intro_classes,
2.40 + (assumption |
2.41 + rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
2.42 +
2.43 +(**** The simproc abel_cancel ****)
2.44 +
2.45 +(*** Two lemmas needed for the simprocs ***)
2.46 +
2.47 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
2.48 +lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)"
2.49 +apply (subst hypreal_add_left_commute)
2.50 +apply (rule hypreal_add_left_cancel)
2.51 +done
2.52 +
2.53 +(*A further rule to deal with the case that
2.54 + everything gets cancelled on the right.*)
2.55 +lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)"
2.56 +apply (subst hypreal_add_left_commute)
2.57 +apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel)
2.58 +apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric])
2.59 +done
2.60 +
2.61 +ML{*
2.62 +val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21";
2.63 +val hypreal_add_cancel_end = thm "hypreal_add_cancel_end";
2.64 +
2.65 +structure Hyperreal_Cancel_Data =
2.66 +struct
2.67 + val ss = HOL_ss
2.68 + val eq_reflection = eq_reflection
2.69 +
2.70 + val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
2.71 + val T = Type("HyperDef.hypreal",[])
2.72 + val zero = Const ("0", T)
2.73 + val restrict_to_left = restrict_to_left
2.74 + val add_cancel_21 = hypreal_add_cancel_21
2.75 + val add_cancel_end = hypreal_add_cancel_end
2.76 + val add_left_cancel = hypreal_add_left_cancel
2.77 + val add_assoc = hypreal_add_assoc
2.78 + val add_commute = hypreal_add_commute
2.79 + val add_left_commute = hypreal_add_left_commute
2.80 + val add_0 = hypreal_add_zero_left
2.81 + val add_0_right = hypreal_add_zero_right
2.82 +
2.83 + val eq_diff_eq = hypreal_eq_diff_eq
2.84 + val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
2.85 + fun dest_eqI th =
2.86 + #1 (HOLogic.dest_bin "op =" HOLogic.boolT
2.87 + (HOLogic.dest_Trueprop (concl_of th)))
2.88 +
2.89 + val diff_def = hypreal_diff_def
2.90 + val minus_add_distrib = hypreal_minus_add_distrib
2.91 + val minus_minus = hypreal_minus_minus
2.92 + val minus_0 = hypreal_minus_zero
2.93 + val add_inverses = [hypreal_add_minus, hypreal_add_minus_left]
2.94 + val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
2.95 +end;
2.96 +
2.97 +structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
2.98 +
2.99 +Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
2.100 +*}
2.101 +
2.102 +lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)"
2.103 +apply (simp (no_asm))
2.104 +done
2.105 +declare hypreal_minus_diff_eq [simp]
2.106 +
2.107 +
2.108 +lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)"
2.109 +apply (subst hypreal_less_minus_iff)
2.110 +apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst])
2.111 +apply (simp (no_asm) add: hypreal_add_commute)
2.112 +done
2.113 +
2.114 +lemma hypreal_gt_zero_iff:
2.115 + "((0::hypreal) < x) = (-x < x)"
2.116 +apply (unfold hypreal_zero_def)
2.117 +apply (rule_tac z = x in eq_Abs_hypreal)
2.118 +apply (auto simp add: hypreal_less hypreal_minus, ultra+)
2.119 +done
2.120 +
2.121 +lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C"
2.122 +apply (rule_tac z = A in eq_Abs_hypreal)
2.123 +apply (rule_tac z = B in eq_Abs_hypreal)
2.124 +apply (rule_tac z = C in eq_Abs_hypreal)
2.125 +apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
2.126 +done
2.127 +
2.128 +lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B"
2.129 +by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute)
2.130 +
2.131 +lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)"
2.132 +apply (rule hypreal_minus_zero_less_iff [THEN subst])
2.133 +apply (subst hypreal_gt_zero_iff)
2.134 +apply (simp (no_asm_use))
2.135 +done
2.136 +
2.137 +lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"
2.138 +apply (unfold hypreal_zero_def)
2.139 +apply (rule_tac z = x in eq_Abs_hypreal)
2.140 +apply (rule_tac z = y in eq_Abs_hypreal)
2.141 +apply (auto simp add: hypreal_less_def hypreal_add)
2.142 +apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
2.143 +done
2.144 +
2.145 +lemma hypreal_add_order_le: "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"
2.146 +by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order)
2.147 +
2.148 +lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"
2.149 +apply (unfold hypreal_zero_def)
2.150 +apply (rule_tac z = x in eq_Abs_hypreal)
2.151 +apply (rule_tac z = y in eq_Abs_hypreal)
2.152 +apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra)
2.153 +apply (auto intro: real_mult_order)
2.154 +done
2.155 +
2.156 +lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"
2.157 +apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+
2.158 +apply (drule hypreal_mult_order, assumption, simp)
2.159 +done
2.160 +
2.161 +lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"
2.162 +apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
2.163 +apply (drule hypreal_mult_order, assumption)
2.164 +apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp)
2.165 +done
2.166 +
2.167 +lemma hypreal_zero_less_one: "0 < (1::hypreal)"
2.168 +apply (unfold hypreal_one_def hypreal_zero_def hypreal_less_def)
2.169 +apply (rule_tac x = "%n. 0" in exI)
2.170 +apply (rule_tac x = "%n. 1" in exI)
2.171 +apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set)
2.172 +done
2.173 +
2.174 +lemma hypreal_le_add_order: "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"
2.175 +apply (drule order_le_imp_less_or_eq)+
2.176 +apply (auto intro: hypreal_add_order order_less_imp_le)
2.177 +done
2.178 +
2.179 +(*** Monotonicity results ***)
2.180 +
2.181 +lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
2.182 +apply (simp (no_asm))
2.183 +done
2.184 +
2.185 +lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
2.186 +apply (simp (no_asm))
2.187 +done
2.188 +
2.189 +declare hypreal_add_right_cancel_less [simp]
2.190 + hypreal_add_left_cancel_less [simp]
2.191 +
2.192 +lemma hypreal_add_right_cancel_le: "(v+z <= w+z) = (v <= (w::hypreal))"
2.193 +apply (simp (no_asm))
2.194 +done
2.195 +
2.196 +lemma hypreal_add_left_cancel_le: "(z+v <= z+w) = (v <= (w::hypreal))"
2.197 +apply (simp (no_asm))
2.198 +done
2.199 +
2.200 +declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp]
2.201 +
2.202 +lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"
2.203 +apply (drule hypreal_less_minus_iff [THEN iffD1])
2.204 +apply (drule hypreal_less_minus_iff [THEN iffD1])
2.205 +apply (drule hypreal_add_order, assumption)
2.206 +apply (erule_tac V = "0 < y2 + - z2" in thin_rl)
2.207 +apply (drule_tac C = "z1 + z2" in hypreal_add_less_mono1)
2.208 +apply (auto simp add: hypreal_minus_add_distrib [symmetric]
2.209 + hypreal_add_ac simp del: hypreal_minus_add_distrib)
2.210 +done
2.211 +
2.212 +lemma hypreal_add_left_le_mono1: "(q1::hypreal) <= q2 ==> x + q1 <= x + q2"
2.213 +apply (drule order_le_imp_less_or_eq)
2.214 +apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute)
2.215 +done
2.216 +
2.217 +lemma hypreal_add_le_mono1: "(q1::hypreal) <= q2 ==> q1 + x <= q2 + x"
2.218 +by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute)
2.219 +
2.220 +lemma hypreal_add_le_mono: "[|(i::hypreal)<=j; k<=l |] ==> i + k <= j + l"
2.221 +apply (erule hypreal_add_le_mono1 [THEN order_trans])
2.222 +apply (simp (no_asm))
2.223 +done
2.224 +
2.225 +lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j; k<=l |] ==> i + k < j + l"
2.226 +by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
2.227 +
2.228 +lemma hypreal_add_le_less_mono: "[|(i::hypreal)<=j; k<l |] ==> i + k < j + l"
2.229 +by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono)
2.230 +
2.231 +lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
2.232 +apply (simp (no_asm_use))
2.233 +done
2.234 +
2.235 +lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
2.236 +apply (simp (no_asm_use))
2.237 +done
2.238 +
2.239 +lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) <= y|] ==> r < x + y"
2.240 +by (auto dest: hypreal_add_less_le_mono)
2.241 +
2.242 +lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C <= B + C ==> A <= B"
2.243 +apply (drule_tac x = "-C" in hypreal_add_le_mono1)
2.244 +apply (simp add: hypreal_add_assoc)
2.245 +done
2.246 +
2.247 +lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A <= C + B ==> A <= B"
2.248 +apply (drule_tac x = "-C" in hypreal_add_left_le_mono1)
2.249 +apply (simp add: hypreal_add_assoc [symmetric])
2.250 +done
2.251 +
2.252 +lemma hypreal_le_square: "(0::hypreal) <= x*x"
2.253 +apply (rule_tac x = 0 and y = x in hypreal_linear_less2)
2.254 +apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le)
2.255 +done
2.256 +declare hypreal_le_square [simp]
2.257 +
2.258 +lemma hypreal_less_minus_square: "- (x*x) <= (0::hypreal)"
2.259 +apply (unfold hypreal_le_def)
2.260 +apply (auto dest!: hypreal_le_square [THEN order_le_less_trans]
2.261 + simp add: hypreal_minus_zero_less_iff)
2.262 +done
2.263 +declare hypreal_less_minus_square [simp]
2.264 +
2.265 +lemma hypreal_mult_0_less: "(0*x<r)=((0::hypreal)<r)"
2.266 +apply (simp (no_asm))
2.267 +done
2.268 +
2.269 +lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"
2.270 +apply (rotate_tac 1)
2.271 +apply (drule hypreal_less_minus_iff [THEN iffD1])
2.272 +apply (rule hypreal_less_minus_iff [THEN iffD2])
2.273 +apply (drule hypreal_mult_order, assumption)
2.274 +apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute)
2.275 +done
2.276 +
2.277 +lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
2.278 +apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1)
2.279 +done
2.280 +
2.281 +lemma hypreal_mult_le_less_mono1: "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"
2.282 +apply (rule hypreal_less_or_eq_imp_le)
2.283 +apply (drule order_le_imp_less_or_eq)
2.284 +apply (auto intro: hypreal_mult_less_mono1)
2.285 +done
2.286 +
2.287 +lemma hypreal_mult_le_less_mono2: "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"
2.288 +apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_le_less_mono1)
2.289 +done
2.290 +
2.291 +lemma hypreal_mult_less_mono: "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
2.292 +apply (erule hypreal_mult_less_mono1 [THEN order_less_trans], assumption)
2.293 +apply (erule hypreal_mult_less_mono2, assumption)
2.294 +done
2.295 +
2.296 +(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
2.297 +lemma hypreal_mult_less_mono': "[| x < y; r1 < r2; (0::hypreal) <= r1; 0 <= x|] ==> r1 * x < r2 * y"
2.298 +apply (subgoal_tac "0<r2")
2.299 +prefer 2 apply (blast intro: order_le_less_trans)
2.300 +apply (case_tac "x=0")
2.301 +apply (auto dest!: order_le_imp_less_or_eq intro: hypreal_mult_less_mono hypreal_mult_order)
2.302 +done
2.303 +
2.304 +lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
2.305 +apply (rule ccontr)
2.306 +apply (drule hypreal_leI)
2.307 +apply (frule hypreal_minus_zero_less_iff2 [THEN iffD2])
2.308 +apply (frule hypreal_not_refl2 [THEN not_sym])
2.309 +apply (drule hypreal_not_refl2 [THEN not_sym, THEN hypreal_inverse_not_zero])
2.310 +apply (drule order_le_imp_less_or_eq, safe)
2.311 +apply (drule hypreal_mult_less_zero1, assumption)
2.312 +apply (auto intro: hypreal_zero_less_one [THEN hypreal_less_asym]
2.313 + simp add: hypreal_minus_zero_less_iff)
2.314 +done
2.315 +
2.316 +lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
2.317 +apply (frule hypreal_not_refl2)
2.318 +apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
2.319 +apply (rule hypreal_minus_zero_less_iff [THEN iffD1])
2.320 +apply (subst hypreal_minus_inverse [symmetric])
2.321 +apply (auto intro: hypreal_inverse_gt_0)
2.322 +done
2.323 +
2.324 +lemma hypreal_self_le_add_pos: "(x::hypreal)*x <= x*x + y*y"
2.325 +apply (rule_tac z = x in eq_Abs_hypreal)
2.326 +apply (rule_tac z = y in eq_Abs_hypreal)
2.327 +apply (auto simp add: hypreal_mult hypreal_add hypreal_le)
2.328 +done
2.329 +declare hypreal_self_le_add_pos [simp]
2.330 +
2.331 +(*lcp: new lemma unfortunately needed...*)
2.332 +lemma minus_square_le_square: "-(x*x) <= (y*y::real)"
2.333 +apply (rule order_trans)
2.334 +apply (rule_tac [2] real_le_square, auto)
2.335 +done
2.336 +
2.337 +lemma hypreal_self_le_add_pos2: "(x::hypreal)*x <= x*x + y*y + z*z"
2.338 +apply (rule_tac z = x in eq_Abs_hypreal)
2.339 +apply (rule_tac z = y in eq_Abs_hypreal)
2.340 +apply (rule_tac z = z in eq_Abs_hypreal)
2.341 +apply (auto simp add: hypreal_mult hypreal_add hypreal_le minus_square_le_square)
2.342 +done
2.343 +declare hypreal_self_le_add_pos2 [simp]
2.344 +
2.345 +
2.346 +(*----------------------------------------------------------------------------
2.347 + Existence of infinite hyperreal number
2.348 + ----------------------------------------------------------------------------*)
2.349 +
2.350 +lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal"
2.351 +
2.352 +apply (unfold omega_def)
2.353 +apply (rule Rep_hypreal)
2.354 +done
2.355 +
2.356 +(* existence of infinite number not corresponding to any real number *)
2.357 +(* use assumption that member FreeUltrafilterNat is not finite *)
2.358 +(* a few lemmas first *)
2.359 +
2.360 +lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
2.361 + (EX y. {n::nat. x = real n} = {y})"
2.362 +by (force dest: inj_real_of_nat [THEN injD])
2.363 +
2.364 +lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
2.365 +by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
2.366 +
2.367 +lemma not_ex_hypreal_of_real_eq_omega:
2.368 + "~ (EX x. hypreal_of_real x = omega)"
2.369 +apply (unfold omega_def hypreal_of_real_def)
2.370 +apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
2.371 +done
2.372 +
2.373 +lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega"
2.374 +by (cut_tac not_ex_hypreal_of_real_eq_omega, auto)
2.375 +
2.376 +(* existence of infinitesimal number also not *)
2.377 +(* corresponding to any real number *)
2.378 +
2.379 +lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y"
2.380 +by (rule inj_real_of_nat [THEN injD], simp)
2.381 +
2.382 +lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} |
2.383 + (EX y. {n::nat. x = inverse(real(Suc n))} = {y})"
2.384 +apply (auto simp add: inj_real_of_nat [THEN inj_eq])
2.385 +done
2.386 +
2.387 +lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
2.388 +by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
2.389 +
2.390 +lemma not_ex_hypreal_of_real_eq_epsilon:
2.391 + "~ (EX x. hypreal_of_real x = epsilon)"
2.392 +apply (unfold epsilon_def hypreal_of_real_def)
2.393 +apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
2.394 +done
2.395 +
2.396 +lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon"
2.397 +by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
2.398 +
2.399 +lemma hypreal_epsilon_not_zero: "epsilon ~= 0"
2.400 +by (unfold epsilon_def hypreal_zero_def, auto)
2.401 +
2.402 +lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
2.403 +by (simp add: hypreal_inverse omega_def epsilon_def)
2.404 +
2.405 +
2.406 +(* this proof is so much simpler than one for reals!! *)
2.407 +lemma hypreal_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"
2.408 +apply (rule_tac z = x in eq_Abs_hypreal)
2.409 +apply (rule_tac z = r in eq_Abs_hypreal)
2.410 +apply (auto simp add: hypreal_inverse hypreal_less hypreal_zero_def, ultra)
2.411 +done
2.412 +
2.413 +lemma hypreal_inverse_less_iff: "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"
2.414 +apply (auto intro: hypreal_inverse_less_swap)
2.415 +apply (rule_tac t = r in hypreal_inverse_inverse [THEN subst])
2.416 +apply (rule_tac t = x in hypreal_inverse_inverse [THEN subst])
2.417 +apply (rule hypreal_inverse_less_swap)
2.418 +apply (auto simp add: hypreal_inverse_gt_0)
2.419 +done
2.420 +
2.421 +lemma hypreal_mult_inverse_less_mono1: "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)"
2.422 +by (blast intro!: hypreal_mult_less_mono1 hypreal_inverse_gt_0)
2.423 +
2.424 +lemma hypreal_mult_inverse_less_mono2: "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y"
2.425 +by (blast intro!: hypreal_mult_less_mono2 hypreal_inverse_gt_0)
2.426 +
2.427 +lemma hypreal_less_mult_right_cancel: "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"
2.428 +apply (frule_tac x = "x*z" in hypreal_mult_inverse_less_mono1)
2.429 +apply (drule_tac [2] hypreal_not_refl2 [THEN not_sym])
2.430 +apply (auto dest!: hypreal_mult_inverse simp add: hypreal_mult_ac)
2.431 +done
2.432 +
2.433 +lemma hypreal_less_mult_left_cancel: "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"
2.434 +by (auto intro: hypreal_less_mult_right_cancel simp add: hypreal_mult_commute)
2.435 +
2.436 +lemma hypreal_mult_less_gt_zero: "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y"
2.437 +apply (frule_tac y = r in order_less_trans)
2.438 +apply (drule_tac [2] z = ra and x = r in hypreal_mult_less_mono1)
2.439 +apply (drule_tac [3] z = x and x = ra in hypreal_mult_less_mono2)
2.440 +apply (auto intro: order_less_trans)
2.441 +done
2.442 +
2.443 +lemma hypreal_mult_le_ge_zero: "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y"
2.444 +apply (drule order_le_imp_less_or_eq)+
2.445 +apply (rule hypreal_less_or_eq_imp_le)
2.446 +apply (auto intro: hypreal_mult_less_mono1 hypreal_mult_less_mono2 hypreal_mult_less_gt_zero)
2.447 +done
2.448 +
2.449 +(*----------------------------------------------------------------------------
2.450 + Some convenient biconditionals for products of signs
2.451 + ----------------------------------------------------------------------------*)
2.452 +
2.453 +lemma hypreal_0_less_mult_iff: "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
2.454 + apply (auto simp add: order_le_less linorder_not_less hypreal_mult_order hypreal_mult_less_zero1)
2.455 +apply (rule_tac [!] ccontr)
2.456 +apply (auto simp add: order_le_less linorder_not_less)
2.457 +apply (erule_tac [!] rev_mp)
2.458 +apply (drule_tac [!] hypreal_mult_less_zero)
2.459 +apply (auto dest: order_less_not_sym simp add: hypreal_mult_commute)
2.460 +done
2.461 +
2.462 +lemma hypreal_0_le_mult_iff: "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"
2.463 +by (auto dest: hypreal_mult_zero_disj simp add: order_le_less linorder_not_less hypreal_0_less_mult_iff)
2.464 +
2.465 +lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"
2.466 +apply (auto simp add: hypreal_0_le_mult_iff linorder_not_le [symmetric])
2.467 +apply (auto dest: order_less_not_sym simp add: linorder_not_le)
2.468 +done
2.469 +
2.470 +lemma hypreal_mult_le_0_iff: "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"
2.471 +by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric])
2.472 +
2.473 +lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0"
2.474 +by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero)
2.475 +
2.476 +
2.477 +ML
2.478 +{*
2.479 +val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21";
2.480 +val hypreal_add_cancel_end = thm"hypreal_add_cancel_end";
2.481 +val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq";
2.482 +val hypreal_less_swap_iff = thm"hypreal_less_swap_iff";
2.483 +val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff";
2.484 +val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1";
2.485 +val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2";
2.486 +val hypreal_lt_zero_iff = thm"hypreal_lt_zero_iff";
2.487 +val hypreal_add_order = thm"hypreal_add_order";
2.488 +val hypreal_add_order_le = thm"hypreal_add_order_le";
2.489 +val hypreal_mult_order = thm"hypreal_mult_order";
2.490 +val hypreal_mult_less_zero1 = thm"hypreal_mult_less_zero1";
2.491 +val hypreal_mult_less_zero = thm"hypreal_mult_less_zero";
2.492 +val hypreal_zero_less_one = thm"hypreal_zero_less_one";
2.493 +val hypreal_le_add_order = thm"hypreal_le_add_order";
2.494 +val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less";
2.495 +val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less";
2.496 +val hypreal_add_right_cancel_le = thm"hypreal_add_right_cancel_le";
2.497 +val hypreal_add_left_cancel_le = thm"hypreal_add_left_cancel_le";
2.498 +val hypreal_add_less_mono = thm"hypreal_add_less_mono";
2.499 +val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1";
2.500 +val hypreal_add_le_mono1 = thm"hypreal_add_le_mono1";
2.501 +val hypreal_add_le_mono = thm"hypreal_add_le_mono";
2.502 +val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono";
2.503 +val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono";
2.504 +val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel";
2.505 +val hypreal_less_add_left_cancel = thm"hypreal_less_add_left_cancel";
2.506 +val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono";
2.507 +val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel";
2.508 +val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel";
2.509 +val hypreal_le_square = thm"hypreal_le_square";
2.510 +val hypreal_less_minus_square = thm"hypreal_less_minus_square";
2.511 +val hypreal_mult_0_less = thm"hypreal_mult_0_less";
2.512 +val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1";
2.513 +val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
2.514 +val hypreal_mult_le_less_mono1 = thm"hypreal_mult_le_less_mono1";
2.515 +val hypreal_mult_le_less_mono2 = thm"hypreal_mult_le_less_mono2";
2.516 +val hypreal_mult_less_mono = thm"hypreal_mult_less_mono";
2.517 +val hypreal_mult_less_mono' = thm"hypreal_mult_less_mono'";
2.518 +val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0";
2.519 +val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0";
2.520 +val hypreal_self_le_add_pos = thm"hypreal_self_le_add_pos";
2.521 +val minus_square_le_square = thm"minus_square_le_square";
2.522 +val hypreal_self_le_add_pos2 = thm"hypreal_self_le_add_pos2";
2.523 +val Rep_hypreal_omega = thm"Rep_hypreal_omega";
2.524 +val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
2.525 +val lemma_finite_omega_set = thm"lemma_finite_omega_set";
2.526 +val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
2.527 +val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
2.528 +val real_of_nat_inverse_inj = thm"real_of_nat_inverse_inj";
2.529 +val lemma_epsilon_empty_singleton_disj = thm"lemma_epsilon_empty_singleton_disj";
2.530 +val lemma_finite_epsilon_set = thm"lemma_finite_epsilon_set";
2.531 +val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
2.532 +val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
2.533 +val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
2.534 +val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
2.535 +val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap";
2.536 +val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff";
2.537 +val hypreal_mult_inverse_less_mono1 = thm"hypreal_mult_inverse_less_mono1";
2.538 +val hypreal_mult_inverse_less_mono2 = thm"hypreal_mult_inverse_less_mono2";
2.539 +val hypreal_less_mult_right_cancel = thm"hypreal_less_mult_right_cancel";
2.540 +val hypreal_less_mult_left_cancel = thm"hypreal_less_mult_left_cancel";
2.541 +val hypreal_mult_less_gt_zero = thm"hypreal_mult_less_gt_zero";
2.542 +val hypreal_mult_le_ge_zero = thm"hypreal_mult_le_ge_zero";
2.543 +val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff";
2.544 +val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff";
2.545 +val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff";
2.546 +val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff";
2.547 +val hypreal_mult_less_zero2 = thm"hypreal_mult_less_zero2";
2.548 +*}
2.549
2.550 end
3.1 --- a/src/HOL/Hyperreal/fuf.ML Mon Dec 15 17:08:41 2003 +0100
3.2 +++ b/src/HOL/Hyperreal/fuf.ML Tue Dec 16 15:38:09 2003 +0100
3.3 @@ -60,14 +60,6 @@
3.4
3.5
3.6 (*---------------------------------------------------------------
3.7 - All in one -- not really needed.
3.8 - ---------------------------------------------------------------*)
3.9 -
3.10 -fun fuf_auto_tac css i = SOLVE (fuf_empty_tac css i) ORELSE TRY (fuf_tac css i);
3.11 -fun Fuf_auto_tac i = fuf_auto_tac (clasimpset ()) i;
3.12 -
3.13 -
3.14 -(*---------------------------------------------------------------
3.15 In fact could make this the only tactic: just need to
3.16 use contraposition and then look for empty set.
3.17 ---------------------------------------------------------------*)
4.1 --- a/src/HOL/IsaMakefile Mon Dec 15 17:08:41 2003 +0100
4.2 +++ b/src/HOL/IsaMakefile Tue Dec 16 15:38:09 2003 +0100
4.3 @@ -153,7 +153,7 @@
4.4 Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
4.5 Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\
4.6 Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
4.7 - Hyperreal/HyperOrd.ML Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
4.8 + Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
4.9 Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
4.10 Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.ML Hyperreal/Log.thy\
4.11 Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\