# HG changeset patch
# User huffman
# Date 1266964686 28800
# Node ID be0c69c06176c434197eea8aa82f27310c0d0589
# Parent  8e1f994c6e54cb447d7c5b0e4928c3768d3d782c
remove redundant simp rules from RealPow.thy

diff -r 8e1f994c6e54 -r be0c69c06176 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Tue Feb 23 12:35:32 2010 -0800
+++ b/src/HOL/Probability/Borel.thy	Tue Feb 23 14:38:06 2010 -0800
@@ -82,7 +82,7 @@
     fix w n
     assume le: "f w \<le> g w - inverse(real(Suc n))"
     hence "0 < inverse(real(Suc n))"
-      by (metis inverse_real_of_nat_gt_zero)
+      by simp
     thus "f w < g w" using le
       by arith 
   qed
diff -r 8e1f994c6e54 -r be0c69c06176 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 23 12:35:32 2010 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 23 14:38:06 2010 -0800
@@ -9,9 +9,11 @@
 imports RealDef
 begin
 
+(* FIXME: declare this in Rings.thy or not at all *)
 declare abs_mult_self [simp]
 
-lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
+(* used by Import/HOL/real.imp *)
+lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
 by simp
 
 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
@@ -30,18 +32,9 @@
 apply (simp split add: nat_diff_split)
 done
 
-lemma realpow_two_mult_inverse [simp]:
-     "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
-by (simp add:  real_mult_assoc [symmetric])
-
-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)
-apply (simp add: algebra_simps)
-done
+by (simp add: algebra_simps)
 
 lemma realpow_two_disj:
      "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
@@ -49,11 +42,6 @@
 apply auto
 done
 
-lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
-apply (induct "n")
-apply (auto simp add: zero_less_mult_iff)
-done
-
 (* used by AFP Integration theory *)
 lemma realpow_increasing:
      "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
@@ -72,9 +60,6 @@
 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
 by simp
 
-lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y"
-by (rule sum_squares_ge_zero)
-
 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
 by (simp add: real_add_eq_0_iff [symmetric])
 
@@ -151,12 +136,6 @@
 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
 done
 
-lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))"
-by simp
-
-lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
-by simp
-
 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
 by (case_tac "n", auto)