src/HOL/Real/RealPow.thy
changeset 14352 a8b1a44d8264
parent 14348 744c868ee0b7
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Real/RealPow.thy	Mon Jan 12 14:35:07 2004 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Mon Jan 12 16:45:35 2004 +0100
     1.3 @@ -148,10 +148,6 @@
     1.4  declare power_real_number_of [of _ "number_of w", standard, simp]
     1.5  
     1.6  
     1.7 -lemma real_power_two: "(r::real)\<twosuperior> = r * r"
     1.8 -  by (simp add: numeral_2_eq_2)
     1.9 -
    1.10 -
    1.11  subsection{*Various Other Theorems*}
    1.12  
    1.13  text{*Used several times in Hyperreal/Transcendental.ML*}
    1.14 @@ -213,17 +209,17 @@
    1.15  lemma realpow_two_sum_zero_iff [simp]:
    1.16       "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
    1.17  apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
    1.18 -                   simp add: real_power_two)
    1.19 +                   simp add: power2_eq_square)
    1.20  done
    1.21  
    1.22  lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
    1.23  apply (rule real_le_add_order)
    1.24 -apply (auto simp add: real_power_two)
    1.25 +apply (auto simp add: power2_eq_square)
    1.26  done
    1.27  
    1.28  lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    1.29  apply (rule real_le_add_order)+
    1.30 -apply (auto simp add: real_power_two)
    1.31 +apply (auto simp add: power2_eq_square)
    1.32  done
    1.33  
    1.34  lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
    1.35 @@ -241,7 +237,7 @@
    1.36  by (rule_tac j = 0 in real_le_trans, auto)
    1.37  
    1.38  lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
    1.39 -by (auto simp add: real_power_two)
    1.40 +by (auto simp add: power2_eq_square)
    1.41  
    1.42  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
    1.43  by (case_tac "n", auto)
    1.44 @@ -259,7 +255,7 @@
    1.45  done
    1.46  
    1.47  lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
    1.48 -by (simp add: real_power_two)
    1.49 +by (simp add: power2_eq_square)
    1.50  
    1.51  
    1.52  
    1.53 @@ -294,7 +290,6 @@
    1.54  val zero_le_realpow_abs = thm "zero_le_realpow_abs";
    1.55  val real_of_int_power = thm "real_of_int_power";
    1.56  val power_real_number_of = thm "power_real_number_of";
    1.57 -val real_power_two = thm "real_power_two";
    1.58  val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
    1.59  val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
    1.60  val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";