Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
authorpaulson
Thu Nov 27 10:47:55 2003 +0100 (2003-11-27)
changeset 142685cf13e80be0e
parent 14267 b963e9cee2a0
child 14269 502a7c95de73
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
New theorems for Ring_and_Field. Fixing affected proofs.
src/HOL/Hyperreal/ExtraThms2.ML
src/HOL/Hyperreal/ExtraThms2.thy
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperOrd.ML
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Hyperreal/NatStar.ML
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/Int.thy
src/HOL/IsaMakefile
src/HOL/Real/RComplete.ML
src/HOL/Real/RealArith0.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealOrd.thy
src/HOL/Real/RealPow.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/ExtraThms2.ML	Tue Nov 25 10:37:03 2003 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,557 +0,0 @@
     1.4 -(*lcp: needed for binary 2 MOVE UP???*)
     1.5 -
     1.6 -Goal "(0::real) <= x^2";
     1.7 -by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2]) 1); 
     1.8 -qed "zero_le_x_squared";
     1.9 -Addsimps [zero_le_x_squared];
    1.10 -
    1.11 -fun multl_by_tac x i = 
    1.12 -       let val cancel_thm = 
    1.13 -           CLAIM "[| (0::real)<z; z*x<z*y |] ==> x<y" 
    1.14 -       in
    1.15 -           res_inst_tac [("z",x)] cancel_thm i 
    1.16 -       end;
    1.17 -
    1.18 -fun multr_by_tac x i = 
    1.19 -       let val cancel_thm = 
    1.20 -           CLAIM "[| (0::real)<z; x*z<y*z |] ==> x<y" 
    1.21 -       in
    1.22 -           res_inst_tac [("z",x)] cancel_thm i 
    1.23 -       end;
    1.24 -
    1.25 -(* unused? *)
    1.26 -Goal "ALL x y. x < y --> (f::real=>real) x < f y ==> inj f";
    1.27 -by (rtac injI 1 THEN rtac ccontr 1);
    1.28 -by (dtac (ARITH_PROVE "x ~= y ==> x < y | y < (x::real)") 1);
    1.29 -by (Step_tac 1);
    1.30 -by (auto_tac (claset() addSDs [spec],simpset()));
    1.31 -qed "real_monofun_inj";
    1.32 -
    1.33 -(* HyperDef *)
    1.34 -
    1.35 -Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
    1.36 -by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
    1.37 -qed "hypreal_zero_num";
    1.38 -
    1.39 -Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
    1.40 -by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
    1.41 -qed "hypreal_one_num";
    1.42 -
    1.43 -(* RealOrd *)
    1.44 -
    1.45 -Goalw [real_of_posnat_def] "0 < real_of_posnat n";
    1.46 -by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
    1.47 -by (Blast_tac 1);
    1.48 -qed "real_of_posnat_gt_zero";
    1.49 -
    1.50 -Addsimps [real_of_posnat_gt_zero];
    1.51 -
    1.52 -bind_thm ("real_inv_real_of_posnat_gt_zero",
    1.53 -          real_of_posnat_gt_zero RS real_inverse_gt_0);
    1.54 -Addsimps [real_inv_real_of_posnat_gt_zero];
    1.55 -
    1.56 -bind_thm ("real_of_posnat_ge_zero",real_of_posnat_gt_zero RS order_less_imp_le);
    1.57 -Addsimps [real_of_posnat_ge_zero];
    1.58 -
    1.59 -Goal "real_of_posnat n ~= 0";
    1.60 -by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1);
    1.61 -qed "real_of_posnat_not_eq_zero";
    1.62 -Addsimps[real_of_posnat_not_eq_zero];
    1.63 -
    1.64 -Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_left];
    1.65 -Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_right];
    1.66 -
    1.67 -Goal "1 <= real_of_posnat n";
    1.68 -by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
    1.69 -by (induct_tac "n" 1);
    1.70 -by (auto_tac (claset(),
    1.71 -	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
    1.72 -				   order_less_imp_le]));
    1.73 -qed "real_of_posnat_ge_one";
    1.74 -Addsimps [real_of_posnat_ge_one];
    1.75 -
    1.76 -Goal "inverse(real_of_posnat n) ~= 0";
    1.77 -by (rtac ((real_of_posnat_gt_zero RS 
    1.78 -    real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1);
    1.79 -qed "real_of_posnat_real_inv_not_zero";
    1.80 -Addsimps [real_of_posnat_real_inv_not_zero];
    1.81 -
    1.82 -Goal "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y";
    1.83 -by (rtac (inj_real_of_posnat RS injD) 1);
    1.84 -by (res_inst_tac [("n2","x")] 
    1.85 -    (real_of_posnat_real_inv_not_zero RS real_mult_left_cancel RS iffD1) 1);
    1.86 -by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS 
    1.87 -    real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
    1.88 -qed "real_of_posnat_real_inv_inj";
    1.89 -
    1.90 -Goal "r < r + inverse(real_of_posnat n)";
    1.91 -by Auto_tac;
    1.92 -qed "real_add_inv_real_of_posnat_less";
    1.93 -Addsimps [real_add_inv_real_of_posnat_less];
    1.94 -
    1.95 -Goal "r <= r + inverse(real_of_posnat n)";
    1.96 -by Auto_tac;
    1.97 -qed "real_add_inv_real_of_posnat_le";
    1.98 -Addsimps [real_add_inv_real_of_posnat_le];
    1.99 -
   1.100 -Goal "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r";
   1.101 -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
   1.102 -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
   1.103 -by (auto_tac (claset() addIs [real_mult_order],simpset() 
   1.104 -    addsimps [real_add_assoc RS sym,real_minus_zero_less_iff2]));
   1.105 -qed "real_mult_less_self";
   1.106 -
   1.107 -Goal "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)";
   1.108 -by (Step_tac 1);
   1.109 -by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
   1.110 -                       RS real_mult_less_mono1) 1);
   1.111 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   1.112 -        real_inverse_gt_0 RS real_mult_less_mono1) 2);
   1.113 -by (auto_tac (claset(),
   1.114 -	      simpset() addsimps [(real_of_posnat_gt_zero RS 
   1.115 -    real_not_refl2 RS not_sym),real_mult_assoc]));
   1.116 -qed "real_of_posnat_inv_Ex_iff";
   1.117 -
   1.118 -Goal "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)";
   1.119 -by (Step_tac 1);
   1.120 -by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero 
   1.121 -                       RS real_mult_less_mono1) 1);
   1.122 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   1.123 -        real_inverse_gt_0 RS real_mult_less_mono1) 2);
   1.124 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
   1.125 -qed "real_of_posnat_inv_iff";
   1.126 -
   1.127 -Goal "[| (0::real) <=z; x<y |] ==> z*x<=z*y";
   1.128 -by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
   1.129 -qed "real_mult_le_less_mono2";
   1.130 -
   1.131 -Goal "[| (0::real) <=z; x<=y |] ==> z*x<=z*y";
   1.132 -by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
   1.133 -by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
   1.134 -qed "real_mult_le_le_mono1";
   1.135 -
   1.136 -Goal "[| (0::real)<=z; x<=y |] ==> x*z<=y*z";
   1.137 -by (dtac (real_mult_le_le_mono1) 1);
   1.138 -by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
   1.139 -qed "real_mult_le_le_mono2";
   1.140 -
   1.141 -Goal "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)";
   1.142 -by (Step_tac 1);
   1.143 -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
   1.144 -    order_less_imp_le RS real_mult_le_le_mono1) 1);
   1.145 -by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS 
   1.146 -        real_inverse_gt_0 RS order_less_imp_le RS 
   1.147 -        real_mult_le_le_mono1) 2);
   1.148 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   1.149 -qed "real_of_posnat_inv_le_iff";
   1.150 -
   1.151 -Goalw [real_of_posnat_def] 
   1.152 -      "(real_of_posnat n < real_of_posnat m) = (n < m)";
   1.153 -by Auto_tac;
   1.154 -qed "real_of_posnat_less_iff";
   1.155 -Addsimps [real_of_posnat_less_iff];
   1.156 -
   1.157 -Goal "(real_of_posnat n <= real_of_posnat m) = (n <= m)";
   1.158 -by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],
   1.159 -    simpset() addsimps [real_le_less,le_eq_less_or_eq]));
   1.160 -qed "real_of_posnat_le_iff";
   1.161 -Addsimps [real_of_posnat_le_iff];
   1.162 -
   1.163 -Goal "[| (0::real)<z; x*z<y*z |] ==> x<y";
   1.164 -by Auto_tac;
   1.165 -qed "real_mult_less_cancel3";
   1.166 -
   1.167 -Goal "[| (0::real)<z; z*x<z*y |] ==> x<y";
   1.168 -by Auto_tac;
   1.169 -qed "real_mult_less_cancel4";
   1.170 -
   1.171 -Goal "0 < u  ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))";
   1.172 -by (Step_tac 1);
   1.173 -by (res_inst_tac [("n2","n")] ((real_of_posnat_gt_zero RS 
   1.174 -    real_inverse_gt_0) RS real_mult_less_cancel3) 1);
   1.175 -by (res_inst_tac [("x1","u")] ( real_inverse_gt_0
   1.176 -   RS real_mult_less_cancel3) 2);
   1.177 -by (auto_tac (claset(),
   1.178 -	      simpset() addsimps [real_not_refl2 RS not_sym]));
   1.179 -by (res_inst_tac [("z","u")] real_mult_less_cancel4 1);
   1.180 -by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS 
   1.181 -    real_mult_less_cancel4) 3);
   1.182 -by (auto_tac (claset(),
   1.183 -	      simpset() addsimps [real_not_refl2 RS not_sym,
   1.184 -              real_mult_assoc RS sym]));
   1.185 -qed "real_of_posnat_less_inv_iff";
   1.186 -
   1.187 -Goal "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)";
   1.188 -by Auto_tac;
   1.189 -qed "real_of_posnat_inv_eq_iff";
   1.190 -
   1.191 -Goal "0 <= 1 + -inverse(real_of_posnat n)";
   1.192 -by (res_inst_tac [("C","inverse(real_of_posnat n)")] real_le_add_right_cancel 1);
   1.193 -by (simp_tac (simpset() addsimps [real_add_assoc,
   1.194 -    real_of_posnat_inv_le_iff]) 1);
   1.195 -qed "real_add_one_minus_inv_ge_zero";
   1.196 -
   1.197 -Goal "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))";
   1.198 -by (dtac (real_add_one_minus_inv_ge_zero RS real_mult_le_less_mono1) 1);
   1.199 -by (Auto_tac);
   1.200 -qed "real_mult_add_one_minus_ge_zero";
   1.201 -
   1.202 -Goal "x*y = (1::real) ==> y = inverse x";
   1.203 -by (case_tac "x ~= 0" 1);
   1.204 -by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
   1.205 -by Auto_tac;
   1.206 -qed "real_inverse_unique";
   1.207 -
   1.208 -Goal "[| (0::real) < x; x < 1 |] ==> 1 < inverse x";
   1.209 -by (auto_tac (claset() addDs [real_inverse_less_swap],simpset()));
   1.210 -qed "real_inverse_gt_one";
   1.211 -
   1.212 -Goal "(0 < real (n::nat)) = (0 < n)";
   1.213 -by (rtac (real_of_nat_less_iff RS subst) 1);
   1.214 -by Auto_tac;
   1.215 -qed "real_of_nat_gt_zero_cancel_iff";
   1.216 -Addsimps [real_of_nat_gt_zero_cancel_iff];
   1.217 -
   1.218 -Goal "(real (n::nat) <= 0) = (n = 0)";
   1.219 -by (rtac ((real_of_nat_zero) RS subst) 1);
   1.220 -by (stac real_of_nat_le_iff 1);
   1.221 -by Auto_tac;
   1.222 -qed "real_of_nat_le_zero_cancel_iff";
   1.223 -Addsimps [real_of_nat_le_zero_cancel_iff];
   1.224 -
   1.225 -Goal "~ real (n::nat) < 0";
   1.226 -by (simp_tac (simpset() addsimps [symmetric real_le_def,
   1.227 -    real_of_nat_ge_zero]) 1);
   1.228 -qed "not_real_of_nat_less_zero";
   1.229 -Addsimps [not_real_of_nat_less_zero];
   1.230 -
   1.231 -Goalw [real_le_def,le_def] 
   1.232 -      "(0 <= real (n::nat)) = (0 <= n)";
   1.233 -by (Simp_tac 1);
   1.234 -qed "real_of_nat_ge_zero_cancel_iff";
   1.235 -Addsimps [real_of_nat_ge_zero_cancel_iff];
   1.236 -
   1.237 -Goal "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))";
   1.238 -by (case_tac "n" 1);
   1.239 -by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc]));
   1.240 -qed "real_of_nat_num_if";
   1.241 -
   1.242 -Goal "4 * real n = real (4 * (n::nat))";
   1.243 -by Auto_tac;
   1.244 -qed "real_of_nat_mult_num_4_eq";
   1.245 -
   1.246 -(*REDUNDANT
   1.247 -    Goal "x * x = -(y * y) ==> x = (0::real)";
   1.248 -    by (auto_tac (claset() addIs [
   1.249 -	real_sum_squares_cancel],simpset()));
   1.250 -    qed "real_sum_squares_cancel1a";
   1.251 -
   1.252 -    Goal "x * x = -(y * y) ==> y = (0::real)";
   1.253 -    by (auto_tac (claset() addIs [
   1.254 -	real_sum_squares_cancel],simpset()));
   1.255 -    qed "real_sum_squares_cancel2a";
   1.256 -*)
   1.257 -
   1.258 -Goal "x * x = -(y * y) ==> x = (0::real) & y=0";
   1.259 -by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset()));
   1.260 -qed "real_sum_squares_cancel_a";
   1.261 -
   1.262 -Goal "x*x - (1::real) = (x + 1)*(x - 1)";
   1.263 -by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib,
   1.264 -    real_add_mult_distrib2,real_diff_def]));
   1.265 -qed "real_squared_diff_one_factored";
   1.266 -
   1.267 -Goal "(x*x = (1::real)) = (x = 1 | x = - 1)";
   1.268 -by Auto_tac;
   1.269 -by (dtac (CLAIM "x = (y::real) ==> x - y = 0") 1);
   1.270 -by (auto_tac (claset(),simpset() addsimps [real_squared_diff_one_factored]));
   1.271 -qed "real_mult_is_one";
   1.272 -AddIffs [real_mult_is_one];
   1.273 -
   1.274 -Goal "(x + y/2 <= (y::real)) = (x <= y /2)";
   1.275 -by Auto_tac;
   1.276 -qed "real_le_add_half_cancel";
   1.277 -Addsimps [real_le_add_half_cancel];
   1.278 -
   1.279 -Goal "(x::real) - x/2 = x/2";
   1.280 -by Auto_tac;
   1.281 -qed "real_minus_half_eq";
   1.282 -Addsimps [real_minus_half_eq];
   1.283 -
   1.284 -Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> inverse x * y < inverse x1 * u";
   1.285 -by (multl_by_tac "x" 1);
   1.286 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
   1.287 -by (simp_tac (simpset() addsimps real_mult_ac) 1);
   1.288 -by (multr_by_tac "x1" 1);
   1.289 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
   1.290 -qed "real_mult_inverse_cancel";
   1.291 -
   1.292 -Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1";
   1.293 -by (auto_tac (claset() addDs [real_mult_inverse_cancel],simpset() addsimps real_mult_ac));
   1.294 -qed "real_mult_inverse_cancel2";
   1.295 -
   1.296 -Goal "0 < inverse (real (Suc n))";
   1.297 -by Auto_tac;
   1.298 -qed "inverse_real_of_nat_gt_zero";
   1.299 -Addsimps [ inverse_real_of_nat_gt_zero];
   1.300 -
   1.301 -Goal "0 <= inverse (real (Suc n))";
   1.302 -by Auto_tac;
   1.303 -qed "inverse_real_of_nat_ge_zero";
   1.304 -Addsimps [ inverse_real_of_nat_ge_zero];
   1.305 -
   1.306 -Goal "x ~= 0 ==> x * x + y * y ~= (0::real)";
   1.307 -by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
   1.308 -by (dtac (real_sum_squares_cancel) 1);
   1.309 -by (Asm_full_simp_tac 1);
   1.310 -qed "real_sum_squares_not_zero";
   1.311 -
   1.312 -Goal "y ~= 0 ==> x * x + y * y ~= (0::real)";
   1.313 -by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
   1.314 -by (dtac (real_sum_squares_cancel2) 1);
   1.315 -by (Asm_full_simp_tac 1);
   1.316 -qed "real_sum_squares_not_zero2";
   1.317 -
   1.318 -(* RealAbs *)
   1.319 -
   1.320 -(* nice theorem *)
   1.321 -Goal "abs x * abs x = x * (x::real)";
   1.322 -by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
   1.323 -by (auto_tac (claset(),simpset() addsimps [abs_eqI2,abs_minus_eqI2]));
   1.324 -qed "abs_mult_abs";
   1.325 -Addsimps [abs_mult_abs];
   1.326 -
   1.327 -(* RealPow *)
   1.328 -Goalw [real_divide_def]
   1.329 -    "(x/y) ^ n = ((x::real) ^ n/ y ^ n)";
   1.330 -by (auto_tac (claset(),simpset() addsimps [realpow_mult,
   1.331 -    realpow_inverse]));
   1.332 -qed "realpow_divide";
   1.333 -
   1.334 -Goal "isCont (%x. x ^ n) x";
   1.335 -by (rtac (DERIV_pow RS DERIV_isCont) 1);
   1.336 -qed "isCont_realpow";
   1.337 -Addsimps [isCont_realpow];
   1.338 -
   1.339 -Goal "(0::real) <= r --> 0 <= r ^ n";
   1.340 -by (induct_tac "n" 1);
   1.341 -by (auto_tac (claset(),simpset() addsimps [real_0_le_mult_iff]));
   1.342 -qed_spec_mp "realpow_ge_zero2";
   1.343 -
   1.344 -Goal "(0::real) <= x & x <= y --> x ^ n <= y ^ n";
   1.345 -by (induct_tac "n" 1);
   1.346 -by (auto_tac (claset() addSIs [real_mult_le_mono],
   1.347 -    simpset() addsimps [realpow_ge_zero2]));
   1.348 -qed_spec_mp "realpow_le2";
   1.349 -
   1.350 -Goal "(1::real) < r ==> 1 < r ^ (Suc n)";
   1.351 -by (forw_inst_tac [("n","n")] realpow_ge_one 1);
   1.352 -by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
   1.353 -by (forward_tac [(real_zero_less_one RS real_less_trans)] 1);
   1.354 -by (dres_inst_tac [("y","r ^ n")] (real_mult_less_mono2) 1);
   1.355 -by (assume_tac 1);
   1.356 -by (auto_tac (claset() addDs [real_less_trans],simpset()));
   1.357 -qed "realpow_Suc_gt_one";
   1.358 -
   1.359 -Goal "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)";
   1.360 -by (auto_tac (claset() addIs [real_sum_squares_cancel, real_sum_squares_cancel2], 
   1.361 -              simpset() addsimps [numeral_2_eq_2]));
   1.362 -qed "realpow_two_sum_zero_iff";
   1.363 -Addsimps [realpow_two_sum_zero_iff];
   1.364 -
   1.365 -Goal "(0::real) <= u ^ 2 + v ^ 2";
   1.366 -by (rtac (real_le_add_order) 1);
   1.367 -by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   1.368 -qed "realpow_two_le_add_order";
   1.369 -Addsimps [realpow_two_le_add_order];
   1.370 -
   1.371 -Goal "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2";
   1.372 -by (REPEAT(rtac (real_le_add_order) 1));
   1.373 -by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   1.374 -qed "realpow_two_le_add_order2";
   1.375 -Addsimps [realpow_two_le_add_order2];
   1.376 -
   1.377 -Goal "(0::real) <= x*x + y*y";
   1.378 -by (cut_inst_tac [("u","x"),("v","y")] realpow_two_le_add_order 1);
   1.379 -by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   1.380 -qed "real_mult_self_sum_ge_zero";
   1.381 -Addsimps [real_mult_self_sum_ge_zero];
   1.382 -Addsimps [real_mult_self_sum_ge_zero RS abs_eqI1];
   1.383 -
   1.384 -Goal "x ~= 0 ==> (0::real) < x * x + y * y";
   1.385 -by (cut_inst_tac [("x","x"),("y","y")] real_mult_self_sum_ge_zero 1);
   1.386 -by (dtac real_le_imp_less_or_eq 1);
   1.387 -by (dres_inst_tac [("y","y")] real_sum_squares_not_zero 1);
   1.388 -by Auto_tac;
   1.389 -qed "real_sum_square_gt_zero";
   1.390 -
   1.391 -Goal "y ~= 0 ==> (0::real) < x * x + y * y";
   1.392 -by (rtac (real_add_commute RS subst) 1);
   1.393 -by (etac real_sum_square_gt_zero 1);
   1.394 -qed "real_sum_square_gt_zero2";
   1.395 -
   1.396 -Goal "-(u * u) <= (x * (x::real))";
   1.397 -by (res_inst_tac [("j","0")] real_le_trans 1);
   1.398 -by Auto_tac;
   1.399 -qed "real_minus_mult_self_le";
   1.400 -Addsimps [real_minus_mult_self_le];
   1.401 -
   1.402 -Goal "-(u ^ 2) <= (x::real) ^ 2";
   1.403 -by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
   1.404 -qed "realpow_square_minus_le";
   1.405 -Addsimps [realpow_square_minus_le];
   1.406 -
   1.407 -Goal "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))";
   1.408 -by (case_tac "n" 1);
   1.409 -by Auto_tac;
   1.410 -qed "realpow_num_eq_if";
   1.411 -
   1.412 -Goal "0 < (2::real) ^ (4*d)";
   1.413 -by (induct_tac "d" 1);
   1.414 -by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
   1.415 -qed "real_num_zero_less_two_pow";
   1.416 -Addsimps [real_num_zero_less_two_pow];
   1.417 -
   1.418 -Goal "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)";
   1.419 -by (subgoal_tac "(2::real) ^ 8 = 4 * (2 ^ 6)" 1);
   1.420 -by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
   1.421 -by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
   1.422 -qed "lemma_realpow_num_two_mono";
   1.423 -
   1.424 -Goal "2 ^ 2 = (4::real)";
   1.425 -by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
   1.426 -val lemma_realpow_4 = result();
   1.427 -Addsimps [lemma_realpow_4];
   1.428 -
   1.429 -Goal "2 ^ 4 = (16::real)";
   1.430 -by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
   1.431 -val lemma_realpow_16 = result();
   1.432 -Addsimps [lemma_realpow_16];
   1.433 -
   1.434 -(* HyperOrd *)
   1.435 -
   1.436 -Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
   1.437 -by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
   1.438 -    hypreal_mult_less_zero]));
   1.439 -qed "hypreal_mult_less_zero2";
   1.440 -
   1.441 -(* HyperPow *)
   1.442 -Goal "(0::hypreal) <= x * x";
   1.443 -by (auto_tac (claset(),simpset() addsimps 
   1.444 -    [hypreal_0_le_mult_iff]));
   1.445 -qed "hypreal_mult_self_ge_zero";
   1.446 -Addsimps [hypreal_mult_self_ge_zero];
   1.447 -
   1.448 -(* deleted from distribution but I prefer to have it *)
   1.449 -Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
   1.450 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.451 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   1.452 -by (auto_tac (claset(),simpset() addsimps 
   1.453 -    [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
   1.454 -by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
   1.455 -    simpset()) 1);
   1.456 -qed "hrealpow_Suc_cancel_eq";
   1.457 -
   1.458 -(* NSA.ML: next two were there before? Not in distrib though *)
   1.459 -
   1.460 -Goal "[| x + y : HInfinite; y: HFinite |] ==> x : HInfinite";
   1.461 -by (rtac ccontr 1);
   1.462 -by (dtac (HFinite_HInfinite_iff RS iffD2) 1);
   1.463 -by (auto_tac (claset() addDs [HFinite_add],simpset() 
   1.464 -    addsimps [HInfinite_HFinite_iff]));
   1.465 -qed "HInfinite_HFinite_add_cancel";
   1.466 -
   1.467 -Goal "[| x : HInfinite; y : HFinite |] ==> x + y : HInfinite";
   1.468 -by (res_inst_tac [("y","-y")] HInfinite_HFinite_add_cancel 1);
   1.469 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc,
   1.470 -    HFinite_minus_iff]));
   1.471 -qed "HInfinite_HFinite_add";
   1.472 -
   1.473 -Goal "[| x : HInfinite; x <= y; 0 <= x |] ==> y : HInfinite";
   1.474 -by (auto_tac (claset() addIs [HFinite_bounded],simpset() 
   1.475 -    addsimps [HInfinite_HFinite_iff]));
   1.476 -qed "HInfinite_ge_HInfinite";
   1.477 -
   1.478 -Goal "[| x : Infinitesimal; x ~= 0 |] ==> inverse x : HInfinite";
   1.479 -by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
   1.480 -by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult2],simpset()));
   1.481 -qed "Infinitesimal_inverse_HInfinite";
   1.482 -
   1.483 -Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
   1.484 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.485 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
   1.486 -    HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
   1.487 -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   1.488 -by Auto_tac;
   1.489 -by (dres_inst_tac [("x","m + 1")] spec 1);
   1.490 -by (Ultra_tac 1);
   1.491 -by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
   1.492 -by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
   1.493 -by (rtac real_inverse_less_swap 1);
   1.494 -by Auto_tac;
   1.495 -qed "HNatInfinite_inverse_Infinitesimal";
   1.496 -Addsimps [HNatInfinite_inverse_Infinitesimal];
   1.497 -
   1.498 -Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
   1.499 -by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
   1.500 -qed "HNatInfinite_inverse_not_zero";
   1.501 -Addsimps [HNatInfinite_inverse_not_zero];
   1.502 -
   1.503 -Goal "N : HNatInfinite \
   1.504 -\     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
   1.505 -by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   1.506 -by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   1.507 -by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
   1.508 -qed "starfunNat_inverse_real_of_nat_Infinitesimal";
   1.509 -Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
   1.510 -
   1.511 -Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
   1.512 -\     ==> x * y : HInfinite";
   1.513 -by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1); 
   1.514 -by (ftac HFinite_Infinitesimal_not_zero 1);
   1.515 -by (dtac HFinite_not_Infinitesimal_inverse 1);
   1.516 -by (Step_tac 1 THEN dtac HFinite_mult 1);
   1.517 -by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
   1.518 -    HFinite_HInfinite_iff]));
   1.519 -qed "HInfinite_HFinite_not_Infinitesimal_mult";
   1.520 -
   1.521 -Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
   1.522 -\     ==> y * x : HInfinite";
   1.523 -by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
   1.524 -    HInfinite_HFinite_not_Infinitesimal_mult]));
   1.525 -qed "HInfinite_HFinite_not_Infinitesimal_mult2";
   1.526 -
   1.527 -Goal "[| x : HInfinite; 0 < x; y : Reals |] ==> y < x";
   1.528 -by (auto_tac (claset() addSDs [bspec],simpset() addsimps 
   1.529 -    [HInfinite_def,hrabs_def,order_less_imp_le]));
   1.530 -qed "HInfinite_gt_SReal";
   1.531 -
   1.532 -Goal "[| x : HInfinite; 0 < x |] ==> 1 < x";
   1.533 -by (auto_tac (claset() addIs [HInfinite_gt_SReal],simpset()));
   1.534 -qed "HInfinite_gt_zero_gt_one";
   1.535 -
   1.536 -(* not added at proof?? *)
   1.537 -Addsimps [HInfinite_omega];
   1.538 -
   1.539 -(* Add in HyperDef.ML? *)
   1.540 -Goalw [omega_def] "0 < omega";
   1.541 -by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
   1.542 -qed "hypreal_omega_gt_zero";
   1.543 -Addsimps [hypreal_omega_gt_zero];
   1.544 -
   1.545 -Goal "1 ~: HInfinite";
   1.546 -by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
   1.547 -qed "not_HInfinite_one";
   1.548 -Addsimps [not_HInfinite_one];
   1.549 -
   1.550 -
   1.551 -(* RComplete.ML *)
   1.552 -
   1.553 -Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x";
   1.554 -by (Step_tac 1);
   1.555 -by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1);
   1.556 -by (Step_tac 1);
   1.557 -by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1);
   1.558 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def]));
   1.559 -qed "reals_Archimedean3";
   1.560 -
     2.1 --- a/src/HOL/Hyperreal/ExtraThms2.thy	Tue Nov 25 10:37:03 2003 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1 +0,0 @@
     2.4 -ExtraThms2 = HSeries 
     2.5 \ No newline at end of file
     3.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Tue Nov 25 10:37:03 2003 +0100
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.ML	Thu Nov 27 10:47:55 2003 +0100
     3.3 @@ -1238,3 +1238,20 @@
     3.4       (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
     3.5  qed "hypreal_eq_eqI";
     3.6  
     3.7 +
     3.8 +(*MOVE UP*)
     3.9 +Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
    3.10 +by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
    3.11 +qed "hypreal_zero_num";
    3.12 +
    3.13 +Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
    3.14 +by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
    3.15 +qed "hypreal_one_num";
    3.16 +
    3.17 +
    3.18 +(*MOVE UP*)
    3.19 +
    3.20 +Goalw [omega_def] "0 < omega";
    3.21 +by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
    3.22 +qed "hypreal_omega_gt_zero";
    3.23 +Addsimps [hypreal_omega_gt_zero];
     4.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Tue Nov 25 10:37:03 2003 +0100
     4.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Thu Nov 27 10:47:55 2003 +0100
     4.3 @@ -1308,3 +1308,22 @@
     4.4  
     4.5  
     4.6  
     4.7 +(*MOVE UP*)
     4.8 +Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
     4.9 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    4.10 +by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
    4.11 +    HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
    4.12 +by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    4.13 +by Auto_tac;
    4.14 +by (dres_inst_tac [("x","m + 1")] spec 1);
    4.15 +by (Ultra_tac 1);
    4.16 +by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
    4.17 +by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
    4.18 +qed "HNatInfinite_inverse_Infinitesimal";
    4.19 +Addsimps [HNatInfinite_inverse_Infinitesimal];
    4.20 +
    4.21 +Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
    4.22 +by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
    4.23 +qed "HNatInfinite_inverse_not_zero";
    4.24 +Addsimps [HNatInfinite_inverse_not_zero];
    4.25 +
     5.1 --- a/src/HOL/Hyperreal/HyperOrd.ML	Tue Nov 25 10:37:03 2003 +0100
     5.2 +++ b/src/HOL/Hyperreal/HyperOrd.ML	Thu Nov 27 10:47:55 2003 +0100
     5.3 @@ -523,3 +523,7 @@
     5.4                                    linorder_not_less RS sym]));
     5.5  qed "hypreal_mult_le_0_iff";
     5.6  
     5.7 +Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
     5.8 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
     5.9 +    hypreal_mult_less_zero]));
    5.10 +qed "hypreal_mult_less_zero2";
     6.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Tue Nov 25 10:37:03 2003 +0100
     6.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Thu Nov 27 10:47:55 2003 +0100
     6.3 @@ -533,3 +533,20 @@
     6.4                          hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
     6.5                delsimps [hypnat_of_nat_less_iff RS sym]));
     6.6  qed "Infinitesimal_hrealpow";
     6.7 +
     6.8 +(* MOVE UP *)
     6.9 +Goal "(0::hypreal) <= x * x";
    6.10 +by (auto_tac (claset(),simpset() addsimps 
    6.11 +    [hypreal_0_le_mult_iff]));
    6.12 +qed "hypreal_mult_self_ge_zero";
    6.13 +Addsimps [hypreal_mult_self_ge_zero];
    6.14 +
    6.15 +Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
    6.16 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    6.17 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    6.18 +by (auto_tac (claset(),simpset() addsimps 
    6.19 +    [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
    6.20 +by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
    6.21 +    simpset()) 1);
    6.22 +qed "hrealpow_Suc_cancel_eq";
    6.23 +
     7.1 --- a/src/HOL/Hyperreal/NSA.ML	Tue Nov 25 10:37:03 2003 +0100
     7.2 +++ b/src/HOL/Hyperreal/NSA.ML	Thu Nov 27 10:47:55 2003 +0100
     7.3 @@ -2177,6 +2177,7 @@
     7.4  by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
     7.5                                    FreeUltrafilterNat_omega]) 1);
     7.6  qed "HInfinite_omega";
     7.7 +Addsimps [HInfinite_omega];
     7.8  
     7.9  (*-----------------------------------------------
    7.10         Epsilon is a member of Infinitesimal
    7.11 @@ -2324,3 +2325,62 @@
    7.12              [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
    7.13               hypreal_inverse]));
    7.14  qed "real_seq_to_hypreal_Infinitesimal2";
    7.15 +
    7.16 +
    7.17 +
    7.18 +
    7.19 +
    7.20 +(*MOVE UP*)
    7.21 +Goal "[| x + y : HInfinite; y: HFinite |] ==> x : HInfinite";
    7.22 +by (rtac ccontr 1);
    7.23 +by (dtac (HFinite_HInfinite_iff RS iffD2) 1);
    7.24 +by (auto_tac (claset() addDs [HFinite_add],simpset() 
    7.25 +    addsimps [HInfinite_HFinite_iff]));
    7.26 +qed "HInfinite_HFinite_add_cancel";
    7.27 +
    7.28 +Goal "[| x : HInfinite; y : HFinite |] ==> x + y : HInfinite";
    7.29 +by (res_inst_tac [("y","-y")] HInfinite_HFinite_add_cancel 1);
    7.30 +by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc,
    7.31 +    HFinite_minus_iff]));
    7.32 +qed "HInfinite_HFinite_add";
    7.33 +
    7.34 +Goal "[| x : HInfinite; x <= y; 0 <= x |] ==> y : HInfinite";
    7.35 +by (auto_tac (claset() addIs [HFinite_bounded],simpset() 
    7.36 +    addsimps [HInfinite_HFinite_iff]));
    7.37 +qed "HInfinite_ge_HInfinite";
    7.38 +
    7.39 +Goal "[| x : Infinitesimal; x ~= 0 |] ==> inverse x : HInfinite";
    7.40 +by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
    7.41 +by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult2],simpset()));
    7.42 +qed "Infinitesimal_inverse_HInfinite";
    7.43 +
    7.44 +Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
    7.45 +\     ==> x * y : HInfinite";
    7.46 +by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1); 
    7.47 +by (ftac HFinite_Infinitesimal_not_zero 1);
    7.48 +by (dtac HFinite_not_Infinitesimal_inverse 1);
    7.49 +by (Step_tac 1 THEN dtac HFinite_mult 1);
    7.50 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
    7.51 +    HFinite_HInfinite_iff]));
    7.52 +qed "HInfinite_HFinite_not_Infinitesimal_mult";
    7.53 +
    7.54 +Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
    7.55 +\     ==> y * x : HInfinite";
    7.56 +by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
    7.57 +    HInfinite_HFinite_not_Infinitesimal_mult]));
    7.58 +qed "HInfinite_HFinite_not_Infinitesimal_mult2";
    7.59 +
    7.60 +Goal "[| x : HInfinite; 0 < x; y : Reals |] ==> y < x";
    7.61 +by (auto_tac (claset() addSDs [bspec],simpset() addsimps 
    7.62 +    [HInfinite_def,hrabs_def,order_less_imp_le]));
    7.63 +qed "HInfinite_gt_SReal";
    7.64 +
    7.65 +Goal "[| x : HInfinite; 0 < x |] ==> 1 < x";
    7.66 +by (auto_tac (claset() addIs [HInfinite_gt_SReal],simpset()));
    7.67 +qed "HInfinite_gt_zero_gt_one";
    7.68 +
    7.69 +
    7.70 +Goal "1 ~: HInfinite";
    7.71 +by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
    7.72 +qed "not_HInfinite_one";
    7.73 +Addsimps [not_HInfinite_one];
     8.1 --- a/src/HOL/Hyperreal/NatStar.ML	Tue Nov 25 10:37:03 2003 +0100
     8.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Thu Nov 27 10:47:55 2003 +0100
     8.3 @@ -479,3 +479,15 @@
     8.4  by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
     8.5  by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
     8.6  qed "starfun_eq_iff";
     8.7 +
     8.8 +
     8.9 +
    8.10 +(*MOVE UP*)
    8.11 +
    8.12 +Goal "N : HNatInfinite \
    8.13 +\     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
    8.14 +by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
    8.15 +by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
    8.16 +by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
    8.17 +qed "starfunNat_inverse_real_of_nat_Infinitesimal";
    8.18 +Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
     9.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Nov 25 10:37:03 2003 +0100
     9.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Thu Nov 27 10:47:55 2003 +0100
     9.3 @@ -5,4 +5,4 @@
     9.4                     http://www.math.unl.edu/~webnotes
     9.5  *)
     9.6  
     9.7 -NthRoot = SEQ + ExtraThms2
     9.8 +NthRoot = SEQ + HSeries
    10.1 --- a/src/HOL/Hyperreal/SEQ.ML	Tue Nov 25 10:37:03 2003 +0100
    10.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Thu Nov 27 10:47:55 2003 +0100
    10.3 @@ -661,7 +661,7 @@
    10.4  by (dtac lemma_converg3 1);
    10.5  by (dtac isLub_le_isUb 1 THEN assume_tac 1);
    10.6  by (auto_tac (claset() addDs [order_less_le_trans],
    10.7 -              simpset() addsimps [real_minus_zero_le_iff]));
    10.8 +              simpset()));
    10.9  val lemma_converg4 = result();
   10.10  
   10.11  (*-------------------------------------------------------------------
    11.1 --- a/src/HOL/Hyperreal/Transcendental.ML	Tue Nov 25 10:37:03 2003 +0100
    11.2 +++ b/src/HOL/Hyperreal/Transcendental.ML	Thu Nov 27 10:47:55 2003 +0100
    11.3 @@ -5,6 +5,13 @@
    11.4      Description : Power Series
    11.5  *)
    11.6  
    11.7 +fun multr_by_tac x i = 
    11.8 +       let val cancel_thm = 
    11.9 +           CLAIM "[| (0::real)<z; x*z<y*z |] ==> x<y" 
   11.10 +       in
   11.11 +           res_inst_tac [("z",x)] cancel_thm i 
   11.12 +       end;
   11.13 +
   11.14  Goalw [root_def] "root (Suc n) 0 = 0";
   11.15  by (safe_tac (claset() addSIs [some_equality,realpow_zero] 
   11.16      addSEs [realpow_zero_zero]));
    12.1 --- a/src/HOL/Integ/Int.thy	Tue Nov 25 10:37:03 2003 +0100
    12.2 +++ b/src/HOL/Integ/Int.thy	Thu Nov 27 10:47:55 2003 +0100
    12.3 @@ -393,11 +393,6 @@
    12.4  lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
    12.5    by (rule Ring_and_Field.mult_strict_right_mono)
    12.6  
    12.7 -(* < monotonicity, BOTH arguments*)
    12.8 -lemma zmult_zless_mono:
    12.9 -     "[| i < j;  k < l;  (0::int) < j;  (0::int) < k |] ==> i*k < j*l"
   12.10 -  by (rule Ring_and_Field.mult_strict_mono)
   12.11 -
   12.12  lemma zmult_zless_mono1_neg: "[| i<j;  k < (0::int) |] ==> j*k < i*k"
   12.13    by (rule Ring_and_Field.mult_strict_right_mono_neg)
   12.14  
   12.15 @@ -501,7 +496,6 @@
   12.16  val zmult_zle_mono = thm "zmult_zle_mono";
   12.17  val zmult_zless_mono2 = thm "zmult_zless_mono2";
   12.18  val zmult_zless_mono1 = thm "zmult_zless_mono1";
   12.19 -val zmult_zless_mono = thm "zmult_zless_mono";
   12.20  val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
   12.21  val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
   12.22  val zmult_eq_0_iff = thm "zmult_eq_0_iff";
    13.1 --- a/src/HOL/IsaMakefile	Tue Nov 25 10:37:03 2003 +0100
    13.2 +++ b/src/HOL/IsaMakefile	Thu Nov 27 10:47:55 2003 +0100
    13.3 @@ -147,8 +147,8 @@
    13.4    Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
    13.5    Real/RealInt.thy Real/RealOrd.thy \
    13.6    Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
    13.7 -  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
    13.8 -  Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
    13.9 +  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
   13.10 +  Hyperreal/Fact.ML Hyperreal/Fact.thy\
   13.11    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
   13.12    Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   13.13    Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
    14.1 --- a/src/HOL/Real/RComplete.ML	Tue Nov 25 10:37:03 2003 +0100
    14.2 +++ b/src/HOL/Real/RComplete.ML	Thu Nov 27 10:47:55 2003 +0100
    14.3 @@ -238,10 +238,16 @@
    14.4  by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1);
    14.5  by (forw_inst_tac [("y","inverse x")] real_mult_less_mono1 1);
    14.6  by Auto_tac;  
    14.7 -by (dres_inst_tac [("y","1"),("z","real (Suc n)")]
    14.8 -    (rotate_prems 1 real_mult_less_mono2) 1);
    14.9 -by (auto_tac (claset(),
   14.10 -	      simpset() addsimps [real_of_nat_Suc_gt_zero,
   14.11 -				  real_not_refl2 RS not_sym,
   14.12 -				  real_mult_assoc RS sym]));
   14.13 +by (rtac (thm "less_imp_inverse_less") 1); 
   14.14 +by (assume_tac 1); 
   14.15 +by (assume_tac 1); 
   14.16  qed "reals_Archimedean2";
   14.17 +
   14.18 +Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x";
   14.19 +by (Step_tac 1);
   14.20 +by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1);
   14.21 +by (Step_tac 1);
   14.22 +by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1);
   14.23 +by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def]));
   14.24 +qed "reals_Archimedean3";
   14.25 +
    15.1 --- a/src/HOL/Real/RealArith0.ML	Tue Nov 25 10:37:03 2003 +0100
    15.2 +++ b/src/HOL/Real/RealArith0.ML	Thu Nov 27 10:47:55 2003 +0100
    15.3 @@ -79,8 +79,6 @@
    15.4  
    15.5  Goal "(inverse(x::real) = 0) = (x = 0)";
    15.6  by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO]));
    15.7 -by (rtac ccontr 1);
    15.8 -by (blast_tac (claset() addDs [real_inverse_not_zero]) 1);
    15.9  qed "real_inverse_zero_iff";
   15.10  Addsimps [real_inverse_zero_iff];
   15.11  
   15.12 @@ -480,14 +478,8 @@
   15.13                                    real_eq_divide_eq, real_mult_eq_cancel1]));
   15.14  qed "real_divide_eq_cancel1";
   15.15  
   15.16 -(*Moved from RealOrd.ML to use 0 *)
   15.17  Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
   15.18  by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
   15.19 -by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
   15.20 -by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
   15.21 -by (auto_tac (claset() addIs [real_inverse_less_swap],
   15.22 -              simpset() delsimps [real_inverse_inverse]
   15.23 -                        addsimps [real_inverse_gt_0]));
   15.24  qed "real_inverse_less_iff";
   15.25  
   15.26  Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
    16.1 --- a/src/HOL/Real/RealDef.ML	Tue Nov 25 10:37:03 2003 +0100
    16.2 +++ b/src/HOL/Real/RealDef.ML	Thu Nov 27 10:47:55 2003 +0100
    16.3 @@ -497,7 +497,7 @@
    16.4  
    16.5  Goal "a / (0::real) = 0";
    16.6  by (simp_tac (simpset() addsimps [real_divide_def, INVERSE_ZERO]) 1);
    16.7 -qed "DIVISION_BY_ZERO";  (*NOT for adding to default simpset*)
    16.8 +qed "DIVISION_BY_ZERO"; 
    16.9  
   16.10  fun real_div_undefined_case_tac s i =
   16.11    case_tac s i THEN 
    17.1 --- a/src/HOL/Real/RealOrd.thy	Tue Nov 25 10:37:03 2003 +0100
    17.2 +++ b/src/HOL/Real/RealOrd.thy	Thu Nov 27 10:47:55 2003 +0100
    17.3 @@ -113,46 +113,12 @@
    17.4  lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
    17.5  by (blast intro!: real_less_all_preal real_leI)
    17.6  
    17.7 -lemma real_lemma_add_positive_imp_less: "[| R + L = S;  (0::real) < L |] ==> R < S"
    17.8 -apply (rule real_less_sum_gt_0_iff [THEN iffD1])
    17.9 -apply (auto simp add: real_add_ac)
   17.10 -done
   17.11 -
   17.12 -lemma real_ex_add_positive_left_less: "\<exists>T::real. 0 < T & R + T = S ==> R < S"
   17.13 -by (blast intro: real_lemma_add_positive_imp_less)
   17.14 -
   17.15 -(*Alternative definition for real_less.  NOT for rewriting*)
   17.16 -lemma real_less_iff_add: "(R < S) = (\<exists>T::real. 0 < T & R + T = S)"
   17.17 -by (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
   17.18 -
   17.19  lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
   17.20  apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
   17.21  apply (drule order_le_less_trans, assumption)
   17.22  apply (erule preal_less_irrefl)
   17.23  done
   17.24  
   17.25 -lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
   17.26 -apply (auto simp add: real_gt_zero_preal_Ex)
   17.27 -apply (rule_tac x = "y*ya" in exI)
   17.28 -apply (simp (no_asm_use) add: real_of_preal_mult)
   17.29 -done
   17.30 -
   17.31 -lemma neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y"
   17.32 -apply (drule real_minus_zero_less_iff [THEN iffD2])+
   17.33 -apply (drule real_mult_order, assumption, simp)
   17.34 -done
   17.35 -
   17.36 -lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)"
   17.37 -apply (drule real_minus_zero_less_iff [THEN iffD2])
   17.38 -apply (drule real_mult_order, assumption)
   17.39 -apply (rule real_minus_zero_less_iff [THEN iffD1], simp)
   17.40 -done
   17.41 -
   17.42 -lemma real_zero_less_one: "0 < (1::real)"
   17.43 -by (auto intro: real_gt_zero_preal_Ex [THEN iffD2] 
   17.44 -         simp add: real_one_def real_of_preal_def)
   17.45 -
   17.46 -
   17.47  subsection{*Monotonicity of Addition*}
   17.48  
   17.49  lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
   17.50 @@ -167,97 +133,17 @@
   17.51  lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
   17.52  by simp
   17.53  
   17.54 -(*"v\<le>w ==> v+z \<le> w+z"*)
   17.55 -lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
   17.56 -
   17.57 -(*"v\<le>w ==> v+z \<le> w+z"*)
   17.58 -lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
   17.59 -
   17.60 -lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
   17.61 -by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
   17.62 -
   17.63 -lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
   17.64 -by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
   17.65 -
   17.66 -lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
   17.67 -by simp
   17.68 -
   17.69 -lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
   17.70 -apply (simp (no_asm_use))
   17.71 -done
   17.72 -
   17.73 -lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
   17.74 -apply (simp (no_asm_use))
   17.75 -done
   17.76 -
   17.77 -lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
   17.78 -apply (simp (no_asm_use))
   17.79 -done
   17.80 -
   17.81 -lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
   17.82 -apply (simp (no_asm_use))
   17.83 -done
   17.84 -
   17.85 -lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
   17.86 -apply (erule order_less_trans)
   17.87 -apply (drule real_add_less_mono2)
   17.88 -apply (simp (no_asm_use))
   17.89 -done
   17.90 -
   17.91 -lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
   17.92 -apply (drule order_le_imp_less_or_eq)+
   17.93 -apply (auto intro: real_add_order order_less_imp_le)
   17.94 -done
   17.95 -
   17.96 -lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"
   17.97 -apply (drule real_add_less_mono1)
   17.98 -apply (erule order_less_trans)
   17.99 -apply (erule real_add_less_mono2)
  17.100 -done
  17.101 -
  17.102 -lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2  ==> x + q1 \<le> x + q2"
  17.103 -by simp
  17.104 -
  17.105 -lemma real_add_le_mono: "[|i\<le>j;  k\<le>l |] ==> i + k \<le> j + (l::real)"
  17.106 -apply (drule real_add_le_mono1)
  17.107 -apply (erule order_trans, simp)
  17.108 -done
  17.109 -
  17.110 -lemma real_less_Ex: "\<exists>(x::real). x < y"
  17.111 -apply (rule real_add_zero_right [THEN subst])
  17.112 -apply (rule_tac x = "y + (- (1::real))" in exI)
  17.113 -apply (auto intro!: real_add_less_mono2 simp add: real_minus_zero_less_iff2 real_zero_less_one)
  17.114 -done
  17.115 -
  17.116 -lemma real_add_minus_positive_less_self: "(0::real) < r ==>  u + (-r) < u"
  17.117 -apply (rule_tac C = r in real_less_add_right_cancel)
  17.118 -apply (simp add: real_add_assoc)
  17.119 -done
  17.120 -
  17.121 -lemma real_le_minus_iff [simp]: "(-s \<le> -r) = ((r::real) \<le> s)"
  17.122 -apply (rule sym, safe)
  17.123 -apply (drule_tac x = "-s" in real_add_left_le_mono1)
  17.124 -apply (drule_tac [2] x = r in real_add_left_le_mono1, auto)
  17.125 -apply (drule_tac z = "-r" in real_add_le_mono1)
  17.126 -apply (drule_tac [2] z = s in real_add_le_mono1)
  17.127 -apply (auto simp add: real_add_assoc)
  17.128 -done
  17.129 -
  17.130 -lemma real_le_square [simp]: "(0::real) \<le> x*x"
  17.131 -apply (rule_tac real_linear_less2 [of x 0])
  17.132 -apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le)
  17.133 -done
  17.134 -
  17.135 -lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
  17.136 -apply (rotate_tac 1)
  17.137 -apply (drule real_less_sum_gt_zero)
  17.138 -apply (rule real_sum_gt_zero_less)
  17.139 -apply (drule real_mult_order, assumption)
  17.140 -apply (simp add: real_add_mult_distrib2 real_mult_commute)
  17.141 +lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
  17.142 +apply (auto simp add: real_gt_zero_preal_Ex)
  17.143 +apply (rule_tac x = "y*ya" in exI)
  17.144 +apply (simp (no_asm_use) add: real_of_preal_mult)
  17.145  done
  17.146  
  17.147  lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
  17.148 -apply (simp (no_asm_simp) add: real_mult_commute real_mult_less_mono1)
  17.149 +apply (rule real_sum_gt_zero_less)
  17.150 +apply (drule real_less_sum_gt_zero [of x y])
  17.151 +apply (drule real_mult_order, assumption)
  17.152 +apply (simp add: real_add_mult_distrib2)
  17.153  done
  17.154  
  17.155  
  17.156 @@ -286,11 +172,57 @@
  17.157    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
  17.158  qed
  17.159  
  17.160 +(*"v\<le>w ==> v+z \<le> w+z"*)
  17.161 +lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
  17.162 +
  17.163 +(*"v\<le>w ==> v+z \<le> w+z"*)
  17.164 +lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
  17.165 +
  17.166 +lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
  17.167 +by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
  17.168 +
  17.169 +lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
  17.170 +by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
  17.171 +
  17.172 +lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
  17.173 +by simp
  17.174 +
  17.175 +lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
  17.176 +apply simp
  17.177 +done
  17.178 +
  17.179 +lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
  17.180 +apply simp
  17.181 +done
  17.182 +
  17.183 +lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
  17.184 +apply simp
  17.185 +done
  17.186 +
  17.187 +lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
  17.188 +apply simp
  17.189 +done
  17.190 +
  17.191 +lemma real_zero_less_one: "0 < (1::real)"
  17.192 +  by (rule Ring_and_Field.zero_less_one)
  17.193 +
  17.194 +lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)"
  17.195 + by (rule Ring_and_Field.add_strict_mono)
  17.196 +
  17.197 +lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2  ==> x + q1 \<le> x + q2"
  17.198 +by simp
  17.199 +
  17.200 +lemma real_add_le_mono: "[|i\<le>j;  k\<le>l |] ==> i + k \<le> j + (l::real)"
  17.201 + by (rule Ring_and_Field.add_mono)
  17.202 +
  17.203 +lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
  17.204 + by (rule Ring_and_Field.neg_le_iff_le)
  17.205 +
  17.206 +lemma real_le_square [simp]: "(0::real) \<le> x*x"
  17.207 + by (rule Ring_and_Field.zero_le_square)
  17.208  
  17.209  
  17.210 -(*----------------------------------------------------------------------------
  17.211 -             An embedding of the naturals in the reals
  17.212 - ----------------------------------------------------------------------------*)
  17.213 +subsection{*An Embedding of the Naturals in the Reals*}
  17.214  
  17.215  lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
  17.216  by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
  17.217 @@ -387,32 +319,25 @@
  17.218    qed
  17.219  
  17.220  lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
  17.221 -apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero)
  17.222 +apply (simp add: neg_nat real_of_nat_zero)
  17.223  done
  17.224  
  17.225  
  17.226 -(*----------------------------------------------------------------------------
  17.227 -     inverse, etc.
  17.228 - ----------------------------------------------------------------------------*)
  17.229 +subsection{*Inverse and Division*}
  17.230 +
  17.231 +instance real :: division_by_zero
  17.232 +proof
  17.233 +  fix x :: real
  17.234 +  show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
  17.235 +  show "x/0 = 0" by (rule DIVISION_BY_ZERO) 
  17.236 +qed
  17.237 +
  17.238  
  17.239  lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
  17.240 -apply (rule ccontr) 
  17.241 -apply (drule real_leI) 
  17.242 -apply (frule real_minus_zero_less_iff2 [THEN iffD2])
  17.243 -apply (frule real_not_refl2 [THEN not_sym])
  17.244 -apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero])
  17.245 -apply (drule order_le_imp_less_or_eq, safe)
  17.246 -apply (drule neg_real_mult_order, assumption)
  17.247 -apply (auto intro: real_zero_less_one [THEN real_less_asym])
  17.248 -done
  17.249 +  by (rule Ring_and_Field.inverse_gt_0)
  17.250  
  17.251  lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
  17.252 -apply (frule real_not_refl2)
  17.253 -apply (drule real_minus_zero_less_iff [THEN iffD2])
  17.254 -apply (rule real_minus_zero_less_iff [THEN iffD1])
  17.255 -apply (subst real_minus_inverse [symmetric])
  17.256 -apply (auto intro: real_inverse_gt_0)
  17.257 -done
  17.258 +  by (rule Ring_and_Field.inverse_less_0)
  17.259  
  17.260  lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
  17.261  by (force simp add: Ring_and_Field.mult_less_cancel_right 
  17.262 @@ -423,6 +348,13 @@
  17.263  apply (simp add: real_mult_commute)
  17.264  done
  17.265  
  17.266 +lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
  17.267 + by (rule Ring_and_Field.mult_strict_right_mono)
  17.268 +
  17.269 +lemma real_mult_less_mono:
  17.270 +     "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
  17.271 + by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
  17.272 +
  17.273  lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
  17.274  by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
  17.275  
  17.276 @@ -430,22 +362,12 @@
  17.277  by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
  17.278  
  17.279  (* 05/00 *)
  17.280 -lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
  17.281 -by (auto simp add: real_le_def)
  17.282 -
  17.283 -lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
  17.284 +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
  17.285  by (auto simp add: real_le_def)
  17.286  
  17.287 -lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
  17.288 -apply (rule real_less_or_eq_imp_le)
  17.289 -apply (drule order_le_imp_less_or_eq)
  17.290 -apply (auto intro: real_mult_less_mono1)
  17.291 -done
  17.292 +lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
  17.293 +by (auto simp add: real_le_def)
  17.294  
  17.295 -lemma real_mult_less_mono: "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y"
  17.296 - by (rule Ring_and_Field.mult_strict_mono)
  17.297 -
  17.298 -text{*Variant of the theorem above; sometimes it's stronger*}
  17.299  lemma real_mult_less_mono':
  17.300       "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
  17.301  apply (subgoal_tac "0<r2")
  17.302 @@ -455,28 +377,9 @@
  17.303              intro: real_mult_less_mono real_mult_order)
  17.304  done
  17.305  
  17.306 -lemma real_mult_self_le: "[| (1::real) < r; (1::real) \<le> x |]  ==> x \<le> r * x"
  17.307 -apply (subgoal_tac "0\<le>x") 
  17.308 -apply (force dest!: real_mult_le_less_mono1)
  17.309 -apply (force intro: order_trans [OF zero_less_one [THEN order_less_imp_le]])
  17.310 -done
  17.311 -
  17.312 -lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |]  ==> x \<le> r * x"
  17.313 -apply (drule order_le_imp_less_or_eq)
  17.314 -apply (auto intro: real_mult_self_le)
  17.315 -done
  17.316 -
  17.317 -lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
  17.318 -apply (frule order_less_trans, assumption)
  17.319 -apply (frule real_inverse_gt_0)
  17.320 -apply (frule_tac x = x in real_inverse_gt_0)
  17.321 -apply (frule_tac x = r and z = "inverse r" in real_mult_less_mono1, assumption)
  17.322 -apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right])
  17.323 -apply (frule real_inverse_gt_0)
  17.324 -apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2)
  17.325 -apply assumption
  17.326 -apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric])
  17.327 -done
  17.328 +lemma real_inverse_less_swap:
  17.329 +     "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
  17.330 +  by (rule Ring_and_Field.less_imp_inverse_less)
  17.331  
  17.332  lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
  17.333  by auto
  17.334 @@ -489,13 +392,6 @@
  17.335  apply (simp add: real_add_commute)
  17.336  done
  17.337  
  17.338 -(* 05/00 *)
  17.339 -lemma real_minus_zero_le_iff [simp]: "(0 \<le> -R) = (R \<le> (0::real))"
  17.340 -by (auto dest: sym simp add: real_le_less)
  17.341 -
  17.342 -lemma real_minus_zero_le_iff2 [simp]: "(-R \<le> 0) = ((0::real) \<le> R)"
  17.343 -by (auto simp add: real_minus_zero_less_iff2 real_le_less)
  17.344 -
  17.345  lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
  17.346  apply (drule real_add_minus_eq_minus)
  17.347  apply (cut_tac x = x in real_le_square)
  17.348 @@ -507,9 +403,8 @@
  17.349  apply (simp add: real_add_commute)
  17.350  done
  17.351  
  17.352 -(*----------------------------------------------------------------------------
  17.353 -     Some convenient biconditionals for products of signs (lcp)
  17.354 - ----------------------------------------------------------------------------*)
  17.355 +
  17.356 +subsection{*Convenient Biconditionals for Products of Signs*}
  17.357  
  17.358  lemma real_0_less_mult_iff: "((0::real) < x*y) = (0<x & 0<y | x<0 & y<0)"
  17.359    by (rule Ring_and_Field.zero_less_mult_iff) 
  17.360 @@ -523,6 +418,195 @@
  17.361  lemma real_mult_le_0_iff: "(x*y \<le> (0::real)) = (0\<le>x & y\<le>0 | x\<le>0 & 0\<le>y)"
  17.362    by (rule mult_le_0_iff) 
  17.363  
  17.364 +subsection{*Hardly Used Theorems to be Deleted*}
  17.365 +
  17.366 +lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
  17.367 +apply (erule order_less_trans)
  17.368 +apply (drule real_add_less_mono2)
  17.369 +apply simp
  17.370 +done
  17.371 +
  17.372 +lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
  17.373 +apply (drule order_le_imp_less_or_eq)+
  17.374 +apply (auto intro: real_add_order order_less_imp_le)
  17.375 +done
  17.376 +
  17.377 +(*One use in HahnBanach/Aux.thy*)
  17.378 +lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
  17.379 +apply (rule real_less_or_eq_imp_le)
  17.380 +apply (drule order_le_imp_less_or_eq)
  17.381 +apply (auto intro: real_mult_less_mono1)
  17.382 +done
  17.383 +
  17.384 +
  17.385 +lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
  17.386 +apply (unfold real_of_posnat_def)
  17.387 +apply (rule real_gt_zero_preal_Ex [THEN iffD2])
  17.388 +apply blast
  17.389 +done
  17.390 +
  17.391 +declare real_of_posnat_gt_zero [simp]
  17.392 +
  17.393 +lemmas real_inv_real_of_posnat_gt_zero =  real_of_posnat_gt_zero [THEN real_inverse_gt_0, standard]
  17.394 +declare real_inv_real_of_posnat_gt_zero [simp]
  17.395 +
  17.396 +lemmas real_of_posnat_ge_zero = real_of_posnat_gt_zero [THEN order_less_imp_le, standard]
  17.397 +declare real_of_posnat_ge_zero [simp]
  17.398 +
  17.399 +lemma real_of_posnat_not_eq_zero: "real_of_posnat n ~= 0"
  17.400 +apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
  17.401 +done
  17.402 +declare real_of_posnat_not_eq_zero [simp]
  17.403 +
  17.404 +declare real_of_posnat_not_eq_zero [THEN real_mult_inv_left, simp]
  17.405 +declare real_of_posnat_not_eq_zero [THEN real_mult_inv_right, simp]
  17.406 +
  17.407 +lemma real_of_posnat_ge_one: "1 <= real_of_posnat n"
  17.408 +apply (simp (no_asm) add: real_of_posnat_one [symmetric])
  17.409 +apply (induct_tac "n")
  17.410 +apply (auto simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le)
  17.411 +done
  17.412 +declare real_of_posnat_ge_one [simp]
  17.413 +
  17.414 +lemma real_of_posnat_real_inv_not_zero: "inverse(real_of_posnat n) ~= 0"
  17.415 +apply (rule real_inverse_not_zero) 
  17.416 +apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
  17.417 +done
  17.418 +declare real_of_posnat_real_inv_not_zero [simp]
  17.419 +
  17.420 +lemma real_of_posnat_real_inv_inj: "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y"
  17.421 +apply (rule inj_real_of_posnat [THEN injD])
  17.422 +apply (rule real_of_posnat_real_inv_not_zero
  17.423 +              [THEN real_mult_left_cancel, THEN iffD1, of x])
  17.424 +apply (simp add: real_mult_inv_left
  17.425 +             real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
  17.426 +done
  17.427 +
  17.428 +lemma real_mult_less_self: "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r"
  17.429 +apply (simp (no_asm) add: real_add_mult_distrib2)
  17.430 +apply (rule_tac C = "-r" in real_less_add_left_cancel)
  17.431 +apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2)
  17.432 +done
  17.433 +
  17.434 +lemma real_of_posnat_inv_Ex_iff: "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)"
  17.435 +apply safe
  17.436 +apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
  17.437 +apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1])
  17.438 +apply (auto simp add: real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_assoc)
  17.439 +done
  17.440 +
  17.441 +lemma real_of_posnat_inv_iff: "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)"
  17.442 +apply safe
  17.443 +apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
  17.444 +apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1]) 
  17.445 +apply (auto simp add: real_mult_assoc)
  17.446 +done
  17.447 +
  17.448 +lemma real_mult_le_le_mono1: "[| (0::real) <=z; x<=y |] ==> z*x<=z*y"
  17.449 +  by (rule Ring_and_Field.mult_left_mono)
  17.450 +
  17.451 +lemma real_mult_le_le_mono2: "[| (0::real)<=z; x<=y |] ==> x*z<=y*z"
  17.452 +  by (rule Ring_and_Field.mult_right_mono)
  17.453 +
  17.454 +lemma real_of_posnat_inv_le_iff: "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)"
  17.455 +apply safe
  17.456 +apply (drule_tac n2=n in real_of_posnat_gt_zero [THEN order_less_imp_le, THEN real_mult_le_le_mono1])
  17.457 +apply (drule_tac [2] n3=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN order_less_imp_le, THEN real_mult_le_le_mono1])
  17.458 +apply (auto simp add: real_mult_ac)
  17.459 +done
  17.460 +
  17.461 +lemma real_of_posnat_less_iff: 
  17.462 +      "(real_of_posnat n < real_of_posnat m) = (n < m)"
  17.463 +apply (unfold real_of_posnat_def)
  17.464 +apply auto
  17.465 +done
  17.466 +declare real_of_posnat_less_iff [simp]
  17.467 +
  17.468 +lemma real_of_posnat_le_iff: "(real_of_posnat n <= real_of_posnat m) = (n <= m)"
  17.469 +apply (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq)
  17.470 +done
  17.471 +declare real_of_posnat_le_iff [simp]
  17.472 +
  17.473 +lemma real_mult_less_cancel3: "[| (0::real)<z; x*z<y*z |] ==> x<y"
  17.474 +apply auto
  17.475 +done
  17.476 +
  17.477 +lemma real_mult_less_cancel4: "[| (0::real)<z; z*x<z*y |] ==> x<y"
  17.478 +apply auto
  17.479 +done
  17.480 +
  17.481 +lemma real_of_posnat_less_inv_iff: "0 < u  ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))"
  17.482 +apply safe
  17.483 +apply (rule_tac n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_cancel3])
  17.484 +apply (rule_tac [2] x1 = "u" in real_inverse_gt_0 [THEN real_mult_less_cancel3])
  17.485 +apply (auto simp add: real_not_refl2 [THEN not_sym])
  17.486 +apply (rule_tac z = "u" in real_mult_less_cancel4)
  17.487 +apply (rule_tac [3] n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_cancel4])
  17.488 +apply (auto simp add: real_not_refl2 [THEN not_sym] real_mult_assoc [symmetric])
  17.489 +done
  17.490 +
  17.491 +lemma real_of_posnat_inv_eq_iff: "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)"
  17.492 +apply auto
  17.493 +done
  17.494 +
  17.495 +lemma real_add_one_minus_inv_ge_zero: "0 <= 1 + -inverse(real_of_posnat n)"
  17.496 +apply (rule_tac C = "inverse (real_of_posnat n) " in real_le_add_right_cancel)
  17.497 +apply (simp (no_asm) add: real_add_assoc real_of_posnat_inv_le_iff)
  17.498 +done
  17.499 +
  17.500 +lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))"
  17.501 +apply (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1])
  17.502 +apply auto
  17.503 +done
  17.504 +
  17.505 +lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
  17.506 +apply (case_tac "x ~= 0")
  17.507 +apply (rule_tac c1 = "x" in real_mult_left_cancel [THEN iffD1])
  17.508 +apply auto
  17.509 +done
  17.510 +
  17.511 +lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
  17.512 +apply (auto dest: real_inverse_less_swap)
  17.513 +done
  17.514 +
  17.515 +lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)"
  17.516 +apply (rule real_of_nat_less_iff [THEN subst])
  17.517 +apply auto
  17.518 +done
  17.519 +declare real_of_nat_gt_zero_cancel_iff [simp]
  17.520 +
  17.521 +lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)"
  17.522 +apply (rule real_of_nat_zero [THEN subst])
  17.523 +apply (subst real_of_nat_le_iff)
  17.524 +apply auto
  17.525 +done
  17.526 +declare real_of_nat_le_zero_cancel_iff [simp]
  17.527 +
  17.528 +lemma not_real_of_nat_less_zero: "~ real (n::nat) < 0"
  17.529 +apply (simp (no_asm) add: real_le_def [symmetric] real_of_nat_ge_zero)
  17.530 +done
  17.531 +declare not_real_of_nat_less_zero [simp]
  17.532 +
  17.533 +lemma real_of_nat_ge_zero_cancel_iff: 
  17.534 +      "(0 <= real (n::nat)) = (0 <= n)"
  17.535 +apply (unfold real_le_def le_def)
  17.536 +apply (simp (no_asm))
  17.537 +done
  17.538 +declare real_of_nat_ge_zero_cancel_iff [simp]
  17.539 +
  17.540 +lemma real_of_nat_num_if: "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))"
  17.541 +apply (case_tac "n")
  17.542 +apply (auto simp add: real_of_nat_Suc)
  17.543 +done
  17.544 +
  17.545 +(*RING AND FIELD*)
  17.546 +		lemma mult_less_imp_less_left:
  17.547 +		    "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
  17.548 +		  by (force elim: order_less_asym simp add: mult_less_cancel_left)
  17.549 +
  17.550 +		lemma mult_less_imp_less_right:
  17.551 +		    "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
  17.552 +		  by (force elim: order_less_asym simp add: mult_less_cancel_right)
  17.553  
  17.554  ML
  17.555  {*
  17.556 @@ -534,13 +618,8 @@
  17.557  val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
  17.558  val real_less_all_preal = thm "real_less_all_preal";
  17.559  val real_less_all_real2 = thm "real_less_all_real2";
  17.560 -val real_lemma_add_positive_imp_less = thm "real_lemma_add_positive_imp_less";
  17.561 -val real_ex_add_positive_left_less = thm "real_ex_add_positive_left_less";
  17.562 -val real_less_iff_add = thm "real_less_iff_add";
  17.563  val real_of_preal_le_iff = thm "real_of_preal_le_iff";
  17.564  val real_mult_order = thm "real_mult_order";
  17.565 -val neg_real_mult_order = thm "neg_real_mult_order";
  17.566 -val real_mult_less_0 = thm "real_mult_less_0";
  17.567  val real_zero_less_one = thm "real_zero_less_one";
  17.568  val real_add_right_cancel_less = thm "real_add_right_cancel_less";
  17.569  val real_add_left_cancel_less = thm "real_add_left_cancel_less";
  17.570 @@ -560,8 +639,6 @@
  17.571  val real_add_less_mono = thm "real_add_less_mono";
  17.572  val real_add_left_le_mono1 = thm "real_add_left_le_mono1";
  17.573  val real_add_le_mono = thm "real_add_le_mono";
  17.574 -val real_less_Ex = thm "real_less_Ex";
  17.575 -val real_add_minus_positive_less_self = thm "real_add_minus_positive_less_self";
  17.576  val real_le_minus_iff = thm "real_le_minus_iff";
  17.577  val real_le_square = thm "real_le_square";
  17.578  val real_mult_less_mono1 = thm "real_mult_less_mono1";
  17.579 @@ -593,22 +670,46 @@
  17.580  val real_mult_less_iff2 = thm "real_mult_less_iff2";
  17.581  val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
  17.582  val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
  17.583 -val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1";
  17.584  val real_mult_less_mono = thm "real_mult_less_mono";
  17.585  val real_mult_less_mono' = thm "real_mult_less_mono'";
  17.586 -val real_mult_self_le = thm "real_mult_self_le";
  17.587 -val real_mult_self_le2 = thm "real_mult_self_le2";
  17.588  val real_inverse_less_swap = thm "real_inverse_less_swap";
  17.589  val real_mult_is_0 = thm "real_mult_is_0";
  17.590  val real_inverse_add = thm "real_inverse_add";
  17.591 -val real_minus_zero_le_iff = thm "real_minus_zero_le_iff";
  17.592 -val real_minus_zero_le_iff2 = thm "real_minus_zero_le_iff2";
  17.593  val real_sum_squares_cancel = thm "real_sum_squares_cancel";
  17.594  val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
  17.595  val real_0_less_mult_iff = thm "real_0_less_mult_iff";
  17.596  val real_0_le_mult_iff = thm "real_0_le_mult_iff";
  17.597  val real_mult_less_0_iff = thm "real_mult_less_0_iff";
  17.598  val real_mult_le_0_iff = thm "real_mult_le_0_iff";
  17.599 +
  17.600 +val real_of_posnat_gt_zero = thm "real_of_posnat_gt_zero";
  17.601 +val real_inv_real_of_posnat_gt_zero = thm "real_inv_real_of_posnat_gt_zero";
  17.602 +val real_of_posnat_ge_zero = thm "real_of_posnat_ge_zero";
  17.603 +val real_of_posnat_not_eq_zero = thm "real_of_posnat_not_eq_zero";
  17.604 +val real_of_posnat_ge_one = thm "real_of_posnat_ge_one";
  17.605 +val real_of_posnat_real_inv_not_zero = thm "real_of_posnat_real_inv_not_zero";
  17.606 +val real_of_posnat_real_inv_inj = thm "real_of_posnat_real_inv_inj";
  17.607 +val real_mult_less_self = thm "real_mult_less_self";
  17.608 +val real_of_posnat_inv_Ex_iff = thm "real_of_posnat_inv_Ex_iff";
  17.609 +val real_of_posnat_inv_iff = thm "real_of_posnat_inv_iff";
  17.610 +val real_mult_le_le_mono1 = thm "real_mult_le_le_mono1";
  17.611 +val real_mult_le_le_mono2 = thm "real_mult_le_le_mono2";
  17.612 +val real_of_posnat_inv_le_iff = thm "real_of_posnat_inv_le_iff";
  17.613 +val real_of_posnat_less_iff = thm "real_of_posnat_less_iff";
  17.614 +val real_of_posnat_le_iff = thm "real_of_posnat_le_iff";
  17.615 +val real_mult_less_cancel3 = thm "real_mult_less_cancel3";
  17.616 +val real_mult_less_cancel4 = thm "real_mult_less_cancel4";
  17.617 +val real_of_posnat_less_inv_iff = thm "real_of_posnat_less_inv_iff";
  17.618 +val real_of_posnat_inv_eq_iff = thm "real_of_posnat_inv_eq_iff";
  17.619 +val real_add_one_minus_inv_ge_zero = thm "real_add_one_minus_inv_ge_zero";
  17.620 +val real_mult_add_one_minus_ge_zero = thm "real_mult_add_one_minus_ge_zero";
  17.621 +val real_inverse_unique = thm "real_inverse_unique";
  17.622 +val real_inverse_gt_one = thm "real_inverse_gt_one";
  17.623 +val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
  17.624 +val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
  17.625 +val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
  17.626 +val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
  17.627 +val real_of_nat_num_if = thm "real_of_nat_num_if";
  17.628  *}
  17.629  
  17.630  end
    18.1 --- a/src/HOL/Real/RealPow.thy	Tue Nov 25 10:37:03 2003 +0100
    18.2 +++ b/src/HOL/Real/RealPow.thy	Thu Nov 27 10:47:55 2003 +0100
    18.3 @@ -18,18 +18,11 @@
    18.4       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    18.5  
    18.6  
    18.7 -(*FIXME: most of the theorems for Suc (Suc 0) are redundant!
    18.8 -*)
    18.9 +lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0"
   18.10 +by auto
   18.11  
   18.12 -lemma realpow_zero: "(0::real) ^ (Suc n) = 0"
   18.13 -apply auto
   18.14 -done
   18.15 -declare realpow_zero [simp]
   18.16 -
   18.17 -lemma realpow_not_zero [rule_format (no_asm)]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
   18.18 -apply (induct_tac "n")
   18.19 -apply auto
   18.20 -done
   18.21 +lemma realpow_not_zero [rule_format]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
   18.22 +by (induct_tac "n", auto)
   18.23  
   18.24  lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
   18.25  apply (rule ccontr)
   18.26 @@ -51,26 +44,23 @@
   18.27  apply (auto simp add: real_mult_ac)
   18.28  done
   18.29  
   18.30 -lemma realpow_one: "(r::real) ^ 1 = r"
   18.31 -apply (simp (no_asm))
   18.32 -done
   18.33 -declare realpow_one [simp]
   18.34 +lemma realpow_one [simp]: "(r::real) ^ 1 = r"
   18.35 +by simp
   18.36  
   18.37  lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
   18.38 -apply (simp (no_asm))
   18.39 -done
   18.40 +by simp
   18.41  
   18.42 -lemma realpow_gt_zero [rule_format (no_asm)]: "(0::real) < r --> 0 < r ^ n"
   18.43 +lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
   18.44  apply (induct_tac "n")
   18.45  apply (auto intro: real_mult_order simp add: real_zero_less_one)
   18.46  done
   18.47  
   18.48 -lemma realpow_ge_zero [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
   18.49 +lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
   18.50  apply (induct_tac "n")
   18.51  apply (auto simp add: real_0_le_mult_iff)
   18.52  done
   18.53  
   18.54 -lemma realpow_le [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
   18.55 +lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
   18.56  apply (induct_tac "n")
   18.57  apply (auto intro!: real_mult_le_mono)
   18.58  apply (simp (no_asm_simp) add: realpow_ge_zero)
   18.59 @@ -78,70 +68,55 @@
   18.60  
   18.61  lemma realpow_0_left [rule_format, simp]:
   18.62       "0 < n --> 0 ^ n = (0::real)"
   18.63 -apply (induct_tac "n")
   18.64 -apply (auto ); 
   18.65 +apply (induct_tac "n", auto) 
   18.66  done
   18.67  
   18.68  lemma realpow_less' [rule_format]:
   18.69       "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
   18.70  apply (induct n) 
   18.71 -apply (auto simp add: real_mult_less_mono' realpow_ge_zero); 
   18.72 +apply (auto simp add: real_mult_less_mono' realpow_ge_zero) 
   18.73  done
   18.74  
   18.75  text{*Legacy: weaker version of the theorem above*}
   18.76 -lemma realpow_less [rule_format]:
   18.77 +lemma realpow_less:
   18.78       "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
   18.79 -apply (rule realpow_less') 
   18.80 -apply (auto ); 
   18.81 +apply (rule realpow_less', auto) 
   18.82  done
   18.83  
   18.84 -lemma realpow_eq_one: "1 ^ n = (1::real)"
   18.85 -apply (induct_tac "n")
   18.86 -apply auto
   18.87 -done
   18.88 -declare realpow_eq_one [simp]
   18.89 +lemma realpow_eq_one [simp]: "1 ^ n = (1::real)"
   18.90 +by (induct_tac "n", auto)
   18.91  
   18.92 -lemma abs_realpow_minus_one: "abs((-1) ^ n) = (1::real)"
   18.93 +lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
   18.94  apply (induct_tac "n")
   18.95  apply (auto simp add: abs_mult)
   18.96  done
   18.97 -declare abs_realpow_minus_one [simp]
   18.98  
   18.99  lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
  18.100  apply (induct_tac "n")
  18.101  apply (auto simp add: real_mult_ac)
  18.102  done
  18.103  
  18.104 -lemma realpow_two_le: "(0::real) \<le> r^ Suc (Suc 0)"
  18.105 -apply (simp (no_asm) add: real_le_square)
  18.106 -done
  18.107 -declare realpow_two_le [simp]
  18.108 +lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
  18.109 +by (simp add: real_le_square)
  18.110  
  18.111 -lemma abs_realpow_two: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
  18.112 -apply (simp (no_asm) add: abs_eqI1 real_le_square)
  18.113 -done
  18.114 -declare abs_realpow_two [simp]
  18.115 +lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
  18.116 +by (simp add: abs_eqI1 real_le_square)
  18.117  
  18.118 -lemma realpow_two_abs: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
  18.119 -apply (simp (no_asm) add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
  18.120 -done
  18.121 -declare realpow_two_abs [simp]
  18.122 +lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
  18.123 +by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
  18.124  
  18.125  lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
  18.126  apply auto
  18.127  apply (cut_tac real_zero_less_one)
  18.128 -apply (frule_tac x = "0" in order_less_trans)
  18.129 -apply assumption
  18.130 -apply (drule_tac  z = "r" and x = "1" in real_mult_less_mono1)
  18.131 +apply (frule_tac x = 0 in order_less_trans, assumption)
  18.132 +apply (drule_tac  z = r and x = 1 in real_mult_less_mono1)
  18.133  apply (auto intro: order_less_trans)
  18.134  done
  18.135  
  18.136 -lemma realpow_ge_one [rule_format (no_asm)]: "(1::real) < r --> 1 \<le> r ^ n"
  18.137 -apply (induct_tac "n")
  18.138 -apply auto
  18.139 +lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
  18.140 +apply (induct_tac "n", auto)
  18.141  apply (subgoal_tac "1*1 \<le> r * r^n")
  18.142 -apply (rule_tac [2] real_mult_le_mono)
  18.143 -apply auto
  18.144 +apply (rule_tac [2] real_mult_le_mono, auto)
  18.145  done
  18.146  
  18.147  lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
  18.148 @@ -149,167 +124,118 @@
  18.149  apply (auto dest: realpow_ge_one)
  18.150  done
  18.151  
  18.152 -lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
  18.153 +lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
  18.154  apply (rule_tac y = "1 ^ n" in order_trans)
  18.155  apply (rule_tac [2] realpow_le)
  18.156  apply (auto intro: order_less_imp_le)
  18.157  done
  18.158  
  18.159 -lemma two_realpow_gt: "real (n::nat) < 2 ^ n"
  18.160 +lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
  18.161  apply (induct_tac "n")
  18.162  apply (auto simp add: real_of_nat_Suc)
  18.163  apply (subst real_mult_2)
  18.164  apply (rule real_add_less_le_mono)
  18.165  apply (auto simp add: two_realpow_ge_one)
  18.166  done
  18.167 -declare two_realpow_gt [simp] two_realpow_ge_one [simp]
  18.168  
  18.169 -lemma realpow_minus_one: "(-1) ^ (2*n) = (1::real)"
  18.170 -apply (induct_tac "n")
  18.171 -apply auto
  18.172 -done
  18.173 -declare realpow_minus_one [simp]
  18.174 +lemma realpow_minus_one [simp]: "(-1) ^ (2*n) = (1::real)"
  18.175 +by (induct_tac "n", auto)
  18.176 +
  18.177 +lemma realpow_minus_one_odd [simp]: "(-1) ^ Suc (2*n) = -(1::real)"
  18.178 +by auto
  18.179  
  18.180 -lemma realpow_minus_one_odd: "(-1) ^ Suc (2*n) = -(1::real)"
  18.181 -apply auto
  18.182 -done
  18.183 -declare realpow_minus_one_odd [simp]
  18.184 +lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
  18.185 +by auto
  18.186  
  18.187 -lemma realpow_minus_one_even: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
  18.188 -apply auto
  18.189 -done
  18.190 -declare realpow_minus_one_even [simp]
  18.191 +lemma realpow_Suc_less [rule_format]:
  18.192 +     "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
  18.193 +  by (induct_tac "n", auto)
  18.194  
  18.195 -lemma realpow_Suc_less [rule_format (no_asm)]: "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
  18.196 -apply (induct_tac "n")
  18.197 -apply auto
  18.198 -done
  18.199 -
  18.200 -lemma realpow_Suc_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  18.201 +lemma realpow_Suc_le [rule_format]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  18.202  apply (induct_tac "n")
  18.203  apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
  18.204  done
  18.205  
  18.206 -lemma realpow_zero_le: "(0::real) \<le> 0 ^ n"
  18.207 -apply (case_tac "n")
  18.208 -apply auto
  18.209 -done
  18.210 -declare realpow_zero_le [simp]
  18.211 +lemma realpow_zero_le [simp]: "(0::real) \<le> 0 ^ n"
  18.212 +by (case_tac "n", auto)
  18.213  
  18.214 -lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  18.215 -apply (blast intro!: order_less_imp_le realpow_Suc_less)
  18.216 -done
  18.217 +lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  18.218 +by (blast intro!: order_less_imp_le realpow_Suc_less)
  18.219  
  18.220  lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
  18.221  apply (erule order_le_imp_less_or_eq [THEN disjE])
  18.222 -apply (rule realpow_Suc_le2)
  18.223 -apply auto
  18.224 +apply (rule realpow_Suc_le2, auto)
  18.225  done
  18.226  
  18.227 -lemma realpow_less_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
  18.228 +lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
  18.229  apply (induct_tac "N")
  18.230  apply (simp_all (no_asm_simp))
  18.231  apply clarify
  18.232 -apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n")
  18.233 -apply simp
  18.234 +apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
  18.235  apply (rule real_mult_le_mono)
  18.236  apply (auto simp add: realpow_ge_zero less_Suc_eq)
  18.237  done
  18.238  
  18.239  lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
  18.240 -apply (drule_tac n = "N" in le_imp_less_or_eq)
  18.241 +apply (drule_tac n = N in le_imp_less_or_eq)
  18.242  apply (auto intro: realpow_less_le)
  18.243  done
  18.244  
  18.245  lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
  18.246 -apply (drule_tac n = "1" and N = "Suc n" in order_less_imp_le [THEN realpow_le_le])
  18.247 -apply auto
  18.248 -done
  18.249 +by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto)
  18.250  
  18.251  lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
  18.252 -apply (blast intro: realpow_Suc_le_self order_le_less_trans)
  18.253 -done
  18.254 +by (blast intro: realpow_Suc_le_self order_le_less_trans)
  18.255 +
  18.256 +lemma realpow_le_Suc [rule_format]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
  18.257 +by (induct_tac "n", auto)
  18.258 +
  18.259 +lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
  18.260 +by (induct_tac "n", auto)
  18.261  
  18.262 -lemma realpow_le_Suc [rule_format (no_asm)]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
  18.263 -apply (induct_tac "n")
  18.264 -apply auto
  18.265 +lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
  18.266 +by (blast intro!: order_less_imp_le realpow_less_Suc)
  18.267 +
  18.268 +(*One use in RealPow.thy*)
  18.269 +lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |]  ==> x \<le> r * x"
  18.270 +apply (subgoal_tac "1 * x \<le> r * x", simp) 
  18.271 +apply (rule mult_right_mono, auto) 
  18.272  done
  18.273  
  18.274 -lemma realpow_less_Suc [rule_format (no_asm)]: "(1::real) < r --> r ^ n < r ^ Suc n"
  18.275 -apply (induct_tac "n")
  18.276 -apply auto
  18.277 -done
  18.278 -
  18.279 -lemma realpow_le_Suc2 [rule_format (no_asm)]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
  18.280 -apply (blast intro!: order_less_imp_le realpow_less_Suc)
  18.281 -done
  18.282 -
  18.283 -lemma realpow_gt_ge [rule_format (no_asm)]: "(1::real) < r & n < N --> r ^ n \<le> r ^ N"
  18.284 -apply (induct_tac "N")
  18.285 -apply auto
  18.286 -apply (frule_tac [!] n = "na" in realpow_ge_one)
  18.287 -apply (drule_tac [!] real_mult_self_le)
  18.288 -apply assumption
  18.289 -prefer 2 apply (assumption)
  18.290 +lemma realpow_gt_ge2 [rule_format]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
  18.291 +apply (induct_tac "N", auto)
  18.292 +apply (frule_tac [!] n = na in realpow_ge_one2)
  18.293 +apply (drule_tac [!] real_mult_self_le2, assumption)
  18.294 +prefer 2 apply assumption
  18.295  apply (auto intro: order_trans simp add: less_Suc_eq)
  18.296  done
  18.297  
  18.298 -lemma realpow_gt_ge2 [rule_format (no_asm)]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
  18.299 -apply (induct_tac "N")
  18.300 -apply auto
  18.301 -apply (frule_tac [!] n = "na" in realpow_ge_one2)
  18.302 -apply (drule_tac [!] real_mult_self_le2)
  18.303 -apply assumption
  18.304 -prefer 2 apply (assumption)
  18.305 -apply (auto intro: order_trans simp add: less_Suc_eq)
  18.306 -done
  18.307 -
  18.308 -lemma realpow_ge_ge: "[| (1::real) < r; n \<le> N |] ==> r ^ n \<le> r ^ N"
  18.309 -apply (drule_tac n = "N" in le_imp_less_or_eq)
  18.310 -apply (auto intro: realpow_gt_ge)
  18.311 -done
  18.312 -
  18.313  lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
  18.314 -apply (drule_tac n = "N" in le_imp_less_or_eq)
  18.315 +apply (drule_tac n = N in le_imp_less_or_eq)
  18.316  apply (auto intro: realpow_gt_ge2)
  18.317  done
  18.318  
  18.319 -lemma realpow_Suc_ge_self [rule_format (no_asm)]: "(1::real) < r ==> r \<le> r ^ Suc n"
  18.320 -apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge)
  18.321 -apply auto
  18.322 -done
  18.323 +lemma realpow_Suc_ge_self2: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
  18.324 +by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto)
  18.325  
  18.326 -lemma realpow_Suc_ge_self2 [rule_format (no_asm)]: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
  18.327 -apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge2)
  18.328 -apply auto
  18.329 -done
  18.330 -
  18.331 -lemma realpow_ge_self: "[| (1::real) < r; 0 < n |] ==> r \<le> r ^ n"
  18.332 -apply (drule less_not_refl2 [THEN not0_implies_Suc])
  18.333 -apply (auto intro!: realpow_Suc_ge_self)
  18.334 -done
  18.335 -
  18.336 +(*Used ONCE in Hyperreal/NthRoot.ML*)
  18.337  lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
  18.338  apply (drule less_not_refl2 [THEN not0_implies_Suc])
  18.339  apply (auto intro!: realpow_Suc_ge_self2)
  18.340  done
  18.341  
  18.342 -lemma realpow_minus_mult [rule_format (no_asm)]: "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
  18.343 +lemma realpow_minus_mult [rule_format, simp]:
  18.344 +     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
  18.345  apply (induct_tac "n")
  18.346  apply (auto simp add: real_mult_commute)
  18.347  done
  18.348 -declare realpow_minus_mult [simp]
  18.349  
  18.350 -lemma realpow_two_mult_inverse: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
  18.351 -apply (simp (no_asm_simp) add: realpow_two real_mult_assoc [symmetric])
  18.352 -done
  18.353 -declare realpow_two_mult_inverse [simp]
  18.354 +lemma realpow_two_mult_inverse [simp]: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
  18.355 +by (simp add: realpow_two real_mult_assoc [symmetric])
  18.356  
  18.357  (* 05/00 *)
  18.358 -lemma realpow_two_minus: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
  18.359 -apply (simp (no_asm))
  18.360 -done
  18.361 -declare realpow_two_minus [simp]
  18.362 +lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
  18.363 +by simp
  18.364  
  18.365  lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
  18.366  apply (unfold real_diff_def)
  18.367 @@ -317,25 +243,23 @@
  18.368  done
  18.369  
  18.370  lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
  18.371 -apply (cut_tac x = "x" and y = "y" in realpow_two_diff)
  18.372 +apply (cut_tac x = x and y = y in realpow_two_diff)
  18.373  apply (auto simp del: realpow_Suc)
  18.374  done
  18.375  
  18.376  (* used in Transc *)
  18.377  lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
  18.378 -apply (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
  18.379 -done
  18.380 +by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
  18.381  
  18.382  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
  18.383  apply (induct_tac "n")
  18.384  apply (auto simp add: real_of_nat_one real_of_nat_mult)
  18.385  done
  18.386  
  18.387 -lemma realpow_real_of_nat_two_pos: "0 < real (Suc (Suc 0) ^ n)"
  18.388 +lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
  18.389  apply (induct_tac "n")
  18.390  apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
  18.391  done
  18.392 -declare realpow_real_of_nat_two_pos [simp] 
  18.393  
  18.394  lemma realpow_increasing:
  18.395    assumes xnonneg: "(0::real) \<le> x"
  18.396 @@ -352,29 +276,23 @@
  18.397   qed
  18.398    
  18.399  lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
  18.400 -apply (blast intro: realpow_increasing order_antisym order_eq_refl sym)
  18.401 -done
  18.402 +by (blast intro: realpow_increasing order_antisym order_eq_refl sym)
  18.403  
  18.404  
  18.405  (*** Logical equivalences for inequalities ***)
  18.406  
  18.407 -lemma realpow_eq_0_iff: "(x^n = 0) = (x = (0::real) & 0<n)"
  18.408 -apply (induct_tac "n")
  18.409 -apply auto
  18.410 -done
  18.411 -declare realpow_eq_0_iff [simp]
  18.412 +lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
  18.413 +by (induct_tac "n", auto)
  18.414  
  18.415 -lemma zero_less_realpow_abs_iff: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
  18.416 +lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
  18.417  apply (induct_tac "n")
  18.418  apply (auto simp add: real_0_less_mult_iff)
  18.419  done
  18.420 -declare zero_less_realpow_abs_iff [simp]
  18.421  
  18.422 -lemma zero_le_realpow_abs: "(0::real) \<le> (abs x)^n"
  18.423 +lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
  18.424  apply (induct_tac "n")
  18.425  apply (auto simp add: real_0_le_mult_iff)
  18.426  done
  18.427 -declare zero_le_realpow_abs [simp]
  18.428  
  18.429  
  18.430  (*** Literal arithmetic involving powers, type real ***)
  18.431 @@ -386,8 +304,7 @@
  18.432  declare real_of_int_power [symmetric, simp]
  18.433  
  18.434  lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
  18.435 -apply (simp only: real_number_of_def real_of_int_power)
  18.436 -done
  18.437 +by (simp only: real_number_of_def real_of_int_power)
  18.438  
  18.439  declare power_real_number_of [of _ "number_of w", standard, simp]
  18.440  
  18.441 @@ -410,6 +327,182 @@
  18.442    by simp
  18.443  
  18.444  
  18.445 +subsection{*Various Other Theorems*}
  18.446 +
  18.447 +text{*Used several times in Hyperreal/Transcendental.ML*}
  18.448 +lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
  18.449 +  by (auto intro: real_sum_squares_cancel)
  18.450 +
  18.451 +lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
  18.452 +apply (auto simp add: real_add_mult_distrib real_add_mult_distrib2 real_diff_def)
  18.453 +done
  18.454 +
  18.455 +lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
  18.456 +apply auto
  18.457 +apply (drule right_minus_eq [THEN iffD2]) 
  18.458 +apply (auto simp add: real_squared_diff_one_factored)
  18.459 +done
  18.460 +declare real_mult_is_one [iff]
  18.461 +
  18.462 +lemma real_le_add_half_cancel: "(x + y/2 <= (y::real)) = (x <= y /2)"
  18.463 +apply auto
  18.464 +done
  18.465 +declare real_le_add_half_cancel [simp]
  18.466 +
  18.467 +lemma real_minus_half_eq: "(x::real) - x/2 = x/2"
  18.468 +apply auto
  18.469 +done
  18.470 +declare real_minus_half_eq [simp]
  18.471 +
  18.472 +lemma real_mult_inverse_cancel:
  18.473 +     "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
  18.474 +      ==> inverse x * y < inverse x1 * u"
  18.475 +apply (rule_tac c=x in mult_less_imp_less_left) 
  18.476 +apply (auto simp add: real_mult_assoc [symmetric])
  18.477 +apply (simp (no_asm) add: real_mult_ac)
  18.478 +apply (rule_tac c=x1 in mult_less_imp_less_right) 
  18.479 +apply (auto simp add: real_mult_ac)
  18.480 +done
  18.481 +
  18.482 +text{*Used once: in Hyperreal/Transcendental.ML*}
  18.483 +lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
  18.484 +apply (auto dest: real_mult_inverse_cancel simp add: real_mult_ac)
  18.485 +done
  18.486 +
  18.487 +lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
  18.488 +apply auto
  18.489 +done
  18.490 +declare inverse_real_of_nat_gt_zero [simp]
  18.491 +
  18.492 +lemma inverse_real_of_nat_ge_zero: "0 <= inverse (real (Suc n))"
  18.493 +apply auto
  18.494 +done
  18.495 +declare inverse_real_of_nat_ge_zero [simp]
  18.496 +
  18.497 +lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
  18.498 +apply (blast dest!: real_sum_squares_cancel) 
  18.499 +done
  18.500 +
  18.501 +lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
  18.502 +apply (blast dest!: real_sum_squares_cancel2) 
  18.503 +done
  18.504 +
  18.505 +(* nice theorem *)
  18.506 +lemma abs_mult_abs: "abs x * abs x = x * (x::real)"
  18.507 +apply (insert linorder_less_linear [of x 0]) 
  18.508 +apply (auto simp add: abs_eqI2 abs_minus_eqI2)
  18.509 +done
  18.510 +declare abs_mult_abs [simp]
  18.511 +
  18.512 +
  18.513 +subsection {*Various Other Theorems*}
  18.514 +
  18.515 +lemma realpow_divide: 
  18.516 +    "(x/y) ^ n = ((x::real) ^ n/ y ^ n)"
  18.517 +apply (unfold real_divide_def)
  18.518 +apply (auto simp add: realpow_mult realpow_inverse)
  18.519 +done
  18.520 +
  18.521 +lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) <= r --> 0 <= r ^ n"
  18.522 +apply (induct_tac "n")
  18.523 +apply (auto simp add: real_0_le_mult_iff)
  18.524 +done
  18.525 +
  18.526 +lemma realpow_le2 [rule_format (no_asm)]: "(0::real) <= x & x <= y --> x ^ n <= y ^ n"
  18.527 +apply (induct_tac "n")
  18.528 +apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
  18.529 +done
  18.530 +
  18.531 +lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
  18.532 +apply (frule_tac n = "n" in realpow_ge_one)
  18.533 +apply (drule real_le_imp_less_or_eq, safe)
  18.534 +apply (frule real_zero_less_one [THEN real_less_trans])
  18.535 +apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
  18.536 +apply assumption
  18.537 +apply (auto dest: real_less_trans)
  18.538 +done
  18.539 +
  18.540 +lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
  18.541 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2)
  18.542 +done
  18.543 +declare realpow_two_sum_zero_iff [simp]
  18.544 +
  18.545 +lemma realpow_two_le_add_order: "(0::real) <= u ^ 2 + v ^ 2"
  18.546 +apply (rule real_le_add_order)
  18.547 +apply (auto simp add: numeral_2_eq_2)
  18.548 +done
  18.549 +declare realpow_two_le_add_order [simp]
  18.550 +
  18.551 +lemma realpow_two_le_add_order2: "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2"
  18.552 +apply (rule real_le_add_order)+
  18.553 +apply (auto simp add: numeral_2_eq_2)
  18.554 +done
  18.555 +declare realpow_two_le_add_order2 [simp]
  18.556 +
  18.557 +lemma real_mult_self_sum_ge_zero: "(0::real) <= x*x + y*y"
  18.558 +apply (cut_tac u = "x" and v = "y" in realpow_two_le_add_order)
  18.559 +apply (auto simp add: numeral_2_eq_2)
  18.560 +done
  18.561 +declare real_mult_self_sum_ge_zero [simp]
  18.562 +declare real_mult_self_sum_ge_zero [THEN abs_eqI1, simp]
  18.563 +
  18.564 +lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
  18.565 +apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
  18.566 +apply (drule real_le_imp_less_or_eq)
  18.567 +apply (drule_tac y = "y" in real_sum_squares_not_zero)
  18.568 +apply auto
  18.569 +done
  18.570 +
  18.571 +lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
  18.572 +apply (rule real_add_commute [THEN subst])
  18.573 +apply (erule real_sum_square_gt_zero)
  18.574 +done
  18.575 +
  18.576 +lemma real_minus_mult_self_le: "-(u * u) <= (x * (x::real))"
  18.577 +apply (rule_tac j = "0" in real_le_trans)
  18.578 +apply auto
  18.579 +done
  18.580 +declare real_minus_mult_self_le [simp]
  18.581 +
  18.582 +lemma realpow_square_minus_le: "-(u ^ 2) <= (x::real) ^ 2"
  18.583 +apply (auto simp add: numeral_2_eq_2)
  18.584 +done
  18.585 +declare realpow_square_minus_le [simp]
  18.586 +
  18.587 +lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
  18.588 +apply (case_tac "n")
  18.589 +apply auto
  18.590 +done
  18.591 +
  18.592 +lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)"
  18.593 +apply (induct_tac "d")
  18.594 +apply (auto simp add: realpow_num_eq_if)
  18.595 +done
  18.596 +declare real_num_zero_less_two_pow [simp]
  18.597 +
  18.598 +lemma lemma_realpow_num_two_mono: "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
  18.599 +apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
  18.600 +apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
  18.601 +apply (auto simp add: realpow_num_eq_if)
  18.602 +done
  18.603 +
  18.604 +lemma lemma_realpow_4: "2 ^ 2 = (4::real)"
  18.605 +apply (simp (no_asm) add: realpow_num_eq_if)
  18.606 +done
  18.607 +declare lemma_realpow_4 [simp]
  18.608 +
  18.609 +lemma lemma_realpow_16: "2 ^ 4 = (16::real)"
  18.610 +apply (simp (no_asm) add: realpow_num_eq_if)
  18.611 +done
  18.612 +declare lemma_realpow_16 [simp]
  18.613 +
  18.614 +lemma zero_le_x_squared: "(0::real) <= x^2"
  18.615 +apply (simp add: numeral_2_eq_2)
  18.616 +done
  18.617 +declare zero_le_x_squared [simp]
  18.618 +
  18.619 +
  18.620 +
  18.621  ML
  18.622  {*
  18.623  val realpow_0 = thm "realpow_0";
  18.624 @@ -454,18 +547,13 @@
  18.625  val realpow_le_Suc = thm "realpow_le_Suc";
  18.626  val realpow_less_Suc = thm "realpow_less_Suc";
  18.627  val realpow_le_Suc2 = thm "realpow_le_Suc2";
  18.628 -val realpow_gt_ge = thm "realpow_gt_ge";
  18.629  val realpow_gt_ge2 = thm "realpow_gt_ge2";
  18.630 -val realpow_ge_ge = thm "realpow_ge_ge";
  18.631  val realpow_ge_ge2 = thm "realpow_ge_ge2";
  18.632 -val realpow_Suc_ge_self = thm "realpow_Suc_ge_self";
  18.633  val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
  18.634 -val realpow_ge_self = thm "realpow_ge_self";
  18.635  val realpow_ge_self2 = thm "realpow_ge_self2";
  18.636  val realpow_minus_mult = thm "realpow_minus_mult";
  18.637  val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
  18.638  val realpow_two_minus = thm "realpow_two_minus";
  18.639 -val realpow_two_diff = thm "realpow_two_diff";
  18.640  val realpow_two_disj = thm "realpow_two_disj";
  18.641  val realpow_diff = thm "realpow_diff";
  18.642  val realpow_real_of_nat = thm "realpow_real_of_nat";
  18.643 @@ -481,6 +569,38 @@
  18.644  val real_sqr_ge_zero = thm "real_sqr_ge_zero";
  18.645  val real_sqr_gt_zero = thm "real_sqr_gt_zero";
  18.646  val real_sqr_not_zero = thm "real_sqr_not_zero";
  18.647 +val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
  18.648 +val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
  18.649 +val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
  18.650 +val real_mult_is_one = thm "real_mult_is_one";
  18.651 +val real_le_add_half_cancel = thm "real_le_add_half_cancel";
  18.652 +val real_minus_half_eq = thm "real_minus_half_eq";
  18.653 +val real_mult_inverse_cancel = thm "real_mult_inverse_cancel";
  18.654 +val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
  18.655 +val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero";
  18.656 +val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
  18.657 +val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
  18.658 +val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
  18.659 +val abs_mult_abs = thm "abs_mult_abs";
  18.660 +
  18.661 +val realpow_divide = thm "realpow_divide";
  18.662 +val realpow_ge_zero2 = thm "realpow_ge_zero2";
  18.663 +val realpow_le2 = thm "realpow_le2";
  18.664 +val realpow_Suc_gt_one = thm "realpow_Suc_gt_one";
  18.665 +val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
  18.666 +val realpow_two_le_add_order = thm "realpow_two_le_add_order";
  18.667 +val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
  18.668 +val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
  18.669 +val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
  18.670 +val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
  18.671 +val real_minus_mult_self_le = thm "real_minus_mult_self_le";
  18.672 +val realpow_square_minus_le = thm "realpow_square_minus_le";
  18.673 +val realpow_num_eq_if = thm "realpow_num_eq_if";
  18.674 +val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
  18.675 +val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
  18.676 +val lemma_realpow_4 = thm "lemma_realpow_4";
  18.677 +val lemma_realpow_16 = thm "lemma_realpow_16";
  18.678 +val zero_le_x_squared = thm "zero_le_x_squared";
  18.679  *}
  18.680  
  18.681  
    19.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 25 10:37:03 2003 +0100
    19.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Nov 27 10:47:55 2003 +0100
    19.3 @@ -45,8 +45,8 @@
    19.4  axclass ordered_field \<subseteq> ordered_ring, field
    19.5  
    19.6  axclass division_by_zero \<subseteq> zero, inverse
    19.7 -  inverse_zero: "inverse 0 = 0"
    19.8 -  divide_zero: "a / 0 = 0"
    19.9 +  inverse_zero [simp]: "inverse 0 = 0"
   19.10 +  divide_zero [simp]: "a / 0 = 0"
   19.11  
   19.12  
   19.13  subsection {* Derived rules for addition *}
   19.14 @@ -87,7 +87,7 @@
   19.15       "(a + b = a + c) = (b = (c::'a::ring))"
   19.16  proof
   19.17    assume eq: "a + b = a + c"
   19.18 -  then have "(-a + a) + b = (-a + a) + c"
   19.19 +  hence "(-a + a) + b = (-a + a) + c"
   19.20      by (simp only: eq add_assoc)
   19.21    thus "b = c" by simp
   19.22  next
   19.23 @@ -116,7 +116,7 @@
   19.24  lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
   19.25    proof 
   19.26      assume "- a = - b"
   19.27 -    then have "- (- a) = - (- b)"
   19.28 +    hence "- (- a) = - (- b)"
   19.29        by simp
   19.30      thus "a=b" by simp
   19.31    next
   19.32 @@ -145,7 +145,7 @@
   19.33  
   19.34  theorems mult_ac = mult_assoc mult_commute mult_left_commute
   19.35  
   19.36 -lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = 1"
   19.37 +lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
   19.38  proof -
   19.39    have "a * inverse a = inverse a * a" by (simp add: mult_ac)
   19.40    also assume "a \<noteq> 0"
   19.41 @@ -207,6 +207,9 @@
   19.42  apply (simp add: right_distrib [symmetric]) 
   19.43  done
   19.44  
   19.45 +lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
   19.46 +  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
   19.47 +
   19.48  lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
   19.49  by (simp add: right_distrib diff_minus 
   19.50                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   19.51 @@ -223,14 +226,28 @@
   19.52    apply (simp add: add_commute add_left_mono)
   19.53    done
   19.54  
   19.55 +lemma add_strict_left_mono:
   19.56 +     "a < b ==> c + a < c + (b::'a::ordered_ring)"
   19.57 + by (simp add: order_less_le add_left_mono) 
   19.58 +
   19.59 +lemma add_strict_right_mono:
   19.60 +     "a < b ==> a + c < b + (c::'a::ordered_ring)"
   19.61 + by (simp add: add_commute [of _ c] add_strict_left_mono)
   19.62 +
   19.63 +text{*Strict monotonicity in both arguments*}
   19.64 +lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_ring)"
   19.65 +apply (erule add_strict_right_mono [THEN order_less_trans])
   19.66 +apply (erule add_strict_left_mono)
   19.67 +done
   19.68 +
   19.69  lemma le_imp_neg_le:
   19.70     assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
   19.71    proof -
   19.72    have "-a+a \<le> -a+b"
   19.73      by (rule add_left_mono) 
   19.74 -  then have "0 \<le> -a+b"
   19.75 +  hence "0 \<le> -a+b"
   19.76      by simp
   19.77 -  then have "0 + (-b) \<le> (-a + b) + (-b)"
   19.78 +  hence "0 + (-b) \<le> (-a + b) + (-b)"
   19.79      by (rule add_right_mono) 
   19.80    thus ?thesis
   19.81      by (simp add: add_assoc)
   19.82 @@ -239,7 +256,7 @@
   19.83  lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
   19.84    proof 
   19.85      assume "- b \<le> - a"
   19.86 -    then have "- (- a) \<le> - (- b)"
   19.87 +    hence "- (- a) \<le> - (- b)"
   19.88        by (rule le_imp_neg_le)
   19.89      thus "a\<le>b" by simp
   19.90    next
   19.91 @@ -288,73 +305,6 @@
   19.92  apply (simp_all add: minus_mult_right [symmetric]) 
   19.93  done
   19.94  
   19.95 -lemma mult_left_mono_neg:
   19.96 -     "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
   19.97 -apply (drule mult_left_mono [of _ _ "-c"]) 
   19.98 -apply (simp_all add: minus_mult_left [symmetric]) 
   19.99 -done
  19.100 -
  19.101 -lemma mult_right_mono_neg:
  19.102 -     "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
  19.103 -  by (simp add: mult_left_mono_neg mult_commute [of _ c]) 
  19.104 -
  19.105 -text{*Strict monotonicity in both arguments*}
  19.106 -lemma mult_strict_mono:
  19.107 -     "[|a<b; c<d; 0<b; 0<c|] ==> a * c < b * (d::'a::ordered_semiring)"
  19.108 -apply (erule mult_strict_right_mono [THEN order_less_trans], assumption)
  19.109 -apply (erule mult_strict_left_mono, assumption)
  19.110 -done
  19.111 -
  19.112 -lemma mult_mono:
  19.113 -     "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
  19.114 -      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
  19.115 -apply (erule mult_right_mono [THEN order_trans], assumption)
  19.116 -apply (erule mult_left_mono, assumption)
  19.117 -done
  19.118 -
  19.119 -
  19.120 -subsection{*Cancellation Laws for Relationships With a Common Factor*}
  19.121 -
  19.122 -text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  19.123 -   also with the relations @{text "\<le>"} and equality.*}
  19.124 -
  19.125 -lemma mult_less_cancel_right:
  19.126 -    "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
  19.127 -apply (case_tac "c = 0")
  19.128 -apply (auto simp add: linorder_neq_iff mult_strict_right_mono 
  19.129 -                      mult_strict_right_mono_neg)
  19.130 -apply (auto simp add: linorder_not_less 
  19.131 -                      linorder_not_le [symmetric, of "a*c"]
  19.132 -                      linorder_not_le [symmetric, of a])
  19.133 -apply (erule_tac [!] notE)
  19.134 -apply (auto simp add: order_less_imp_le mult_right_mono 
  19.135 -                      mult_right_mono_neg)
  19.136 -done
  19.137 -
  19.138 -lemma mult_less_cancel_left:
  19.139 -    "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
  19.140 -by (simp add: mult_commute [of c] mult_less_cancel_right)
  19.141 -
  19.142 -lemma mult_le_cancel_right:
  19.143 -     "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
  19.144 -by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
  19.145 -
  19.146 -lemma mult_le_cancel_left:
  19.147 -     "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
  19.148 -by (simp add: mult_commute [of c] mult_le_cancel_right)
  19.149 -
  19.150 -text{*Cancellation of equalities with a common factor*}
  19.151 -lemma mult_cancel_right [simp]:
  19.152 -     "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
  19.153 -apply (cut_tac linorder_less_linear [of 0 c])
  19.154 -apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
  19.155 -             simp add: linorder_neq_iff)
  19.156 -done
  19.157 -
  19.158 -lemma mult_cancel_left [simp]:
  19.159 -     "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
  19.160 -by (simp add: mult_commute [of c] mult_cancel_right)
  19.161 -
  19.162  
  19.163  subsection{* Products of Signs *}
  19.164  
  19.165 @@ -413,6 +363,99 @@
  19.166  apply (simp add: order_less_le) 
  19.167  done
  19.168  
  19.169 +lemma zero_le_one: "(0::'a::ordered_ring) \<le> 1"
  19.170 +  by (rule zero_less_one [THEN order_less_imp_le]) 
  19.171 +
  19.172 +
  19.173 +subsection{*More Monotonicity*}
  19.174 +
  19.175 +lemma mult_left_mono_neg:
  19.176 +     "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
  19.177 +apply (drule mult_left_mono [of _ _ "-c"]) 
  19.178 +apply (simp_all add: minus_mult_left [symmetric]) 
  19.179 +done
  19.180 +
  19.181 +lemma mult_right_mono_neg:
  19.182 +     "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
  19.183 +  by (simp add: mult_left_mono_neg mult_commute [of _ c]) 
  19.184 +
  19.185 +text{*Strict monotonicity in both arguments*}
  19.186 +lemma mult_strict_mono:
  19.187 +     "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_ring)"
  19.188 +apply (case_tac "c=0")
  19.189 + apply (simp add: mult_pos) 
  19.190 +apply (erule mult_strict_right_mono [THEN order_less_trans])
  19.191 + apply (force simp add: order_le_less) 
  19.192 +apply (erule mult_strict_left_mono, assumption)
  19.193 +done
  19.194 +
  19.195 +text{*This weaker variant has more natural premises*}
  19.196 +lemma mult_strict_mono':
  19.197 +     "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_ring)"
  19.198 +apply (rule mult_strict_mono)
  19.199 +apply (blast intro: order_le_less_trans)+
  19.200 +done
  19.201 +
  19.202 +lemma mult_mono:
  19.203 +     "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
  19.204 +      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
  19.205 +apply (erule mult_right_mono [THEN order_trans], assumption)
  19.206 +apply (erule mult_left_mono, assumption)
  19.207 +done
  19.208 +
  19.209 +
  19.210 +subsection{*Cancellation Laws for Relationships With a Common Factor*}
  19.211 +
  19.212 +text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  19.213 +   also with the relations @{text "\<le>"} and equality.*}
  19.214 +
  19.215 +lemma mult_less_cancel_right:
  19.216 +    "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
  19.217 +apply (case_tac "c = 0")
  19.218 +apply (auto simp add: linorder_neq_iff mult_strict_right_mono 
  19.219 +                      mult_strict_right_mono_neg)
  19.220 +apply (auto simp add: linorder_not_less 
  19.221 +                      linorder_not_le [symmetric, of "a*c"]
  19.222 +                      linorder_not_le [symmetric, of a])
  19.223 +apply (erule_tac [!] notE)
  19.224 +apply (auto simp add: order_less_imp_le mult_right_mono 
  19.225 +                      mult_right_mono_neg)
  19.226 +done
  19.227 +
  19.228 +lemma mult_less_cancel_left:
  19.229 +    "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
  19.230 +by (simp add: mult_commute [of c] mult_less_cancel_right)
  19.231 +
  19.232 +lemma mult_le_cancel_right:
  19.233 +     "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
  19.234 +by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
  19.235 +
  19.236 +lemma mult_le_cancel_left:
  19.237 +     "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
  19.238 +by (simp add: mult_commute [of c] mult_le_cancel_right)
  19.239 +
  19.240 +lemma mult_less_imp_less_left:
  19.241 +    "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
  19.242 +  by (force elim: order_less_asym simp add: mult_less_cancel_left)
  19.243 +
  19.244 +lemma mult_less_imp_less_right:
  19.245 +    "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
  19.246 +  by (force elim: order_less_asym simp add: mult_less_cancel_right)
  19.247 +
  19.248 +text{*Cancellation of equalities with a common factor*}
  19.249 +lemma mult_cancel_right [simp]:
  19.250 +     "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
  19.251 +apply (cut_tac linorder_less_linear [of 0 c])
  19.252 +apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
  19.253 +             simp add: linorder_neq_iff)
  19.254 +done
  19.255 +
  19.256 +text{*These cancellation theorems require an ordering. Versions are proved
  19.257 +      below that work for fields without an ordering.*}
  19.258 +lemma mult_cancel_left [simp]:
  19.259 +     "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
  19.260 +by (simp add: mult_commute [of c] mult_cancel_right)
  19.261 +
  19.262  
  19.263  subsection {* Absolute Value *}
  19.264  
  19.265 @@ -440,5 +483,217 @@
  19.266  
  19.267  subsection {* Fields *}
  19.268  
  19.269 +text{*Cancellation of equalities with a common factor*}
  19.270 +lemma field_mult_cancel_right_lemma:
  19.271 +  assumes cnz: "c \<noteq> (0::'a::field)"
  19.272 +      and eq:  "a*c = b*c"
  19.273 +     shows "a=b"
  19.274 +  proof -
  19.275 +  have "(a * c) * inverse c = (b * c) * inverse c"
  19.276 +    by (simp add: eq)
  19.277 +  thus "a=b"
  19.278 +    by (simp add: mult_assoc cnz)
  19.279 +  qed
  19.280 +
  19.281 +lemma field_mult_cancel_right:
  19.282 +     "(a*c = b*c) = (c = (0::'a::field) | a=b)"
  19.283 +  proof (cases "c=0")
  19.284 +    assume "c=0" thus ?thesis by simp
  19.285 +  next
  19.286 +    assume "c\<noteq>0" 
  19.287 +    thus ?thesis by (force dest: field_mult_cancel_right_lemma)
  19.288 +  qed
  19.289 +
  19.290 +lemma field_mult_cancel_left:
  19.291 +     "(c*a = c*b) = (c = (0::'a::field) | a=b)"
  19.292 +  by (simp add: mult_commute [of c] field_mult_cancel_right) 
  19.293 +
  19.294 +lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
  19.295 +  proof
  19.296 +  assume ianz: "inverse a = 0"
  19.297 +  assume "a \<noteq> 0"
  19.298 +  hence "1 = a * inverse a" by simp
  19.299 +  also have "... = 0" by (simp add: ianz)
  19.300 +  finally have "1 = (0::'a::field)" .
  19.301 +  thus False by (simp add: eq_commute)
  19.302 +  qed
  19.303 +
  19.304 +lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
  19.305 +apply (rule ccontr) 
  19.306 +apply (blast dest: nonzero_imp_inverse_nonzero) 
  19.307 +done
  19.308 +
  19.309 +lemma inverse_nonzero_imp_nonzero:
  19.310 +   "inverse a = 0 ==> a = (0::'a::field)"
  19.311 +apply (rule ccontr) 
  19.312 +apply (blast dest: nonzero_imp_inverse_nonzero) 
  19.313 +done
  19.314 +
  19.315 +lemma inverse_nonzero_iff_nonzero [simp]:
  19.316 +   "(inverse a = 0) = (a = (0::'a::{field,division_by_zero}))"
  19.317 +by (force dest: inverse_nonzero_imp_nonzero) 
  19.318 +
  19.319 +lemma nonzero_inverse_minus_eq:
  19.320 +     "a\<noteq>0 ==> inverse(-a) = -inverse(a::'a::field)";
  19.321 +  proof -
  19.322 +    assume "a\<noteq>0" 
  19.323 +    hence "-a * inverse (- a) = -a * - inverse a"
  19.324 +      by simp
  19.325 +    thus ?thesis 
  19.326 +      by (simp only: field_mult_cancel_left, simp add: prems)
  19.327 +  qed
  19.328 +
  19.329 +lemma inverse_minus_eq [simp]:
  19.330 +     "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
  19.331 +  proof (cases "a=0")
  19.332 +    assume "a=0" thus ?thesis by (simp add: inverse_zero)
  19.333 +  next
  19.334 +    assume "a\<noteq>0" 
  19.335 +    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
  19.336 +  qed
  19.337 +
  19.338 +lemma nonzero_inverse_eq_imp_eq:
  19.339 +   assumes inveq: "inverse a = inverse b"
  19.340 +       and anz:  "a \<noteq> 0"
  19.341 +       and bnz:  "b \<noteq> 0"
  19.342 +      shows "a = (b::'a::field)"
  19.343 +  proof -
  19.344 +  have "a * inverse b = a * inverse a"
  19.345 +    by (simp add: inveq)
  19.346 +  hence "(a * inverse b) * b = (a * inverse a) * b"
  19.347 +    by simp
  19.348 +  thus "a = b"
  19.349 +    by (simp add: mult_assoc anz bnz)
  19.350 +  qed
  19.351 +
  19.352 +lemma inverse_eq_imp_eq:
  19.353 +     "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"
  19.354 +apply (case_tac "a=0 | b=0") 
  19.355 + apply (force dest!: inverse_zero_imp_zero
  19.356 +              simp add: eq_commute [of "0::'a"])
  19.357 +apply (force dest!: nonzero_inverse_eq_imp_eq) 
  19.358 +done
  19.359 +
  19.360 +lemma inverse_eq_iff_eq [simp]:
  19.361 +     "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
  19.362 +by (force dest!: inverse_eq_imp_eq) 
  19.363 +
  19.364 +
  19.365 +subsection {* Ordered Fields *}
  19.366 +
  19.367 +lemma inverse_gt_0: 
  19.368 +    assumes a_gt_0: "0 < a"
  19.369 +      shows "0 < inverse (a::'a::ordered_field)"
  19.370 +  proof -
  19.371 +  have "0 < a * inverse a" 
  19.372 +    by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
  19.373 +  thus "0 < inverse a" 
  19.374 +    by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
  19.375 +  qed
  19.376 +
  19.377 +lemma inverse_less_0:
  19.378 +     "a < 0 ==> inverse a < (0::'a::ordered_field)"
  19.379 +  by (insert inverse_gt_0 [of "-a"], 
  19.380 +      simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 
  19.381 +
  19.382 +lemma inverse_le_imp_le:
  19.383 +   assumes invle: "inverse a \<le> inverse b"
  19.384 +       and apos:  "0 < a"
  19.385 +      shows "b \<le> (a::'a::ordered_field)"
  19.386 +  proof (rule classical)
  19.387 +  assume "~ b \<le> a"
  19.388 +  hence "a < b"
  19.389 +    by (simp add: linorder_not_le)
  19.390 +  hence bpos: "0 < b"
  19.391 +    by (blast intro: apos order_less_trans)
  19.392 +  hence "a * inverse a \<le> a * inverse b"
  19.393 +    by (simp add: apos invle order_less_imp_le mult_left_mono)
  19.394 +  hence "(a * inverse a) * b \<le> (a * inverse b) * b"
  19.395 +    by (simp add: bpos order_less_imp_le mult_right_mono)
  19.396 +  thus "b \<le> a"
  19.397 +    by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
  19.398 +  qed
  19.399 +
  19.400 +lemma less_imp_inverse_less:
  19.401 +   assumes less: "a < b"
  19.402 +       and apos:  "0 < a"
  19.403 +     shows "inverse b < inverse (a::'a::ordered_field)"
  19.404 +  proof (rule ccontr)
  19.405 +  assume "~ inverse b < inverse a"
  19.406 +  hence "inverse a \<le> inverse b"
  19.407 +    by (simp add: linorder_not_less)
  19.408 +  hence "~ (a < b)"
  19.409 +    by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
  19.410 +  thus False
  19.411 +    by (rule notE [OF _ less])
  19.412 +  qed
  19.413 +
  19.414 +lemma inverse_less_imp_less:
  19.415 +   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
  19.416 +apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
  19.417 +apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
  19.418 +done
  19.419 +
  19.420 +text{*Both premises are essential. Consider -1 and 1.*}
  19.421 +lemma inverse_less_iff_less [simp]:
  19.422 +     "[|0 < a; 0 < b|] 
  19.423 +      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  19.424 +by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
  19.425 +
  19.426 +lemma le_imp_inverse_le:
  19.427 +   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  19.428 +  by (force simp add: order_le_less less_imp_inverse_less)
  19.429 +
  19.430 +lemma inverse_le_iff_le [simp]:
  19.431 +     "[|0 < a; 0 < b|] 
  19.432 +      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  19.433 +by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
  19.434 +
  19.435 +
  19.436 +text{*These results refer to both operands being negative.  The opposite-sign
  19.437 +case is trivial, since inverse preserves signs.*}
  19.438 +lemma inverse_le_imp_le_neg:
  19.439 +   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
  19.440 +  apply (rule classical) 
  19.441 +  apply (subgoal_tac "a < 0") 
  19.442 +   prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
  19.443 +  apply (insert inverse_le_imp_le [of "-b" "-a"])
  19.444 +  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  19.445 +  done
  19.446 +
  19.447 +lemma less_imp_inverse_less_neg:
  19.448 +   "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
  19.449 +  apply (subgoal_tac "a < 0") 
  19.450 +   prefer 2 apply (blast intro: order_less_trans) 
  19.451 +  apply (insert less_imp_inverse_less [of "-b" "-a"])
  19.452 +  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  19.453 +  done
  19.454 +
  19.455 +lemma inverse_less_imp_less_neg:
  19.456 +   "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
  19.457 +  apply (rule classical) 
  19.458 +  apply (subgoal_tac "a < 0") 
  19.459 +   prefer 2
  19.460 +   apply (force simp add: linorder_not_less intro: order_le_less_trans) 
  19.461 +  apply (insert inverse_less_imp_less [of "-b" "-a"])
  19.462 +  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  19.463 +  done
  19.464 +
  19.465 +lemma inverse_less_iff_less_neg [simp]:
  19.466 +     "[|a < 0; b < 0|] 
  19.467 +      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
  19.468 +  apply (insert inverse_less_iff_less [of "-b" "-a"])
  19.469 +  apply (simp del: inverse_less_iff_less 
  19.470 +	      add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
  19.471 +  done
  19.472 +
  19.473 +lemma le_imp_inverse_le_neg:
  19.474 +   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
  19.475 +  by (force simp add: order_le_less less_imp_inverse_less_neg)
  19.476 +
  19.477 +lemma inverse_le_iff_le_neg [simp]:
  19.478 +     "[|a < 0; b < 0|] 
  19.479 +      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
  19.480 +by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
  19.481  
  19.482  end