# HG changeset patch # User paulson # Date 1069926475 -3600 # Node ID 5cf13e80be0e0b653e60f1b16de1755f23ee47e4 # Parent b963e9cee2a0877f08921315abfa2e3c1f7d88f2 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs. diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/ExtraThms2.ML --- 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) x x (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 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) x x (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"; - diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/ExtraThms2.thy --- 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 diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/HyperDef.ML --- 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]; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/HyperNat.ML --- 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]; + diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/HyperOrd.ML --- 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"; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/HyperPow.ML --- 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"; + diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/NSA.ML --- 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]; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/NatStar.ML --- 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]; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/NthRoot.thy --- 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 diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/SEQ.ML --- 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(); (*------------------------------------------------------------------- diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Hyperreal/Transcendental.ML --- 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) x 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 < 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"; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/IsaMakefile --- 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\ diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Real/RComplete.ML --- 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"; + diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Real/RealArith0.ML --- 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))"; diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Real/RealDef.ML --- 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 diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Real/RealOrd.thy --- 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 ==> \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: "\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) = (\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 \ real_of_preal m2) = (m1 \ 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 \ z+w) = (v \ (w::real))" by simp -(*"v\w ==> v+z \ w+z"*) -lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard] - -(*"v\w ==> v+z \ 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'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'\w; 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 \ B + C ==> A \ B" -apply (simp (no_asm_use)) -done - -lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ 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 \ x; 0 \ y |] ==> (0::real) \ 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 \ q2 ==> x + q1 \ x + q2" -by simp - -lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" -apply (drule real_add_le_mono1) -apply (erule order_trans, simp) -done - -lemma real_less_Ex: "\(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 \ -r) = ((r::real) \ 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) \ 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 \ 0 ==> x / y = x * inverse y" by (simp add: real_divide_def) qed +(*"v\w ==> v+z \ w+z"*) +lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard] + +(*"v\w ==> v+z \ 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'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'\w; 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 \ B + C ==> A \ B" +apply simp +done + +lemma real_le_add_left_cancel: "!!(A::real). C + A \ C + B ==> A \ 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 \ q2 ==> x + q1 \ x + q2" +by simp + +lemma real_add_le_mono: "[|i\j; k\l |] ==> i + k \ j + (l::real)" + by (rule Ring_and_Field.add_mono) + +lemma real_le_minus_iff: "(-s \ -r) = ((r::real) \ s)" + by (rule Ring_and_Field.neg_le_iff_le) + +lemma real_le_square [simp]: "(0::real) \ 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 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 \ y*z) = (x \ y)" -by (auto simp add: real_le_def) - -lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x \ y)" +lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x\y)" by (auto simp add: real_le_def) -lemma real_mult_le_less_mono1: "[| (0::real) \ z; x < y |] ==> x*z \ 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 \ z*y) = (x\y)" +by (auto simp add: real_le_def) -lemma real_mult_less_mono: "[| u 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) \ r1; 0 \ x|] ==> r1 * x < r2 * y" apply (subgoal_tac "0 x |] ==> x \ r * x" -apply (subgoal_tac "0\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) \ r; (1::real) \ x |] ==> x \ 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 \ -R) = (R \ (0::real))" -by (auto dest: sym simp add: real_le_less) - -lemma real_minus_zero_le_iff2 [simp]: "(-R \ 0) = ((0::real) \ 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 (0::real)) = (0\x & y\0 | x\0 & 0\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 \ x; 0 \ y |] ==> (0::real) \ 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) \ z; x < y |] ==> x*z \ 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) x x (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 diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Real/RealPow.thy --- 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 \ (0::real) --> r ^ n \ 0" -apply (induct_tac "n") -apply auto -done +lemma realpow_not_zero [rule_format]: "r \ (0::real) --> r ^ n \ 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) \ r --> 0 \ r ^ n" +lemma realpow_ge_zero [rule_format]: "(0::real) \ r --> 0 \ 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) \ x & x \ y --> x ^ n \ y ^ n" +lemma realpow_le [rule_format]: "(0::real) \ x & x \ y --> x ^ n \ 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) \ 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) \ 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) \ 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 \ r ^ n" -apply (induct_tac "n") -apply auto +lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \ r ^ n" +apply (induct_tac "n", auto) apply (subgoal_tac "1*1 \ 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) \ r ==> 1 \ r ^ n" @@ -149,167 +124,118 @@ apply (auto dest: realpow_ge_one) done -lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" +lemma two_realpow_ge_one [simp]: "(1::real) \ 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 \ r & r < (1::real) --> r ^ Suc n \ r ^ n" +lemma realpow_Suc_le [rule_format]: "0 \ r & r < (1::real) --> r ^ Suc n \ 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) \ 0 ^ n" -apply (case_tac "n") -apply auto -done -declare realpow_zero_le [simp] +lemma realpow_zero_le [simp]: "(0::real) \ 0 ^ n" +by (case_tac "n", auto) -lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \ 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 \ r ^ n" +by (blast intro!: order_less_imp_le realpow_Suc_less) lemma realpow_Suc_le3: "[| 0 \ r; r < (1::real) |] ==> r ^ Suc n \ 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 \ r & r < (1::real) & n < N --> r ^ N \ r ^ n" +lemma realpow_less_le [rule_format]: "0 \ r & r < (1::real) & n < N --> r ^ N \ r ^ n" apply (induct_tac "N") apply (simp_all (no_asm_simp)) apply clarify -apply (subgoal_tac "r * r ^ na \ 1 * r ^ n") -apply simp +apply (subgoal_tac "r * r ^ na \ 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 \ r; r < (1::real); n \ N |] ==> r ^ N \ 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 \ 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) \ r --> r ^ n \ 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) \ r --> r ^ n \ r ^ Suc n" -apply (induct_tac "n") -apply auto +lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \ 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) \ r; (1::real) \ x |] ==> x \ r * x" +apply (subgoal_tac "1 * x \ 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 \ 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 \ 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) \ r & n < N --> r ^ n \ 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) \ r & n < N --> r ^ n \ 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 \ N |] ==> r ^ n \ 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) \ r; n \ N |] ==> r ^ n \ 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 \ 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) \ r ==> r \ 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) \ r ==> r \ 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 \ 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) \ r; 0 < n |] ==> r \ 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 \ 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 \ 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) \ 0; m \ 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) \ x" @@ -352,29 +276,23 @@ qed lemma realpow_Suc_cancel_eq: "[| (0::real) \ x; 0 \ 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 (0::real) | n=0)" +lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \ (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) \ (abs x)^n" +lemma zero_le_realpow_abs [simp]: "(0::real) \ (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"; *} diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/Ring_and_Field.thy --- 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 \ ordered_ring, field axclass division_by_zero \ 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 \ 0 ==> a * inverse (a::'a::field) = 1" +lemma right_inverse [simp]: "a \ 0 ==> a * inverse (a::'a::field) = 1" proof - have "a * inverse a = inverse a * a" by (simp add: mult_ac) also assume "a \ 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 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 \ (b::'a::ordered_ring)" shows "-b \ -a" proof - have "-a+a \ -a+b" by (rule add_left_mono) - then have "0 \ -a+b" + hence "0 \ -a+b" by simp - then have "0 + (-b) \ (-a + b) + (-b)" + hence "0 + (-b) \ (-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 \ -a) = (a \ (b::'a::ordered_ring))" proof assume "- b \ - a" - then have "- (- a) \ - (- b)" + hence "- (- a) \ - (- b)" by (rule le_imp_neg_le) thus "a\b" by simp next @@ -288,73 +305,6 @@ apply (simp_all add: minus_mult_right [symmetric]) done -lemma mult_left_mono_neg: - "[|b \ a; c \ 0|] ==> c * a \ 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 \ a; c \ 0|] ==> a * c \ 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 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 \ b; c \ d; 0 \ b; 0 \ c|] - ==> a * c \ 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 "\"} 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 \ b*c) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring)))" -by (simp add: linorder_not_less [symmetric] mult_less_cancel_right) - -lemma mult_le_cancel_left: - "(c*a \ c*b) = ((0 a\b) & (c<0 --> b \ (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) \ 1" + by (rule zero_less_one [THEN order_less_imp_le]) + + +subsection{*More Monotonicity*} + +lemma mult_left_mono_neg: + "[|b \ a; c \ 0|] ==> c * a \ 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 \ a; c \ 0|] ==> a * c \ 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: + "[|ac|] ==> 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 a; 0 \ 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 \ b; c \ d; 0 \ b; 0 \ c|] + ==> a * c \ 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 "\"} 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 \ b*c) = ((0 a\b) & (c<0 --> b \ (a::'a::ordered_ring)))" +by (simp add: linorder_not_less [symmetric] mult_less_cancel_right) + +lemma mult_le_cancel_left: + "(c*a \ c*b) = ((0 a\b) & (c<0 --> b \ (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 \ (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\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 \ 0 ==> inverse a \ (0::'a::field)" + proof + assume ianz: "inverse a = 0" + assume "a \ 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\0 ==> inverse(-a) = -inverse(a::'a::field)"; + proof - + assume "a\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\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 \ 0" + and bnz: "b \ 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 \ inverse b" + and apos: "0 < a" + shows "b \ (a::'a::ordered_field)" + proof (rule classical) + assume "~ b \ 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 \ a * inverse b" + by (simp add: apos invle order_less_imp_le mult_left_mono) + hence "(a * inverse a) * b \ (a * inverse b) * b" + by (simp add: bpos order_less_imp_le mult_right_mono) + thus "b \ 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 \ 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 \ b; 0 < a|] ==> inverse b \ 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 \ inverse b) = (b \ (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 \ 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_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 \ b; b < 0|] ==> inverse b \ 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 \ inverse b) = (b \ (a::'a::ordered_field))" +by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) end