src/HOL/Real/RealPow.thy
changeset 19765 dfe940911617
parent 19279 48b527d0331b
child 20517 86343f2386a8
     1.1 --- a/src/HOL/Real/RealPow.thy	Fri Jun 02 20:12:59 2006 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Jun 02 23:22:29 2006 +0200
     1.3 @@ -37,8 +37,7 @@
     1.4  lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
     1.5  by simp
     1.6  
     1.7 -text{*Legacy: weaker version of the theorem @{text power_strict_mono},
     1.8 -used 6 times in NthRoot and Transcendental*}
     1.9 +text{*Legacy: weaker version of the theorem @{text power_strict_mono}*}
    1.10  lemma realpow_less:
    1.11       "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.12  apply (rule power_strict_mono, auto) 
    1.13 @@ -67,11 +66,9 @@
    1.14  lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
    1.15  by (insert power_decreasing [of 1 "Suc n" r], simp)
    1.16  
    1.17 -text{*Used ONCE in Transcendental*}
    1.18  lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
    1.19  by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
    1.20  
    1.21 -text{*Used ONCE in Lim.ML*}
    1.22  lemma realpow_minus_mult [rule_format]:
    1.23       "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
    1.24  apply (simp split add: nat_diff_split)
    1.25 @@ -140,7 +137,6 @@
    1.26  
    1.27  subsection{*Various Other Theorems*}
    1.28  
    1.29 -text{*Used several times in Hyperreal/Transcendental.ML*}
    1.30  lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
    1.31    apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
    1.32    apply (auto dest: real_sum_squares_cancel simp add: add_commute)
    1.33 @@ -171,7 +167,6 @@
    1.34  apply (auto simp add: mult_ac)
    1.35  done
    1.36  
    1.37 -text{*Used once: in Hyperreal/Transcendental.ML*}
    1.38  lemma real_mult_inverse_cancel2:
    1.39       "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
    1.40  apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
    1.41 @@ -272,59 +267,4 @@
    1.42  apply (auto simp add: realpow_num_eq_if)
    1.43  done
    1.44  
    1.45 -
    1.46 -ML
    1.47 -{*
    1.48 -val realpow_0 = thm "realpow_0";
    1.49 -val realpow_Suc = thm "realpow_Suc";
    1.50 -
    1.51 -val realpow_not_zero = thm "realpow_not_zero";
    1.52 -val realpow_zero_zero = thm "realpow_zero_zero";
    1.53 -val realpow_two = thm "realpow_two";
    1.54 -val realpow_less = thm "realpow_less";
    1.55 -val realpow_two_le = thm "realpow_two_le";
    1.56 -val abs_realpow_two = thm "abs_realpow_two";
    1.57 -val realpow_two_abs = thm "realpow_two_abs";
    1.58 -val two_realpow_ge_one = thm "two_realpow_ge_one";
    1.59 -val two_realpow_gt = thm "two_realpow_gt";
    1.60 -val realpow_Suc_le_self = thm "realpow_Suc_le_self";
    1.61 -val realpow_Suc_less_one = thm "realpow_Suc_less_one";
    1.62 -val realpow_minus_mult = thm "realpow_minus_mult";
    1.63 -val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
    1.64 -val realpow_two_minus = thm "realpow_two_minus";
    1.65 -val realpow_two_disj = thm "realpow_two_disj";
    1.66 -val realpow_real_of_nat = thm "realpow_real_of_nat";
    1.67 -val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
    1.68 -val realpow_increasing = thm "realpow_increasing";
    1.69 -val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
    1.70 -val zero_le_realpow_abs = thm "zero_le_realpow_abs";
    1.71 -val real_of_int_power = thm "real_of_int_power";
    1.72 -val power_real_number_of = thm "power_real_number_of";
    1.73 -val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
    1.74 -val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
    1.75 -val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
    1.76 -val real_mult_is_one = thm "real_mult_is_one";
    1.77 -val real_le_add_half_cancel = thm "real_le_add_half_cancel";
    1.78 -val real_minus_half_eq = thm "real_minus_half_eq";
    1.79 -val real_mult_inverse_cancel = thm "real_mult_inverse_cancel";
    1.80 -val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
    1.81 -val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero";
    1.82 -val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
    1.83 -val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
    1.84 -val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
    1.85 -
    1.86 -val realpow_divide = thm "realpow_divide";
    1.87 -val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
    1.88 -val realpow_two_le_add_order = thm "realpow_two_le_add_order";
    1.89 -val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
    1.90 -val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
    1.91 -val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
    1.92 -val real_minus_mult_self_le = thm "real_minus_mult_self_le";
    1.93 -val realpow_square_minus_le = thm "realpow_square_minus_le";
    1.94 -val realpow_num_eq_if = thm "realpow_num_eq_if";
    1.95 -val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
    1.96 -val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
    1.97 -*}
    1.98 -
    1.99 -
   1.100  end