1.1 --- a/src/HOL/RealPow.thy	Tue May 11 06:27:06 2010 -0700
     1.2 +++ b/src/HOL/RealPow.thy	Tue May 11 06:30:48 2010 -0700
     1.3 @@ -124,31 +124,4 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -subsection {*Various Other Theorems*}
     1.8 -
     1.9 -lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
    1.10 -by auto
    1.11 -
    1.12 -lemma real_mult_inverse_cancel:
    1.13 -     "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
    1.14 -      ==> inverse x * y < inverse x1 * u"
    1.15 -apply (rule_tac c=x in mult_less_imp_less_left) 
    1.16 -apply (auto simp add: mult_assoc [symmetric])
    1.17 -apply (simp (no_asm) add: mult_ac)
    1.18 -apply (rule_tac c=x1 in mult_less_imp_less_right) 
    1.19 -apply (auto simp add: mult_ac)
    1.20 -done
    1.21 -
    1.22 -lemma real_mult_inverse_cancel2:
    1.23 -     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
    1.24 -apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
    1.25 -done
    1.26 -
    1.27 -(* TODO: no longer real-specific; rename and move elsewhere *)
    1.28 -lemma realpow_num_eq_if:
    1.29 -  fixes m :: "'a::power"
    1.30 -  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    1.31 -by (cases n, auto)
    1.32 -
    1.33 -
    1.34  end

     2.1 --- a/src/HOL/Transcendental.thy	Tue May 11 06:27:06 2010 -0700
     2.2 +++ b/src/HOL/Transcendental.thy	Tue May 11 06:30:48 2010 -0700
     2.3 @@ -1663,6 +1663,26 @@
     2.4  lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
     2.5  by simp
     2.6  
     2.7 +lemma real_mult_inverse_cancel:
     2.8 +     "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
     2.9 +      ==> inverse x * y < inverse x1 * u"
    2.10 +apply (rule_tac c=x in mult_less_imp_less_left) 
    2.11 +apply (auto simp add: mult_assoc [symmetric])
    2.12 +apply (simp (no_asm) add: mult_ac)
    2.13 +apply (rule_tac c=x1 in mult_less_imp_less_right) 
    2.14 +apply (auto simp add: mult_ac)
    2.15 +done
    2.16 +
    2.17 +lemma real_mult_inverse_cancel2:
    2.18 +     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
    2.19 +apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
    2.20 +done
    2.21 +
    2.22 +lemma realpow_num_eq_if:
    2.23 +  fixes m :: "'a::power"
    2.24 +  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    2.25 +by (cases n, auto)
    2.26 +
    2.27  lemma cos_two_less_zero [simp]: "cos (2) < 0"
    2.28  apply (cut_tac x = 2 in cos_paired)
    2.29  apply (drule sums_minus)