paulson@3390: (* Title: HOL/Power.thy paulson@3390: ID: $Id$ paulson@3390: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@3390: Copyright 1997 University of Cambridge paulson@3390: paulson@3390: *) paulson@3390: nipkow@16733: header{*Exponentiation*} paulson@14348: nipkow@15131: theory Power haftmann@21413: imports Nat nipkow@15131: begin paulson@14348: krauss@21199: subsection{*Powers for Arbitrary Monoids*} paulson@14348: haftmann@22390: class recpower = monoid_mult + power + haftmann@22390: assumes power_0 [simp]: "a \<^loc>^ 0 = \<^loc>1" haftmann@22390: assumes power_Suc: "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)" paulson@14348: krauss@21199: lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" paulson@14348: by (simp add: power_Suc) paulson@14348: paulson@14348: text{*It looks plausible as a simprule, but its effect can be strange.*} krauss@21199: lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))" paulson@15251: by (induct "n", auto) paulson@14348: paulson@15004: lemma power_one [simp]: "1^n = (1::'a::recpower)" paulson@15251: apply (induct "n") wenzelm@14577: apply (auto simp add: power_Suc) paulson@14348: done paulson@14348: paulson@15004: lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a" paulson@14348: by (simp add: power_Suc) paulson@14348: krauss@21199: lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n" krauss@21199: by (induct "n") (simp_all add:power_Suc mult_assoc) krauss@21199: paulson@15004: lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)" krauss@21199: apply (induct "m") paulson@14348: apply (simp_all add: power_Suc mult_ac) paulson@14348: done paulson@14348: paulson@15004: lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n" krauss@21199: apply (induct "n") paulson@14348: apply (simp_all add: power_Suc power_add) paulson@14348: done paulson@14348: krauss@21199: lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)" paulson@15251: apply (induct "n") paulson@14348: apply (auto simp add: power_Suc mult_ac) paulson@14348: done paulson@14348: paulson@14348: lemma zero_less_power: paulson@15004: "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" paulson@15251: apply (induct "n") avigad@16775: apply (simp_all add: power_Suc zero_less_one mult_pos_pos) paulson@14348: done paulson@14348: paulson@14348: lemma zero_le_power: paulson@15004: "0 \ (a::'a::{ordered_semidom,recpower}) ==> 0 \ a^n" paulson@14348: apply (simp add: order_le_less) wenzelm@14577: apply (erule disjE) paulson@14348: apply (simp_all add: zero_less_power zero_less_one power_0_left) paulson@14348: done paulson@14348: paulson@14348: lemma one_le_power: paulson@15004: "1 \ (a::'a::{ordered_semidom,recpower}) ==> 1 \ a^n" paulson@15251: apply (induct "n") paulson@14348: apply (simp_all add: power_Suc) wenzelm@14577: apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) wenzelm@14577: apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) paulson@14348: done paulson@14348: obua@14738: lemma gt1_imp_ge0: "1 < a ==> 0 \ (a::'a::ordered_semidom)" paulson@14348: by (simp add: order_trans [OF zero_le_one order_less_imp_le]) paulson@14348: paulson@14348: lemma power_gt1_lemma: paulson@15004: assumes gt1: "1 < (a::'a::{ordered_semidom,recpower})" wenzelm@14577: shows "1 < a * a^n" paulson@14348: proof - wenzelm@14577: have "1*1 < a*1" using gt1 by simp wenzelm@14577: also have "\ \ a * a^n" using gt1 wenzelm@14577: by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le wenzelm@14577: zero_le_one order_refl) wenzelm@14577: finally show ?thesis by simp paulson@14348: qed paulson@14348: paulson@14348: lemma power_gt1: paulson@15004: "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)" paulson@14348: by (simp add: power_gt1_lemma power_Suc) paulson@14348: paulson@14348: lemma power_le_imp_le_exp: paulson@15004: assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a" wenzelm@14577: shows "!!n. a^m \ a^n ==> m \ n" wenzelm@14577: proof (induct m) paulson@14348: case 0 wenzelm@14577: show ?case by simp paulson@14348: next paulson@14348: case (Suc m) wenzelm@14577: show ?case wenzelm@14577: proof (cases n) wenzelm@14577: case 0 wenzelm@14577: from prems have "a * a^m \ 1" by (simp add: power_Suc) wenzelm@14577: with gt1 show ?thesis wenzelm@14577: by (force simp only: power_gt1_lemma wenzelm@14577: linorder_not_less [symmetric]) wenzelm@14577: next wenzelm@14577: case (Suc n) wenzelm@14577: from prems show ?thesis wenzelm@14577: by (force dest: mult_left_le_imp_le wenzelm@14577: simp add: power_Suc order_less_trans [OF zero_less_one gt1]) wenzelm@14577: qed paulson@14348: qed paulson@14348: wenzelm@14577: text{*Surely we can strengthen this? It holds for @{text "0 (a^m = a^n) = (m=n)" wenzelm@14577: by (force simp add: order_antisym power_le_imp_le_exp) paulson@14348: paulson@14348: text{*Can relax the first premise to @{term "0 m < n" wenzelm@14577: by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] wenzelm@14577: power_le_imp_le_exp) paulson@14348: paulson@14348: paulson@14348: lemma power_mono: paulson@15004: "[|a \ b; (0::'a::{recpower,ordered_semidom}) \ a|] ==> a^n \ b^n" paulson@15251: apply (induct "n") paulson@14348: apply (simp_all add: power_Suc) paulson@14348: apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b]) paulson@14348: done paulson@14348: paulson@14348: lemma power_strict_mono [rule_format]: paulson@15004: "[|a < b; (0::'a::{recpower,ordered_semidom}) \ a|] wenzelm@14577: ==> 0 < n --> a^n < b^n" paulson@15251: apply (induct "n") paulson@14348: apply (auto simp add: mult_strict_mono zero_le_power power_Suc paulson@14348: order_le_less_trans [of 0 a b]) paulson@14348: done paulson@14348: paulson@14348: lemma power_eq_0_iff [simp]: paulson@15004: "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0 (0::'a::{field,recpower}) ==> a^n \ 0" paulson@14348: by force paulson@14348: paulson@14353: lemma nonzero_power_inverse: paulson@15004: "a \ 0 ==> inverse ((a::'a::{field,recpower}) ^ n) = (inverse a) ^ n" paulson@15251: apply (induct "n") paulson@14353: apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute) paulson@14353: done paulson@14353: paulson@14348: text{*Perhaps these should be simprules.*} paulson@14348: lemma power_inverse: paulson@15004: "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n" paulson@15251: apply (induct "n") paulson@14348: apply (auto simp add: power_Suc inverse_mult_distrib) paulson@14348: done paulson@14348: avigad@16775: lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = avigad@16775: (1 / a)^n" avigad@16775: apply (simp add: divide_inverse) avigad@16775: apply (rule power_inverse) avigad@16775: done avigad@16775: wenzelm@14577: lemma nonzero_power_divide: paulson@15004: "b \ 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)" paulson@14353: by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) paulson@14353: wenzelm@14577: lemma power_divide: paulson@15004: "(a/b) ^ n = ((a::'a::{field,division_by_zero,recpower}) ^ n / b ^ n)" paulson@14353: apply (case_tac "b=0", simp add: power_0_left) wenzelm@14577: apply (rule nonzero_power_divide) wenzelm@14577: apply assumption paulson@14353: done paulson@14353: paulson@15004: lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n" paulson@15251: apply (induct "n") paulson@14348: apply (auto simp add: power_Suc abs_mult) paulson@14348: done paulson@14348: paulson@14353: lemma zero_less_power_abs_iff [simp]: paulson@15004: "(0 < (abs a)^n) = (a \ (0::'a::{ordered_idom,recpower}) | n=0)" paulson@14353: proof (induct "n") paulson@14353: case 0 paulson@14353: show ?case by (simp add: zero_less_one) paulson@14353: next paulson@14353: case (Suc n) paulson@14353: show ?case by (force simp add: prems power_Suc zero_less_mult_iff) paulson@14353: qed paulson@14353: paulson@14353: lemma zero_le_power_abs [simp]: paulson@15004: "(0::'a::{ordered_idom,recpower}) \ (abs a)^n" huffman@22957: by (rule zero_le_power [OF abs_ge_zero]) paulson@14353: paulson@15004: lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,recpower}) ^ n" paulson@14348: proof - paulson@14348: have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) paulson@14348: thus ?thesis by (simp only: power_mult_distrib) paulson@14348: qed paulson@14348: paulson@14348: text{*Lemma for @{text power_strict_decreasing}*} paulson@14348: lemma power_Suc_less: paulson@15004: "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|] paulson@14348: ==> a * a^n < a^n" paulson@15251: apply (induct n) wenzelm@14577: apply (auto simp add: power_Suc mult_strict_left_mono) paulson@14348: done paulson@14348: paulson@14348: lemma power_strict_decreasing: paulson@15004: "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|] paulson@14348: ==> a^N < a^n" wenzelm@14577: apply (erule rev_mp) paulson@15251: apply (induct "N") wenzelm@14577: apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) wenzelm@14577: apply (rename_tac m) paulson@14348: apply (subgoal_tac "a * a^m < 1 * a^n", simp) wenzelm@14577: apply (rule mult_strict_mono) paulson@14348: apply (auto simp add: zero_le_power zero_less_one order_less_imp_le) paulson@14348: done paulson@14348: paulson@14348: text{*Proof resembles that of @{text power_strict_decreasing}*} paulson@14348: lemma power_decreasing: paulson@15004: "[|n \ N; 0 \ a; a \ (1::'a::{ordered_semidom,recpower})|] paulson@14348: ==> a^N \ a^n" wenzelm@14577: apply (erule rev_mp) paulson@15251: apply (induct "N") wenzelm@14577: apply (auto simp add: power_Suc le_Suc_eq) wenzelm@14577: apply (rename_tac m) paulson@14348: apply (subgoal_tac "a * a^m \ 1 * a^n", simp) wenzelm@14577: apply (rule mult_mono) paulson@14348: apply (auto simp add: zero_le_power zero_le_one) paulson@14348: done paulson@14348: paulson@14348: lemma power_Suc_less_one: paulson@15004: "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1" wenzelm@14577: apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) paulson@14348: done paulson@14348: paulson@14348: text{*Proof again resembles that of @{text power_strict_decreasing}*} paulson@14348: lemma power_increasing: paulson@15004: "[|n \ N; (1::'a::{ordered_semidom,recpower}) \ a|] ==> a^n \ a^N" wenzelm@14577: apply (erule rev_mp) paulson@15251: apply (induct "N") wenzelm@14577: apply (auto simp add: power_Suc le_Suc_eq) paulson@14348: apply (rename_tac m) paulson@14348: apply (subgoal_tac "1 * a^n \ a * a^m", simp) wenzelm@14577: apply (rule mult_mono) paulson@14348: apply (auto simp add: order_trans [OF zero_le_one] zero_le_power) paulson@14348: done paulson@14348: paulson@14348: text{*Lemma for @{text power_strict_increasing}*} paulson@14348: lemma power_less_power_Suc: paulson@15004: "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n" paulson@15251: apply (induct n) wenzelm@14577: apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) paulson@14348: done paulson@14348: paulson@14348: lemma power_strict_increasing: paulson@15004: "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N" wenzelm@14577: apply (erule rev_mp) paulson@15251: apply (induct "N") wenzelm@14577: apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) paulson@14348: apply (rename_tac m) paulson@14348: apply (subgoal_tac "1 * a^n < a * a^m", simp) wenzelm@14577: apply (rule mult_strict_mono) paulson@14348: apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power paulson@14348: order_less_imp_le) paulson@14348: done paulson@14348: paulson@15066: lemma power_increasing_iff [simp]: paulson@15066: "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \ b ^ y) = (x \ y)" paulson@15066: by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) paulson@15066: paulson@15066: lemma power_strict_increasing_iff [simp]: paulson@15066: "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)" paulson@15066: by (blast intro: power_less_imp_less_exp power_strict_increasing) paulson@15066: paulson@14348: lemma power_le_imp_le_base: paulson@14348: assumes le: "a ^ Suc n \ b ^ Suc n" huffman@22624: and ynonneg: "(0::'a::{ordered_semidom,recpower}) \ b" paulson@14348: shows "a \ b" paulson@14348: proof (rule ccontr) paulson@14348: assume "~ a \ b" paulson@14348: then have "b < a" by (simp only: linorder_not_le) paulson@14348: then have "b ^ Suc n < a ^ Suc n" wenzelm@14577: by (simp only: prems power_strict_mono) paulson@14348: from le and this show "False" paulson@14348: by (simp add: linorder_not_less [symmetric]) paulson@14348: qed wenzelm@14577: huffman@22853: lemma power_less_imp_less_base: huffman@22853: fixes a b :: "'a::{ordered_semidom,recpower}" huffman@22853: assumes less: "a ^ n < b ^ n" huffman@22853: assumes nonneg: "0 \ b" huffman@22853: shows "a < b" huffman@22853: proof (rule contrapos_pp [OF less]) huffman@22853: assume "~ a < b" huffman@22853: hence "b \ a" by (simp only: linorder_not_less) huffman@22853: hence "b ^ n \ a ^ n" using nonneg by (rule power_mono) huffman@22853: thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less) huffman@22853: qed huffman@22853: paulson@14348: lemma power_inject_base: wenzelm@14577: "[| a ^ Suc n = b ^ Suc n; 0 \ a; 0 \ b |] paulson@15004: ==> a = (b::'a::{ordered_semidom,recpower})" paulson@14348: by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) paulson@14348: huffman@22955: lemma power_eq_imp_eq_base: huffman@22955: fixes a b :: "'a::{ordered_semidom,recpower}" huffman@22955: shows "\a ^ n = b ^ n; 0 \ a; 0 \ b; 0 < n\ \ a = b" huffman@22955: by (cases n, simp_all, rule power_inject_base) huffman@22955: paulson@14348: paulson@14348: subsection{*Exponentiation for the Natural Numbers*} paulson@3390: haftmann@21456: instance nat :: power .. haftmann@21456: wenzelm@8844: primrec (power) paulson@3390: "p ^ 0 = 1" paulson@3390: "p ^ (Suc n) = (p::nat) * (p ^ n)" wenzelm@14577: paulson@15004: instance nat :: recpower paulson@14348: proof paulson@14438: fix z n :: nat paulson@14348: show "z^0 = 1" by simp paulson@14348: show "z^(Suc n) = z * (z^n)" by simp paulson@14348: qed paulson@14348: paulson@14348: lemma nat_one_le_power [simp]: "1 \ i ==> Suc 0 \ i^n" paulson@14348: by (insert one_le_power [of i n], simp) paulson@14348: haftmann@21413: lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \ (0::nat) | n=0)" haftmann@21413: by (induct "n", auto) paulson@14348: paulson@14348: text{*Valid for the naturals, but what if @{text"0nat)" haftmann@21413: assumes less: "i^m < i^n" haftmann@21413: shows "m < n" haftmann@21413: proof (cases "i = 1") haftmann@21413: case True with less power_one [where 'a = nat] show ?thesis by simp haftmann@21413: next haftmann@21413: case False with nonneg have "1 < i" by auto haftmann@21413: from power_strict_increasing_iff [OF this] less show ?thesis .. haftmann@21413: qed paulson@14348: ballarin@17149: lemma power_diff: ballarin@17149: assumes nz: "a ~= 0" ballarin@17149: shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)" ballarin@17149: by (induct m n rule: diff_induct) ballarin@17149: (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz) ballarin@17149: ballarin@17149: paulson@14348: text{*ML bindings for the general exponentiation theorems*} paulson@14348: ML paulson@14348: {* paulson@14348: val power_0 = thm"power_0"; paulson@14348: val power_Suc = thm"power_Suc"; paulson@14348: val power_0_Suc = thm"power_0_Suc"; paulson@14348: val power_0_left = thm"power_0_left"; paulson@14348: val power_one = thm"power_one"; paulson@14348: val power_one_right = thm"power_one_right"; paulson@14348: val power_add = thm"power_add"; paulson@14348: val power_mult = thm"power_mult"; paulson@14348: val power_mult_distrib = thm"power_mult_distrib"; paulson@14348: val zero_less_power = thm"zero_less_power"; paulson@14348: val zero_le_power = thm"zero_le_power"; paulson@14348: val one_le_power = thm"one_le_power"; paulson@14348: val gt1_imp_ge0 = thm"gt1_imp_ge0"; paulson@14348: val power_gt1_lemma = thm"power_gt1_lemma"; paulson@14348: val power_gt1 = thm"power_gt1"; paulson@14348: val power_le_imp_le_exp = thm"power_le_imp_le_exp"; paulson@14348: val power_inject_exp = thm"power_inject_exp"; paulson@14348: val power_less_imp_less_exp = thm"power_less_imp_less_exp"; paulson@14348: val power_mono = thm"power_mono"; paulson@14348: val power_strict_mono = thm"power_strict_mono"; paulson@14348: val power_eq_0_iff = thm"power_eq_0_iff"; paulson@14348: val field_power_eq_0_iff = thm"field_power_eq_0_iff"; paulson@14348: val field_power_not_zero = thm"field_power_not_zero"; paulson@14348: val power_inverse = thm"power_inverse"; paulson@14353: val nonzero_power_divide = thm"nonzero_power_divide"; paulson@14353: val power_divide = thm"power_divide"; paulson@14348: val power_abs = thm"power_abs"; paulson@14353: val zero_less_power_abs_iff = thm"zero_less_power_abs_iff"; paulson@14353: val zero_le_power_abs = thm "zero_le_power_abs"; paulson@14348: val power_minus = thm"power_minus"; paulson@14348: val power_Suc_less = thm"power_Suc_less"; paulson@14348: val power_strict_decreasing = thm"power_strict_decreasing"; paulson@14348: val power_decreasing = thm"power_decreasing"; paulson@14348: val power_Suc_less_one = thm"power_Suc_less_one"; paulson@14348: val power_increasing = thm"power_increasing"; paulson@14348: val power_strict_increasing = thm"power_strict_increasing"; paulson@14348: val power_le_imp_le_base = thm"power_le_imp_le_base"; paulson@14348: val power_inject_base = thm"power_inject_base"; paulson@14348: *} wenzelm@14577: paulson@14348: text{*ML bindings for the remaining theorems*} paulson@14348: ML paulson@14348: {* paulson@14348: val nat_one_le_power = thm"nat_one_le_power"; paulson@14348: val nat_power_less_imp_less = thm"nat_power_less_imp_less"; paulson@14348: val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; paulson@14348: *} paulson@3390: paulson@3390: end paulson@3390: