author huffman Tue, 12 Sep 2006 17:05:44 +0200 changeset 20517 86343f2386a8 parent 20516 2d2e1d323a05 child 20518 9125f0d95449
simplify some proofs, remove obsolete realpow_divide
 src/HOL/Real/RealPow.thy file | annotate | diff | comparison | revisions
```--- 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 \<le> 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 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
shows "x \<le> y"
-proof (rule ccontr)
-  assume "\<not>(x \<le> y)"
-  then have ylx: "y < x" by simp
-  hence "y \<le> x" by simp
-  with xgt0 have "x*y \<le> x*x"
-  moreover
-  have "\<not> (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) \<le> y ^ Suc (Suc 0)"
+    by (simp only: numeral_2_eq_2)
+  thus "x \<le> 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")