Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
New theorems for Ring_and_Field. Fixing affected proofs.
--- a/src/HOL/Hyperreal/ExtraThms2.ML Tue Nov 25 10:37:03 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,557 +0,0 @@
-(*lcp: needed for binary 2 MOVE UP???*)
-
-Goal "(0::real) <= x^2";
-by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2]) 1);
-qed "zero_le_x_squared";
-Addsimps [zero_le_x_squared];
-
-fun multl_by_tac x i =
- let val cancel_thm =
- CLAIM "[| (0::real)<z; z*x<z*y |] ==> x<y"
- in
- res_inst_tac [("z",x)] cancel_thm i
- end;
-
-fun multr_by_tac x i =
- let val cancel_thm =
- CLAIM "[| (0::real)<z; x*z<y*z |] ==> x<y"
- in
- res_inst_tac [("z",x)] cancel_thm i
- end;
-
-(* unused? *)
-Goal "ALL x y. x < y --> (f::real=>real) x < f y ==> inj f";
-by (rtac injI 1 THEN rtac ccontr 1);
-by (dtac (ARITH_PROVE "x ~= y ==> x < y | y < (x::real)") 1);
-by (Step_tac 1);
-by (auto_tac (claset() addSDs [spec],simpset()));
-qed "real_monofun_inj";
-
-(* HyperDef *)
-
-Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
-by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
-qed "hypreal_zero_num";
-
-Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
-by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
-qed "hypreal_one_num";
-
-(* RealOrd *)
-
-Goalw [real_of_posnat_def] "0 < real_of_posnat n";
-by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
-by (Blast_tac 1);
-qed "real_of_posnat_gt_zero";
-
-Addsimps [real_of_posnat_gt_zero];
-
-bind_thm ("real_inv_real_of_posnat_gt_zero",
- real_of_posnat_gt_zero RS real_inverse_gt_0);
-Addsimps [real_inv_real_of_posnat_gt_zero];
-
-bind_thm ("real_of_posnat_ge_zero",real_of_posnat_gt_zero RS order_less_imp_le);
-Addsimps [real_of_posnat_ge_zero];
-
-Goal "real_of_posnat n ~= 0";
-by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1);
-qed "real_of_posnat_not_eq_zero";
-Addsimps[real_of_posnat_not_eq_zero];
-
-Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_left];
-Addsimps [real_of_posnat_not_eq_zero RS real_mult_inv_right];
-
-Goal "1 <= real_of_posnat n";
-by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1);
-by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
- order_less_imp_le]));
-qed "real_of_posnat_ge_one";
-Addsimps [real_of_posnat_ge_one];
-
-Goal "inverse(real_of_posnat n) ~= 0";
-by (rtac ((real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1);
-qed "real_of_posnat_real_inv_not_zero";
-Addsimps [real_of_posnat_real_inv_not_zero];
-
-Goal "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y";
-by (rtac (inj_real_of_posnat RS injD) 1);
-by (res_inst_tac [("n2","x")]
- (real_of_posnat_real_inv_not_zero RS real_mult_left_cancel RS iffD1) 1);
-by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1);
-qed "real_of_posnat_real_inv_inj";
-
-Goal "r < r + inverse(real_of_posnat n)";
-by Auto_tac;
-qed "real_add_inv_real_of_posnat_less";
-Addsimps [real_add_inv_real_of_posnat_less];
-
-Goal "r <= r + inverse(real_of_posnat n)";
-by Auto_tac;
-qed "real_add_inv_real_of_posnat_le";
-Addsimps [real_add_inv_real_of_posnat_le];
-
-Goal "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r";
-by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
-by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
-by (auto_tac (claset() addIs [real_mult_order],simpset()
- addsimps [real_add_assoc RS sym,real_minus_zero_less_iff2]));
-qed "real_mult_less_self";
-
-Goal "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero
- RS real_mult_less_mono1) 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_0 RS real_mult_less_mono1) 2);
-by (auto_tac (claset(),
- simpset() addsimps [(real_of_posnat_gt_zero RS
- real_not_refl2 RS not_sym),real_mult_assoc]));
-qed "real_of_posnat_inv_Ex_iff";
-
-Goal "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero
- RS real_mult_less_mono1) 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_0 RS real_mult_less_mono1) 2);
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
-qed "real_of_posnat_inv_iff";
-
-Goal "[| (0::real) <=z; x<y |] ==> z*x<=z*y";
-by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
-qed "real_mult_le_less_mono2";
-
-Goal "[| (0::real) <=z; x<=y |] ==> z*x<=z*y";
-by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
-qed "real_mult_le_le_mono1";
-
-Goal "[| (0::real)<=z; x<=y |] ==> x*z<=y*z";
-by (dtac (real_mult_le_le_mono1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
-qed "real_mult_le_le_mono2";
-
-Goal "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)";
-by (Step_tac 1);
-by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS
- order_less_imp_le RS real_mult_le_le_mono1) 1);
-by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS
- real_inverse_gt_0 RS order_less_imp_le RS
- real_mult_le_le_mono1) 2);
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
-qed "real_of_posnat_inv_le_iff";
-
-Goalw [real_of_posnat_def]
- "(real_of_posnat n < real_of_posnat m) = (n < m)";
-by Auto_tac;
-qed "real_of_posnat_less_iff";
-Addsimps [real_of_posnat_less_iff];
-
-Goal "(real_of_posnat n <= real_of_posnat m) = (n <= m)";
-by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],
- simpset() addsimps [real_le_less,le_eq_less_or_eq]));
-qed "real_of_posnat_le_iff";
-Addsimps [real_of_posnat_le_iff];
-
-Goal "[| (0::real)<z; x*z<y*z |] ==> x<y";
-by Auto_tac;
-qed "real_mult_less_cancel3";
-
-Goal "[| (0::real)<z; z*x<z*y |] ==> x<y";
-by Auto_tac;
-qed "real_mult_less_cancel4";
-
-Goal "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))";
-by (Step_tac 1);
-by (res_inst_tac [("n2","n")] ((real_of_posnat_gt_zero RS
- real_inverse_gt_0) RS real_mult_less_cancel3) 1);
-by (res_inst_tac [("x1","u")] ( real_inverse_gt_0
- RS real_mult_less_cancel3) 2);
-by (auto_tac (claset(),
- simpset() addsimps [real_not_refl2 RS not_sym]));
-by (res_inst_tac [("z","u")] real_mult_less_cancel4 1);
-by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS
- real_mult_less_cancel4) 3);
-by (auto_tac (claset(),
- simpset() addsimps [real_not_refl2 RS not_sym,
- real_mult_assoc RS sym]));
-qed "real_of_posnat_less_inv_iff";
-
-Goal "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)";
-by Auto_tac;
-qed "real_of_posnat_inv_eq_iff";
-
-Goal "0 <= 1 + -inverse(real_of_posnat n)";
-by (res_inst_tac [("C","inverse(real_of_posnat n)")] real_le_add_right_cancel 1);
-by (simp_tac (simpset() addsimps [real_add_assoc,
- real_of_posnat_inv_le_iff]) 1);
-qed "real_add_one_minus_inv_ge_zero";
-
-Goal "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))";
-by (dtac (real_add_one_minus_inv_ge_zero RS real_mult_le_less_mono1) 1);
-by (Auto_tac);
-qed "real_mult_add_one_minus_ge_zero";
-
-Goal "x*y = (1::real) ==> y = inverse x";
-by (case_tac "x ~= 0" 1);
-by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
-by Auto_tac;
-qed "real_inverse_unique";
-
-Goal "[| (0::real) < x; x < 1 |] ==> 1 < inverse x";
-by (auto_tac (claset() addDs [real_inverse_less_swap],simpset()));
-qed "real_inverse_gt_one";
-
-Goal "(0 < real (n::nat)) = (0 < n)";
-by (rtac (real_of_nat_less_iff RS subst) 1);
-by Auto_tac;
-qed "real_of_nat_gt_zero_cancel_iff";
-Addsimps [real_of_nat_gt_zero_cancel_iff];
-
-Goal "(real (n::nat) <= 0) = (n = 0)";
-by (rtac ((real_of_nat_zero) RS subst) 1);
-by (stac real_of_nat_le_iff 1);
-by Auto_tac;
-qed "real_of_nat_le_zero_cancel_iff";
-Addsimps [real_of_nat_le_zero_cancel_iff];
-
-Goal "~ real (n::nat) < 0";
-by (simp_tac (simpset() addsimps [symmetric real_le_def,
- real_of_nat_ge_zero]) 1);
-qed "not_real_of_nat_less_zero";
-Addsimps [not_real_of_nat_less_zero];
-
-Goalw [real_le_def,le_def]
- "(0 <= real (n::nat)) = (0 <= n)";
-by (Simp_tac 1);
-qed "real_of_nat_ge_zero_cancel_iff";
-Addsimps [real_of_nat_ge_zero_cancel_iff];
-
-Goal "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))";
-by (case_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc]));
-qed "real_of_nat_num_if";
-
-Goal "4 * real n = real (4 * (n::nat))";
-by Auto_tac;
-qed "real_of_nat_mult_num_4_eq";
-
-(*REDUNDANT
- Goal "x * x = -(y * y) ==> x = (0::real)";
- by (auto_tac (claset() addIs [
- real_sum_squares_cancel],simpset()));
- qed "real_sum_squares_cancel1a";
-
- Goal "x * x = -(y * y) ==> y = (0::real)";
- by (auto_tac (claset() addIs [
- real_sum_squares_cancel],simpset()));
- qed "real_sum_squares_cancel2a";
-*)
-
-Goal "x * x = -(y * y) ==> x = (0::real) & y=0";
-by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset()));
-qed "real_sum_squares_cancel_a";
-
-Goal "x*x - (1::real) = (x + 1)*(x - 1)";
-by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib,
- real_add_mult_distrib2,real_diff_def]));
-qed "real_squared_diff_one_factored";
-
-Goal "(x*x = (1::real)) = (x = 1 | x = - 1)";
-by Auto_tac;
-by (dtac (CLAIM "x = (y::real) ==> x - y = 0") 1);
-by (auto_tac (claset(),simpset() addsimps [real_squared_diff_one_factored]));
-qed "real_mult_is_one";
-AddIffs [real_mult_is_one];
-
-Goal "(x + y/2 <= (y::real)) = (x <= y /2)";
-by Auto_tac;
-qed "real_le_add_half_cancel";
-Addsimps [real_le_add_half_cancel];
-
-Goal "(x::real) - x/2 = x/2";
-by Auto_tac;
-qed "real_minus_half_eq";
-Addsimps [real_minus_half_eq];
-
-Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> inverse x * y < inverse x1 * u";
-by (multl_by_tac "x" 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
-by (simp_tac (simpset() addsimps real_mult_ac) 1);
-by (multr_by_tac "x1" 1);
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
-qed "real_mult_inverse_cancel";
-
-Goal "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1";
-by (auto_tac (claset() addDs [real_mult_inverse_cancel],simpset() addsimps real_mult_ac));
-qed "real_mult_inverse_cancel2";
-
-Goal "0 < inverse (real (Suc n))";
-by Auto_tac;
-qed "inverse_real_of_nat_gt_zero";
-Addsimps [ inverse_real_of_nat_gt_zero];
-
-Goal "0 <= inverse (real (Suc n))";
-by Auto_tac;
-qed "inverse_real_of_nat_ge_zero";
-Addsimps [ inverse_real_of_nat_ge_zero];
-
-Goal "x ~= 0 ==> x * x + y * y ~= (0::real)";
-by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
-by (dtac (real_sum_squares_cancel) 1);
-by (Asm_full_simp_tac 1);
-qed "real_sum_squares_not_zero";
-
-Goal "y ~= 0 ==> x * x + y * y ~= (0::real)";
-by (rtac (CLAIM "!!x. ((x = y ==> False)) ==> x ~= y") 1);
-by (dtac (real_sum_squares_cancel2) 1);
-by (Asm_full_simp_tac 1);
-qed "real_sum_squares_not_zero2";
-
-(* RealAbs *)
-
-(* nice theorem *)
-Goal "abs x * abs x = x * (x::real)";
-by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI2,abs_minus_eqI2]));
-qed "abs_mult_abs";
-Addsimps [abs_mult_abs];
-
-(* RealPow *)
-Goalw [real_divide_def]
- "(x/y) ^ n = ((x::real) ^ n/ y ^ n)";
-by (auto_tac (claset(),simpset() addsimps [realpow_mult,
- realpow_inverse]));
-qed "realpow_divide";
-
-Goal "isCont (%x. x ^ n) x";
-by (rtac (DERIV_pow RS DERIV_isCont) 1);
-qed "isCont_realpow";
-Addsimps [isCont_realpow];
-
-Goal "(0::real) <= r --> 0 <= r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [real_0_le_mult_iff]));
-qed_spec_mp "realpow_ge_zero2";
-
-Goal "(0::real) <= x & x <= y --> x ^ n <= y ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [real_mult_le_mono],
- simpset() addsimps [realpow_ge_zero2]));
-qed_spec_mp "realpow_le2";
-
-Goal "(1::real) < r ==> 1 < r ^ (Suc n)";
-by (forw_inst_tac [("n","n")] realpow_ge_one 1);
-by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
-by (forward_tac [(real_zero_less_one RS real_less_trans)] 1);
-by (dres_inst_tac [("y","r ^ n")] (real_mult_less_mono2) 1);
-by (assume_tac 1);
-by (auto_tac (claset() addDs [real_less_trans],simpset()));
-qed "realpow_Suc_gt_one";
-
-Goal "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)";
-by (auto_tac (claset() addIs [real_sum_squares_cancel, real_sum_squares_cancel2],
- simpset() addsimps [numeral_2_eq_2]));
-qed "realpow_two_sum_zero_iff";
-Addsimps [realpow_two_sum_zero_iff];
-
-Goal "(0::real) <= u ^ 2 + v ^ 2";
-by (rtac (real_le_add_order) 1);
-by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2]));
-qed "realpow_two_le_add_order";
-Addsimps [realpow_two_le_add_order];
-
-Goal "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2";
-by (REPEAT(rtac (real_le_add_order) 1));
-by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2]));
-qed "realpow_two_le_add_order2";
-Addsimps [realpow_two_le_add_order2];
-
-Goal "(0::real) <= x*x + y*y";
-by (cut_inst_tac [("u","x"),("v","y")] realpow_two_le_add_order 1);
-by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2]));
-qed "real_mult_self_sum_ge_zero";
-Addsimps [real_mult_self_sum_ge_zero];
-Addsimps [real_mult_self_sum_ge_zero RS abs_eqI1];
-
-Goal "x ~= 0 ==> (0::real) < x * x + y * y";
-by (cut_inst_tac [("x","x"),("y","y")] real_mult_self_sum_ge_zero 1);
-by (dtac real_le_imp_less_or_eq 1);
-by (dres_inst_tac [("y","y")] real_sum_squares_not_zero 1);
-by Auto_tac;
-qed "real_sum_square_gt_zero";
-
-Goal "y ~= 0 ==> (0::real) < x * x + y * y";
-by (rtac (real_add_commute RS subst) 1);
-by (etac real_sum_square_gt_zero 1);
-qed "real_sum_square_gt_zero2";
-
-Goal "-(u * u) <= (x * (x::real))";
-by (res_inst_tac [("j","0")] real_le_trans 1);
-by Auto_tac;
-qed "real_minus_mult_self_le";
-Addsimps [real_minus_mult_self_le];
-
-Goal "-(u ^ 2) <= (x::real) ^ 2";
-by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2]));
-qed "realpow_square_minus_le";
-Addsimps [realpow_square_minus_le];
-
-Goal "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "realpow_num_eq_if";
-
-Goal "0 < (2::real) ^ (4*d)";
-by (induct_tac "d" 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
-qed "real_num_zero_less_two_pow";
-Addsimps [real_num_zero_less_two_pow];
-
-Goal "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)";
-by (subgoal_tac "(2::real) ^ 8 = 4 * (2 ^ 6)" 1);
-by (asm_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_num_eq_if]));
-qed "lemma_realpow_num_two_mono";
-
-Goal "2 ^ 2 = (4::real)";
-by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
-val lemma_realpow_4 = result();
-Addsimps [lemma_realpow_4];
-
-Goal "2 ^ 4 = (16::real)";
-by (simp_tac (simpset() addsimps [realpow_num_eq_if]) 1);
-val lemma_realpow_16 = result();
-Addsimps [lemma_realpow_16];
-
-(* HyperOrd *)
-
-Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
- hypreal_mult_less_zero]));
-qed "hypreal_mult_less_zero2";
-
-(* HyperPow *)
-Goal "(0::hypreal) <= x * x";
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_0_le_mult_iff]));
-qed "hypreal_mult_self_ge_zero";
-Addsimps [hypreal_mult_self_ge_zero];
-
-(* deleted from distribution but I prefer to have it *)
-Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps
- [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
-by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
- simpset()) 1);
-qed "hrealpow_Suc_cancel_eq";
-
-(* NSA.ML: next two were there before? Not in distrib though *)
-
-Goal "[| x + y : HInfinite; y: HFinite |] ==> x : HInfinite";
-by (rtac ccontr 1);
-by (dtac (HFinite_HInfinite_iff RS iffD2) 1);
-by (auto_tac (claset() addDs [HFinite_add],simpset()
- addsimps [HInfinite_HFinite_iff]));
-qed "HInfinite_HFinite_add_cancel";
-
-Goal "[| x : HInfinite; y : HFinite |] ==> x + y : HInfinite";
-by (res_inst_tac [("y","-y")] HInfinite_HFinite_add_cancel 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc,
- HFinite_minus_iff]));
-qed "HInfinite_HFinite_add";
-
-Goal "[| x : HInfinite; x <= y; 0 <= x |] ==> y : HInfinite";
-by (auto_tac (claset() addIs [HFinite_bounded],simpset()
- addsimps [HInfinite_HFinite_iff]));
-qed "HInfinite_ge_HInfinite";
-
-Goal "[| x : Infinitesimal; x ~= 0 |] ==> inverse x : HInfinite";
-by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
-by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult2],simpset()));
-qed "Infinitesimal_inverse_HInfinite";
-
-Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
- HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by Auto_tac;
-by (dres_inst_tac [("x","m + 1")] spec 1);
-by (Ultra_tac 1);
-by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
-by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
-by (rtac real_inverse_less_swap 1);
-by Auto_tac;
-qed "HNatInfinite_inverse_Infinitesimal";
-Addsimps [HNatInfinite_inverse_Infinitesimal];
-
-Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
-by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
-qed "HNatInfinite_inverse_not_zero";
-Addsimps [HNatInfinite_inverse_not_zero];
-
-Goal "N : HNatInfinite \
-\ ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
-by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
-by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
-qed "starfunNat_inverse_real_of_nat_Infinitesimal";
-Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
-
-Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
-\ ==> x * y : HInfinite";
-by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
-by (ftac HFinite_Infinitesimal_not_zero 1);
-by (dtac HFinite_not_Infinitesimal_inverse 1);
-by (Step_tac 1 THEN dtac HFinite_mult 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
- HFinite_HInfinite_iff]));
-qed "HInfinite_HFinite_not_Infinitesimal_mult";
-
-Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
-\ ==> y * x : HInfinite";
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
- HInfinite_HFinite_not_Infinitesimal_mult]));
-qed "HInfinite_HFinite_not_Infinitesimal_mult2";
-
-Goal "[| x : HInfinite; 0 < x; y : Reals |] ==> y < x";
-by (auto_tac (claset() addSDs [bspec],simpset() addsimps
- [HInfinite_def,hrabs_def,order_less_imp_le]));
-qed "HInfinite_gt_SReal";
-
-Goal "[| x : HInfinite; 0 < x |] ==> 1 < x";
-by (auto_tac (claset() addIs [HInfinite_gt_SReal],simpset()));
-qed "HInfinite_gt_zero_gt_one";
-
-(* not added at proof?? *)
-Addsimps [HInfinite_omega];
-
-(* Add in HyperDef.ML? *)
-Goalw [omega_def] "0 < omega";
-by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
-qed "hypreal_omega_gt_zero";
-Addsimps [hypreal_omega_gt_zero];
-
-Goal "1 ~: HInfinite";
-by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
-qed "not_HInfinite_one";
-Addsimps [not_HInfinite_one];
-
-
-(* RComplete.ML *)
-
-Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x";
-by (Step_tac 1);
-by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1);
-by (Step_tac 1);
-by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def]));
-qed "reals_Archimedean3";
-
--- a/src/HOL/Hyperreal/ExtraThms2.thy Tue Nov 25 10:37:03 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-ExtraThms2 = HSeries
\ No newline at end of file
--- a/src/HOL/Hyperreal/HyperDef.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/HyperDef.ML Thu Nov 27 10:47:55 2003 +0100
@@ -1238,3 +1238,20 @@
(simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
qed "hypreal_eq_eqI";
+
+(*MOVE UP*)
+Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
+by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
+qed "hypreal_zero_num";
+
+Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
+by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
+qed "hypreal_one_num";
+
+
+(*MOVE UP*)
+
+Goalw [omega_def] "0 < omega";
+by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
+qed "hypreal_omega_gt_zero";
+Addsimps [hypreal_omega_gt_zero];
--- a/src/HOL/Hyperreal/HyperNat.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML Thu Nov 27 10:47:55 2003 +0100
@@ -1308,3 +1308,22 @@
+(*MOVE UP*)
+Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
+ HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
+by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
+by Auto_tac;
+by (dres_inst_tac [("x","m + 1")] spec 1);
+by (Ultra_tac 1);
+by (subgoal_tac "abs(inverse (real (Y x))) = inverse(real (Y x))" 1);
+by (auto_tac (claset() addSIs [abs_eqI2],simpset()));
+qed "HNatInfinite_inverse_Infinitesimal";
+Addsimps [HNatInfinite_inverse_Infinitesimal];
+
+Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
+by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
+qed "HNatInfinite_inverse_not_zero";
+Addsimps [HNatInfinite_inverse_not_zero];
+
--- a/src/HOL/Hyperreal/HyperOrd.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.ML Thu Nov 27 10:47:55 2003 +0100
@@ -523,3 +523,7 @@
linorder_not_less RS sym]));
qed "hypreal_mult_le_0_iff";
+Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
+by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
+ hypreal_mult_less_zero]));
+qed "hypreal_mult_less_zero2";
--- a/src/HOL/Hyperreal/HyperPow.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Thu Nov 27 10:47:55 2003 +0100
@@ -533,3 +533,20 @@
hypnat_of_nat_less_iff,hypnat_of_nat_zero]
delsimps [hypnat_of_nat_less_iff RS sym]));
qed "Infinitesimal_hrealpow";
+
+(* MOVE UP *)
+Goal "(0::hypreal) <= x * x";
+by (auto_tac (claset(),simpset() addsimps
+ [hypreal_0_le_mult_iff]));
+qed "hypreal_mult_self_ge_zero";
+Addsimps [hypreal_mult_self_ge_zero];
+
+Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps
+ [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
+by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
+ simpset()) 1);
+qed "hrealpow_Suc_cancel_eq";
+
--- a/src/HOL/Hyperreal/NSA.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Thu Nov 27 10:47:55 2003 +0100
@@ -2177,6 +2177,7 @@
by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
FreeUltrafilterNat_omega]) 1);
qed "HInfinite_omega";
+Addsimps [HInfinite_omega];
(*-----------------------------------------------
Epsilon is a member of Infinitesimal
@@ -2324,3 +2325,62 @@
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal2";
+
+
+
+
+
+(*MOVE UP*)
+Goal "[| x + y : HInfinite; y: HFinite |] ==> x : HInfinite";
+by (rtac ccontr 1);
+by (dtac (HFinite_HInfinite_iff RS iffD2) 1);
+by (auto_tac (claset() addDs [HFinite_add],simpset()
+ addsimps [HInfinite_HFinite_iff]));
+qed "HInfinite_HFinite_add_cancel";
+
+Goal "[| x : HInfinite; y : HFinite |] ==> x + y : HInfinite";
+by (res_inst_tac [("y","-y")] HInfinite_HFinite_add_cancel 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc,
+ HFinite_minus_iff]));
+qed "HInfinite_HFinite_add";
+
+Goal "[| x : HInfinite; x <= y; 0 <= x |] ==> y : HInfinite";
+by (auto_tac (claset() addIs [HFinite_bounded],simpset()
+ addsimps [HInfinite_HFinite_iff]));
+qed "HInfinite_ge_HInfinite";
+
+Goal "[| x : Infinitesimal; x ~= 0 |] ==> inverse x : HInfinite";
+by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
+by (auto_tac (claset() addDs [Infinitesimal_HFinite_mult2],simpset()));
+qed "Infinitesimal_inverse_HInfinite";
+
+Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
+\ ==> x * y : HInfinite";
+by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
+by (ftac HFinite_Infinitesimal_not_zero 1);
+by (dtac HFinite_not_Infinitesimal_inverse 1);
+by (Step_tac 1 THEN dtac HFinite_mult 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
+ HFinite_HInfinite_iff]));
+qed "HInfinite_HFinite_not_Infinitesimal_mult";
+
+Goal "[| x : HInfinite; y : HFinite - Infinitesimal |] \
+\ ==> y * x : HInfinite";
+by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
+ HInfinite_HFinite_not_Infinitesimal_mult]));
+qed "HInfinite_HFinite_not_Infinitesimal_mult2";
+
+Goal "[| x : HInfinite; 0 < x; y : Reals |] ==> y < x";
+by (auto_tac (claset() addSDs [bspec],simpset() addsimps
+ [HInfinite_def,hrabs_def,order_less_imp_le]));
+qed "HInfinite_gt_SReal";
+
+Goal "[| x : HInfinite; 0 < x |] ==> 1 < x";
+by (auto_tac (claset() addIs [HInfinite_gt_SReal],simpset()));
+qed "HInfinite_gt_zero_gt_one";
+
+
+Goal "1 ~: HInfinite";
+by (simp_tac (simpset() addsimps [HInfinite_HFinite_iff]) 1);
+qed "not_HInfinite_one";
+Addsimps [not_HInfinite_one];
--- a/src/HOL/Hyperreal/NatStar.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Thu Nov 27 10:47:55 2003 +0100
@@ -479,3 +479,15 @@
by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
qed "starfun_eq_iff";
+
+
+
+(*MOVE UP*)
+
+Goal "N : HNatInfinite \
+\ ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
+by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
+by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
+by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
+qed "starfunNat_inverse_real_of_nat_Infinitesimal";
+Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
--- a/src/HOL/Hyperreal/NthRoot.thy Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy Thu Nov 27 10:47:55 2003 +0100
@@ -5,4 +5,4 @@
http://www.math.unl.edu/~webnotes
*)
-NthRoot = SEQ + ExtraThms2
+NthRoot = SEQ + HSeries
--- a/src/HOL/Hyperreal/SEQ.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Thu Nov 27 10:47:55 2003 +0100
@@ -661,7 +661,7 @@
by (dtac lemma_converg3 1);
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [order_less_le_trans],
- simpset() addsimps [real_minus_zero_le_iff]));
+ simpset()));
val lemma_converg4 = result();
(*-------------------------------------------------------------------
--- a/src/HOL/Hyperreal/Transcendental.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Thu Nov 27 10:47:55 2003 +0100
@@ -5,6 +5,13 @@
Description : Power Series
*)
+fun multr_by_tac x i =
+ let val cancel_thm =
+ CLAIM "[| (0::real)<z; x*z<y*z |] ==> x<y"
+ in
+ res_inst_tac [("z",x)] cancel_thm i
+ end;
+
Goalw [root_def] "root (Suc n) 0 = 0";
by (safe_tac (claset() addSIs [some_equality,realpow_zero]
addSEs [realpow_zero_zero]));
--- a/src/HOL/Integ/Int.thy Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Integ/Int.thy Thu Nov 27 10:47:55 2003 +0100
@@ -393,11 +393,6 @@
lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
by (rule Ring_and_Field.mult_strict_right_mono)
-(* < monotonicity, BOTH arguments*)
-lemma zmult_zless_mono:
- "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"
- by (rule Ring_and_Field.mult_strict_mono)
-
lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
by (rule Ring_and_Field.mult_strict_right_mono_neg)
@@ -501,7 +496,6 @@
val zmult_zle_mono = thm "zmult_zle_mono";
val zmult_zless_mono2 = thm "zmult_zless_mono2";
val zmult_zless_mono1 = thm "zmult_zless_mono1";
-val zmult_zless_mono = thm "zmult_zless_mono";
val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
val zmult_eq_0_iff = thm "zmult_eq_0_iff";
--- a/src/HOL/IsaMakefile Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/IsaMakefile Thu Nov 27 10:47:55 2003 +0100
@@ -147,8 +147,8 @@
Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
Real/RealInt.thy Real/RealOrd.thy \
Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
- Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
- Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
+ Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
+ Hyperreal/Fact.ML Hyperreal/Fact.thy\
Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
--- a/src/HOL/Real/RComplete.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Real/RComplete.ML Thu Nov 27 10:47:55 2003 +0100
@@ -238,10 +238,16 @@
by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1);
by (forw_inst_tac [("y","inverse x")] real_mult_less_mono1 1);
by Auto_tac;
-by (dres_inst_tac [("y","1"),("z","real (Suc n)")]
- (rotate_prems 1 real_mult_less_mono2) 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_of_nat_Suc_gt_zero,
- real_not_refl2 RS not_sym,
- real_mult_assoc RS sym]));
+by (rtac (thm "less_imp_inverse_less") 1);
+by (assume_tac 1);
+by (assume_tac 1);
qed "reals_Archimedean2";
+
+Goal "0 < x ==> ALL y. EX (n::nat). y < real n * x";
+by (Step_tac 1);
+by (cut_inst_tac [("x","y*inverse(x)")] reals_Archimedean2 1);
+by (Step_tac 1);
+by (forw_inst_tac [("x","y * inverse x")] (real_mult_less_mono1) 1);
+by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,real_of_nat_def]));
+qed "reals_Archimedean3";
+
--- a/src/HOL/Real/RealArith0.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Real/RealArith0.ML Thu Nov 27 10:47:55 2003 +0100
@@ -79,8 +79,6 @@
Goal "(inverse(x::real) = 0) = (x = 0)";
by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO]));
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [real_inverse_not_zero]) 1);
qed "real_inverse_zero_iff";
Addsimps [real_inverse_zero_iff];
@@ -480,14 +478,8 @@
real_eq_divide_eq, real_mult_eq_cancel1]));
qed "real_divide_eq_cancel1";
-(*Moved from RealOrd.ML to use 0 *)
Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
-by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
-by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
-by (auto_tac (claset() addIs [real_inverse_less_swap],
- simpset() delsimps [real_inverse_inverse]
- addsimps [real_inverse_gt_0]));
qed "real_inverse_less_iff";
Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
--- a/src/HOL/Real/RealDef.ML Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Real/RealDef.ML Thu Nov 27 10:47:55 2003 +0100
@@ -497,7 +497,7 @@
Goal "a / (0::real) = 0";
by (simp_tac (simpset() addsimps [real_divide_def, INVERSE_ZERO]) 1);
-qed "DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)
+qed "DIVISION_BY_ZERO";
fun real_div_undefined_case_tac s i =
case_tac s i THEN
--- a/src/HOL/Real/RealOrd.thy Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Thu Nov 27 10:47:55 2003 +0100
@@ -113,46 +113,12 @@
lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
by (blast intro!: real_less_all_preal real_leI)
-lemma real_lemma_add_positive_imp_less: "[| R + L = S; (0::real) < L |] ==> R < S"
-apply (rule real_less_sum_gt_0_iff [THEN iffD1])
-apply (auto simp add: real_add_ac)
-done
-
-lemma real_ex_add_positive_left_less: "\<exists>T::real. 0 < T & R + T = S ==> R < S"
-by (blast intro: real_lemma_add_positive_imp_less)
-
-(*Alternative definition for real_less. NOT for rewriting*)
-lemma real_less_iff_add: "(R < S) = (\<exists>T::real. 0 < T & R + T = S)"
-by (blast intro!: real_less_add_positive_left_Ex real_ex_add_positive_left_less)
-
lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
apply (drule order_le_less_trans, assumption)
apply (erule preal_less_irrefl)
done
-lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
-apply (auto simp add: real_gt_zero_preal_Ex)
-apply (rule_tac x = "y*ya" in exI)
-apply (simp (no_asm_use) add: real_of_preal_mult)
-done
-
-lemma neg_real_mult_order: "[| x < 0; y < 0 |] ==> (0::real) < x * y"
-apply (drule real_minus_zero_less_iff [THEN iffD2])+
-apply (drule real_mult_order, assumption, simp)
-done
-
-lemma real_mult_less_0: "[| 0 < x; y < 0 |] ==> x*y < (0::real)"
-apply (drule real_minus_zero_less_iff [THEN iffD2])
-apply (drule real_mult_order, assumption)
-apply (rule real_minus_zero_less_iff [THEN iffD1], simp)
-done
-
-lemma real_zero_less_one: "0 < (1::real)"
-by (auto intro: real_gt_zero_preal_Ex [THEN iffD2]
- simp add: real_one_def real_of_preal_def)
-
-
subsection{*Monotonicity of Addition*}
lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
@@ -167,97 +133,17 @@
lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
by simp
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
-
-lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
-by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
-
-lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
-
-lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
-by simp
-
-lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
-apply (simp (no_asm_use))
-done
-
-lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
-apply (simp (no_asm_use))
-done
-
-lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
-apply (simp (no_asm_use))
-done
-
-lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
-apply (simp (no_asm_use))
-done
-
-lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
-apply (erule order_less_trans)
-apply (drule real_add_less_mono2)
-apply (simp (no_asm_use))
-done
-
-lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
-apply (drule order_le_imp_less_or_eq)+
-apply (auto intro: real_add_order order_less_imp_le)
-done
-
-lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)"
-apply (drule real_add_less_mono1)
-apply (erule order_less_trans)
-apply (erule real_add_less_mono2)
-done
-
-lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
-by simp
-
-lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
-apply (drule real_add_le_mono1)
-apply (erule order_trans, simp)
-done
-
-lemma real_less_Ex: "\<exists>(x::real). x < y"
-apply (rule real_add_zero_right [THEN subst])
-apply (rule_tac x = "y + (- (1::real))" in exI)
-apply (auto intro!: real_add_less_mono2 simp add: real_minus_zero_less_iff2 real_zero_less_one)
-done
-
-lemma real_add_minus_positive_less_self: "(0::real) < r ==> u + (-r) < u"
-apply (rule_tac C = r in real_less_add_right_cancel)
-apply (simp add: real_add_assoc)
-done
-
-lemma real_le_minus_iff [simp]: "(-s \<le> -r) = ((r::real) \<le> s)"
-apply (rule sym, safe)
-apply (drule_tac x = "-s" in real_add_left_le_mono1)
-apply (drule_tac [2] x = r in real_add_left_le_mono1, auto)
-apply (drule_tac z = "-r" in real_add_le_mono1)
-apply (drule_tac [2] z = s in real_add_le_mono1)
-apply (auto simp add: real_add_assoc)
-done
-
-lemma real_le_square [simp]: "(0::real) \<le> x*x"
-apply (rule_tac real_linear_less2 [of x 0])
-apply (auto intro: real_mult_order neg_real_mult_order order_less_imp_le)
-done
-
-lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
-apply (rotate_tac 1)
-apply (drule real_less_sum_gt_zero)
-apply (rule real_sum_gt_zero_less)
-apply (drule real_mult_order, assumption)
-apply (simp add: real_add_mult_distrib2 real_mult_commute)
+lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
+apply (auto simp add: real_gt_zero_preal_Ex)
+apply (rule_tac x = "y*ya" in exI)
+apply (simp (no_asm_use) add: real_of_preal_mult)
done
lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
-apply (simp (no_asm_simp) add: real_mult_commute real_mult_less_mono1)
+apply (rule real_sum_gt_zero_less)
+apply (drule real_less_sum_gt_zero [of x y])
+apply (drule real_mult_order, assumption)
+apply (simp add: real_add_mult_distrib2)
done
@@ -286,11 +172,57 @@
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
qed
+(*"v\<le>w ==> v+z \<le> w+z"*)
+lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
+
+(*"v\<le>w ==> v+z \<le> w+z"*)
+lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
+
+lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
+by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
+
+lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
+by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
+
+lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
+by simp
+
+lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
+apply simp
+done
+
+lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
+apply simp
+done
+
+lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
+apply simp
+done
+
+lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
+apply simp
+done
+
+lemma real_zero_less_one: "0 < (1::real)"
+ by (rule Ring_and_Field.zero_less_one)
+
+lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)"
+ by (rule Ring_and_Field.add_strict_mono)
+
+lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
+by simp
+
+lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
+ by (rule Ring_and_Field.add_mono)
+
+lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
+ by (rule Ring_and_Field.neg_le_iff_le)
+
+lemma real_le_square [simp]: "(0::real) \<le> x*x"
+ by (rule Ring_and_Field.zero_le_square)
-(*----------------------------------------------------------------------------
- An embedding of the naturals in the reals
- ----------------------------------------------------------------------------*)
+subsection{*An Embedding of the Naturals in the Reals*}
lemma real_of_posnat_one: "real_of_posnat 0 = (1::real)"
by (simp add: real_of_posnat_def pnat_one_iff [symmetric]
@@ -387,32 +319,25 @@
qed
lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
-apply (simp (no_asm_simp) add: neg_nat real_of_nat_zero)
+apply (simp add: neg_nat real_of_nat_zero)
done
-(*----------------------------------------------------------------------------
- inverse, etc.
- ----------------------------------------------------------------------------*)
+subsection{*Inverse and Division*}
+
+instance real :: division_by_zero
+proof
+ fix x :: real
+ show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
+ show "x/0 = 0" by (rule DIVISION_BY_ZERO)
+qed
+
lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
-apply (rule ccontr)
-apply (drule real_leI)
-apply (frule real_minus_zero_less_iff2 [THEN iffD2])
-apply (frule real_not_refl2 [THEN not_sym])
-apply (drule real_not_refl2 [THEN not_sym, THEN real_inverse_not_zero])
-apply (drule order_le_imp_less_or_eq, safe)
-apply (drule neg_real_mult_order, assumption)
-apply (auto intro: real_zero_less_one [THEN real_less_asym])
-done
+ by (rule Ring_and_Field.inverse_gt_0)
lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
-apply (frule real_not_refl2)
-apply (drule real_minus_zero_less_iff [THEN iffD2])
-apply (rule real_minus_zero_less_iff [THEN iffD1])
-apply (subst real_minus_inverse [symmetric])
-apply (auto intro: real_inverse_gt_0)
-done
+ by (rule Ring_and_Field.inverse_less_0)
lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
by (force simp add: Ring_and_Field.mult_less_cancel_right
@@ -423,6 +348,13 @@
apply (simp add: real_mult_commute)
done
+lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
+ by (rule Ring_and_Field.mult_strict_right_mono)
+
+lemma real_mult_less_mono:
+ "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y"
+ by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
+
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
@@ -430,22 +362,12 @@
by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
(* 05/00 *)
-lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x \<le> y)"
-by (auto simp add: real_le_def)
-
-lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x \<le> y)"
+lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
by (auto simp add: real_le_def)
-lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
-apply (rule real_less_or_eq_imp_le)
-apply (drule order_le_imp_less_or_eq)
-apply (auto intro: real_mult_less_mono1)
-done
+lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
+by (auto simp add: real_le_def)
-lemma real_mult_less_mono: "[| u<v; x<y; (0::real) < v; 0 < x |] ==> u*x < v* y"
- by (rule Ring_and_Field.mult_strict_mono)
-
-text{*Variant of the theorem above; sometimes it's stronger*}
lemma real_mult_less_mono':
"[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
apply (subgoal_tac "0<r2")
@@ -455,28 +377,9 @@
intro: real_mult_less_mono real_mult_order)
done
-lemma real_mult_self_le: "[| (1::real) < r; (1::real) \<le> x |] ==> x \<le> r * x"
-apply (subgoal_tac "0\<le>x")
-apply (force dest!: real_mult_le_less_mono1)
-apply (force intro: order_trans [OF zero_less_one [THEN order_less_imp_le]])
-done
-
-lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
-apply (drule order_le_imp_less_or_eq)
-apply (auto intro: real_mult_self_le)
-done
-
-lemma real_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
-apply (frule order_less_trans, assumption)
-apply (frule real_inverse_gt_0)
-apply (frule_tac x = x in real_inverse_gt_0)
-apply (frule_tac x = r and z = "inverse r" in real_mult_less_mono1, assumption)
-apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_right])
-apply (frule real_inverse_gt_0)
-apply (frule_tac x = " (1::real) " and z = "inverse x" in real_mult_less_mono2)
-apply assumption
-apply (simp add: real_not_refl2 [THEN not_sym, THEN real_mult_inv_left] real_mult_assoc [symmetric])
-done
+lemma real_inverse_less_swap:
+ "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
+ by (rule Ring_and_Field.less_imp_inverse_less)
lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
by auto
@@ -489,13 +392,6 @@
apply (simp add: real_add_commute)
done
-(* 05/00 *)
-lemma real_minus_zero_le_iff [simp]: "(0 \<le> -R) = (R \<le> (0::real))"
-by (auto dest: sym simp add: real_le_less)
-
-lemma real_minus_zero_le_iff2 [simp]: "(-R \<le> 0) = ((0::real) \<le> R)"
-by (auto simp add: real_minus_zero_less_iff2 real_le_less)
-
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
apply (drule real_add_minus_eq_minus)
apply (cut_tac x = x in real_le_square)
@@ -507,9 +403,8 @@
apply (simp add: real_add_commute)
done
-(*----------------------------------------------------------------------------
- Some convenient biconditionals for products of signs (lcp)
- ----------------------------------------------------------------------------*)
+
+subsection{*Convenient Biconditionals for Products of Signs*}
lemma real_0_less_mult_iff: "((0::real) < x*y) = (0<x & 0<y | x<0 & y<0)"
by (rule Ring_and_Field.zero_less_mult_iff)
@@ -523,6 +418,195 @@
lemma real_mult_le_0_iff: "(x*y \<le> (0::real)) = (0\<le>x & y\<le>0 | x\<le>0 & 0\<le>y)"
by (rule mult_le_0_iff)
+subsection{*Hardly Used Theorems to be Deleted*}
+
+lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
+apply (erule order_less_trans)
+apply (drule real_add_less_mono2)
+apply simp
+done
+
+lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
+apply (drule order_le_imp_less_or_eq)+
+apply (auto intro: real_add_order order_less_imp_le)
+done
+
+(*One use in HahnBanach/Aux.thy*)
+lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
+apply (rule real_less_or_eq_imp_le)
+apply (drule order_le_imp_less_or_eq)
+apply (auto intro: real_mult_less_mono1)
+done
+
+
+lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
+apply (unfold real_of_posnat_def)
+apply (rule real_gt_zero_preal_Ex [THEN iffD2])
+apply blast
+done
+
+declare real_of_posnat_gt_zero [simp]
+
+lemmas real_inv_real_of_posnat_gt_zero = real_of_posnat_gt_zero [THEN real_inverse_gt_0, standard]
+declare real_inv_real_of_posnat_gt_zero [simp]
+
+lemmas real_of_posnat_ge_zero = real_of_posnat_gt_zero [THEN order_less_imp_le, standard]
+declare real_of_posnat_ge_zero [simp]
+
+lemma real_of_posnat_not_eq_zero: "real_of_posnat n ~= 0"
+apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
+done
+declare real_of_posnat_not_eq_zero [simp]
+
+declare real_of_posnat_not_eq_zero [THEN real_mult_inv_left, simp]
+declare real_of_posnat_not_eq_zero [THEN real_mult_inv_right, simp]
+
+lemma real_of_posnat_ge_one: "1 <= real_of_posnat n"
+apply (simp (no_asm) add: real_of_posnat_one [symmetric])
+apply (induct_tac "n")
+apply (auto simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le)
+done
+declare real_of_posnat_ge_one [simp]
+
+lemma real_of_posnat_real_inv_not_zero: "inverse(real_of_posnat n) ~= 0"
+apply (rule real_inverse_not_zero)
+apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
+done
+declare real_of_posnat_real_inv_not_zero [simp]
+
+lemma real_of_posnat_real_inv_inj: "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y"
+apply (rule inj_real_of_posnat [THEN injD])
+apply (rule real_of_posnat_real_inv_not_zero
+ [THEN real_mult_left_cancel, THEN iffD1, of x])
+apply (simp add: real_mult_inv_left
+ real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
+done
+
+lemma real_mult_less_self: "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r"
+apply (simp (no_asm) add: real_add_mult_distrib2)
+apply (rule_tac C = "-r" in real_less_add_left_cancel)
+apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2)
+done
+
+lemma real_of_posnat_inv_Ex_iff: "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)"
+apply safe
+apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
+apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1])
+apply (auto simp add: real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_assoc)
+done
+
+lemma real_of_posnat_inv_iff: "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)"
+apply safe
+apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
+apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1])
+apply (auto simp add: real_mult_assoc)
+done
+
+lemma real_mult_le_le_mono1: "[| (0::real) <=z; x<=y |] ==> z*x<=z*y"
+ by (rule Ring_and_Field.mult_left_mono)
+
+lemma real_mult_le_le_mono2: "[| (0::real)<=z; x<=y |] ==> x*z<=y*z"
+ by (rule Ring_and_Field.mult_right_mono)
+
+lemma real_of_posnat_inv_le_iff: "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)"
+apply safe
+apply (drule_tac n2=n in real_of_posnat_gt_zero [THEN order_less_imp_le, THEN real_mult_le_le_mono1])
+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])
+apply (auto simp add: real_mult_ac)
+done
+
+lemma real_of_posnat_less_iff:
+ "(real_of_posnat n < real_of_posnat m) = (n < m)"
+apply (unfold real_of_posnat_def)
+apply auto
+done
+declare real_of_posnat_less_iff [simp]
+
+lemma real_of_posnat_le_iff: "(real_of_posnat n <= real_of_posnat m) = (n <= m)"
+apply (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq)
+done
+declare real_of_posnat_le_iff [simp]
+
+lemma real_mult_less_cancel3: "[| (0::real)<z; x*z<y*z |] ==> x<y"
+apply auto
+done
+
+lemma real_mult_less_cancel4: "[| (0::real)<z; z*x<z*y |] ==> x<y"
+apply auto
+done
+
+lemma real_of_posnat_less_inv_iff: "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))"
+apply safe
+apply (rule_tac n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_cancel3])
+apply (rule_tac [2] x1 = "u" in real_inverse_gt_0 [THEN real_mult_less_cancel3])
+apply (auto simp add: real_not_refl2 [THEN not_sym])
+apply (rule_tac z = "u" in real_mult_less_cancel4)
+apply (rule_tac [3] n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_cancel4])
+apply (auto simp add: real_not_refl2 [THEN not_sym] real_mult_assoc [symmetric])
+done
+
+lemma real_of_posnat_inv_eq_iff: "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)"
+apply auto
+done
+
+lemma real_add_one_minus_inv_ge_zero: "0 <= 1 + -inverse(real_of_posnat n)"
+apply (rule_tac C = "inverse (real_of_posnat n) " in real_le_add_right_cancel)
+apply (simp (no_asm) add: real_add_assoc real_of_posnat_inv_le_iff)
+done
+
+lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))"
+apply (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1])
+apply auto
+done
+
+lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
+apply (case_tac "x ~= 0")
+apply (rule_tac c1 = "x" in real_mult_left_cancel [THEN iffD1])
+apply auto
+done
+
+lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
+apply (auto dest: real_inverse_less_swap)
+done
+
+lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)"
+apply (rule real_of_nat_less_iff [THEN subst])
+apply auto
+done
+declare real_of_nat_gt_zero_cancel_iff [simp]
+
+lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)"
+apply (rule real_of_nat_zero [THEN subst])
+apply (subst real_of_nat_le_iff)
+apply auto
+done
+declare real_of_nat_le_zero_cancel_iff [simp]
+
+lemma not_real_of_nat_less_zero: "~ real (n::nat) < 0"
+apply (simp (no_asm) add: real_le_def [symmetric] real_of_nat_ge_zero)
+done
+declare not_real_of_nat_less_zero [simp]
+
+lemma real_of_nat_ge_zero_cancel_iff:
+ "(0 <= real (n::nat)) = (0 <= n)"
+apply (unfold real_le_def le_def)
+apply (simp (no_asm))
+done
+declare real_of_nat_ge_zero_cancel_iff [simp]
+
+lemma real_of_nat_num_if: "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))"
+apply (case_tac "n")
+apply (auto simp add: real_of_nat_Suc)
+done
+
+(*RING AND FIELD*)
+ lemma mult_less_imp_less_left:
+ "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
+ by (force elim: order_less_asym simp add: mult_less_cancel_left)
+
+ lemma mult_less_imp_less_right:
+ "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
+ by (force elim: order_less_asym simp add: mult_less_cancel_right)
ML
{*
@@ -534,13 +618,8 @@
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
val real_less_all_preal = thm "real_less_all_preal";
val real_less_all_real2 = thm "real_less_all_real2";
-val real_lemma_add_positive_imp_less = thm "real_lemma_add_positive_imp_less";
-val real_ex_add_positive_left_less = thm "real_ex_add_positive_left_less";
-val real_less_iff_add = thm "real_less_iff_add";
val real_of_preal_le_iff = thm "real_of_preal_le_iff";
val real_mult_order = thm "real_mult_order";
-val neg_real_mult_order = thm "neg_real_mult_order";
-val real_mult_less_0 = thm "real_mult_less_0";
val real_zero_less_one = thm "real_zero_less_one";
val real_add_right_cancel_less = thm "real_add_right_cancel_less";
val real_add_left_cancel_less = thm "real_add_left_cancel_less";
@@ -560,8 +639,6 @@
val real_add_less_mono = thm "real_add_less_mono";
val real_add_left_le_mono1 = thm "real_add_left_le_mono1";
val real_add_le_mono = thm "real_add_le_mono";
-val real_less_Ex = thm "real_less_Ex";
-val real_add_minus_positive_less_self = thm "real_add_minus_positive_less_self";
val real_le_minus_iff = thm "real_le_minus_iff";
val real_le_square = thm "real_le_square";
val real_mult_less_mono1 = thm "real_mult_less_mono1";
@@ -593,22 +670,46 @@
val real_mult_less_iff2 = thm "real_mult_less_iff2";
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
-val real_mult_le_less_mono1 = thm "real_mult_le_less_mono1";
val real_mult_less_mono = thm "real_mult_less_mono";
val real_mult_less_mono' = thm "real_mult_less_mono'";
-val real_mult_self_le = thm "real_mult_self_le";
-val real_mult_self_le2 = thm "real_mult_self_le2";
val real_inverse_less_swap = thm "real_inverse_less_swap";
val real_mult_is_0 = thm "real_mult_is_0";
val real_inverse_add = thm "real_inverse_add";
-val real_minus_zero_le_iff = thm "real_minus_zero_le_iff";
-val real_minus_zero_le_iff2 = thm "real_minus_zero_le_iff2";
val real_sum_squares_cancel = thm "real_sum_squares_cancel";
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
val real_0_less_mult_iff = thm "real_0_less_mult_iff";
val real_0_le_mult_iff = thm "real_0_le_mult_iff";
val real_mult_less_0_iff = thm "real_mult_less_0_iff";
val real_mult_le_0_iff = thm "real_mult_le_0_iff";
+
+val real_of_posnat_gt_zero = thm "real_of_posnat_gt_zero";
+val real_inv_real_of_posnat_gt_zero = thm "real_inv_real_of_posnat_gt_zero";
+val real_of_posnat_ge_zero = thm "real_of_posnat_ge_zero";
+val real_of_posnat_not_eq_zero = thm "real_of_posnat_not_eq_zero";
+val real_of_posnat_ge_one = thm "real_of_posnat_ge_one";
+val real_of_posnat_real_inv_not_zero = thm "real_of_posnat_real_inv_not_zero";
+val real_of_posnat_real_inv_inj = thm "real_of_posnat_real_inv_inj";
+val real_mult_less_self = thm "real_mult_less_self";
+val real_of_posnat_inv_Ex_iff = thm "real_of_posnat_inv_Ex_iff";
+val real_of_posnat_inv_iff = thm "real_of_posnat_inv_iff";
+val real_mult_le_le_mono1 = thm "real_mult_le_le_mono1";
+val real_mult_le_le_mono2 = thm "real_mult_le_le_mono2";
+val real_of_posnat_inv_le_iff = thm "real_of_posnat_inv_le_iff";
+val real_of_posnat_less_iff = thm "real_of_posnat_less_iff";
+val real_of_posnat_le_iff = thm "real_of_posnat_le_iff";
+val real_mult_less_cancel3 = thm "real_mult_less_cancel3";
+val real_mult_less_cancel4 = thm "real_mult_less_cancel4";
+val real_of_posnat_less_inv_iff = thm "real_of_posnat_less_inv_iff";
+val real_of_posnat_inv_eq_iff = thm "real_of_posnat_inv_eq_iff";
+val real_add_one_minus_inv_ge_zero = thm "real_add_one_minus_inv_ge_zero";
+val real_mult_add_one_minus_ge_zero = thm "real_mult_add_one_minus_ge_zero";
+val real_inverse_unique = thm "real_inverse_unique";
+val real_inverse_gt_one = thm "real_inverse_gt_one";
+val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
+val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
+val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
+val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
+val real_of_nat_num_if = thm "real_of_nat_num_if";
*}
end
--- a/src/HOL/Real/RealPow.thy Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Real/RealPow.thy Thu Nov 27 10:47:55 2003 +0100
@@ -18,18 +18,11 @@
realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
-(*FIXME: most of the theorems for Suc (Suc 0) are redundant!
-*)
+lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0"
+by auto
-lemma realpow_zero: "(0::real) ^ (Suc n) = 0"
-apply auto
-done
-declare realpow_zero [simp]
-
-lemma realpow_not_zero [rule_format (no_asm)]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
-apply (induct_tac "n")
-apply auto
-done
+lemma realpow_not_zero [rule_format]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
+by (induct_tac "n", auto)
lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
apply (rule ccontr)
@@ -51,26 +44,23 @@
apply (auto simp add: real_mult_ac)
done
-lemma realpow_one: "(r::real) ^ 1 = r"
-apply (simp (no_asm))
-done
-declare realpow_one [simp]
+lemma realpow_one [simp]: "(r::real) ^ 1 = r"
+by simp
lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
-apply (simp (no_asm))
-done
+by simp
-lemma realpow_gt_zero [rule_format (no_asm)]: "(0::real) < r --> 0 < r ^ n"
+lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
apply (induct_tac "n")
apply (auto intro: real_mult_order simp add: real_zero_less_one)
done
-lemma realpow_ge_zero [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
+lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
apply (induct_tac "n")
apply (auto simp add: real_0_le_mult_iff)
done
-lemma realpow_le [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
+lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
apply (induct_tac "n")
apply (auto intro!: real_mult_le_mono)
apply (simp (no_asm_simp) add: realpow_ge_zero)
@@ -78,70 +68,55 @@
lemma realpow_0_left [rule_format, simp]:
"0 < n --> 0 ^ n = (0::real)"
-apply (induct_tac "n")
-apply (auto );
+apply (induct_tac "n", auto)
done
lemma realpow_less' [rule_format]:
"[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
apply (induct n)
-apply (auto simp add: real_mult_less_mono' realpow_ge_zero);
+apply (auto simp add: real_mult_less_mono' realpow_ge_zero)
done
text{*Legacy: weaker version of the theorem above*}
-lemma realpow_less [rule_format]:
+lemma realpow_less:
"[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
-apply (rule realpow_less')
-apply (auto );
+apply (rule realpow_less', auto)
done
-lemma realpow_eq_one: "1 ^ n = (1::real)"
-apply (induct_tac "n")
-apply auto
-done
-declare realpow_eq_one [simp]
+lemma realpow_eq_one [simp]: "1 ^ n = (1::real)"
+by (induct_tac "n", auto)
-lemma abs_realpow_minus_one: "abs((-1) ^ n) = (1::real)"
+lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
apply (induct_tac "n")
apply (auto simp add: abs_mult)
done
-declare abs_realpow_minus_one [simp]
lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
apply (induct_tac "n")
apply (auto simp add: real_mult_ac)
done
-lemma realpow_two_le: "(0::real) \<le> r^ Suc (Suc 0)"
-apply (simp (no_asm) add: real_le_square)
-done
-declare realpow_two_le [simp]
+lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
+by (simp add: real_le_square)
-lemma abs_realpow_two: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
-apply (simp (no_asm) add: abs_eqI1 real_le_square)
-done
-declare abs_realpow_two [simp]
+lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
+by (simp add: abs_eqI1 real_le_square)
-lemma realpow_two_abs: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
-apply (simp (no_asm) add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
-done
-declare realpow_two_abs [simp]
+lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
+by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
apply auto
apply (cut_tac real_zero_less_one)
-apply (frule_tac x = "0" in order_less_trans)
-apply assumption
-apply (drule_tac z = "r" and x = "1" in real_mult_less_mono1)
+apply (frule_tac x = 0 in order_less_trans, assumption)
+apply (drule_tac z = r and x = 1 in real_mult_less_mono1)
apply (auto intro: order_less_trans)
done
-lemma realpow_ge_one [rule_format (no_asm)]: "(1::real) < r --> 1 \<le> r ^ n"
-apply (induct_tac "n")
-apply auto
+lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
+apply (induct_tac "n", auto)
apply (subgoal_tac "1*1 \<le> r * r^n")
-apply (rule_tac [2] real_mult_le_mono)
-apply auto
+apply (rule_tac [2] real_mult_le_mono, auto)
done
lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
@@ -149,167 +124,118 @@
apply (auto dest: realpow_ge_one)
done
-lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
+lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
apply (rule_tac y = "1 ^ n" in order_trans)
apply (rule_tac [2] realpow_le)
apply (auto intro: order_less_imp_le)
done
-lemma two_realpow_gt: "real (n::nat) < 2 ^ n"
+lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
apply (induct_tac "n")
apply (auto simp add: real_of_nat_Suc)
apply (subst real_mult_2)
apply (rule real_add_less_le_mono)
apply (auto simp add: two_realpow_ge_one)
done
-declare two_realpow_gt [simp] two_realpow_ge_one [simp]
-lemma realpow_minus_one: "(-1) ^ (2*n) = (1::real)"
-apply (induct_tac "n")
-apply auto
-done
-declare realpow_minus_one [simp]
+lemma realpow_minus_one [simp]: "(-1) ^ (2*n) = (1::real)"
+by (induct_tac "n", auto)
+
+lemma realpow_minus_one_odd [simp]: "(-1) ^ Suc (2*n) = -(1::real)"
+by auto
-lemma realpow_minus_one_odd: "(-1) ^ Suc (2*n) = -(1::real)"
-apply auto
-done
-declare realpow_minus_one_odd [simp]
+lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
+by auto
-lemma realpow_minus_one_even: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
-apply auto
-done
-declare realpow_minus_one_even [simp]
+lemma realpow_Suc_less [rule_format]:
+ "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
+ by (induct_tac "n", auto)
-lemma realpow_Suc_less [rule_format (no_asm)]: "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
-apply (induct_tac "n")
-apply auto
-done
-
-lemma realpow_Suc_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
+lemma realpow_Suc_le [rule_format]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
apply (induct_tac "n")
apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
done
-lemma realpow_zero_le: "(0::real) \<le> 0 ^ n"
-apply (case_tac "n")
-apply auto
-done
-declare realpow_zero_le [simp]
+lemma realpow_zero_le [simp]: "(0::real) \<le> 0 ^ n"
+by (case_tac "n", auto)
-lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
-apply (blast intro!: order_less_imp_le realpow_Suc_less)
-done
+lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
+by (blast intro!: order_less_imp_le realpow_Suc_less)
lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
apply (erule order_le_imp_less_or_eq [THEN disjE])
-apply (rule realpow_Suc_le2)
-apply auto
+apply (rule realpow_Suc_le2, auto)
done
-lemma realpow_less_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
+lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
apply (induct_tac "N")
apply (simp_all (no_asm_simp))
apply clarify
-apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n")
-apply simp
+apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
apply (rule real_mult_le_mono)
apply (auto simp add: realpow_ge_zero less_Suc_eq)
done
lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
-apply (drule_tac n = "N" in le_imp_less_or_eq)
+apply (drule_tac n = N in le_imp_less_or_eq)
apply (auto intro: realpow_less_le)
done
lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
-apply (drule_tac n = "1" and N = "Suc n" in order_less_imp_le [THEN realpow_le_le])
-apply auto
-done
+by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto)
lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
-apply (blast intro: realpow_Suc_le_self order_le_less_trans)
-done
+by (blast intro: realpow_Suc_le_self order_le_less_trans)
+
+lemma realpow_le_Suc [rule_format]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
+by (induct_tac "n", auto)
+
+lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
+by (induct_tac "n", auto)
-lemma realpow_le_Suc [rule_format (no_asm)]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
-apply (induct_tac "n")
-apply auto
+lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
+by (blast intro!: order_less_imp_le realpow_less_Suc)
+
+(*One use in RealPow.thy*)
+lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
+apply (subgoal_tac "1 * x \<le> r * x", simp)
+apply (rule mult_right_mono, auto)
done
-lemma realpow_less_Suc [rule_format (no_asm)]: "(1::real) < r --> r ^ n < r ^ Suc n"
-apply (induct_tac "n")
-apply auto
-done
-
-lemma realpow_le_Suc2 [rule_format (no_asm)]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
-apply (blast intro!: order_less_imp_le realpow_less_Suc)
-done
-
-lemma realpow_gt_ge [rule_format (no_asm)]: "(1::real) < r & n < N --> r ^ n \<le> r ^ N"
-apply (induct_tac "N")
-apply auto
-apply (frule_tac [!] n = "na" in realpow_ge_one)
-apply (drule_tac [!] real_mult_self_le)
-apply assumption
-prefer 2 apply (assumption)
+lemma realpow_gt_ge2 [rule_format]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
+apply (induct_tac "N", auto)
+apply (frule_tac [!] n = na in realpow_ge_one2)
+apply (drule_tac [!] real_mult_self_le2, assumption)
+prefer 2 apply assumption
apply (auto intro: order_trans simp add: less_Suc_eq)
done
-lemma realpow_gt_ge2 [rule_format (no_asm)]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
-apply (induct_tac "N")
-apply auto
-apply (frule_tac [!] n = "na" in realpow_ge_one2)
-apply (drule_tac [!] real_mult_self_le2)
-apply assumption
-prefer 2 apply (assumption)
-apply (auto intro: order_trans simp add: less_Suc_eq)
-done
-
-lemma realpow_ge_ge: "[| (1::real) < r; n \<le> N |] ==> r ^ n \<le> r ^ N"
-apply (drule_tac n = "N" in le_imp_less_or_eq)
-apply (auto intro: realpow_gt_ge)
-done
-
lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
-apply (drule_tac n = "N" in le_imp_less_or_eq)
+apply (drule_tac n = N in le_imp_less_or_eq)
apply (auto intro: realpow_gt_ge2)
done
-lemma realpow_Suc_ge_self [rule_format (no_asm)]: "(1::real) < r ==> r \<le> r ^ Suc n"
-apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge)
-apply auto
-done
+lemma realpow_Suc_ge_self2: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
+by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto)
-lemma realpow_Suc_ge_self2 [rule_format (no_asm)]: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
-apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge2)
-apply auto
-done
-
-lemma realpow_ge_self: "[| (1::real) < r; 0 < n |] ==> r \<le> r ^ n"
-apply (drule less_not_refl2 [THEN not0_implies_Suc])
-apply (auto intro!: realpow_Suc_ge_self)
-done
-
+(*Used ONCE in Hyperreal/NthRoot.ML*)
lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
apply (drule less_not_refl2 [THEN not0_implies_Suc])
apply (auto intro!: realpow_Suc_ge_self2)
done
-lemma realpow_minus_mult [rule_format (no_asm)]: "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+lemma realpow_minus_mult [rule_format, simp]:
+ "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
apply (induct_tac "n")
apply (auto simp add: real_mult_commute)
done
-declare realpow_minus_mult [simp]
-lemma realpow_two_mult_inverse: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
-apply (simp (no_asm_simp) add: realpow_two real_mult_assoc [symmetric])
-done
-declare realpow_two_mult_inverse [simp]
+lemma realpow_two_mult_inverse [simp]: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
+by (simp add: realpow_two real_mult_assoc [symmetric])
(* 05/00 *)
-lemma realpow_two_minus: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
-apply (simp (no_asm))
-done
-declare realpow_two_minus [simp]
+lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
+by simp
lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
apply (unfold real_diff_def)
@@ -317,25 +243,23 @@
done
lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-apply (cut_tac x = "x" and y = "y" in realpow_two_diff)
+apply (cut_tac x = x and y = y in realpow_two_diff)
apply (auto simp del: realpow_Suc)
done
(* used in Transc *)
lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
-apply (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
-done
+by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
apply (induct_tac "n")
apply (auto simp add: real_of_nat_one real_of_nat_mult)
done
-lemma realpow_real_of_nat_two_pos: "0 < real (Suc (Suc 0) ^ n)"
+lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
apply (induct_tac "n")
apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
done
-declare realpow_real_of_nat_two_pos [simp]
lemma realpow_increasing:
assumes xnonneg: "(0::real) \<le> x"
@@ -352,29 +276,23 @@
qed
lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
-apply (blast intro: realpow_increasing order_antisym order_eq_refl sym)
-done
+by (blast intro: realpow_increasing order_antisym order_eq_refl sym)
(*** Logical equivalences for inequalities ***)
-lemma realpow_eq_0_iff: "(x^n = 0) = (x = (0::real) & 0<n)"
-apply (induct_tac "n")
-apply auto
-done
-declare realpow_eq_0_iff [simp]
+lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
+by (induct_tac "n", auto)
-lemma zero_less_realpow_abs_iff: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
+lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
apply (induct_tac "n")
apply (auto simp add: real_0_less_mult_iff)
done
-declare zero_less_realpow_abs_iff [simp]
-lemma zero_le_realpow_abs: "(0::real) \<le> (abs x)^n"
+lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
apply (induct_tac "n")
apply (auto simp add: real_0_le_mult_iff)
done
-declare zero_le_realpow_abs [simp]
(*** Literal arithmetic involving powers, type real ***)
@@ -386,8 +304,7 @@
declare real_of_int_power [symmetric, simp]
lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
-apply (simp only: real_number_of_def real_of_int_power)
-done
+by (simp only: real_number_of_def real_of_int_power)
declare power_real_number_of [of _ "number_of w", standard, simp]
@@ -410,6 +327,182 @@
by simp
+subsection{*Various Other Theorems*}
+
+text{*Used several times in Hyperreal/Transcendental.ML*}
+lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
+ by (auto intro: real_sum_squares_cancel)
+
+lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
+apply (auto simp add: real_add_mult_distrib real_add_mult_distrib2 real_diff_def)
+done
+
+lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
+apply auto
+apply (drule right_minus_eq [THEN iffD2])
+apply (auto simp add: real_squared_diff_one_factored)
+done
+declare real_mult_is_one [iff]
+
+lemma real_le_add_half_cancel: "(x + y/2 <= (y::real)) = (x <= y /2)"
+apply auto
+done
+declare real_le_add_half_cancel [simp]
+
+lemma real_minus_half_eq: "(x::real) - x/2 = x/2"
+apply auto
+done
+declare real_minus_half_eq [simp]
+
+lemma real_mult_inverse_cancel:
+ "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
+ ==> inverse x * y < inverse x1 * u"
+apply (rule_tac c=x in mult_less_imp_less_left)
+apply (auto simp add: real_mult_assoc [symmetric])
+apply (simp (no_asm) add: real_mult_ac)
+apply (rule_tac c=x1 in mult_less_imp_less_right)
+apply (auto simp add: real_mult_ac)
+done
+
+text{*Used once: in Hyperreal/Transcendental.ML*}
+lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
+apply (auto dest: real_mult_inverse_cancel simp add: real_mult_ac)
+done
+
+lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
+apply auto
+done
+declare inverse_real_of_nat_gt_zero [simp]
+
+lemma inverse_real_of_nat_ge_zero: "0 <= inverse (real (Suc n))"
+apply auto
+done
+declare inverse_real_of_nat_ge_zero [simp]
+
+lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
+apply (blast dest!: real_sum_squares_cancel)
+done
+
+lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
+apply (blast dest!: real_sum_squares_cancel2)
+done
+
+(* nice theorem *)
+lemma abs_mult_abs: "abs x * abs x = x * (x::real)"
+apply (insert linorder_less_linear [of x 0])
+apply (auto simp add: abs_eqI2 abs_minus_eqI2)
+done
+declare abs_mult_abs [simp]
+
+
+subsection {*Various Other Theorems*}
+
+lemma realpow_divide:
+ "(x/y) ^ n = ((x::real) ^ n/ y ^ n)"
+apply (unfold real_divide_def)
+apply (auto simp add: realpow_mult realpow_inverse)
+done
+
+lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) <= r --> 0 <= r ^ n"
+apply (induct_tac "n")
+apply (auto simp add: real_0_le_mult_iff)
+done
+
+lemma realpow_le2 [rule_format (no_asm)]: "(0::real) <= x & x <= y --> x ^ n <= y ^ n"
+apply (induct_tac "n")
+apply (auto intro!: real_mult_le_mono simp add: realpow_ge_zero2)
+done
+
+lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
+apply (frule_tac n = "n" in realpow_ge_one)
+apply (drule real_le_imp_less_or_eq, safe)
+apply (frule real_zero_less_one [THEN real_less_trans])
+apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
+apply assumption
+apply (auto dest: real_less_trans)
+done
+
+lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
+apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2)
+done
+declare realpow_two_sum_zero_iff [simp]
+
+lemma realpow_two_le_add_order: "(0::real) <= u ^ 2 + v ^ 2"
+apply (rule real_le_add_order)
+apply (auto simp add: numeral_2_eq_2)
+done
+declare realpow_two_le_add_order [simp]
+
+lemma realpow_two_le_add_order2: "(0::real) <= u ^ 2 + v ^ 2 + w ^ 2"
+apply (rule real_le_add_order)+
+apply (auto simp add: numeral_2_eq_2)
+done
+declare realpow_two_le_add_order2 [simp]
+
+lemma real_mult_self_sum_ge_zero: "(0::real) <= x*x + y*y"
+apply (cut_tac u = "x" and v = "y" in realpow_two_le_add_order)
+apply (auto simp add: numeral_2_eq_2)
+done
+declare real_mult_self_sum_ge_zero [simp]
+declare real_mult_self_sum_ge_zero [THEN abs_eqI1, simp]
+
+lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
+apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
+apply (drule real_le_imp_less_or_eq)
+apply (drule_tac y = "y" in real_sum_squares_not_zero)
+apply auto
+done
+
+lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
+apply (rule real_add_commute [THEN subst])
+apply (erule real_sum_square_gt_zero)
+done
+
+lemma real_minus_mult_self_le: "-(u * u) <= (x * (x::real))"
+apply (rule_tac j = "0" in real_le_trans)
+apply auto
+done
+declare real_minus_mult_self_le [simp]
+
+lemma realpow_square_minus_le: "-(u ^ 2) <= (x::real) ^ 2"
+apply (auto simp add: numeral_2_eq_2)
+done
+declare realpow_square_minus_le [simp]
+
+lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+apply (case_tac "n")
+apply auto
+done
+
+lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)"
+apply (induct_tac "d")
+apply (auto simp add: realpow_num_eq_if)
+done
+declare real_num_zero_less_two_pow [simp]
+
+lemma lemma_realpow_num_two_mono: "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
+apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
+apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
+apply (auto simp add: realpow_num_eq_if)
+done
+
+lemma lemma_realpow_4: "2 ^ 2 = (4::real)"
+apply (simp (no_asm) add: realpow_num_eq_if)
+done
+declare lemma_realpow_4 [simp]
+
+lemma lemma_realpow_16: "2 ^ 4 = (16::real)"
+apply (simp (no_asm) add: realpow_num_eq_if)
+done
+declare lemma_realpow_16 [simp]
+
+lemma zero_le_x_squared: "(0::real) <= x^2"
+apply (simp add: numeral_2_eq_2)
+done
+declare zero_le_x_squared [simp]
+
+
+
ML
{*
val realpow_0 = thm "realpow_0";
@@ -454,18 +547,13 @@
val realpow_le_Suc = thm "realpow_le_Suc";
val realpow_less_Suc = thm "realpow_less_Suc";
val realpow_le_Suc2 = thm "realpow_le_Suc2";
-val realpow_gt_ge = thm "realpow_gt_ge";
val realpow_gt_ge2 = thm "realpow_gt_ge2";
-val realpow_ge_ge = thm "realpow_ge_ge";
val realpow_ge_ge2 = thm "realpow_ge_ge2";
-val realpow_Suc_ge_self = thm "realpow_Suc_ge_self";
val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
-val realpow_ge_self = thm "realpow_ge_self";
val realpow_ge_self2 = thm "realpow_ge_self2";
val realpow_minus_mult = thm "realpow_minus_mult";
val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
val realpow_two_minus = thm "realpow_two_minus";
-val realpow_two_diff = thm "realpow_two_diff";
val realpow_two_disj = thm "realpow_two_disj";
val realpow_diff = thm "realpow_diff";
val realpow_real_of_nat = thm "realpow_real_of_nat";
@@ -481,6 +569,38 @@
val real_sqr_ge_zero = thm "real_sqr_ge_zero";
val real_sqr_gt_zero = thm "real_sqr_gt_zero";
val real_sqr_not_zero = thm "real_sqr_not_zero";
+val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
+val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
+val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
+val real_mult_is_one = thm "real_mult_is_one";
+val real_le_add_half_cancel = thm "real_le_add_half_cancel";
+val real_minus_half_eq = thm "real_minus_half_eq";
+val real_mult_inverse_cancel = thm "real_mult_inverse_cancel";
+val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
+val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero";
+val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
+val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
+val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
+val abs_mult_abs = thm "abs_mult_abs";
+
+val realpow_divide = thm "realpow_divide";
+val realpow_ge_zero2 = thm "realpow_ge_zero2";
+val realpow_le2 = thm "realpow_le2";
+val realpow_Suc_gt_one = thm "realpow_Suc_gt_one";
+val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
+val realpow_two_le_add_order = thm "realpow_two_le_add_order";
+val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
+val real_mult_self_sum_ge_zero = thm "real_mult_self_sum_ge_zero";
+val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
+val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
+val real_minus_mult_self_le = thm "real_minus_mult_self_le";
+val realpow_square_minus_le = thm "realpow_square_minus_le";
+val realpow_num_eq_if = thm "realpow_num_eq_if";
+val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
+val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
+val lemma_realpow_4 = thm "lemma_realpow_4";
+val lemma_realpow_16 = thm "lemma_realpow_16";
+val zero_le_x_squared = thm "zero_le_x_squared";
*}
--- a/src/HOL/Ring_and_Field.thy Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Thu Nov 27 10:47:55 2003 +0100
@@ -45,8 +45,8 @@
axclass ordered_field \<subseteq> ordered_ring, field
axclass division_by_zero \<subseteq> zero, inverse
- inverse_zero: "inverse 0 = 0"
- divide_zero: "a / 0 = 0"
+ inverse_zero [simp]: "inverse 0 = 0"
+ divide_zero [simp]: "a / 0 = 0"
subsection {* Derived rules for addition *}
@@ -87,7 +87,7 @@
"(a + b = a + c) = (b = (c::'a::ring))"
proof
assume eq: "a + b = a + c"
- then have "(-a + a) + b = (-a + a) + c"
+ hence "(-a + a) + b = (-a + a) + c"
by (simp only: eq add_assoc)
thus "b = c" by simp
next
@@ -116,7 +116,7 @@
lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
proof
assume "- a = - b"
- then have "- (- a) = - (- b)"
+ hence "- (- a) = - (- b)"
by simp
thus "a=b" by simp
next
@@ -145,7 +145,7 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
+lemma right_inverse [simp]: "a \<noteq> 0 ==> a * inverse (a::'a::field) = 1"
proof -
have "a * inverse a = inverse a * a" by (simp add: mult_ac)
also assume "a \<noteq> 0"
@@ -207,6 +207,9 @@
apply (simp add: right_distrib [symmetric])
done
+lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
+ by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+
lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
by (simp add: right_distrib diff_minus
minus_mult_left [symmetric] minus_mult_right [symmetric])
@@ -223,14 +226,28 @@
apply (simp add: add_commute add_left_mono)
done
+lemma add_strict_left_mono:
+ "a < b ==> c + a < c + (b::'a::ordered_ring)"
+ by (simp add: order_less_le add_left_mono)
+
+lemma add_strict_right_mono:
+ "a < b ==> a + c < b + (c::'a::ordered_ring)"
+ by (simp add: add_commute [of _ c] add_strict_left_mono)
+
+text{*Strict monotonicity in both arguments*}
+lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_ring)"
+apply (erule add_strict_right_mono [THEN order_less_trans])
+apply (erule add_strict_left_mono)
+done
+
lemma le_imp_neg_le:
assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
proof -
have "-a+a \<le> -a+b"
by (rule add_left_mono)
- then have "0 \<le> -a+b"
+ hence "0 \<le> -a+b"
by simp
- then have "0 + (-b) \<le> (-a + b) + (-b)"
+ hence "0 + (-b) \<le> (-a + b) + (-b)"
by (rule add_right_mono)
thus ?thesis
by (simp add: add_assoc)
@@ -239,7 +256,7 @@
lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
proof
assume "- b \<le> - a"
- then have "- (- a) \<le> - (- b)"
+ hence "- (- a) \<le> - (- b)"
by (rule le_imp_neg_le)
thus "a\<le>b" by simp
next
@@ -288,73 +305,6 @@
apply (simp_all add: minus_mult_right [symmetric])
done
-lemma mult_left_mono_neg:
- "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
-apply (drule mult_left_mono [of _ _ "-c"])
-apply (simp_all add: minus_mult_left [symmetric])
-done
-
-lemma mult_right_mono_neg:
- "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
- by (simp add: mult_left_mono_neg mult_commute [of _ c])
-
-text{*Strict monotonicity in both arguments*}
-lemma mult_strict_mono:
- "[|a<b; c<d; 0<b; 0<c|] ==> a * c < b * (d::'a::ordered_semiring)"
-apply (erule mult_strict_right_mono [THEN order_less_trans], assumption)
-apply (erule mult_strict_left_mono, assumption)
-done
-
-lemma mult_mono:
- "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]
- ==> a * c \<le> b * (d::'a::ordered_ring)"
-apply (erule mult_right_mono [THEN order_trans], assumption)
-apply (erule mult_left_mono, assumption)
-done
-
-
-subsection{*Cancellation Laws for Relationships With a Common Factor*}
-
-text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
- also with the relations @{text "\<le>"} and equality.*}
-
-lemma mult_less_cancel_right:
- "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
-apply (case_tac "c = 0")
-apply (auto simp add: linorder_neq_iff mult_strict_right_mono
- mult_strict_right_mono_neg)
-apply (auto simp add: linorder_not_less
- linorder_not_le [symmetric, of "a*c"]
- linorder_not_le [symmetric, of a])
-apply (erule_tac [!] notE)
-apply (auto simp add: order_less_imp_le mult_right_mono
- mult_right_mono_neg)
-done
-
-lemma mult_less_cancel_left:
- "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
-by (simp add: mult_commute [of c] mult_less_cancel_right)
-
-lemma mult_le_cancel_right:
- "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
-by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
-
-lemma mult_le_cancel_left:
- "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
-by (simp add: mult_commute [of c] mult_le_cancel_right)
-
-text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp]:
- "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
-apply (cut_tac linorder_less_linear [of 0 c])
-apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
- simp add: linorder_neq_iff)
-done
-
-lemma mult_cancel_left [simp]:
- "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
-by (simp add: mult_commute [of c] mult_cancel_right)
-
subsection{* Products of Signs *}
@@ -413,6 +363,99 @@
apply (simp add: order_less_le)
done
+lemma zero_le_one: "(0::'a::ordered_ring) \<le> 1"
+ by (rule zero_less_one [THEN order_less_imp_le])
+
+
+subsection{*More Monotonicity*}
+
+lemma mult_left_mono_neg:
+ "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
+apply (drule mult_left_mono [of _ _ "-c"])
+apply (simp_all add: minus_mult_left [symmetric])
+done
+
+lemma mult_right_mono_neg:
+ "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
+ by (simp add: mult_left_mono_neg mult_commute [of _ c])
+
+text{*Strict monotonicity in both arguments*}
+lemma mult_strict_mono:
+ "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_ring)"
+apply (case_tac "c=0")
+ apply (simp add: mult_pos)
+apply (erule mult_strict_right_mono [THEN order_less_trans])
+ apply (force simp add: order_le_less)
+apply (erule mult_strict_left_mono, assumption)
+done
+
+text{*This weaker variant has more natural premises*}
+lemma mult_strict_mono':
+ "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_ring)"
+apply (rule mult_strict_mono)
+apply (blast intro: order_le_less_trans)+
+done
+
+lemma mult_mono:
+ "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]
+ ==> a * c \<le> b * (d::'a::ordered_ring)"
+apply (erule mult_right_mono [THEN order_trans], assumption)
+apply (erule mult_left_mono, assumption)
+done
+
+
+subsection{*Cancellation Laws for Relationships With a Common Factor*}
+
+text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
+ also with the relations @{text "\<le>"} and equality.*}
+
+lemma mult_less_cancel_right:
+ "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
+apply (case_tac "c = 0")
+apply (auto simp add: linorder_neq_iff mult_strict_right_mono
+ mult_strict_right_mono_neg)
+apply (auto simp add: linorder_not_less
+ linorder_not_le [symmetric, of "a*c"]
+ linorder_not_le [symmetric, of a])
+apply (erule_tac [!] notE)
+apply (auto simp add: order_less_imp_le mult_right_mono
+ mult_right_mono_neg)
+done
+
+lemma mult_less_cancel_left:
+ "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"
+by (simp add: mult_commute [of c] mult_less_cancel_right)
+
+lemma mult_le_cancel_right:
+ "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
+
+lemma mult_le_cancel_left:
+ "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"
+by (simp add: mult_commute [of c] mult_le_cancel_right)
+
+lemma mult_less_imp_less_left:
+ "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
+ by (force elim: order_less_asym simp add: mult_less_cancel_left)
+
+lemma mult_less_imp_less_right:
+ "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
+ by (force elim: order_less_asym simp add: mult_less_cancel_right)
+
+text{*Cancellation of equalities with a common factor*}
+lemma mult_cancel_right [simp]:
+ "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"
+apply (cut_tac linorder_less_linear [of 0 c])
+apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono
+ simp add: linorder_neq_iff)
+done
+
+text{*These cancellation theorems require an ordering. Versions are proved
+ below that work for fields without an ordering.*}
+lemma mult_cancel_left [simp]:
+ "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"
+by (simp add: mult_commute [of c] mult_cancel_right)
+
subsection {* Absolute Value *}
@@ -440,5 +483,217 @@
subsection {* Fields *}
+text{*Cancellation of equalities with a common factor*}
+lemma field_mult_cancel_right_lemma:
+ assumes cnz: "c \<noteq> (0::'a::field)"
+ and eq: "a*c = b*c"
+ shows "a=b"
+ proof -
+ have "(a * c) * inverse c = (b * c) * inverse c"
+ by (simp add: eq)
+ thus "a=b"
+ by (simp add: mult_assoc cnz)
+ qed
+
+lemma field_mult_cancel_right:
+ "(a*c = b*c) = (c = (0::'a::field) | a=b)"
+ proof (cases "c=0")
+ assume "c=0" thus ?thesis by simp
+ next
+ assume "c\<noteq>0"
+ thus ?thesis by (force dest: field_mult_cancel_right_lemma)
+ qed
+
+lemma field_mult_cancel_left:
+ "(c*a = c*b) = (c = (0::'a::field) | a=b)"
+ by (simp add: mult_commute [of c] field_mult_cancel_right)
+
+lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
+ proof
+ assume ianz: "inverse a = 0"
+ assume "a \<noteq> 0"
+ hence "1 = a * inverse a" by simp
+ also have "... = 0" by (simp add: ianz)
+ finally have "1 = (0::'a::field)" .
+ thus False by (simp add: eq_commute)
+ qed
+
+lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
+apply (rule ccontr)
+apply (blast dest: nonzero_imp_inverse_nonzero)
+done
+
+lemma inverse_nonzero_imp_nonzero:
+ "inverse a = 0 ==> a = (0::'a::field)"
+apply (rule ccontr)
+apply (blast dest: nonzero_imp_inverse_nonzero)
+done
+
+lemma inverse_nonzero_iff_nonzero [simp]:
+ "(inverse a = 0) = (a = (0::'a::{field,division_by_zero}))"
+by (force dest: inverse_nonzero_imp_nonzero)
+
+lemma nonzero_inverse_minus_eq:
+ "a\<noteq>0 ==> inverse(-a) = -inverse(a::'a::field)";
+ proof -
+ assume "a\<noteq>0"
+ hence "-a * inverse (- a) = -a * - inverse a"
+ by simp
+ thus ?thesis
+ by (simp only: field_mult_cancel_left, simp add: prems)
+ qed
+
+lemma inverse_minus_eq [simp]:
+ "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
+ proof (cases "a=0")
+ assume "a=0" thus ?thesis by (simp add: inverse_zero)
+ next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+ qed
+
+lemma nonzero_inverse_eq_imp_eq:
+ assumes inveq: "inverse a = inverse b"
+ and anz: "a \<noteq> 0"
+ and bnz: "b \<noteq> 0"
+ shows "a = (b::'a::field)"
+ proof -
+ have "a * inverse b = a * inverse a"
+ by (simp add: inveq)
+ hence "(a * inverse b) * b = (a * inverse a) * b"
+ by simp
+ thus "a = b"
+ by (simp add: mult_assoc anz bnz)
+ qed
+
+lemma inverse_eq_imp_eq:
+ "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"
+apply (case_tac "a=0 | b=0")
+ apply (force dest!: inverse_zero_imp_zero
+ simp add: eq_commute [of "0::'a"])
+apply (force dest!: nonzero_inverse_eq_imp_eq)
+done
+
+lemma inverse_eq_iff_eq [simp]:
+ "(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
+by (force dest!: inverse_eq_imp_eq)
+
+
+subsection {* Ordered Fields *}
+
+lemma inverse_gt_0:
+ assumes a_gt_0: "0 < a"
+ shows "0 < inverse (a::'a::ordered_field)"
+ proof -
+ have "0 < a * inverse a"
+ by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
+ thus "0 < inverse a"
+ by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
+ qed
+
+lemma inverse_less_0:
+ "a < 0 ==> inverse a < (0::'a::ordered_field)"
+ by (insert inverse_gt_0 [of "-a"],
+ simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
+
+lemma inverse_le_imp_le:
+ assumes invle: "inverse a \<le> inverse b"
+ and apos: "0 < a"
+ shows "b \<le> (a::'a::ordered_field)"
+ proof (rule classical)
+ assume "~ b \<le> a"
+ hence "a < b"
+ by (simp add: linorder_not_le)
+ hence bpos: "0 < b"
+ by (blast intro: apos order_less_trans)
+ hence "a * inverse a \<le> a * inverse b"
+ by (simp add: apos invle order_less_imp_le mult_left_mono)
+ hence "(a * inverse a) * b \<le> (a * inverse b) * b"
+ by (simp add: bpos order_less_imp_le mult_right_mono)
+ thus "b \<le> a"
+ by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
+ qed
+
+lemma less_imp_inverse_less:
+ assumes less: "a < b"
+ and apos: "0 < a"
+ shows "inverse b < inverse (a::'a::ordered_field)"
+ proof (rule ccontr)
+ assume "~ inverse b < inverse a"
+ hence "inverse a \<le> inverse b"
+ by (simp add: linorder_not_less)
+ hence "~ (a < b)"
+ by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
+ thus False
+ by (rule notE [OF _ less])
+ qed
+
+lemma inverse_less_imp_less:
+ "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
+apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
+apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
+done
+
+text{*Both premises are essential. Consider -1 and 1.*}
+lemma inverse_less_iff_less [simp]:
+ "[|0 < a; 0 < b|]
+ ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
+by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
+
+lemma le_imp_inverse_le:
+ "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
+ by (force simp add: order_le_less less_imp_inverse_less)
+
+lemma inverse_le_iff_le [simp]:
+ "[|0 < a; 0 < b|]
+ ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
+by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
+
+
+text{*These results refer to both operands being negative. The opposite-sign
+case is trivial, since inverse preserves signs.*}
+lemma inverse_le_imp_le_neg:
+ "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
+ apply (rule classical)
+ apply (subgoal_tac "a < 0")
+ prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
+ apply (insert inverse_le_imp_le [of "-b" "-a"])
+ apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
+ done
+
+lemma less_imp_inverse_less_neg:
+ "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
+ apply (subgoal_tac "a < 0")
+ prefer 2 apply (blast intro: order_less_trans)
+ apply (insert less_imp_inverse_less [of "-b" "-a"])
+ apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
+ done
+
+lemma inverse_less_imp_less_neg:
+ "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
+ apply (rule classical)
+ apply (subgoal_tac "a < 0")
+ prefer 2
+ apply (force simp add: linorder_not_less intro: order_le_less_trans)
+ apply (insert inverse_less_imp_less [of "-b" "-a"])
+ apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
+ done
+
+lemma inverse_less_iff_less_neg [simp]:
+ "[|a < 0; b < 0|]
+ ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
+ apply (insert inverse_less_iff_less [of "-b" "-a"])
+ apply (simp del: inverse_less_iff_less
+ add: order_less_imp_not_eq nonzero_inverse_minus_eq)
+ done
+
+lemma le_imp_inverse_le_neg:
+ "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
+ by (force simp add: order_le_less less_imp_inverse_less_neg)
+
+lemma inverse_le_iff_le_neg [simp]:
+ "[|a < 0; b < 0|]
+ ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
+by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
end