# HG changeset patch # User huffman # Date 1158073544 -7200 # Node ID 86343f2386a8d099bd5ff372924244122f06c3b4 # Parent 2d2e1d323a0594cc33c539d9dfee362999b88d8f simplify some proofs, remove obsolete realpow_divide diff -r 2d2e1d323a05 -r 86343f2386a8 src/HOL/Real/RealPow.thy --- a/src/HOL/Real/RealPow.thy Tue Sep 12 17:03:52 2006 +0200 +++ b/src/HOL/Real/RealPow.thy Tue Sep 12 17:05:44 2006 +0200 @@ -173,10 +173,10 @@ done lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))" -by auto +by simp lemma inverse_real_of_nat_ge_zero [simp]: "0 \ inverse (real (Suc n))" -by auto +by simp lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" by (blast dest!: real_sum_squares_cancel) @@ -187,12 +187,6 @@ subsection {*Various Other Theorems*} -lemma realpow_divide: - "(x/y) ^ n = ((x::real) ^ n/ y ^ n)" -apply (unfold real_divide_def) -apply (auto simp add: power_mult_distrib power_inverse) -done - lemma realpow_two_sum_zero_iff [simp]: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 @@ -231,34 +225,18 @@ fixes x::real assumes xgt0: "0 \ x" and ygt0: "0 \ y" and sq: "x^2 \ y^2" shows "x \ y" -proof (rule ccontr) - assume "\(x \ y)" - then have ylx: "y < x" by simp - hence "y \ x" by simp - with xgt0 have "x*y \ x*x" - by (simp add: pordered_comm_semiring_class.mult_mono) - moreover - have "\ (y = 0)" - proof - assume "y = 0" - with ylx have xg0: "0 < x" by simp - from xg0 xg0 have "0 < x*x" by (rule real_mult_order) - moreover have "y*y = 0" by simp - ultimately show False using sq by auto - qed - with ygt0 have "0 < y" by simp - with ylx have "y*y < x*y" by auto - ultimately have "y*y < x*x" by simp - with sq show False by (auto simp add: power2_eq_square [symmetric]) +proof - + from sq have "x ^ Suc (Suc 0) \ y ^ Suc (Suc 0)" + by (simp only: numeral_2_eq_2) + thus "x \ y" using xgt0 ygt0 + by (rule power_le_imp_le_base) qed lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" by (case_tac "n", auto) lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)" -apply (induct "d") -apply (auto simp add: realpow_num_eq_if) -done +by (simp add: zero_less_power) lemma lemma_realpow_num_two_mono: "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)"