Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
authorpaulson
Thu Sep 23 18:39:05 1999 +0200 (1999-09-23)
changeset 758826384af93359
parent 7587 ee0b835ca8fa
child 7589 59663b367833
Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
RealAbs. RealAbs proofs have been highly streamlined. A couple of RealPow
proofs use #1, #2, etc.
src/HOL/Real/Real.thy
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealAbs.thy
src/HOL/Real/RealBin.ML
src/HOL/Real/RealBin.thy
src/HOL/Real/RealOrd.thy
src/HOL/Real/RealPow.ML
src/HOL/Real/ex/BinEx.ML
     1.1 --- a/src/HOL/Real/Real.thy	Thu Sep 23 14:39:39 1999 +0200
     1.2 +++ b/src/HOL/Real/Real.thy	Thu Sep 23 18:39:05 1999 +0200
     1.3 @@ -1,2 +1,2 @@
     1.4  
     1.5 -Real = Main + RComplete
     1.6 +Real = Main + RComplete + RealPow
     2.1 --- a/src/HOL/Real/RealAbs.ML	Thu Sep 23 14:39:39 1999 +0200
     2.2 +++ b/src/HOL/Real/RealAbs.ML	Thu Sep 23 18:39:05 1999 +0200
     2.3 @@ -20,36 +20,31 @@
     2.4  Addsimps [rabs_zero];
     2.5  
     2.6  Goalw [rabs_def] "rabs 0r = -0r";
     2.7 -by (stac real_minus_zero 1);
     2.8 -by (rtac if_cancel 1);
     2.9 +by (Simp_tac 1);
    2.10  qed "rabs_minus_zero";
    2.11  
    2.12 -val [prem] = goalw thy [rabs_def] "0r<=x ==> rabs x = x";
    2.13 -by (rtac (prem RS if_P) 1);
    2.14 +Goalw [rabs_def] "0r<=x ==> rabs x = x";
    2.15 +by (Asm_simp_tac 1);
    2.16  qed "rabs_eqI1";
    2.17  
    2.18 -val [prem] = goalw thy [rabs_def] "0r<x ==> rabs x = x";
    2.19 -by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1);
    2.20 +Goalw [rabs_def] "0r<x ==> rabs x = x";
    2.21 +by (Asm_simp_tac 1);
    2.22  qed "rabs_eqI2";
    2.23  
    2.24  Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
    2.25  by (Asm_simp_tac 1);
    2.26  qed "rabs_minus_eqI2";
    2.27  
    2.28 -Goal "x<=0r ==> rabs x = -x";
    2.29 -by (dtac real_le_imp_less_or_eq 1);
    2.30 -by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
    2.31 +Goalw [rabs_def] "x<=0r ==> rabs x = -x";
    2.32 +by (asm_full_simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.33  qed "rabs_minus_eqI1";
    2.34  
    2.35 -Goalw [rabs_def,real_le_def] "0r<= rabs x";
    2.36 -by (Full_simp_tac 1);
    2.37 -by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2,
    2.38 -			       real_less_asym]) 1);
    2.39 +Goalw [rabs_def] "0r<= rabs x";
    2.40 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.41  qed "rabs_ge_zero";
    2.42  
    2.43 -Goal "rabs(rabs x)=rabs x";
    2.44 -by (res_inst_tac [("r1","rabs x")] (rabs_iff RS ssubst) 1);
    2.45 -by (blast_tac (claset() addIs [if_P,rabs_ge_zero]) 1);
    2.46 +Goalw [rabs_def] "rabs(rabs x)=rabs x";
    2.47 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.48  qed "rabs_idempotent";
    2.49  
    2.50  Goalw [rabs_def] "(x=0r) = (rabs x = 0r)";
    2.51 @@ -61,13 +56,11 @@
    2.52  qed "rabs_not_zero_iff";
    2.53  
    2.54  Goalw [rabs_def] "x<=rabs x";
    2.55 -by (Full_simp_tac 1);
    2.56 -by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le],
    2.57 -	      simpset() addsimps [real_le_zero_iff]));
    2.58 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.59  qed "rabs_ge_self";
    2.60  
    2.61  Goalw [rabs_def] "-x<=rabs x";
    2.62 -by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1);
    2.63 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.64  qed "rabs_ge_minus_self";
    2.65  
    2.66  (* case splits nightmare *)
    2.67 @@ -76,7 +69,7 @@
    2.68  	      simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
    2.69  				  real_minus_mult_eq2]));
    2.70  by (blast_tac (claset() addDs [real_le_mult_order]) 1);
    2.71 -by (auto_tac (claset() addSDs [not_real_leE],simpset()));
    2.72 +by (auto_tac (claset() addSDs [not_real_leE], simpset()));
    2.73  by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
    2.74  by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
    2.75  by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
    2.76 @@ -96,67 +89,36 @@
    2.77  qed "rabs_rinv";
    2.78  
    2.79  Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))";
    2.80 -by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1);
    2.81 -by (asm_simp_tac (simpset() addsimps [rabs_not_zero_iff RS sym]) 1);
    2.82 -by (asm_simp_tac (simpset() addsimps [rabs_mult RS sym, real_mult_inv_right, 
    2.83 -				 rabs_not_zero_iff RS sym] @ real_mult_ac) 1);
    2.84 +by (asm_simp_tac (simpset() addsimps [rabs_mult, rabs_rinv]) 1);
    2.85  qed "rabs_mult_rinv";
    2.86  
    2.87 -Goal "rabs(x+y) <= rabs x + rabs y";
    2.88 -by (case_tac "0r<=x+y" 1);
    2.89 -by (asm_simp_tac
    2.90 -    (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
    2.91 -by (asm_simp_tac 
    2.92 -    (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono,
    2.93 -			 rabs_ge_minus_self]) 1);
    2.94 +Goalw [rabs_def] "rabs(x+y) <= rabs x + rabs y";
    2.95 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
    2.96  qed "rabs_triangle_ineq";
    2.97  
    2.98 +(*Unused, but perhaps interesting as an example*)
    2.99  Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)";
   2.100 -by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   2.101 -by (blast_tac (claset() addSIs [rabs_triangle_ineq RS real_le_trans,
   2.102 -				real_add_left_le_mono1]) 1);
   2.103 +by (simp_tac (simpset() addsimps [rabs_triangle_ineq RS order_trans]) 1);
   2.104  qed "rabs_triangle_ineq_four";
   2.105  
   2.106  Goalw [rabs_def] "rabs(-x)=rabs(x)";
   2.107 -by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] 
   2.108 -	               addIs [real_le_anti_sym],
   2.109 -		       simpset() addsimps [real_ge_zero_iff]));
   2.110 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   2.111  qed "rabs_minus_cancel";
   2.112  
   2.113 -Goal "rabs(x + (-y)) = rabs (y + (-x))";
   2.114 -by (rtac (rabs_minus_cancel RS subst) 1);
   2.115 -by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   2.116 +Goalw [rabs_def] "rabs(x + (-y)) = rabs (y + (-x))";
   2.117 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   2.118  qed "rabs_minus_add_cancel";
   2.119  
   2.120 -Goal "rabs(x + (-y)) <= rabs x + rabs y";
   2.121 -by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
   2.122 -by (rtac rabs_triangle_ineq 1);
   2.123 +Goalw [rabs_def] "rabs(x + (-y)) <= rabs x + rabs y";
   2.124 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   2.125  qed "rabs_triangle_minus_ineq";
   2.126  
   2.127 -Goal "rabs (x + y + ((-l) + (-m))) <= rabs(x + (-l)) + rabs(y + (-m))";
   2.128 -by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   2.129 -by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
   2.130 -by (rtac (real_add_assoc RS subst) 1);
   2.131 -by (rtac rabs_triangle_ineq 1);
   2.132 -qed "rabs_sum_triangle_ineq";
   2.133 +Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+y) < r+s";
   2.134 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   2.135 +qed_spec_mp "rabs_add_less";
   2.136  
   2.137 -Goal "rabs(x) <= rabs(x + (-y)) + rabs(y)";
   2.138 -by (res_inst_tac [("j","rabs(x + (-y) + y)")] real_le_trans 1);
   2.139 -by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
   2.140 -by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
   2.141 -				  rabs_triangle_ineq]) 1);
   2.142 -qed "rabs_triangle_ineq_minus_cancel";
   2.143 -
   2.144 -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
   2.145 -by (rtac real_le_less_trans 1);
   2.146 -by (rtac rabs_triangle_ineq 1);
   2.147 -by (REPEAT (ares_tac [real_add_less_mono] 1));
   2.148 -qed "rabs_add_less";
   2.149 -
   2.150 -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ (-y)) < r+s";
   2.151 -by (rotate_tac 1 1);
   2.152 -by (dtac (rabs_minus_cancel RS ssubst) 1);
   2.153 -by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
   2.154 +Goalw [rabs_def] "rabs x < r --> rabs y < s --> rabs(x+ (-y)) < r+s";
   2.155 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
   2.156  qed "rabs_add_minus_less";
   2.157  
   2.158  (* lemmas manipulating terms *)
   2.159 @@ -175,7 +137,8 @@
   2.160  			    real_mult_less_trans]) 1);
   2.161  qed "real_mult_le_less_trans";
   2.162  
   2.163 -(* proofs lifted from previous older version *)
   2.164 +(* proofs lifted from previous older version
   2.165 +   FIXME: use a stronger version of real_mult_less_mono *)
   2.166  Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s";
   2.167  by (simp_tac (simpset() addsimps [rabs_mult]) 1);
   2.168  by (rtac real_mult_le_less_trans 1);
   2.169 @@ -214,100 +177,31 @@
   2.170  qed "rabs_less_gt_zero";
   2.171  
   2.172  Goalw [rabs_def] "rabs 1r = 1r";
   2.173 -by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym],
   2.174 -	      simpset() addsimps [real_zero_less_one]));
   2.175 +by (simp_tac (simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]) 1);
   2.176  qed "rabs_one";
   2.177  
   2.178 -Goal "[| 0r < x ; x < r |] ==> rabs x < r";
   2.179 -by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1);
   2.180 -qed "rabs_lessI";
   2.181 -
   2.182 -Goal "rabs x =x | rabs x = -x";
   2.183 -by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
   2.184 -by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
   2.185 -			       rabs_zero,rabs_minus_zero]) 1);
   2.186 +Goalw [rabs_def] "rabs x =x | rabs x = -x";
   2.187 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   2.188  qed "rabs_disj";
   2.189  
   2.190 -Goal "rabs x = y ==> x = y | -x = y";
   2.191 -by (dtac sym 1);
   2.192 -by (hyp_subst_tac 1);
   2.193 -by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
   2.194 -by (REPEAT(Asm_simp_tac 1));
   2.195 -qed "rabs_eq_disj";
   2.196 -
   2.197 -Goal "(rabs x < r) = (-r<x & x<r)";
   2.198 -by Safe_tac;
   2.199 -by (rtac (real_less_swap_iff RS iffD2) 1);
   2.200 -by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
   2.201 -				       RS real_le_less_trans)]) 1);
   2.202 -by (asm_simp_tac (simpset() addsimps [rabs_ge_self RS real_le_less_trans]) 1);
   2.203 -by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, 
   2.204 -            dtac (real_minus_minus RS subst), 
   2.205 -            cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]);
   2.206 -by (assume_tac 3 THEN Auto_tac);
   2.207 +Goalw [rabs_def] "(rabs x < r) = (-r<x & x<r)";
   2.208 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   2.209  qed "rabs_interval_iff";
   2.210  
   2.211 -Goal "(rabs x < r) = (-x < r & x < r)";
   2.212 -by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff]));
   2.213 -by (dtac (real_less_swap_iff RS iffD1) 1);
   2.214 -by (dtac (real_less_swap_iff RS iffD1) 2);
   2.215 -by Auto_tac;
   2.216 -qed "rabs_interval_iff2";
   2.217 -
   2.218 -Goal "rabs x <= r ==> -r<=x & x<=r";
   2.219 -by (dtac real_le_imp_less_or_eq 1);
   2.220 -by (auto_tac (claset() addSDs [real_less_imp_le],
   2.221 -	      simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
   2.222 -by (auto_tac (claset(),simpset() addsimps [real_le_def]));
   2.223 -by (dtac (real_less_swap_iff RS iffD1) 1);
   2.224 -by (auto_tac (claset() addSDs [rabs_ge_minus_self RS real_le_less_trans],
   2.225 -	      simpset() addsimps [real_less_not_refl]));
   2.226 -qed "rabs_leD";
   2.227 -
   2.228 -Goal "[| -r<x; x<=r |] ==> rabs x <= r";
   2.229 -by (dtac real_le_imp_less_or_eq 1);
   2.230 -by (Step_tac 1);
   2.231 -by (blast_tac (claset() addIs 
   2.232 -	       [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
   2.233 -by (auto_tac (claset() addSDs [rabs_eqI2],
   2.234 -	      simpset() addsimps 
   2.235 -	        [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
   2.236 -qed "rabs_leI1";
   2.237 -
   2.238 -Goal "[| -r<=x; x<=r |] ==> rabs x <= r";
   2.239 -by (REPEAT(dtac real_le_imp_less_or_eq 1));
   2.240 -by (Step_tac 1);
   2.241 -by (blast_tac (claset() 
   2.242 -	       addIs [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
   2.243 -by (auto_tac (claset() addSDs [rabs_eqI2],
   2.244 -	      simpset() addsimps 
   2.245 -	      [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
   2.246 -	       rabs_minus_cancel]));
   2.247 -by (cut_inst_tac [("x","r")] rabs_disj 1);
   2.248 -by (rotate_tac 1 1);
   2.249 -by (auto_tac (claset(), simpset() addsimps [real_less_not_refl]));
   2.250 -qed "rabs_leI";
   2.251 -
   2.252 -Goal "(rabs x <= r) = (-r<=x & x<=r)";
   2.253 -by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1);
   2.254 +Goalw [rabs_def] "(rabs x <= r) = (-r<=x & x<=r)";
   2.255 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   2.256  qed "rabs_le_interval_iff";
   2.257  
   2.258 -Goal "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
   2.259 -by (auto_tac (claset(), simpset() addsimps [rabs_interval_iff]));
   2.260 -by (ALLGOALS(dtac real_less_sum_gt_zero));
   2.261 -by (ALLGOALS(dtac real_less_sum_gt_zero));
   2.262 -by (ALLGOALS(rtac real_sum_gt_zero_less));
   2.263 -by (auto_tac (claset(),
   2.264 -	      simpset() addsimps [real_minus_add_distrib] @ real_add_ac));
   2.265 +Goalw [rabs_def] "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
   2.266 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   2.267  qed "rabs_add_minus_interval_iff";
   2.268  
   2.269 -Goal "0r < k ==> 0r < k + rabs(x)";
   2.270 -by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1);
   2.271 -by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1);
   2.272 +Goalw [rabs_def] "0r < k ==> 0r < k + rabs(x)";
   2.273 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
   2.274  qed "rabs_add_pos_gt_zero";
   2.275  
   2.276 -Goal "0r < 1r + rabs(x)";
   2.277 -by (rtac (real_zero_less_one RS rabs_add_pos_gt_zero) 1);
   2.278 +Goalw [rabs_def] "0r < 1r + rabs(x)";
   2.279 +by (auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1]));
   2.280  qed "rabs_add_one_gt_zero";
   2.281  Addsimps [rabs_add_one_gt_zero];
   2.282  
     3.1 --- a/src/HOL/Real/RealAbs.thy	Thu Sep 23 14:39:39 1999 +0200
     3.2 +++ b/src/HOL/Real/RealAbs.thy	Thu Sep 23 18:39:05 1999 +0200
     3.3 @@ -5,10 +5,6 @@
     3.4      Description : Absolute value function for the reals
     3.5  *) 
     3.6  
     3.7 -RealAbs = RealOrd +
     3.8 +RealAbs = RealOrd + RealBin +
     3.9  
    3.10 -constdefs
    3.11 -   rabs   :: real => real
    3.12 -   "rabs r      == if 0r<=r then r else -r" 
    3.13 -
    3.14 -end
    3.15 \ No newline at end of file
    3.16 +end
     4.1 --- a/src/HOL/Real/RealBin.ML	Thu Sep 23 14:39:39 1999 +0200
     4.2 +++ b/src/HOL/Real/RealBin.ML	Thu Sep 23 18:39:05 1999 +0200
     4.3 @@ -58,6 +58,21 @@
     4.4  
     4.5  Addsimps [mult_real_number_of];
     4.6  
     4.7 +Goal "(#2::real) = #1 + #1";
     4.8 +by (Simp_tac 1);
     4.9 +val lemma = result();
    4.10 +
    4.11 +(*For specialist use: NOT as default simprules*)
    4.12 +Goal "#2 * z = (z+z::real)";
    4.13 +by (simp_tac (simpset_of RealDef.thy
    4.14 +	      addsimps [lemma, real_add_mult_distrib,
    4.15 +			one_eq_numeral_1 RS sym]) 1);
    4.16 +qed "real_mult_2";
    4.17 +
    4.18 +Goal "z * #2 = (z+z::real)";
    4.19 +by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
    4.20 +qed "real_mult_2_right";
    4.21 +
    4.22  
    4.23  (*** Comparisons ***)
    4.24  
    4.25 @@ -141,12 +156,6 @@
    4.26  	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
    4.27  	   real_minus_zero_less_iff]);
    4.28  
    4.29 -(** RealPow **)
    4.30 -
    4.31 -Addsimps (map (rename_numerals thy) 
    4.32 -	  [realpow_zero, realpow_two_le, realpow_zero_le,
    4.33 -	   realpow_eq_one, rabs_minus_realpow_one, rabs_realpow_minus_one,
    4.34 -	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
    4.35  
    4.36  (*Perhaps add some theorems that aren't in the default simpset, as
    4.37    done in Integ/NatBin.ML*)
    4.38 @@ -211,290 +220,3 @@
    4.39  
    4.40  arith_tac_split_thms := !arith_tac_split_thms @ [rabs_split];
    4.41  
    4.42 -(** Tests **)
    4.43 -Goal "(x + y = x) = (y = (#0::real))";
    4.44 -by(arith_tac 1);
    4.45 -
    4.46 -Goal "(x + y = y) = (x = (#0::real))";
    4.47 -by(arith_tac 1);
    4.48 -
    4.49 -Goal "(x + y = (#0::real)) = (x = -y)";
    4.50 -by(arith_tac 1);
    4.51 -
    4.52 -Goal "(x + y = (#0::real)) = (y = -x)";
    4.53 -by(arith_tac 1);
    4.54 -
    4.55 -Goal "((x + y) < (x + z)) = (y < (z::real))";
    4.56 -by(arith_tac 1);
    4.57 -
    4.58 -Goal "((x + z) < (y + z)) = (x < (y::real))";
    4.59 -by(arith_tac 1);
    4.60 -
    4.61 -Goal "(~ x < y) = (y <= (x::real))";
    4.62 -by(arith_tac 1);
    4.63 -
    4.64 -Goal "~(x < y & y < (x::real))";
    4.65 -by(arith_tac 1);
    4.66 -
    4.67 -Goal "(x::real) < y ==> ~ y < x";
    4.68 -by(arith_tac 1);
    4.69 -
    4.70 -Goal "((x::real) ~= y) = (x < y | y < x)";
    4.71 -by(arith_tac 1);
    4.72 -
    4.73 -Goal "(~ x <= y) = (y < (x::real))";
    4.74 -by(arith_tac 1);
    4.75 -
    4.76 -Goal "x <= y | y <= (x::real)";
    4.77 -by(arith_tac 1);
    4.78 -
    4.79 -Goal "x <= y | y < (x::real)";
    4.80 -by(arith_tac 1);
    4.81 -
    4.82 -Goal "x < y | y <= (x::real)";
    4.83 -by(arith_tac 1);
    4.84 -
    4.85 -Goal "x <= (x::real)";
    4.86 -by(arith_tac 1);
    4.87 -
    4.88 -Goal "((x::real) <= y) = (x < y | x = y)";
    4.89 -by(arith_tac 1);
    4.90 -
    4.91 -Goal "((x::real) <= y & y <= x) = (x = y)";
    4.92 -by(arith_tac 1);
    4.93 -
    4.94 -Goal "~(x < y & y <= (x::real))";
    4.95 -by(arith_tac 1);
    4.96 -
    4.97 -Goal "~(x <= y & y < (x::real))";
    4.98 -by(arith_tac 1);
    4.99 -
   4.100 -Goal "(-x < (#0::real)) = (#0 < x)";
   4.101 -by(arith_tac 1);
   4.102 -
   4.103 -Goal "((#0::real) < -x) = (x < #0)";
   4.104 -by(arith_tac 1);
   4.105 -
   4.106 -Goal "(-x <= (#0::real)) = (#0 <= x)";
   4.107 -by(arith_tac 1);
   4.108 -
   4.109 -Goal "((#0::real) <= -x) = (x <= #0)";
   4.110 -by(arith_tac 1);
   4.111 -
   4.112 -Goal "(x::real) = y | x < y | y < x";
   4.113 -by(arith_tac 1);
   4.114 -
   4.115 -Goal "(x::real) = #0 | #0 < x | #0 < -x";
   4.116 -by(arith_tac 1);
   4.117 -
   4.118 -Goal "(#0::real) <= x | #0 <= -x";
   4.119 -by(arith_tac 1);
   4.120 -
   4.121 -Goal "((x::real) + y <= x + z) = (y <= z)";
   4.122 -by(arith_tac 1);
   4.123 -
   4.124 -Goal "((x::real) + z <= y + z) = (x <= y)";
   4.125 -by(arith_tac 1);
   4.126 -
   4.127 -Goal "(w::real) < x & y < z ==> w + y < x + z";
   4.128 -by(arith_tac 1);
   4.129 -
   4.130 -Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
   4.131 -by(arith_tac 1);
   4.132 -
   4.133 -Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
   4.134 -by(arith_tac 1);
   4.135 -
   4.136 -Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
   4.137 -by(arith_tac 1);
   4.138 -
   4.139 -Goal "(-x < y) = (#0 < x + (y::real))";
   4.140 -by(arith_tac 1);
   4.141 -
   4.142 -Goal "(x < -y) = (x + y < (#0::real))";
   4.143 -by(arith_tac 1);
   4.144 -
   4.145 -Goal "(y < x + -z) = (y + z < (x::real))";
   4.146 -by(arith_tac 1);
   4.147 -
   4.148 -Goal "(x + -y < z) = (x < z + (y::real))";
   4.149 -by(arith_tac 1);
   4.150 -
   4.151 -Goal "x <= y ==> x < y + (#1::real)";
   4.152 -by(arith_tac 1);
   4.153 -
   4.154 -Goal "(x - y) + y = (x::real)";
   4.155 -by(arith_tac 1);
   4.156 -
   4.157 -Goal "y + (x - y) = (x::real)";
   4.158 -by(arith_tac 1);
   4.159 -
   4.160 -Goal "x - x = (#0::real)";
   4.161 -by(arith_tac 1);
   4.162 -
   4.163 -Goal "(x - y = #0) = (x = (y::real))";
   4.164 -by(arith_tac 1);
   4.165 -
   4.166 -Goal "((#0::real) <= x + x) = (#0 <= x)";
   4.167 -by(arith_tac 1);
   4.168 -
   4.169 -Goal "(-x <= x) = ((#0::real) <= x)";
   4.170 -by(arith_tac 1);
   4.171 -
   4.172 -Goal "(x <= -x) = (x <= (#0::real))";
   4.173 -by(arith_tac 1);
   4.174 -
   4.175 -Goal "(-x = (#0::real)) = (x = #0)";
   4.176 -by(arith_tac 1);
   4.177 -
   4.178 -Goal "-(x - y) = y - (x::real)";
   4.179 -by(arith_tac 1);
   4.180 -
   4.181 -Goal "((#0::real) < x - y) = (y < x)";
   4.182 -by(arith_tac 1);
   4.183 -
   4.184 -Goal "((#0::real) <= x - y) = (y <= x)";
   4.185 -by(arith_tac 1);
   4.186 -
   4.187 -Goal "(x + y) - x = (y::real)";
   4.188 -by(arith_tac 1);
   4.189 -
   4.190 -Goal "(-x = y) = (x = (-y::real))";
   4.191 -by(arith_tac 1);
   4.192 -
   4.193 -Goal "x < (y::real) ==> ~(x = y)";
   4.194 -by(arith_tac 1);
   4.195 -
   4.196 -Goal "(x <= x + y) = ((#0::real) <= y)";
   4.197 -by(arith_tac 1);
   4.198 -
   4.199 -Goal "(y <= x + y) = ((#0::real) <= x)";
   4.200 -by(arith_tac 1);
   4.201 -
   4.202 -Goal "(x < x + y) = ((#0::real) < y)";
   4.203 -by(arith_tac 1);
   4.204 -
   4.205 -Goal "(y < x + y) = ((#0::real) < x)";
   4.206 -by(arith_tac 1);
   4.207 -
   4.208 -Goal "(x - y) - x = (-y::real)";
   4.209 -by(arith_tac 1);
   4.210 -
   4.211 -Goal "(x + y < z) = (x < z - (y::real))";
   4.212 -by(arith_tac 1);
   4.213 -
   4.214 -Goal "(x - y < z) = (x < z + (y::real))";
   4.215 -by(arith_tac 1);
   4.216 -
   4.217 -Goal "(x < y - z) = (x + z < (y::real))";
   4.218 -by(arith_tac 1);
   4.219 -
   4.220 -Goal "(x <= y - z) = (x + z <= (y::real))";
   4.221 -by(arith_tac 1);
   4.222 -
   4.223 -Goal "(x - y <= z) = (x <= z + (y::real))";
   4.224 -by(arith_tac 1);
   4.225 -
   4.226 -Goal "(-x < -y) = (y < (x::real))";
   4.227 -by(arith_tac 1);
   4.228 -
   4.229 -Goal "(-x <= -y) = (y <= (x::real))";
   4.230 -by(arith_tac 1);
   4.231 -
   4.232 -Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
   4.233 -by(arith_tac 1);
   4.234 -
   4.235 -Goal "(#0::real) - x = -x";
   4.236 -by(arith_tac 1);
   4.237 -
   4.238 -Goal "x - (#0::real) = x";
   4.239 -by(arith_tac 1);
   4.240 -
   4.241 -Goal "w <= x & y < z ==> w + y < x + (z::real)";
   4.242 -by(arith_tac 1);
   4.243 -
   4.244 -Goal "w < x & y <= z ==> w + y < x + (z::real)";
   4.245 -by(arith_tac 1);
   4.246 -
   4.247 -Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
   4.248 -by(arith_tac 1);
   4.249 -
   4.250 -Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
   4.251 -by(arith_tac 1);
   4.252 -
   4.253 -Goal "-x - y = -(x + (y::real))";
   4.254 -by(arith_tac 1);
   4.255 -
   4.256 -Goal "x - (-y) = x + (y::real)";
   4.257 -by(arith_tac 1);
   4.258 -
   4.259 -Goal "-x - -y = y - (x::real)";
   4.260 -by(arith_tac 1);
   4.261 -
   4.262 -Goal "(a - b) + (b - c) = a - (c::real)";
   4.263 -by(arith_tac 1);
   4.264 -
   4.265 -Goal "(x = y - z) = (x + z = (y::real))";
   4.266 -by(arith_tac 1);
   4.267 -
   4.268 -Goal "(x - y = z) = (x = z + (y::real))";
   4.269 -by(arith_tac 1);
   4.270 -
   4.271 -Goal "x - (x - y) = (y::real)";
   4.272 -by(arith_tac 1);
   4.273 -
   4.274 -Goal "x - (x + y) = -(y::real)";
   4.275 -by(arith_tac 1);
   4.276 -
   4.277 -Goal "x = y ==> x <= (y::real)";
   4.278 -by(arith_tac 1);
   4.279 -
   4.280 -Goal "(#0::real) < x ==> ~(x = #0)";
   4.281 -by(arith_tac 1);
   4.282 -
   4.283 -Goal "(x + y) * (x - y) = (x * x) - (y * y)";
   4.284 -
   4.285 -Goal "(-x = -y) = (x = (y::real))";
   4.286 -by(arith_tac 1);
   4.287 -
   4.288 -Goal "(-x < -y) = (y < (x::real))";
   4.289 -by(arith_tac 1);
   4.290 -
   4.291 -Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   4.292 -by (fast_arith_tac 1);
   4.293 -
   4.294 -Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)";
   4.295 -by (fast_arith_tac 1);
   4.296 -
   4.297 -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
   4.298 -by (fast_arith_tac 1);
   4.299 -
   4.300 -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
   4.301 -\     ==> a+a <= j+j";
   4.302 -by (fast_arith_tac 1);
   4.303 -
   4.304 -Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
   4.305 -\     ==> a+a < j+j";
   4.306 -by (fast_arith_tac 1);
   4.307 -
   4.308 -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   4.309 -by (arith_tac 1);
   4.310 -
   4.311 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   4.312 -\     ==> a <= l";
   4.313 -by (fast_arith_tac 1);
   4.314 -
   4.315 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   4.316 -\     ==> a+a+a+a <= l+l+l+l";
   4.317 -by (fast_arith_tac 1);
   4.318 -
   4.319 -(* Too slow. Needs "combine_coefficients" simproc
   4.320 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   4.321 -\     ==> a+a+a+a+a <= l+l+l+l+i";
   4.322 -by (fast_arith_tac 1);
   4.323 -
   4.324 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   4.325 -\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   4.326 -by (fast_arith_tac 1);
   4.327 -*)
   4.328 -
     5.1 --- a/src/HOL/Real/RealBin.thy	Thu Sep 23 14:39:39 1999 +0200
     5.2 +++ b/src/HOL/Real/RealBin.thy	Thu Sep 23 18:39:05 1999 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  This case is reduced to that for the integers
     5.5  *)
     5.6  
     5.7 -RealBin = RealInt + Bin + RealPow +
     5.8 +RealBin = RealInt + Bin + 
     5.9  
    5.10  instance
    5.11    real :: number 
     6.1 --- a/src/HOL/Real/RealOrd.thy	Thu Sep 23 14:39:39 1999 +0200
     6.2 +++ b/src/HOL/Real/RealOrd.thy	Thu Sep 23 18:39:05 1999 +0200
     6.3 @@ -11,4 +11,8 @@
     6.4  instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
     6.5  instance real :: linorder (real_le_linear)
     6.6  
     6.7 +constdefs
     6.8 +   rabs   :: real => real
     6.9 +   "rabs r      == if 0r<=r then r else -r" 
    6.10 +
    6.11  end
     7.1 --- a/src/HOL/Real/RealPow.ML	Thu Sep 23 14:39:39 1999 +0200
     7.2 +++ b/src/HOL/Real/RealPow.ML	Thu Sep 23 18:39:05 1999 +0200
     7.3 @@ -94,6 +94,12 @@
     7.4  qed "realpow_eq_one";
     7.5  Addsimps [realpow_eq_one];
     7.6  
     7.7 +(** New versions using #0 and #1 instead of 0r and 1r
     7.8 +    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
     7.9 +
    7.10 +Addsimps (map (rename_numerals thy) [realpow_zero, realpow_eq_one]);
    7.11 +
    7.12 +
    7.13  Goal "rabs(-(1r ^ n)) = 1r";
    7.14  by (simp_tac (simpset() addsimps 
    7.15      [rabs_minus_cancel,rabs_one]) 1);
    7.16 @@ -137,21 +143,13 @@
    7.17  by (auto_tac (claset() addIs [real_less_trans],simpset()));
    7.18  qed "realpow_two_gt_one";
    7.19  
    7.20 -Goal "1r <= r ==> 1r <= r ^ 2";
    7.21 -by (etac (real_le_imp_less_or_eq RS disjE) 1);
    7.22 -by (etac (realpow_two_gt_one RS real_less_imp_le) 1);
    7.23 -by (asm_simp_tac (simpset()) 1);
    7.24 -qed "realpow_two_ge_one";
    7.25 -
    7.26 -(* more general result *)
    7.27  Goal "1r < r --> 1r <= r ^ n";
    7.28  by (induct_tac "n" 1);
    7.29  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
    7.30 -    simpset()));
    7.31 +	      simpset()));
    7.32  by (dtac (real_zero_less_one RS real_mult_less_mono) 1);
    7.33 -by (dtac sym 4);
    7.34  by (auto_tac (claset() addSIs [real_less_imp_le],
    7.35 -    simpset() addsimps [real_zero_less_one]));
    7.36 +	      simpset() addsimps [real_zero_less_one]));
    7.37  qed_spec_mp "realpow_ge_one";
    7.38  
    7.39  Goal "1r < r ==> 1r < r ^ (Suc n)";
    7.40 @@ -166,8 +164,7 @@
    7.41  
    7.42  Goal "1r <= r ==> 1r <= r ^ n";
    7.43  by (dtac real_le_imp_less_or_eq 1); 
    7.44 -by (auto_tac (claset() addDs [realpow_ge_one],
    7.45 -    simpset()));
    7.46 +by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
    7.47  qed "realpow_ge_one2";
    7.48  
    7.49  Goal "0r < r ==> 0r < r ^ Suc n";
    7.50 @@ -181,24 +178,23 @@
    7.51  Goal "0r <= r ==> 0r <= r ^ Suc n";
    7.52  by (etac (real_le_imp_less_or_eq RS disjE) 1);
    7.53  by (etac (realpow_ge_zero) 1);
    7.54 -by (asm_simp_tac (simpset()) 1);
    7.55 +by (Asm_simp_tac 1);
    7.56  qed "realpow_Suc_ge_zero";
    7.57  
    7.58 -Goal "1r <= (1r +1r) ^ n";
    7.59 -by (res_inst_tac [("j","1r ^ n")] real_le_trans 1);
    7.60 +Goal "(#1::real) <= #2 ^ n";
    7.61 +by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
    7.62  by (rtac realpow_le 2);
    7.63  by (auto_tac (claset() addIs [real_less_imp_le],
    7.64 -    simpset() addsimps [real_zero_less_one,
    7.65 -    real_one_less_two]));
    7.66 +	      simpset() addsimps [zero_eq_numeral_0]));
    7.67  qed "two_realpow_ge_one";
    7.68  
    7.69 -Goal "real_of_nat n < (1r + 1r) ^ n";
    7.70 +Goal "real_of_nat n < #2 ^ n";
    7.71  by (induct_tac "n" 1);
    7.72  by (auto_tac (claset(),
    7.73 -	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero,
    7.74 -				  real_zero_less_one,real_add_mult_distrib,
    7.75 -				  real_of_nat_one]));
    7.76 -by (blast_tac (claset() addSIs [real_add_less_le_mono, two_realpow_ge_one]) 1);
    7.77 +	      simpset() addsimps [zero_eq_numeral_0, one_eq_numeral_1,
    7.78 +				  real_mult_2,
    7.79 +				  real_of_nat_Suc, real_of_nat_zero,
    7.80 +				  real_add_less_le_mono, two_realpow_ge_one]));
    7.81  qed "two_realpow_gt";
    7.82  Addsimps [two_realpow_gt,two_realpow_ge_one];
    7.83  
    7.84 @@ -371,3 +367,11 @@
    7.85  qed "realpow_two_mult_rinv";
    7.86  Addsimps [realpow_two_mult_rinv];
    7.87  
    7.88 +
    7.89 +(** New versions using #0 and #1 instead of 0r and 1r
    7.90 +    REMOVE AFTER CONVERTING THIS FILE TO USE #0 AND #1 **)
    7.91 +
    7.92 +Addsimps (map (rename_numerals thy) 
    7.93 +	  [realpow_two_le, realpow_zero_le,
    7.94 +	   rabs_minus_realpow_one, rabs_realpow_minus_one,
    7.95 +	   realpow_minus_one, realpow_minus_one2, realpow_minus_one_odd]);
     8.1 --- a/src/HOL/Real/ex/BinEx.ML	Thu Sep 23 14:39:39 1999 +0200
     8.2 +++ b/src/HOL/Real/ex/BinEx.ML	Thu Sep 23 18:39:05 1999 +0200
     8.3 @@ -67,3 +67,291 @@
     8.4  Goal "(#1234567::real) <= #1234567";  
     8.5  by (Simp_tac 1); 
     8.6  qed "";
     8.7 +
     8.8 +(** Tests **)
     8.9 +Goal "(x + y = x) = (y = (#0::real))";
    8.10 +by(arith_tac 1);
    8.11 +
    8.12 +Goal "(x + y = y) = (x = (#0::real))";
    8.13 +by(arith_tac 1);
    8.14 +
    8.15 +Goal "(x + y = (#0::real)) = (x = -y)";
    8.16 +by(arith_tac 1);
    8.17 +
    8.18 +Goal "(x + y = (#0::real)) = (y = -x)";
    8.19 +by(arith_tac 1);
    8.20 +
    8.21 +Goal "((x + y) < (x + z)) = (y < (z::real))";
    8.22 +by(arith_tac 1);
    8.23 +
    8.24 +Goal "((x + z) < (y + z)) = (x < (y::real))";
    8.25 +by(arith_tac 1);
    8.26 +
    8.27 +Goal "(~ x < y) = (y <= (x::real))";
    8.28 +by(arith_tac 1);
    8.29 +
    8.30 +Goal "~(x < y & y < (x::real))";
    8.31 +by(arith_tac 1);
    8.32 +
    8.33 +Goal "(x::real) < y ==> ~ y < x";
    8.34 +by(arith_tac 1);
    8.35 +
    8.36 +Goal "((x::real) ~= y) = (x < y | y < x)";
    8.37 +by(arith_tac 1);
    8.38 +
    8.39 +Goal "(~ x <= y) = (y < (x::real))";
    8.40 +by(arith_tac 1);
    8.41 +
    8.42 +Goal "x <= y | y <= (x::real)";
    8.43 +by(arith_tac 1);
    8.44 +
    8.45 +Goal "x <= y | y < (x::real)";
    8.46 +by(arith_tac 1);
    8.47 +
    8.48 +Goal "x < y | y <= (x::real)";
    8.49 +by(arith_tac 1);
    8.50 +
    8.51 +Goal "x <= (x::real)";
    8.52 +by(arith_tac 1);
    8.53 +
    8.54 +Goal "((x::real) <= y) = (x < y | x = y)";
    8.55 +by(arith_tac 1);
    8.56 +
    8.57 +Goal "((x::real) <= y & y <= x) = (x = y)";
    8.58 +by(arith_tac 1);
    8.59 +
    8.60 +Goal "~(x < y & y <= (x::real))";
    8.61 +by(arith_tac 1);
    8.62 +
    8.63 +Goal "~(x <= y & y < (x::real))";
    8.64 +by(arith_tac 1);
    8.65 +
    8.66 +Goal "(-x < (#0::real)) = (#0 < x)";
    8.67 +by(arith_tac 1);
    8.68 +
    8.69 +Goal "((#0::real) < -x) = (x < #0)";
    8.70 +by(arith_tac 1);
    8.71 +
    8.72 +Goal "(-x <= (#0::real)) = (#0 <= x)";
    8.73 +by(arith_tac 1);
    8.74 +
    8.75 +Goal "((#0::real) <= -x) = (x <= #0)";
    8.76 +by(arith_tac 1);
    8.77 +
    8.78 +Goal "(x::real) = y | x < y | y < x";
    8.79 +by(arith_tac 1);
    8.80 +
    8.81 +Goal "(x::real) = #0 | #0 < x | #0 < -x";
    8.82 +by(arith_tac 1);
    8.83 +
    8.84 +Goal "(#0::real) <= x | #0 <= -x";
    8.85 +by(arith_tac 1);
    8.86 +
    8.87 +Goal "((x::real) + y <= x + z) = (y <= z)";
    8.88 +by(arith_tac 1);
    8.89 +
    8.90 +Goal "((x::real) + z <= y + z) = (x <= y)";
    8.91 +by(arith_tac 1);
    8.92 +
    8.93 +Goal "(w::real) < x & y < z ==> w + y < x + z";
    8.94 +by(arith_tac 1);
    8.95 +
    8.96 +Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
    8.97 +by(arith_tac 1);
    8.98 +
    8.99 +Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
   8.100 +by(arith_tac 1);
   8.101 +
   8.102 +Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
   8.103 +by(arith_tac 1);
   8.104 +
   8.105 +Goal "(-x < y) = (#0 < x + (y::real))";
   8.106 +by(arith_tac 1);
   8.107 +
   8.108 +Goal "(x < -y) = (x + y < (#0::real))";
   8.109 +by(arith_tac 1);
   8.110 +
   8.111 +Goal "(y < x + -z) = (y + z < (x::real))";
   8.112 +by(arith_tac 1);
   8.113 +
   8.114 +Goal "(x + -y < z) = (x < z + (y::real))";
   8.115 +by(arith_tac 1);
   8.116 +
   8.117 +Goal "x <= y ==> x < y + (#1::real)";
   8.118 +by(arith_tac 1);
   8.119 +
   8.120 +Goal "(x - y) + y = (x::real)";
   8.121 +by(arith_tac 1);
   8.122 +
   8.123 +Goal "y + (x - y) = (x::real)";
   8.124 +by(arith_tac 1);
   8.125 +
   8.126 +Goal "x - x = (#0::real)";
   8.127 +by(arith_tac 1);
   8.128 +
   8.129 +Goal "(x - y = #0) = (x = (y::real))";
   8.130 +by(arith_tac 1);
   8.131 +
   8.132 +Goal "((#0::real) <= x + x) = (#0 <= x)";
   8.133 +by(arith_tac 1);
   8.134 +
   8.135 +Goal "(-x <= x) = ((#0::real) <= x)";
   8.136 +by(arith_tac 1);
   8.137 +
   8.138 +Goal "(x <= -x) = (x <= (#0::real))";
   8.139 +by(arith_tac 1);
   8.140 +
   8.141 +Goal "(-x = (#0::real)) = (x = #0)";
   8.142 +by(arith_tac 1);
   8.143 +
   8.144 +Goal "-(x - y) = y - (x::real)";
   8.145 +by(arith_tac 1);
   8.146 +
   8.147 +Goal "((#0::real) < x - y) = (y < x)";
   8.148 +by(arith_tac 1);
   8.149 +
   8.150 +Goal "((#0::real) <= x - y) = (y <= x)";
   8.151 +by(arith_tac 1);
   8.152 +
   8.153 +Goal "(x + y) - x = (y::real)";
   8.154 +by(arith_tac 1);
   8.155 +
   8.156 +Goal "(-x = y) = (x = (-y::real))";
   8.157 +by(arith_tac 1);
   8.158 +
   8.159 +Goal "x < (y::real) ==> ~(x = y)";
   8.160 +by(arith_tac 1);
   8.161 +
   8.162 +Goal "(x <= x + y) = ((#0::real) <= y)";
   8.163 +by(arith_tac 1);
   8.164 +
   8.165 +Goal "(y <= x + y) = ((#0::real) <= x)";
   8.166 +by(arith_tac 1);
   8.167 +
   8.168 +Goal "(x < x + y) = ((#0::real) < y)";
   8.169 +by(arith_tac 1);
   8.170 +
   8.171 +Goal "(y < x + y) = ((#0::real) < x)";
   8.172 +by(arith_tac 1);
   8.173 +
   8.174 +Goal "(x - y) - x = (-y::real)";
   8.175 +by(arith_tac 1);
   8.176 +
   8.177 +Goal "(x + y < z) = (x < z - (y::real))";
   8.178 +by(arith_tac 1);
   8.179 +
   8.180 +Goal "(x - y < z) = (x < z + (y::real))";
   8.181 +by(arith_tac 1);
   8.182 +
   8.183 +Goal "(x < y - z) = (x + z < (y::real))";
   8.184 +by(arith_tac 1);
   8.185 +
   8.186 +Goal "(x <= y - z) = (x + z <= (y::real))";
   8.187 +by(arith_tac 1);
   8.188 +
   8.189 +Goal "(x - y <= z) = (x <= z + (y::real))";
   8.190 +by(arith_tac 1);
   8.191 +
   8.192 +Goal "(-x < -y) = (y < (x::real))";
   8.193 +by(arith_tac 1);
   8.194 +
   8.195 +Goal "(-x <= -y) = (y <= (x::real))";
   8.196 +by(arith_tac 1);
   8.197 +
   8.198 +Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
   8.199 +by(arith_tac 1);
   8.200 +
   8.201 +Goal "(#0::real) - x = -x";
   8.202 +by(arith_tac 1);
   8.203 +
   8.204 +Goal "x - (#0::real) = x";
   8.205 +by(arith_tac 1);
   8.206 +
   8.207 +Goal "w <= x & y < z ==> w + y < x + (z::real)";
   8.208 +by(arith_tac 1);
   8.209 +
   8.210 +Goal "w < x & y <= z ==> w + y < x + (z::real)";
   8.211 +by(arith_tac 1);
   8.212 +
   8.213 +Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
   8.214 +by(arith_tac 1);
   8.215 +
   8.216 +Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
   8.217 +by(arith_tac 1);
   8.218 +
   8.219 +Goal "-x - y = -(x + (y::real))";
   8.220 +by(arith_tac 1);
   8.221 +
   8.222 +Goal "x - (-y) = x + (y::real)";
   8.223 +by(arith_tac 1);
   8.224 +
   8.225 +Goal "-x - -y = y - (x::real)";
   8.226 +by(arith_tac 1);
   8.227 +
   8.228 +Goal "(a - b) + (b - c) = a - (c::real)";
   8.229 +by(arith_tac 1);
   8.230 +
   8.231 +Goal "(x = y - z) = (x + z = (y::real))";
   8.232 +by(arith_tac 1);
   8.233 +
   8.234 +Goal "(x - y = z) = (x = z + (y::real))";
   8.235 +by(arith_tac 1);
   8.236 +
   8.237 +Goal "x - (x - y) = (y::real)";
   8.238 +by(arith_tac 1);
   8.239 +
   8.240 +Goal "x - (x + y) = -(y::real)";
   8.241 +by(arith_tac 1);
   8.242 +
   8.243 +Goal "x = y ==> x <= (y::real)";
   8.244 +by(arith_tac 1);
   8.245 +
   8.246 +Goal "(#0::real) < x ==> ~(x = #0)";
   8.247 +by(arith_tac 1);
   8.248 +
   8.249 +Goal "(x + y) * (x - y) = (x * x) - (y * y)";
   8.250 +
   8.251 +Goal "(-x = -y) = (x = (y::real))";
   8.252 +by(arith_tac 1);
   8.253 +
   8.254 +Goal "(-x < -y) = (y < (x::real))";
   8.255 +by(arith_tac 1);
   8.256 +
   8.257 +Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   8.258 +by (fast_arith_tac 1);
   8.259 +
   8.260 +Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)";
   8.261 +by (fast_arith_tac 1);
   8.262 +
   8.263 +Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
   8.264 +by (fast_arith_tac 1);
   8.265 +
   8.266 +Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
   8.267 +\     ==> a+a <= j+j";
   8.268 +by (fast_arith_tac 1);
   8.269 +
   8.270 +Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
   8.271 +\     ==> a+a < j+j";
   8.272 +by (fast_arith_tac 1);
   8.273 +
   8.274 +Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   8.275 +by (arith_tac 1);
   8.276 +
   8.277 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   8.278 +\     ==> a <= l";
   8.279 +by (fast_arith_tac 1);
   8.280 +
   8.281 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   8.282 +\     ==> a+a+a+a <= l+l+l+l";
   8.283 +by (fast_arith_tac 1);
   8.284 +
   8.285 +(* Too slow. Needs "combine_coefficients" simproc
   8.286 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   8.287 +\     ==> a+a+a+a+a <= l+l+l+l+i";
   8.288 +by (fast_arith_tac 1);
   8.289 +
   8.290 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   8.291 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   8.292 +by (fast_arith_tac 1);
   8.293 +*)
   8.294 +