equal
deleted
inserted
replaced
65 |
65 |
66 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
66 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
67 by (insert power_decreasing [of 1 "Suc n" r], simp) |
67 by (insert power_decreasing [of 1 "Suc n" r], simp) |
68 |
68 |
69 lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1" |
69 lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1" |
70 by (insert power_strict_decreasing [of 0 "Suc n" r], simp) |
70 by (rule power_Suc_less_one) |
71 |
71 |
72 lemma realpow_minus_mult [rule_format]: |
72 lemma realpow_minus_mult [rule_format]: |
73 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
73 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
74 apply (simp split add: nat_diff_split) |
74 apply (simp split add: nat_diff_split) |
75 done |
75 done |
113 apply (induct "n") |
113 apply (induct "n") |
114 apply (auto simp add: zero_less_mult_iff) |
114 apply (auto simp add: zero_less_mult_iff) |
115 done |
115 done |
116 |
116 |
117 lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n" |
117 lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n" |
118 apply (induct "n") |
118 by (rule zero_le_power_abs) |
119 apply (auto simp add: zero_le_mult_iff) |
|
120 done |
|
121 |
119 |
122 |
120 |
123 subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} |
121 subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} |
124 |
122 |
125 lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" |
123 lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" |