65 done |
64 done |
66 |
65 |
67 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" |
68 by (insert power_decreasing [of 1 "Suc n" r], simp) |
67 by (insert power_decreasing [of 1 "Suc n" r], simp) |
69 |
68 |
70 text{*Used ONCE in Transcendental*} |
|
71 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" |
72 by (insert power_strict_decreasing [of 0 "Suc n" r], simp) |
70 by (insert power_strict_decreasing [of 0 "Suc n" r], simp) |
73 |
71 |
74 text{*Used ONCE in Lim.ML*} |
|
75 lemma realpow_minus_mult [rule_format]: |
72 lemma realpow_minus_mult [rule_format]: |
76 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
73 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
77 apply (simp split add: nat_diff_split) |
74 apply (simp split add: nat_diff_split) |
78 done |
75 done |
79 |
76 |
138 declare power_real_number_of [of _ "number_of w", standard, simp] |
135 declare power_real_number_of [of _ "number_of w", standard, simp] |
139 |
136 |
140 |
137 |
141 subsection{*Various Other Theorems*} |
138 subsection{*Various Other Theorems*} |
142 |
139 |
143 text{*Used several times in Hyperreal/Transcendental.ML*} |
|
144 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
140 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
145 apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric]) |
141 apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric]) |
146 apply (auto dest: real_sum_squares_cancel simp add: add_commute) |
142 apply (auto dest: real_sum_squares_cancel simp add: add_commute) |
147 done |
143 done |
148 |
144 |
169 apply (simp (no_asm) add: mult_ac) |
165 apply (simp (no_asm) add: mult_ac) |
170 apply (rule_tac c=x1 in mult_less_imp_less_right) |
166 apply (rule_tac c=x1 in mult_less_imp_less_right) |
171 apply (auto simp add: mult_ac) |
167 apply (auto simp add: mult_ac) |
172 done |
168 done |
173 |
169 |
174 text{*Used once: in Hyperreal/Transcendental.ML*} |
|
175 lemma real_mult_inverse_cancel2: |
170 lemma real_mult_inverse_cancel2: |
176 "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" |
171 "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" |
177 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) |
172 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) |
178 done |
173 done |
179 |
174 |
270 apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ") |
265 apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ") |
271 apply (simp (no_asm_simp) add: real_mult_assoc [symmetric]) |
266 apply (simp (no_asm_simp) add: real_mult_assoc [symmetric]) |
272 apply (auto simp add: realpow_num_eq_if) |
267 apply (auto simp add: realpow_num_eq_if) |
273 done |
268 done |
274 |
269 |
275 |
|
276 ML |
|
277 {* |
|
278 val realpow_0 = thm "realpow_0"; |
|
279 val realpow_Suc = thm "realpow_Suc"; |
|
280 |
|
281 val realpow_not_zero = thm "realpow_not_zero"; |
|
282 val realpow_zero_zero = thm "realpow_zero_zero"; |
|
283 val realpow_two = thm "realpow_two"; |
|
284 val realpow_less = thm "realpow_less"; |
|
285 val realpow_two_le = thm "realpow_two_le"; |
|
286 val abs_realpow_two = thm "abs_realpow_two"; |
|
287 val realpow_two_abs = thm "realpow_two_abs"; |
|
288 val two_realpow_ge_one = thm "two_realpow_ge_one"; |
|
289 val two_realpow_gt = thm "two_realpow_gt"; |
|
290 val realpow_Suc_le_self = thm "realpow_Suc_le_self"; |
|
291 val realpow_Suc_less_one = thm "realpow_Suc_less_one"; |
|
292 val realpow_minus_mult = thm "realpow_minus_mult"; |
|
293 val realpow_two_mult_inverse = thm "realpow_two_mult_inverse"; |
|
294 val realpow_two_minus = thm "realpow_two_minus"; |
|
295 val realpow_two_disj = thm "realpow_two_disj"; |
|
296 val realpow_real_of_nat = thm "realpow_real_of_nat"; |
|
297 val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos"; |
|
298 val realpow_increasing = thm "realpow_increasing"; |
|
299 val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff"; |
|
300 val zero_le_realpow_abs = thm "zero_le_realpow_abs"; |
|
301 val real_of_int_power = thm "real_of_int_power"; |
|
302 val power_real_number_of = thm "power_real_number_of"; |
|
303 val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a"; |
|
304 val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; |
|
305 val real_squared_diff_one_factored = thm "real_squared_diff_one_factored"; |
|
306 val real_mult_is_one = thm "real_mult_is_one"; |
|
307 val real_le_add_half_cancel = thm "real_le_add_half_cancel"; |
|
308 val real_minus_half_eq = thm "real_minus_half_eq"; |
|
309 val real_mult_inverse_cancel = thm "real_mult_inverse_cancel"; |
|
310 val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2"; |
|
311 val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero"; |
|
312 val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero"; |
|
313 val real_sum_squares_not_zero = thm "real_sum_squares_not_zero"; |
|
314 val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2"; |
|
315 |
|
316 val realpow_divide = thm "realpow_divide"; |
|
317 val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff"; |
|
318 val realpow_two_le_add_order = thm "realpow_two_le_add_order"; |
|
319 val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2"; |
|
320 val real_sum_square_gt_zero = thm "real_sum_square_gt_zero"; |
|
321 val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2"; |
|
322 val real_minus_mult_self_le = thm "real_minus_mult_self_le"; |
|
323 val realpow_square_minus_le = thm "realpow_square_minus_le"; |
|
324 val realpow_num_eq_if = thm "realpow_num_eq_if"; |
|
325 val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow"; |
|
326 val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono"; |
|
327 *} |
|
328 |
|
329 |
|
330 end |
270 end |