410 assumes nz: "a ~= 0" |
410 assumes nz: "a ~= 0" |
411 shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)" |
411 shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)" |
412 by (induct m n rule: diff_induct) |
412 by (induct m n rule: diff_induct) |
413 (simp_all add: nonzero_mult_divide_cancel_left nz) |
413 (simp_all add: nonzero_mult_divide_cancel_left nz) |
414 |
414 |
415 |
|
416 text{*ML bindings for the general exponentiation theorems*} |
|
417 ML |
|
418 {* |
|
419 val power_0 = thm"power_0"; |
|
420 val power_Suc = thm"power_Suc"; |
|
421 val power_0_Suc = thm"power_0_Suc"; |
|
422 val power_0_left = thm"power_0_left"; |
|
423 val power_one = thm"power_one"; |
|
424 val power_one_right = thm"power_one_right"; |
|
425 val power_add = thm"power_add"; |
|
426 val power_mult = thm"power_mult"; |
|
427 val power_mult_distrib = thm"power_mult_distrib"; |
|
428 val zero_less_power = thm"zero_less_power"; |
|
429 val zero_le_power = thm"zero_le_power"; |
|
430 val one_le_power = thm"one_le_power"; |
|
431 val gt1_imp_ge0 = thm"gt1_imp_ge0"; |
|
432 val power_gt1_lemma = thm"power_gt1_lemma"; |
|
433 val power_gt1 = thm"power_gt1"; |
|
434 val power_le_imp_le_exp = thm"power_le_imp_le_exp"; |
|
435 val power_inject_exp = thm"power_inject_exp"; |
|
436 val power_less_imp_less_exp = thm"power_less_imp_less_exp"; |
|
437 val power_mono = thm"power_mono"; |
|
438 val power_strict_mono = thm"power_strict_mono"; |
|
439 val power_eq_0_iff = thm"power_eq_0_iff"; |
|
440 val field_power_eq_0_iff = thm"power_eq_0_iff"; |
|
441 val field_power_not_zero = thm"field_power_not_zero"; |
|
442 val power_inverse = thm"power_inverse"; |
|
443 val nonzero_power_divide = thm"nonzero_power_divide"; |
|
444 val power_divide = thm"power_divide"; |
|
445 val power_abs = thm"power_abs"; |
|
446 val zero_less_power_abs_iff = thm"zero_less_power_abs_iff"; |
|
447 val zero_le_power_abs = thm "zero_le_power_abs"; |
|
448 val power_minus = thm"power_minus"; |
|
449 val power_Suc_less = thm"power_Suc_less"; |
|
450 val power_strict_decreasing = thm"power_strict_decreasing"; |
|
451 val power_decreasing = thm"power_decreasing"; |
|
452 val power_Suc_less_one = thm"power_Suc_less_one"; |
|
453 val power_increasing = thm"power_increasing"; |
|
454 val power_strict_increasing = thm"power_strict_increasing"; |
|
455 val power_le_imp_le_base = thm"power_le_imp_le_base"; |
|
456 val power_inject_base = thm"power_inject_base"; |
|
457 *} |
|
458 |
|
459 text{*ML bindings for the remaining theorems*} |
|
460 ML |
|
461 {* |
|
462 val nat_one_le_power = thm"nat_one_le_power"; |
|
463 val nat_power_less_imp_less = thm"nat_power_less_imp_less"; |
|
464 val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; |
|
465 *} |
|
466 |
|
467 end |
415 end |