# HG changeset patch
# User huffman
# Date 1273584648 25200
# Node ID 2e9a866141b8f0f4f298948a06e54bd689770f3e
# Parent  001d1aad99de73fe225cd41a7f2f23e4da04771d
move some theorems from RealPow.thy to Transcendental.thy

diff -r 001d1aad99de -r 2e9a866141b8 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue May 11 06:27:06 2010 -0700
+++ b/src/HOL/RealPow.thy	Tue May 11 06:30:48 2010 -0700
@@ -124,31 +124,4 @@
     by simp
 qed
 
-subsection {*Various Other Theorems*}
-
-lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
-by auto
-
-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: mult_assoc [symmetric])
-apply (simp (no_asm) add: mult_ac)
-apply (rule_tac c=x1 in mult_less_imp_less_right) 
-apply (auto simp add: mult_ac)
-done
-
-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: mult_ac)
-done
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_num_eq_if:
-  fixes m :: "'a::power"
-  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (cases n, auto)
-
-
 end
diff -r 001d1aad99de -r 2e9a866141b8 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 11 06:27:06 2010 -0700
+++ b/src/HOL/Transcendental.thy	Tue May 11 06:30:48 2010 -0700
@@ -1663,6 +1663,26 @@
 lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
 by 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: mult_assoc [symmetric])
+apply (simp (no_asm) add: mult_ac)
+apply (rule_tac c=x1 in mult_less_imp_less_right) 
+apply (auto simp add: mult_ac)
+done
+
+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: mult_ac)
+done
+
+lemma realpow_num_eq_if:
+  fixes m :: "'a::power"
+  shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+by (cases n, auto)
+
 lemma cos_two_less_zero [simp]: "cos (2) < 0"
 apply (cut_tac x = 2 in cos_paired)
 apply (drule sums_minus)