src/HOL/Real/Hyperreal/HyperDef.ML
changeset 10043 a0364652e115
parent 9969 4753185f1dd2
child 10607 352f6f209775
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -132,15 +132,13 @@
     1.4  by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
     1.5  qed "FreeUltrafilterNat_all";
     1.6  
     1.7 -(*-----------------------------------------
     1.8 +(*-------------------------------------------------------
     1.9       Define and use Ultrafilter tactics
    1.10 - -----------------------------------------*)
    1.11 + -------------------------------------------------------*)
    1.12  use "fuf.ML";
    1.13  
    1.14 -
    1.15 -
    1.16 -(*------------------------------------------------------
    1.17 -   Now prove one further property of our free ultrafilter
    1.18 +(*-------------------------------------------------------
    1.19 +  Now prove one further property of our free ultrafilter
    1.20   -------------------------------------------------------*)
    1.21  Goal "X Un Y: FreeUltrafilterNat \
    1.22  \     ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
    1.23 @@ -148,9 +146,9 @@
    1.24  by (Ultra_tac 1);
    1.25  qed "FreeUltrafilterNat_Un";
    1.26  
    1.27 -(*------------------------------------------------------------------------
    1.28 -                       Properties of hyprel
    1.29 - ------------------------------------------------------------------------*)
    1.30 +(*-------------------------------------------------------
    1.31 +   Properties of hyprel
    1.32 + -------------------------------------------------------*)
    1.33  
    1.34  (** Proving that hyprel is an equivalence relation **)
    1.35  (** Natural deduction for hyprel **)
    1.36 @@ -453,10 +451,10 @@
    1.37  by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
    1.38      hypreal_add,real_minus_add_distrib]));
    1.39  qed "hypreal_minus_add_distrib";
    1.40 +Addsimps [hypreal_minus_add_distrib];
    1.41  
    1.42  Goal "-(y + -(x::hypreal)) = x + -y";
    1.43 -by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
    1.44 -    hypreal_add_commute]) 1);
    1.45 +by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
    1.46  qed "hypreal_minus_distrib1";
    1.47  
    1.48  Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
    1.49 @@ -478,21 +476,21 @@
    1.50  Addsimps [hypreal_add_minus_cancel2];
    1.51  
    1.52  Goal "y + -(x + y) = -(x::hypreal)";
    1.53 -by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
    1.54 +by (Full_simp_tac 1);
    1.55  by (rtac (hypreal_add_left_commute RS subst) 1);
    1.56  by (Full_simp_tac 1);
    1.57  qed "hypreal_add_minus_cancel";
    1.58  Addsimps [hypreal_add_minus_cancel];
    1.59  
    1.60  Goal "y + -(y + x) = -(x::hypreal)";
    1.61 -by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
    1.62 -              hypreal_add_assoc RS sym]) 1);
    1.63 +by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
    1.64  qed "hypreal_add_minus_cancelc";
    1.65  Addsimps [hypreal_add_minus_cancelc];
    1.66  
    1.67  Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
    1.68  by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
    1.69 -    RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
    1.70 +    RS sym, hypreal_add_left_cancel] @ hypreal_add_ac 
    1.71 +    delsimps [hypreal_minus_add_distrib]) 1); 
    1.72  qed "hypreal_add_minus_cancel3";
    1.73  Addsimps [hypreal_add_minus_cancel3];
    1.74  
    1.75 @@ -511,6 +509,15 @@
    1.76  qed "hypreal_add_minus_cancel5";
    1.77  Addsimps [hypreal_add_minus_cancel5];
    1.78  
    1.79 +Goal "z + ((- z) + w) = (w::hypreal)";
    1.80 +by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
    1.81 +qed "hypreal_add_minus_cancelA";
    1.82 +
    1.83 +Goal "(-z) + (z + w) = (w::hypreal)";
    1.84 +by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
    1.85 +qed "hypreal_minus_add_cancelA";
    1.86 +
    1.87 +Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
    1.88  
    1.89  (**** hyperreal multiplication: hypreal_mult  ****)
    1.90  
    1.91 @@ -594,7 +601,6 @@
    1.92  by Auto_tac;
    1.93  qed "hypreal_minus_mult_commute";
    1.94  
    1.95 -
    1.96  (*-----------------------------------------------------------------------------
    1.97      A few more theorems
    1.98   ----------------------------------------------------------------------------*)
    1.99 @@ -623,6 +629,17 @@
   1.100  bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
   1.101  Addsimps hypreal_mult_simps;
   1.102  
   1.103 +(* 07/00 *)
   1.104 +
   1.105 +Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
   1.106 +by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
   1.107 +qed "hypreal_diff_mult_distrib";
   1.108 +
   1.109 +Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
   1.110 +by (simp_tac (simpset() addsimps [hypreal_mult_commute', 
   1.111 +				  hypreal_diff_mult_distrib]) 1);
   1.112 +qed "hypreal_diff_mult_distrib2";
   1.113 +
   1.114  (*** one and zero are distinct ***)
   1.115  Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
   1.116  by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
   1.117 @@ -715,6 +732,11 @@
   1.118  
   1.119  bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
   1.120  
   1.121 +Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
   1.122 +by (auto_tac (claset() addIs [ccontr] addDs 
   1.123 +    [hypreal_mult_not_0],simpset()));
   1.124 +qed "hypreal_mult_zero_disj";
   1.125 +
   1.126  Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
   1.127  by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
   1.128  qed "hypreal_mult_self_not_zero";
   1.129 @@ -789,6 +811,7 @@
   1.130  
   1.131  (*** y < y ==> P ***)
   1.132  bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   1.133 +AddSEs [hypreal_less_irrefl];
   1.134  
   1.135  Goal "!!(x::hypreal). x < y ==> x ~= y";
   1.136  by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
   1.137 @@ -809,7 +832,7 @@
   1.138      [hypreal_less_not_refl]) 1);
   1.139  qed "hypreal_less_asym";
   1.140  
   1.141 -(*--------------------------------------------------------
   1.142 +(*-------------------------------------------------------
   1.143    TODO: The following theorem should have been proved 
   1.144    first and then used througout the proofs as it probably 
   1.145    makes many of them more straightforward. 
   1.146 @@ -827,6 +850,7 @@
   1.147   ---------------------------------------------------------------------------------*)
   1.148  (*** sum order ***)
   1.149  
   1.150 +(***
   1.151  Goalw [hypreal_zero_def] 
   1.152        "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
   1.153  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.154 @@ -849,6 +873,8 @@
   1.155  by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
   1.156  	       simpset()) 1);
   1.157  qed "hypreal_mult_order";
   1.158 +****)
   1.159 +
   1.160  
   1.161  (*---------------------------------------------------------------------------------
   1.162                           Trichotomy of the hyperreals
   1.163 @@ -885,44 +911,23 @@
   1.164  (*----------------------------------------------------------------------------
   1.165              More properties of <
   1.166   ----------------------------------------------------------------------------*)
   1.167 -Goal "!!(A::hypreal). A < B ==> A + C < B + C";
   1.168 -by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
   1.169 -by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
   1.170 -by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
   1.171 -by (auto_tac (claset() addSIs [exI],simpset() addsimps
   1.172 -    [hypreal_less_def,hypreal_add]));
   1.173 -by (Ultra_tac 1);
   1.174 -qed "hypreal_add_less_mono1";
   1.175 -
   1.176 -Goal "!!(A::hypreal). A < B ==> C + A < C + B";
   1.177 -by (auto_tac (claset() addIs [hypreal_add_less_mono1],
   1.178 -    simpset() addsimps [hypreal_add_commute]));
   1.179 -qed "hypreal_add_less_mono2";
   1.180  
   1.181  Goal "((x::hypreal) < y) = (0 < y + -x)";
   1.182 -by (Step_tac 1);
   1.183 -by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
   1.184 -by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
   1.185 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.186 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.187 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.188 +by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   1.189 +    hypreal_zero_def,hypreal_minus,hypreal_less]));
   1.190 +by (ALLGOALS(Ultra_tac));
   1.191  qed "hypreal_less_minus_iff"; 
   1.192  
   1.193 -Goal "((x::hypreal) < y) = (x + -y< 0)";
   1.194 -by (Step_tac 1);
   1.195 -by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
   1.196 -by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
   1.197 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.198 +Goal "((x::hypreal) < y) = (x + -y < 0)";
   1.199 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.200 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.201 +by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   1.202 +    hypreal_zero_def,hypreal_minus,hypreal_less]));
   1.203 +by (ALLGOALS(Ultra_tac));
   1.204  qed "hypreal_less_minus_iff2";
   1.205  
   1.206 -Goal  "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
   1.207 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.208 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.209 -by (dtac hypreal_add_order 1 THEN assume_tac 1);
   1.210 -by (thin_tac "0 < y2 + - z2" 1);
   1.211 -by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
   1.212 -by (auto_tac (claset(),simpset() addsimps 
   1.213 -    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
   1.214 -qed "hypreal_add_less_mono";
   1.215 -
   1.216  Goal "((x::hypreal) = y) = (0 = x + - y)";
   1.217  by Auto_tac;
   1.218  by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   1.219 @@ -935,6 +940,21 @@
   1.220  by Auto_tac;
   1.221  qed "hypreal_eq_minus_iff2"; 
   1.222  
   1.223 +(* 07/00 *)
   1.224 +Goal "(0::hypreal) - x = -x";
   1.225 +by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   1.226 +qed "hypreal_diff_zero";
   1.227 +
   1.228 +Goal "x - (0::hypreal) = x";
   1.229 +by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   1.230 +qed "hypreal_diff_zero_right";
   1.231 +
   1.232 +Goal "x - x = (0::hypreal)";
   1.233 +by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   1.234 +qed "hypreal_diff_self";
   1.235 +
   1.236 +Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self];
   1.237 +
   1.238  Goal "(x = y + z) = (x + -z = (y::hypreal))";
   1.239  by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.240  qed "hypreal_eq_minus_iff3";
   1.241 @@ -957,6 +977,11 @@
   1.242  by Auto_tac;
   1.243  qed "hypreal_linear";
   1.244  
   1.245 +Goal "((w::hypreal) ~= z) = (w<z | z<w)";
   1.246 +by (cut_facts_tac [hypreal_linear] 1);
   1.247 +by (Blast_tac 1);
   1.248 +qed "hypreal_neq_iff";
   1.249 +
   1.250  Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
   1.251  \          y < x ==> P |] ==> P";
   1.252  by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
   1.253 @@ -1015,12 +1040,20 @@
   1.254  Goal "(x <= (y::hypreal)) = (x < y | x=y)";
   1.255  by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
   1.256  qed "hypreal_le_eq_less_or_eq";
   1.257 +val hypreal_le_less = hypreal_le_eq_less_or_eq;
   1.258  
   1.259  Goal "w <= (w::hypreal)";
   1.260  by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
   1.261  qed "hypreal_le_refl";
   1.262  Addsimps [hypreal_le_refl];
   1.263  
   1.264 +(* Axiom 'linorder_linear' of class 'linorder': *)
   1.265 +Goal "(z::hypreal) <= w | w <= z";
   1.266 +by (simp_tac (simpset() addsimps [hypreal_le_less]) 1);
   1.267 +by (cut_facts_tac [hypreal_linear] 1);
   1.268 +by (Blast_tac 1);
   1.269 +qed "hypreal_le_linear";
   1.270 +
   1.271  Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
   1.272  by (dtac hypreal_le_imp_less_or_eq 1);
   1.273  by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
   1.274 @@ -1041,217 +1074,35 @@
   1.275              fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
   1.276  qed "hypreal_le_anti_sym";
   1.277  
   1.278 -Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
   1.279 -by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
   1.280 -              addIs [hypreal_add_order],simpset()));
   1.281 -qed "hypreal_add_order_le";            
   1.282 -
   1.283 -(*------------------------------------------------------------------------
   1.284 - ------------------------------------------------------------------------*)
   1.285 -
   1.286  Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
   1.287  by (rtac not_hypreal_leE 1);
   1.288  by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
   1.289  qed "not_less_not_eq_hypreal_less";
   1.290  
   1.291 +(* Axiom 'order_less_le' of class 'order': *)
   1.292 +Goal "(w::hypreal) < z = (w <= z & w ~= z)";
   1.293 +by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
   1.294 +by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
   1.295 +qed "hypreal_less_le";
   1.296 +
   1.297  Goal "(0 < -R) = (R < (0::hypreal))";
   1.298 -by (Step_tac 1);
   1.299 -by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
   1.300 -by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
   1.301 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.302 +by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   1.303 +by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
   1.304 +    hypreal_less,hypreal_minus]));
   1.305  qed "hypreal_minus_zero_less_iff";
   1.306 +Addsimps [hypreal_minus_zero_less_iff];
   1.307  
   1.308  Goal "(-R < 0) = ((0::hypreal) < R)";
   1.309 -by (Step_tac 1);
   1.310 -by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
   1.311 -by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
   1.312 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.313 +by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   1.314 +by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
   1.315 +    hypreal_less,hypreal_minus]));
   1.316 +by (ALLGOALS(Ultra_tac));
   1.317  qed "hypreal_minus_zero_less_iff2";
   1.318  
   1.319 -Goal "((x::hypreal) < y) = (-y < -x)";
   1.320 -by (stac hypreal_less_minus_iff 1);
   1.321 -by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
   1.322 -by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.323 -qed "hypreal_less_swap_iff";
   1.324 -
   1.325 -Goal "((0::hypreal) < x) = (-x < x)";
   1.326 -by (Step_tac 1);
   1.327 -by (rtac ccontr 2 THEN forward_tac 
   1.328 -    [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
   1.329 -by (Step_tac 2);
   1.330 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
   1.331 -by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
   1.332 -by (Auto_tac );
   1.333 -by (ftac hypreal_add_order 1 THEN assume_tac 1);
   1.334 -by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
   1.335 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   1.336 -qed "hypreal_gt_zero_iff";
   1.337 -
   1.338 -Goal "(x < (0::hypreal)) = (x < -x)";
   1.339 -by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
   1.340 -by (stac hypreal_gt_zero_iff 1);
   1.341 -by (Full_simp_tac 1);
   1.342 -qed "hypreal_lt_zero_iff";
   1.343 -
   1.344 -Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
   1.345 -by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
   1.346 -qed "hypreal_ge_zero_iff";
   1.347 -
   1.348 -Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
   1.349 -by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
   1.350 -qed "hypreal_le_zero_iff";
   1.351 -
   1.352 -Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
   1.353 -by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
   1.354 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.355 -by (Asm_full_simp_tac 1);
   1.356 -qed "hypreal_mult_less_zero1";
   1.357 -
   1.358 -Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
   1.359 -by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.360 -by (auto_tac (claset() addIs [hypreal_mult_order,
   1.361 -    hypreal_less_imp_le],simpset()));
   1.362 -qed "hypreal_le_mult_order";
   1.363 -
   1.364 -Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
   1.365 -by (rtac hypreal_less_or_eq_imp_le 1);
   1.366 -by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.367 -by Auto_tac;
   1.368 -by (dtac hypreal_le_imp_less_or_eq 1);
   1.369 -by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
   1.370 -qed "real_mult_le_zero1";
   1.371 -
   1.372 -Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
   1.373 -by (rtac hypreal_less_or_eq_imp_le 1);
   1.374 -by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
   1.375 -by Auto_tac;
   1.376 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.377 -by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
   1.378 -by (blast_tac (claset() addDs [hypreal_mult_order] 
   1.379 -    addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
   1.380 -qed "hypreal_mult_le_zero";
   1.381 -
   1.382 -Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
   1.383 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.384 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.385 -by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.386 -by (Asm_full_simp_tac 1);
   1.387 -qed "hypreal_mult_less_zero";
   1.388 -
   1.389 -Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
   1.390 -by (res_inst_tac [("x","%n. #0")] exI 1);
   1.391 -by (res_inst_tac [("x","%n. #1")] exI 1);
   1.392 -by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
   1.393 -    FreeUltrafilterNat_Nat_set]));
   1.394 -qed "hypreal_zero_less_one";
   1.395 -
   1.396 -Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
   1.397 -by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.398 -by (auto_tac (claset() addIs [hypreal_add_order,
   1.399 -    hypreal_less_imp_le],simpset()));
   1.400 -qed "hypreal_le_add_order";
   1.401 -
   1.402 -Goal "!!(q1::hypreal). q1 <= q2  ==> x + q1 <= x + q2";
   1.403 -by (dtac hypreal_le_imp_less_or_eq 1);
   1.404 -by (Step_tac 1);
   1.405 -by (auto_tac (claset() addSIs [hypreal_le_refl,
   1.406 -    hypreal_less_imp_le,hypreal_add_less_mono1],
   1.407 -    simpset() addsimps [hypreal_add_commute]));
   1.408 -qed "hypreal_add_left_le_mono1";
   1.409 -
   1.410 -Goal "!!(q1::hypreal). q1 <= q2  ==> q1 + x <= q2 + x";
   1.411 -by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
   1.412 -    simpset() addsimps [hypreal_add_commute]));
   1.413 -qed "hypreal_add_le_mono1";
   1.414 -
   1.415 -Goal "!!k l::hypreal. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.416 -by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
   1.417 -by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   1.418 -(*j moves to the end because it is free while k, l are bound*)
   1.419 -by (etac hypreal_add_le_mono1 1);
   1.420 -qed "hypreal_add_le_mono";
   1.421 -
   1.422 -Goal "!!k l::hypreal. [|i<j;  k<=l |] ==> i + k < j + l";
   1.423 -by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.424 -    addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
   1.425 -qed "hypreal_add_less_le_mono";
   1.426 -
   1.427 -Goal "!!k l::hypreal. [|i<=j;  k<l |] ==> i + k < j + l";
   1.428 -by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
   1.429 -    addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
   1.430 -qed "hypreal_add_le_less_mono";
   1.431 -
   1.432 -Goal "(0*x<r)=((0::hypreal)<r)";
   1.433 -by (Simp_tac 1);
   1.434 -qed "hypreal_mult_0_less";
   1.435 -
   1.436 -Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";       
   1.437 -by (rotate_tac 1 1);
   1.438 -by (dtac (hypreal_less_minus_iff RS iffD1) 1);
   1.439 -by (rtac (hypreal_less_minus_iff RS iffD2) 1);
   1.440 -by (dtac hypreal_mult_order 1 THEN assume_tac 1);
   1.441 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
   1.442 -					   hypreal_mult_commute ]) 1);
   1.443 -qed "hypreal_mult_less_mono1";
   1.444 -
   1.445 -Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";       
   1.446 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
   1.447 -qed "hypreal_mult_less_mono2";
   1.448 -
   1.449 -Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
   1.450 -by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
   1.451 -by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
   1.452 -qed "hypreal_mult_le_less_mono1";
   1.453 -
   1.454 -Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
   1.455 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
   1.456 -				      hypreal_mult_le_less_mono1]) 1);
   1.457 -qed "hypreal_mult_le_less_mono2";
   1.458 -
   1.459 -Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y";
   1.460 -by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.461 -by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
   1.462 -qed "hypreal_mult_le_le_mono1";
   1.463 -
   1.464 -val prem1::prem2::prem3::rest = goal (the_context ())
   1.465 -     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
   1.466 -by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
   1.467 -qed "hypreal_mult_less_trans";
   1.468 -
   1.469 -Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
   1.470 -by (dtac hypreal_le_imp_less_or_eq 1);
   1.471 -by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
   1.472 -qed "hypreal_mult_le_less_trans";
   1.473 -
   1.474 -Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
   1.475 -by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
   1.476 -by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
   1.477 -qed "hypreal_mult_le_le_trans";
   1.478 -
   1.479 -Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \
   1.480 -\                     ==> r1 * x < r2 * y";
   1.481 -by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
   1.482 -by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2);
   1.483 -by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
   1.484 -by Auto_tac;
   1.485 -by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
   1.486 -qed "hypreal_mult_less_mono";
   1.487 -
   1.488 -Goal "[| 0 < r1; r1 <r2; 0 < y|] \
   1.489 -\                           ==> (0::hypreal) < r2 * y";
   1.490 -by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1);
   1.491 -by (assume_tac 1);
   1.492 -by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
   1.493 -qed "hypreal_mult_order_trans";
   1.494 -
   1.495 -Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \
   1.496 -\                  ==> r1 * x <= r2 * y";
   1.497 -by (rtac hypreal_less_or_eq_imp_le 1);
   1.498 -by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.499 -by (auto_tac (claset() addIs [hypreal_mult_less_mono,
   1.500 -    hypreal_mult_less_mono1,hypreal_mult_less_mono2,
   1.501 -    hypreal_mult_order_trans,hypreal_mult_order],simpset()));
   1.502 -qed "hypreal_mult_le_mono";
   1.503 +Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))";
   1.504 +by (simp_tac (simpset() addsimps 
   1.505 +    [hypreal_minus_zero_less_iff2]) 1);
   1.506 +qed "hypreal_minus_zero_le_iff";
   1.507  
   1.508  (*----------------------------------------------------------
   1.509    hypreal_of_real preserves field and order properties
   1.510 @@ -1291,26 +1142,6 @@
   1.511  by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
   1.512  qed "hypreal_of_real_minus";
   1.513  
   1.514 -Goal "0 < x ==> 0 < hrinv x";
   1.515 -by (EVERY1[rtac ccontr, dtac hypreal_leI]);
   1.516 -by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
   1.517 -by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
   1.518 -by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
   1.519 -by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
   1.520 -by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
   1.521 -by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
   1.522 -    simpset() addsimps [hypreal_minus_zero_less_iff]));
   1.523 -qed "hypreal_hrinv_gt_zero";
   1.524 -
   1.525 -Goal "x < 0 ==> hrinv x < 0";
   1.526 -by (ftac hypreal_not_refl2 1);
   1.527 -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
   1.528 -by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
   1.529 -by (dtac (hypreal_minus_hrinv RS sym) 1);
   1.530 -by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
   1.531 -    simpset()));
   1.532 -qed "hypreal_hrinv_less_zero";
   1.533 -
   1.534  Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
   1.535  by (Step_tac 1);
   1.536  qed "hypreal_of_real_one";
   1.537 @@ -1346,136 +1177,10 @@
   1.538  by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
   1.539  qed "hypreal_add_self";
   1.540  
   1.541 -Goal "1hr < 1hr + 1hr";
   1.542 -by (rtac (hypreal_less_minus_iff RS iffD2) 1);
   1.543 -by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
   1.544 -    hypreal_add_assoc]) 1);
   1.545 -qed "hypreal_one_less_two";
   1.546 -
   1.547 -Goal "0 < 1hr + 1hr";
   1.548 -by (rtac ([hypreal_zero_less_one,
   1.549 -          hypreal_one_less_two] MRS hypreal_less_trans) 1);
   1.550 -qed "hypreal_zero_less_two";
   1.551 -
   1.552 -Goal "1hr + 1hr ~= 0";
   1.553 -by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
   1.554 -qed "hypreal_two_not_zero";
   1.555 -Addsimps [hypreal_two_not_zero];
   1.556 -
   1.557 -Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
   1.558 -by (stac hypreal_add_self 1);
   1.559 -by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
   1.560 -qed "hypreal_sum_of_halves";
   1.561 -
   1.562  Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)";
   1.563  by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
   1.564  qed "lemma_chain";
   1.565  
   1.566 -Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
   1.567 -by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
   1.568 -          RS hypreal_mult_less_mono1) 1);
   1.569 -by Auto_tac;
   1.570 -qed "hypreal_half_gt_zero";
   1.571 -
   1.572 -(* TODO: remove redundant  0 < x *)
   1.573 -Goal "[| 0 < r; 0 < x; r < x |] ==> hrinv x < hrinv r";
   1.574 -by (ftac hypreal_hrinv_gt_zero 1);
   1.575 -by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
   1.576 -by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
   1.577 -by (assume_tac 1);
   1.578 -by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
   1.579 -         not_sym RS hypreal_mult_hrinv]) 1);
   1.580 -by (ftac hypreal_hrinv_gt_zero 1);
   1.581 -by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
   1.582 -by (assume_tac 1);
   1.583 -by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
   1.584 -         not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
   1.585 -qed "hypreal_hrinv_less_swap";
   1.586 -
   1.587 -Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
   1.588 -by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
   1.589 -by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
   1.590 -by (etac (hypreal_not_refl2 RS not_sym) 1);
   1.591 -by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
   1.592 -by (etac (hypreal_not_refl2 RS not_sym) 1);
   1.593 -by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
   1.594 -    simpset() addsimps [hypreal_hrinv_gt_zero]));
   1.595 -qed "hypreal_hrinv_less_iff";
   1.596 -
   1.597 -Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
   1.598 -by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
   1.599 -    hypreal_hrinv_gt_zero]) 1);
   1.600 -qed "hypreal_mult_hrinv_less_mono1";
   1.601 -
   1.602 -Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
   1.603 -by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
   1.604 -    hypreal_hrinv_gt_zero]) 1);
   1.605 -qed "hypreal_mult_hrinv_less_mono2";
   1.606 -
   1.607 -Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
   1.608 -by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
   1.609 -by (dtac (hypreal_not_refl2 RS not_sym) 2);
   1.610 -by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
   1.611 -              simpset() addsimps hypreal_mult_ac));
   1.612 -qed "hypreal_less_mult_right_cancel";
   1.613 -
   1.614 -Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
   1.615 -by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
   1.616 -    simpset() addsimps [hypreal_mult_commute]));
   1.617 -qed "hypreal_less_mult_left_cancel";
   1.618 -
   1.619 -Goal "[| 0 < r; (0::hypreal) < ra; \
   1.620 -\                 r < x; ra < y |] \
   1.621 -\              ==> r*ra < x*y";
   1.622 -by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
   1.623 -by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
   1.624 -by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
   1.625 -by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
   1.626 -qed "hypreal_mult_less_gt_zero"; 
   1.627 -
   1.628 -Goal "[| 0 < r; (0::hypreal) < ra; \
   1.629 -\                 r <= x; ra <= y |] \
   1.630 -\              ==> r*ra <= x*y";
   1.631 -by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
   1.632 -by (rtac hypreal_less_or_eq_imp_le 1);
   1.633 -by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
   1.634 -    hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
   1.635 -    simpset()));
   1.636 -qed "hypreal_mult_le_ge_zero"; 
   1.637 -
   1.638 -Goal "EX (x::hypreal). x < y";
   1.639 -by (rtac (hypreal_add_zero_right RS subst) 1);
   1.640 -by (res_inst_tac [("x","y + -1hr")] exI 1);
   1.641 -by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
   1.642 -    simpset() addsimps [hypreal_minus_zero_less_iff2,
   1.643 -    hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
   1.644 -qed "hypreal_less_Ex";
   1.645 -
   1.646 -Goal "!!(A::hypreal). A + C < B + C ==> A < B";
   1.647 -by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
   1.648 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   1.649 -qed "hypreal_less_add_right_cancel";
   1.650 -
   1.651 -Goal "!!(A::hypreal). C + A < C + B ==> A < B";
   1.652 -by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
   1.653 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   1.654 -qed "hypreal_less_add_left_cancel";
   1.655 -
   1.656 -Goal "(0::hypreal) <= x*x";
   1.657 -by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
   1.658 -by (auto_tac (claset() addIs [hypreal_mult_order,
   1.659 -    hypreal_mult_less_zero1,hypreal_less_imp_le],
   1.660 -    simpset()));
   1.661 -qed "hypreal_le_square";
   1.662 -Addsimps [hypreal_le_square];
   1.663 -
   1.664 -Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
   1.665 -by (auto_tac (claset() addSDs [(hypreal_le_square RS 
   1.666 -    hypreal_le_less_trans)],simpset() addsimps 
   1.667 -    [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
   1.668 -qed "hypreal_less_minus_square";
   1.669 -Addsimps [hypreal_less_minus_square];
   1.670 -
   1.671  Goal "[|x ~= 0; y ~= 0 |] ==> \
   1.672  \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
   1.673  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
   1.674 @@ -1486,19 +1191,16 @@
   1.675  qed "hypreal_hrinv_add";
   1.676  
   1.677  Goal "x = -x ==> x = (0::hypreal)";
   1.678 -by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
   1.679 -by (Asm_full_simp_tac 1);
   1.680 -by (dtac (hypreal_add_self RS subst) 1);
   1.681 -by (rtac ccontr 1);
   1.682 -by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
   1.683 -               (2,hypreal_mult_not_0)]) 1);
   1.684 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.685 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   1.686 +    hypreal_zero_def]));
   1.687 +by (Ultra_tac 1);
   1.688  qed "hypreal_self_eq_minus_self_zero";
   1.689  
   1.690  Goal "(x + x = 0) = (x = (0::hypreal))";
   1.691 -by Auto_tac;
   1.692 -by (dtac (hypreal_add_self RS subst) 1);
   1.693 -by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
   1.694 -by Auto_tac;
   1.695 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.696 +by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   1.697 +    hypreal_zero_def]));
   1.698  qed "hypreal_add_self_zero_cancel";
   1.699  Addsimps [hypreal_add_self_zero_cancel];
   1.700  
   1.701 @@ -1525,16 +1227,17 @@
   1.702  Addsimps [hypreal_minus_eq_cancel];
   1.703  
   1.704  Goal "x < x + 1hr";
   1.705 -by (cut_inst_tac [("C","x")] 
   1.706 -    (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
   1.707 -by (Asm_full_simp_tac 1);
   1.708 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.709 +by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   1.710 +    hypreal_one_def,hypreal_less]));
   1.711  qed "hypreal_less_self_add_one";
   1.712  Addsimps [hypreal_less_self_add_one];
   1.713  
   1.714  Goal "((x::hypreal) + x = y + y) = (x = y)";
   1.715 -by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
   1.716 -     hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
   1.717 -     [hypreal_add_mult_distrib]));
   1.718 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.719 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.720 +by (auto_tac (claset(),simpset() addsimps [hypreal_add]));
   1.721 +by (ALLGOALS(Ultra_tac));
   1.722  qed "hypreal_add_self_cancel";
   1.723  Addsimps [hypreal_add_self_cancel];
   1.724  
   1.725 @@ -1552,44 +1255,19 @@
   1.726  qed "hypreal_add_self_minus_cancel2";
   1.727  Addsimps [hypreal_add_self_minus_cancel2];
   1.728  
   1.729 +(* of course, can prove this by "transfer" as well *)
   1.730  Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
   1.731  by Auto_tac;
   1.732  by (dres_inst_tac [("x1","z")] 
   1.733      (hypreal_add_right_cancel RS iffD2) 1);
   1.734  by (asm_full_simp_tac (simpset() addsimps 
   1.735 -    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
   1.736 +    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
   1.737 +    delsimps [hypreal_minus_add_distrib]) 1);
   1.738  by (asm_full_simp_tac (simpset() addsimps 
   1.739       [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
   1.740  qed "hypreal_add_self_minus_cancel3";
   1.741  Addsimps [hypreal_add_self_minus_cancel3];
   1.742  
   1.743 -(* check why this does not work without 2nd substiution anymore! *)
   1.744 -Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
   1.745 -by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
   1.746 -by (dtac (hypreal_add_self RS subst) 1);
   1.747 -by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
   1.748 -          hypreal_mult_less_mono1) 1);
   1.749 -by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
   1.750 -          (hypreal_mult_hrinv RS subst)],simpset() 
   1.751 -          addsimps [hypreal_mult_assoc]));
   1.752 -qed "hypreal_less_half_sum";
   1.753 -
   1.754 -(* check why this does not work without 2nd substiution anymore! *)
   1.755 -Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
   1.756 -by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
   1.757 -by (dtac (hypreal_add_self RS subst) 1);
   1.758 -by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
   1.759 -          hypreal_mult_less_mono1) 1);
   1.760 -by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
   1.761 -          (hypreal_mult_hrinv RS subst)],simpset() 
   1.762 -          addsimps [hypreal_mult_assoc]));
   1.763 -qed "hypreal_gt_half_sum";
   1.764 -
   1.765 -Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
   1.766 -by (blast_tac (claset() addSIs [hypreal_less_half_sum,
   1.767 -    hypreal_gt_half_sum]) 1);
   1.768 -qed "hypreal_dense";
   1.769 -
   1.770  Goal "(x * x = 0) = (x = (0::hypreal))";
   1.771  by Auto_tac;
   1.772  by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
   1.773 @@ -1601,249 +1279,84 @@
   1.774  qed "hypreal_mult_self_eq_zero_iff2";
   1.775  Addsimps [hypreal_mult_self_eq_zero_iff2];
   1.776  
   1.777 -Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
   1.778 -by Auto_tac;
   1.779 -by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
   1.780 -by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
   1.781 -by (ALLGOALS(rtac ccontr));
   1.782 -by (ALLGOALS(dtac hypreal_mult_self_not_zero));
   1.783 -by (cut_inst_tac [("x1","x")] (hypreal_le_square 
   1.784 -        RS hypreal_le_imp_less_or_eq) 1);
   1.785 -by (cut_inst_tac [("x1","y")] (hypreal_le_square 
   1.786 -        RS hypreal_le_imp_less_or_eq) 2);
   1.787 -by (auto_tac (claset() addDs [sym],simpset()));
   1.788 -by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
   1.789 -    RS hypreal_le_less_trans) 1);
   1.790 -by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
   1.791 -    RS hypreal_le_less_trans) 2);
   1.792 -by (auto_tac (claset(),simpset() addsimps 
   1.793 -       [hypreal_less_not_refl]));
   1.794 -qed "hypreal_squares_add_zero_iff";
   1.795 -Addsimps [hypreal_squares_add_zero_iff];
   1.796 +Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
   1.797 +by (rtac hypreal_less_minus_iff2 1);
   1.798 +qed "hypreal_less_eq_diff";
   1.799  
   1.800 -Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
   1.801 -by (cut_inst_tac [("x1","x")] (hypreal_le_square 
   1.802 -        RS hypreal_le_imp_less_or_eq) 1);
   1.803 -by (auto_tac (claset() addSIs 
   1.804 -              [hypreal_add_order_le],simpset()));
   1.805 -qed "hypreal_sum_squares3_gt_zero";
   1.806 +(*** Subtraction laws ***)
   1.807  
   1.808 -Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
   1.809 -by (dtac hypreal_sum_squares3_gt_zero 1);
   1.810 -by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.811 -qed "hypreal_sum_squares3_gt_zero2";
   1.812 -
   1.813 -Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
   1.814 -by (dtac hypreal_sum_squares3_gt_zero 1);
   1.815 -by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
   1.816 -qed "hypreal_sum_squares3_gt_zero3";
   1.817 +Goal "x + (y - z) = (x + y) - (z::hypreal)";
   1.818 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.819 +qed "hypreal_add_diff_eq";
   1.820  
   1.821 -Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
   1.822 -by Auto_tac;
   1.823 -by (ALLGOALS(rtac ccontr));
   1.824 -by (ALLGOALS(dtac hypreal_mult_self_not_zero));
   1.825 -by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
   1.826 -   hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
   1.827 -   hypreal_sum_squares3_gt_zero2],simpset() delsimps
   1.828 -   [hypreal_mult_self_eq_zero_iff]));
   1.829 -qed "hypreal_three_squares_add_zero_iff";
   1.830 -Addsimps [hypreal_three_squares_add_zero_iff];
   1.831 +Goal "(x - y) + z = (x + z) - (y::hypreal)";
   1.832 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.833 +qed "hypreal_diff_add_eq";
   1.834  
   1.835 -Addsimps [rename_numerals real_le_square];
   1.836 -Goal "(x::hypreal)*x <= x*x + y*y";
   1.837 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.838 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.839 -by (auto_tac (claset(),simpset() addsimps 
   1.840 -    [hypreal_mult,hypreal_add,hypreal_le]));
   1.841 -qed "hypreal_self_le_add_pos";
   1.842 -Addsimps [hypreal_self_le_add_pos];
   1.843 +Goal "(x - y) - z = x - (y + (z::hypreal))";
   1.844 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.845 +qed "hypreal_diff_diff_eq";
   1.846  
   1.847 -Goal "(x::hypreal)*x <= x*x + y*y + z*z";
   1.848 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.849 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.850 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   1.851 -by (auto_tac (claset(),
   1.852 -	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
   1.853 -				  rename_numerals real_le_add_order]));
   1.854 -qed "hypreal_self_le_add_pos2";
   1.855 -Addsimps [hypreal_self_le_add_pos2];
   1.856 +Goal "x - (y - z) = (x + z) - (y::hypreal)";
   1.857 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.858 +qed "hypreal_diff_diff_eq2";
   1.859  
   1.860 -(*---------------------------------------------------------------------------------
   1.861 -             Embedding of the naturals in the hyperreals
   1.862 - ---------------------------------------------------------------------------------*)
   1.863 -Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
   1.864 -by (full_simp_tac (simpset() addsimps 
   1.865 -    [pnat_one_iff RS sym,real_of_preal_def]) 1);
   1.866 -by (fold_tac [real_one_def]);
   1.867 -by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
   1.868 -qed "hypreal_of_posnat_one";
   1.869 -
   1.870 -Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
   1.871 -by (full_simp_tac (simpset() addsimps 
   1.872 -		   [real_of_preal_def,
   1.873 -		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
   1.874 -		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
   1.875 -		    hypreal_one_def, real_add,
   1.876 -		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
   1.877 -		    pnat_add_ac) 1);
   1.878 -qed "hypreal_of_posnat_two";
   1.879 +Goal "(x-y < z) = (x < z + (y::hypreal))";
   1.880 +by (stac hypreal_less_eq_diff 1);
   1.881 +by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1);
   1.882 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.883 +qed "hypreal_diff_less_eq";
   1.884  
   1.885 -Goalw [hypreal_of_posnat_def]
   1.886 -          "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
   1.887 -\          hypreal_of_posnat (n1 + n2) + 1hr";
   1.888 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
   1.889 -    hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
   1.890 -    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
   1.891 -qed "hypreal_of_posnat_add";
   1.892 -
   1.893 -Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
   1.894 -by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
   1.895 -by (rtac (hypreal_of_posnat_add RS subst) 1);
   1.896 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
   1.897 -qed "hypreal_of_posnat_add_one";
   1.898 +Goal "(x < z-y) = (x + (y::hypreal) < z)";
   1.899 +by (stac hypreal_less_eq_diff 1);
   1.900 +by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1);
   1.901 +by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
   1.902 +qed "hypreal_less_diff_eq";
   1.903  
   1.904 -Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
   1.905 -      "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
   1.906 -by (rtac refl 1);
   1.907 -qed "hypreal_of_real_of_posnat";
   1.908 -
   1.909 -Goalw [hypreal_of_posnat_def] 
   1.910 -      "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
   1.911 -by Auto_tac;
   1.912 -qed "hypreal_of_posnat_less_iff";
   1.913 -
   1.914 -Addsimps [hypreal_of_posnat_less_iff RS sym];
   1.915 -(*---------------------------------------------------------------------------------
   1.916 -               Existence of infinite hyperreal number
   1.917 - ---------------------------------------------------------------------------------*)
   1.918 -
   1.919 -Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
   1.920 -by Auto_tac;
   1.921 -qed "hypreal_omega";
   1.922 +Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))";
   1.923 +by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1);
   1.924 +qed "hypreal_diff_le_eq";
   1.925  
   1.926 -Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
   1.927 -by (rtac Rep_hypreal 1);
   1.928 -qed "Rep_hypreal_omega";
   1.929 -
   1.930 -(* existence of infinite number not corresponding to any real number *)
   1.931 -(* use assumption that member FreeUltrafilterNat is not finite       *)
   1.932 -(* a few lemmas first *)
   1.933 -
   1.934 -Goal "{n::nat. x = real_of_posnat n} = {} | \
   1.935 -\     (EX y. {n::nat. x = real_of_posnat n} = {y})";
   1.936 -by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
   1.937 -qed "lemma_omega_empty_singleton_disj";
   1.938 +Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)";
   1.939 +by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
   1.940 +qed "hypreal_le_diff_eq";
   1.941  
   1.942 -Goal "finite {n::nat. x = real_of_posnat n}";
   1.943 -by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
   1.944 -by Auto_tac;
   1.945 -qed "lemma_finite_omega_set";
   1.946 -
   1.947 -Goalw [omega_def,hypreal_of_real_def] 
   1.948 -      "~ (EX x. hypreal_of_real x = whr)";
   1.949 -by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
   1.950 -    RS FreeUltrafilterNat_finite]));
   1.951 -qed "not_ex_hypreal_of_real_eq_omega";
   1.952 -
   1.953 -Goal "hypreal_of_real x ~= whr";
   1.954 -by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
   1.955 -by Auto_tac;
   1.956 -qed "hypreal_of_real_not_eq_omega";
   1.957 +Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))";
   1.958 +by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
   1.959 +qed "hypreal_diff_eq_eq";
   1.960  
   1.961 -(* existence of infinitesimal number also not *)
   1.962 -(* corresponding to any real number *)
   1.963 -
   1.964 -Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
   1.965 -\     (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
   1.966 -by (Step_tac 1 THEN Step_tac 1);
   1.967 -by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
   1.968 -qed "lemma_epsilon_empty_singleton_disj";
   1.969 -
   1.970 -Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
   1.971 -by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
   1.972 -by Auto_tac;
   1.973 -qed "lemma_finite_epsilon_set";
   1.974 +Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)";
   1.975 +by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
   1.976 +qed "hypreal_eq_diff_eq";
   1.977  
   1.978 -Goalw [epsilon_def,hypreal_of_real_def] 
   1.979 -      "~ (EX x. hypreal_of_real x = ehr)";
   1.980 -by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
   1.981 -    RS FreeUltrafilterNat_finite]));
   1.982 -qed "not_ex_hypreal_of_real_eq_epsilon";
   1.983 +(*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.984 +  to the top and then moving negative terms to the other side.  
   1.985 +  Use with hypreal_add_ac*)
   1.986 +val hypreal_compare_rls = 
   1.987 +  [symmetric hypreal_diff_def,
   1.988 +   hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, hypreal_diff_diff_eq2, 
   1.989 +   hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, hypreal_le_diff_eq, 
   1.990 +   hypreal_diff_eq_eq, hypreal_eq_diff_eq];
   1.991  
   1.992 -Goal "hypreal_of_real x ~= ehr";
   1.993 -by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
   1.994 -by Auto_tac;
   1.995 -qed "hypreal_of_real_not_eq_epsilon";
   1.996 -
   1.997 -Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
   1.998 -by (auto_tac (claset(),
   1.999 -     simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero]));
  1.1000 -qed "hypreal_epsilon_not_zero";
  1.1001  
  1.1002 -Addsimps [rename_numerals real_of_posnat_not_eq_zero];
  1.1003 -Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
  1.1004 -by (Simp_tac 1);
  1.1005 -qed "hypreal_omega_not_zero";
  1.1006 -
  1.1007 -Goal "ehr = hrinv(whr)";
  1.1008 -by (asm_full_simp_tac (simpset() addsimps 
  1.1009 -    [hypreal_hrinv,omega_def,epsilon_def]
  1.1010 -    addsplits [split_if]) 1);
  1.1011 -qed "hypreal_epsilon_hrinv_omega";
  1.1012 +(** For the cancellation simproc.
  1.1013 +    The idea is to cancel like terms on opposite sides by subtraction **)
  1.1014  
  1.1015 -(*----------------------------------------------------------------
  1.1016 -     Another embedding of the naturals in the 
  1.1017 -    hyperreals (see hypreal_of_posnat)
  1.1018 - ----------------------------------------------------------------*)
  1.1019 -Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
  1.1020 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
  1.1021 -qed "hypreal_of_nat_zero";
  1.1022 -
  1.1023 -Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
  1.1024 -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
  1.1025 -    hypreal_add_assoc]) 1);
  1.1026 -qed "hypreal_of_nat_one";
  1.1027 +Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')";
  1.1028 +by (stac hypreal_less_eq_diff 1);
  1.1029 +by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1);
  1.1030 +by (Asm_simp_tac 1);
  1.1031 +qed "hypreal_less_eqI";
  1.1032  
  1.1033 -Goalw [hypreal_of_nat_def]
  1.1034 -      "hypreal_of_nat n1 + hypreal_of_nat n2 = \
  1.1035 -\      hypreal_of_nat (n1 + n2)";
  1.1036 -by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
  1.1037 -by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
  1.1038 -    hypreal_add_assoc RS sym]) 1);
  1.1039 -by (rtac (hypreal_add_commute RS subst) 1);
  1.1040 -by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
  1.1041 -    hypreal_add_assoc]) 1);
  1.1042 -qed "hypreal_of_nat_add";
  1.1043 -
  1.1044 -Goal "hypreal_of_nat 2 = 1hr + 1hr";
  1.1045 -by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
  1.1046 -    RS sym,hypreal_of_nat_add]) 1);
  1.1047 -qed "hypreal_of_nat_two";
  1.1048 +Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')";
  1.1049 +by (dtac hypreal_less_eqI 1);
  1.1050 +by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1);
  1.1051 +qed "hypreal_le_eqI";
  1.1052  
  1.1053 -Goalw [hypreal_of_nat_def] 
  1.1054 -      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
  1.1055 -by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
  1.1056 -by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
  1.1057 -by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
  1.1058 -qed "hypreal_of_nat_less_iff";
  1.1059 -Addsimps [hypreal_of_nat_less_iff RS sym];
  1.1060 +Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')";
  1.1061 +by Safe_tac;
  1.1062 +by (ALLGOALS
  1.1063 +    (asm_full_simp_tac
  1.1064 +     (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
  1.1065 +qed "hypreal_eq_eqI";
  1.1066  
  1.1067 -(* naturals embedded in hyperreals is an hyperreal *)
  1.1068 -Goalw [hypreal_of_nat_def,real_of_nat_def] 
  1.1069 -      "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
  1.1070 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
  1.1071 -    hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
  1.1072 -qed "hypreal_of_nat_iff";
  1.1073 -
  1.1074 -Goal "inj hypreal_of_nat";
  1.1075 -by (rtac injI 1);
  1.1076 -by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
  1.1077 -        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
  1.1078 -        real_add_right_cancel,inj_real_of_nat RS injD]));
  1.1079 -qed "inj_hypreal_of_nat";
  1.1080 -
  1.1081 -Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
  1.1082 -       real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
  1.1083 -       "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
  1.1084 -by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
  1.1085 -qed "hypreal_of_nat_real_of_nat";