equal
deleted
inserted
replaced
369 Goal "(0::real) <= (abs x)^n"; |
369 Goal "(0::real) <= (abs x)^n"; |
370 by (induct_tac "n" 1); |
370 by (induct_tac "n" 1); |
371 by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff])); |
371 by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff])); |
372 qed "zero_le_realpow_abs"; |
372 qed "zero_le_realpow_abs"; |
373 Addsimps [zero_le_realpow_abs]; |
373 Addsimps [zero_le_realpow_abs]; |
|
374 |
|
375 |
|
376 (*** Literal arithmetic involving powers, type real ***) |
|
377 |
|
378 Goal "real (x::int) ^ n = real (x ^ n)"; |
|
379 by (induct_tac "n" 1); |
|
380 by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib]))); |
|
381 qed "real_of_int_power"; |
|
382 Addsimps [real_of_int_power RS sym]; |
|
383 |
|
384 Goal "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"; |
|
385 by (simp_tac (HOL_ss addsimps [real_number_of_def, real_of_int_power]) 1); |
|
386 qed "power_real_number_of"; |
|
387 |
|
388 Addsimps [inst "n" "number_of ?w" power_real_number_of]; |