paulson@3390: (* Title: HOL/Power.thy paulson@3390: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@3390: Copyright 1997 University of Cambridge paulson@3390: *) paulson@3390: haftmann@30960: header {* Exponentiation *} paulson@14348: nipkow@15131: theory Power huffman@47191: imports Num nipkow@15131: begin paulson@14348: haftmann@30960: subsection {* Powers for Arbitrary Monoids *} haftmann@30960: haftmann@30996: class power = one + times haftmann@30960: begin haftmann@24996: haftmann@30960: primrec power :: "'a \ nat \ 'a" (infixr "^" 80) where haftmann@30960: power_0: "a ^ 0 = 1" haftmann@30960: | power_Suc: "a ^ Suc n = a * a ^ n" paulson@14348: haftmann@30996: notation (latex output) haftmann@30996: power ("(_\<^bsup>_\<^esup>)" [1000] 1000) haftmann@30996: haftmann@30996: notation (HTML output) haftmann@30996: power ("(_\<^bsup>_\<^esup>)" [1000] 1000) haftmann@30996: huffman@47192: text {* Special syntax for squares. *} huffman@47192: huffman@47192: abbreviation (xsymbols) huffman@47192: power2 :: "'a \ 'a" ("(_\)" [1000] 999) where huffman@47192: "x\ \ x ^ 2" huffman@47192: huffman@47192: notation (latex output) huffman@47192: power2 ("(_\)" [1000] 999) huffman@47192: huffman@47192: notation (HTML output) huffman@47192: power2 ("(_\)" [1000] 999) huffman@47192: haftmann@30960: end paulson@14348: haftmann@30996: context monoid_mult haftmann@30996: begin paulson@14348: wenzelm@39438: subclass power . paulson@14348: haftmann@30996: lemma power_one [simp]: haftmann@30996: "1 ^ n = 1" huffman@30273: by (induct n) simp_all paulson@14348: haftmann@30996: lemma power_one_right [simp]: haftmann@31001: "a ^ 1 = a" haftmann@30996: by simp paulson@14348: haftmann@30996: lemma power_commutes: haftmann@30996: "a ^ n * a = a * a ^ n" huffman@30273: by (induct n) (simp_all add: mult_assoc) krauss@21199: haftmann@30996: lemma power_Suc2: haftmann@30996: "a ^ Suc n = a ^ n * a" huffman@30273: by (simp add: power_commutes) huffman@28131: haftmann@30996: lemma power_add: haftmann@30996: "a ^ (m + n) = a ^ m * a ^ n" haftmann@30996: by (induct m) (simp_all add: algebra_simps) paulson@14348: haftmann@30996: lemma power_mult: haftmann@30996: "a ^ (m * n) = (a ^ m) ^ n" huffman@30273: by (induct n) (simp_all add: power_add) paulson@14348: huffman@47192: lemma power2_eq_square: "a\ = a * a" huffman@47192: by (simp add: numeral_2_eq_2) huffman@47192: huffman@47192: lemma power3_eq_cube: "a ^ 3 = a * a * a" huffman@47192: by (simp add: numeral_3_eq_3 mult_assoc) huffman@47192: huffman@47192: lemma power_even_eq: huffman@47192: "a ^ (2*n) = (a ^ n) ^ 2" huffman@47192: by (subst mult_commute) (simp add: power_mult) huffman@47192: huffman@47192: lemma power_odd_eq: huffman@47192: "a ^ Suc (2*n) = a * (a ^ n) ^ 2" huffman@47192: by (simp add: power_even_eq) huffman@47192: huffman@47255: lemma power_numeral_even: huffman@47255: "z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" huffman@47255: unfolding numeral_Bit0 power_add Let_def .. huffman@47255: huffman@47255: lemma power_numeral_odd: huffman@47255: "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" huffman@47255: unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right huffman@47255: unfolding power_Suc power_add Let_def mult_assoc .. huffman@47255: haftmann@30996: end haftmann@30996: haftmann@30996: context comm_monoid_mult haftmann@30996: begin haftmann@30996: haftmann@30996: lemma power_mult_distrib: haftmann@30996: "(a * b) ^ n = (a ^ n) * (b ^ n)" huffman@30273: by (induct n) (simp_all add: mult_ac) paulson@14348: haftmann@30996: end haftmann@30996: huffman@47191: context semiring_numeral huffman@47191: begin huffman@47191: huffman@47191: lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" huffman@47191: by (simp only: sqr_conv_mult numeral_mult) huffman@47191: huffman@47191: lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" huffman@47191: by (induct l, simp_all only: numeral_class.numeral.simps pow.simps huffman@47191: numeral_sqr numeral_mult power_add power_one_right) huffman@47191: huffman@47191: lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" huffman@47191: by (rule numeral_pow [symmetric]) huffman@47191: huffman@47191: end huffman@47191: haftmann@30996: context semiring_1 haftmann@30996: begin haftmann@30996: haftmann@30996: lemma of_nat_power: haftmann@30996: "of_nat (m ^ n) = of_nat m ^ n" haftmann@30996: by (induct n) (simp_all add: of_nat_mult) haftmann@30996: huffman@47191: lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0" huffman@47209: by (simp add: numeral_eq_Suc) huffman@47191: huffman@47192: lemma zero_power2: "0\ = 0" (* delete? *) huffman@47192: by (rule power_zero_numeral) huffman@47192: huffman@47192: lemma one_power2: "1\ = 1" (* delete? *) huffman@47192: by (rule power_one) huffman@47192: haftmann@30996: end haftmann@30996: haftmann@30996: context comm_semiring_1 haftmann@30996: begin haftmann@30996: haftmann@30996: text {* The divides relation *} haftmann@30996: haftmann@30996: lemma le_imp_power_dvd: haftmann@30996: assumes "m \ n" shows "a ^ m dvd a ^ n" haftmann@30996: proof haftmann@30996: have "a ^ n = a ^ (m + (n - m))" haftmann@30996: using `m \ n` by simp haftmann@30996: also have "\ = a ^ m * a ^ (n - m)" haftmann@30996: by (rule power_add) haftmann@30996: finally show "a ^ n = a ^ m * a ^ (n - m)" . haftmann@30996: qed haftmann@30996: haftmann@30996: lemma power_le_dvd: haftmann@30996: "a ^ n dvd b \ m \ n \ a ^ m dvd b" haftmann@30996: by (rule dvd_trans [OF le_imp_power_dvd]) haftmann@30996: haftmann@30996: lemma dvd_power_same: haftmann@30996: "x dvd y \ x ^ n dvd y ^ n" haftmann@30996: by (induct n) (auto simp add: mult_dvd_mono) haftmann@30996: haftmann@30996: lemma dvd_power_le: haftmann@30996: "x dvd y \ m \ n \ x ^ n dvd y ^ m" haftmann@30996: by (rule power_le_dvd [OF dvd_power_same]) paulson@14348: haftmann@30996: lemma dvd_power [simp]: haftmann@30996: assumes "n > (0::nat) \ x = 1" haftmann@30996: shows "x dvd (x ^ n)" haftmann@30996: using assms proof haftmann@30996: assume "0 < n" haftmann@30996: then have "x ^ n = x ^ Suc (n - 1)" by simp haftmann@30996: then show "x dvd (x ^ n)" by simp haftmann@30996: next haftmann@30996: assume "x = 1" haftmann@30996: then show "x dvd (x ^ n)" by simp haftmann@30996: qed haftmann@30996: haftmann@30996: end haftmann@30996: haftmann@30996: context ring_1 haftmann@30996: begin haftmann@30996: haftmann@30996: lemma power_minus: haftmann@30996: "(- a) ^ n = (- 1) ^ n * a ^ n" haftmann@30996: proof (induct n) haftmann@30996: case 0 show ?case by simp haftmann@30996: next haftmann@30996: case (Suc n) then show ?case haftmann@30996: by (simp del: power_Suc add: power_Suc2 mult_assoc) haftmann@30996: qed haftmann@30996: huffman@47191: lemma power_minus_Bit0: huffman@47191: "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" huffman@47191: by (induct k, simp_all only: numeral_class.numeral.simps power_add huffman@47191: power_one_right mult_minus_left mult_minus_right minus_minus) huffman@47191: huffman@47191: lemma power_minus_Bit1: huffman@47191: "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))" huffman@47220: by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) huffman@47191: huffman@47191: lemma power_neg_numeral_Bit0 [simp]: huffman@47191: "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))" huffman@47191: by (simp only: neg_numeral_def power_minus_Bit0 power_numeral) huffman@47191: huffman@47191: lemma power_neg_numeral_Bit1 [simp]: huffman@47191: "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))" huffman@47191: by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps) huffman@47191: huffman@47192: lemma power2_minus [simp]: huffman@47192: "(- a)\ = a\" huffman@47192: by (rule power_minus_Bit0) huffman@47192: huffman@47192: lemma power_minus1_even [simp]: huffman@47192: "-1 ^ (2*n) = 1" huffman@47192: proof (induct n) huffman@47192: case 0 show ?case by simp huffman@47192: next huffman@47192: case (Suc n) then show ?case by (simp add: power_add power2_eq_square) huffman@47192: qed huffman@47192: huffman@47192: lemma power_minus1_odd: huffman@47192: "-1 ^ Suc (2*n) = -1" huffman@47192: by simp huffman@47192: huffman@47192: lemma power_minus_even [simp]: huffman@47192: "(-a) ^ (2*n) = a ^ (2*n)" huffman@47192: by (simp add: power_minus [of a]) huffman@47192: huffman@47192: end huffman@47192: huffman@47192: context ring_1_no_zero_divisors huffman@47192: begin huffman@47192: huffman@47192: lemma field_power_not_zero: huffman@47192: "a \ 0 \ a ^ n \ 0" huffman@47192: by (induct n) auto huffman@47192: huffman@47192: lemma zero_eq_power2 [simp]: huffman@47192: "a\ = 0 \ a = 0" huffman@47192: unfolding power2_eq_square by simp huffman@47192: huffman@47192: lemma power2_eq_1_iff: huffman@47192: "a\ = 1 \ a = 1 \ a = - 1" huffman@47192: unfolding power2_eq_square by (rule square_eq_1_iff) huffman@47192: huffman@47192: end huffman@47192: huffman@47192: context idom huffman@47192: begin huffman@47192: huffman@47192: lemma power2_eq_iff: "x\ = y\ \ x = y \ x = - y" huffman@47192: unfolding power2_eq_square by (rule square_eq_iff) huffman@47192: huffman@47192: end huffman@47192: huffman@47192: context division_ring huffman@47192: begin huffman@47192: huffman@47192: text {* FIXME reorient or rename to @{text nonzero_inverse_power} *} huffman@47192: lemma nonzero_power_inverse: huffman@47192: "a \ 0 \ inverse (a ^ n) = (inverse a) ^ n" huffman@47192: by (induct n) huffman@47192: (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero) huffman@47192: huffman@47192: end huffman@47192: huffman@47192: context field huffman@47192: begin huffman@47192: huffman@47192: lemma nonzero_power_divide: huffman@47192: "b \ 0 \ (a / b) ^ n = a ^ n / b ^ n" huffman@47192: by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) huffman@47192: huffman@47192: end huffman@47192: huffman@47192: huffman@47192: subsection {* Exponentiation on ordered types *} huffman@47192: huffman@47192: context linordered_ring (* TODO: move *) huffman@47192: begin huffman@47192: huffman@47192: lemma sum_squares_ge_zero: huffman@47192: "0 \ x * x + y * y" huffman@47192: by (intro add_nonneg_nonneg zero_le_square) huffman@47192: huffman@47192: lemma not_sum_squares_lt_zero: huffman@47192: "\ x * x + y * y < 0" huffman@47192: by (simp add: not_less sum_squares_ge_zero) huffman@47192: haftmann@30996: end haftmann@30996: haftmann@35028: context linordered_semidom haftmann@30996: begin haftmann@30996: haftmann@30996: lemma zero_less_power [simp]: haftmann@30996: "0 < a \ 0 < a ^ n" haftmann@30996: by (induct n) (simp_all add: mult_pos_pos) haftmann@30996: haftmann@30996: lemma zero_le_power [simp]: haftmann@30996: "0 \ a \ 0 \ a ^ n" haftmann@30996: by (induct n) (simp_all add: mult_nonneg_nonneg) paulson@14348: huffman@47241: lemma power_mono: huffman@47241: "a \ b \ 0 \ a \ a ^ n \ b ^ n" huffman@47241: by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) huffman@47241: huffman@47241: lemma one_le_power [simp]: "1 \ a \ 1 \ a ^ n" huffman@47241: using power_mono [of 1 a n] by simp huffman@47241: huffman@47241: lemma power_le_one: "\0 \ a; a \ 1\ \ a ^ n \ 1" huffman@47241: using power_mono [of a 1 n] by simp paulson@14348: paulson@14348: lemma power_gt1_lemma: haftmann@30996: assumes gt1: "1 < a" haftmann@30996: shows "1 < a * a ^ n" paulson@14348: proof - haftmann@30996: from gt1 have "0 \ a" haftmann@30996: by (fact order_trans [OF zero_le_one less_imp_le]) haftmann@30996: have "1 * 1 < a * 1" using gt1 by simp haftmann@30996: also have "\ \ a * a ^ n" using gt1 haftmann@30996: by (simp only: mult_mono `0 \ a` 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: haftmann@30996: lemma power_gt1: haftmann@30996: "1 < a \ 1 < a ^ Suc n" haftmann@30996: by (simp add: power_gt1_lemma) huffman@24376: haftmann@30996: lemma one_less_power [simp]: haftmann@30996: "1 < a \ 0 < n \ 1 < a ^ n" haftmann@30996: by (cases n) (simp_all add: power_gt1_lemma) paulson@14348: paulson@14348: lemma power_le_imp_le_exp: haftmann@30996: assumes gt1: "1 < a" haftmann@30996: shows "a ^ m \ a ^ n \ m \ n" haftmann@30996: proof (induct m arbitrary: n) 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 haftmann@30996: with Suc.prems Suc.hyps have "a * a ^ m \ 1" by simp wenzelm@14577: with gt1 show ?thesis wenzelm@14577: by (force simp only: power_gt1_lemma haftmann@30996: not_less [symmetric]) wenzelm@14577: next wenzelm@14577: case (Suc n) haftmann@30996: with Suc.prems Suc.hyps show ?thesis wenzelm@14577: by (force dest: mult_left_le_imp_le haftmann@30996: simp add: 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 a ^ m < a ^ n \ m < n" haftmann@30996: by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] haftmann@30996: power_le_imp_le_exp) paulson@14348: paulson@14348: lemma power_strict_mono [rule_format]: haftmann@30996: "a < b \ 0 \ a \ 0 < n \ a ^ n < b ^ n" haftmann@30996: by (induct n) haftmann@30996: (auto simp add: mult_strict_mono le_less_trans [of 0 a b]) paulson@14348: paulson@14348: text{*Lemma for @{text power_strict_decreasing}*} paulson@14348: lemma power_Suc_less: haftmann@30996: "0 < a \ a < 1 \ a * a ^ n < a ^ n" haftmann@30996: by (induct n) haftmann@30996: (auto simp add: mult_strict_left_mono) paulson@14348: haftmann@30996: lemma power_strict_decreasing [rule_format]: haftmann@30996: "n < N \ 0 < a \ a < 1 \ a ^ N < a ^ n" haftmann@30996: proof (induct N) haftmann@30996: case 0 then show ?case by simp haftmann@30996: next haftmann@30996: case (Suc N) then show ?case haftmann@30996: apply (auto simp add: power_Suc_less less_Suc_eq) haftmann@30996: apply (subgoal_tac "a * a^N < 1 * a^n") haftmann@30996: apply simp haftmann@30996: apply (rule mult_strict_mono) apply auto haftmann@30996: done haftmann@30996: qed paulson@14348: paulson@14348: text{*Proof resembles that of @{text power_strict_decreasing}*} haftmann@30996: lemma power_decreasing [rule_format]: haftmann@30996: "n \ N \ 0 \ a \ a \ 1 \ a ^ N \ a ^ n" haftmann@30996: proof (induct N) haftmann@30996: case 0 then show ?case by simp haftmann@30996: next haftmann@30996: case (Suc N) then show ?case haftmann@30996: apply (auto simp add: le_Suc_eq) haftmann@30996: apply (subgoal_tac "a * a^N \ 1 * a^n", simp) haftmann@30996: apply (rule mult_mono) apply auto haftmann@30996: done haftmann@30996: qed paulson@14348: paulson@14348: lemma power_Suc_less_one: haftmann@30996: "0 < a \ a < 1 \ a ^ Suc n < 1" haftmann@30996: using power_strict_decreasing [of 0 "Suc n" a] by simp paulson@14348: paulson@14348: text{*Proof again resembles that of @{text power_strict_decreasing}*} haftmann@30996: lemma power_increasing [rule_format]: haftmann@30996: "n \ N \ 1 \ a \ a ^ n \ a ^ N" haftmann@30996: proof (induct N) haftmann@30996: case 0 then show ?case by simp haftmann@30996: next haftmann@30996: case (Suc N) then show ?case haftmann@30996: apply (auto simp add: le_Suc_eq) haftmann@30996: apply (subgoal_tac "1 * a^n \ a * a^N", simp) haftmann@30996: apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) haftmann@30996: done haftmann@30996: qed paulson@14348: paulson@14348: text{*Lemma for @{text power_strict_increasing}*} paulson@14348: lemma power_less_power_Suc: haftmann@30996: "1 < a \ a ^ n < a * a ^ n" haftmann@30996: by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one]) paulson@14348: haftmann@30996: lemma power_strict_increasing [rule_format]: haftmann@30996: "n < N \ 1 < a \ a ^ n < a ^ N" haftmann@30996: proof (induct N) haftmann@30996: case 0 then show ?case by simp haftmann@30996: next haftmann@30996: case (Suc N) then show ?case haftmann@30996: apply (auto simp add: power_less_power_Suc less_Suc_eq) haftmann@30996: apply (subgoal_tac "1 * a^n < a * a^N", simp) haftmann@30996: apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) haftmann@30996: done haftmann@30996: qed paulson@14348: nipkow@25134: lemma power_increasing_iff [simp]: haftmann@30996: "1 < b \ b ^ x \ b ^ y \ x \ y" haftmann@30996: by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) paulson@15066: paulson@15066: lemma power_strict_increasing_iff [simp]: haftmann@30996: "1 < b \ b ^ x < b ^ y \ x < y" nipkow@25134: by (blast intro: power_less_imp_less_exp power_strict_increasing) paulson@15066: paulson@14348: lemma power_le_imp_le_base: haftmann@30996: assumes le: "a ^ Suc n \ b ^ Suc n" haftmann@30996: and ynonneg: "0 \ b" haftmann@30996: shows "a \ b" nipkow@25134: proof (rule ccontr) nipkow@25134: assume "~ a \ b" nipkow@25134: then have "b < a" by (simp only: linorder_not_le) nipkow@25134: then have "b ^ Suc n < a ^ Suc n" wenzelm@41550: by (simp only: assms power_strict_mono) haftmann@30996: from le and this show False nipkow@25134: by (simp add: linorder_not_less [symmetric]) nipkow@25134: qed wenzelm@14577: huffman@22853: lemma power_less_imp_less_base: 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) haftmann@30996: thus "\ a ^ n < b ^ n" by (simp only: linorder_not_less) huffman@22853: qed huffman@22853: paulson@14348: lemma power_inject_base: haftmann@30996: "a ^ Suc n = b ^ Suc n \ 0 \ a \ 0 \ b \ a = b" haftmann@30996: by (blast intro: power_le_imp_le_base antisym eq_refl sym) paulson@14348: huffman@22955: lemma power_eq_imp_eq_base: haftmann@30996: "a ^ n = b ^ n \ 0 \ a \ 0 \ b \ 0 < n \ a = b" haftmann@30996: by (cases n) (simp_all del: power_Suc, rule power_inject_base) huffman@22955: huffman@47192: lemma power2_le_imp_le: huffman@47192: "x\ \ y\ \ 0 \ y \ x \ y" huffman@47192: unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) huffman@47192: huffman@47192: lemma power2_less_imp_less: huffman@47192: "x\ < y\ \ 0 \ y \ x < y" huffman@47192: by (rule power_less_imp_less_base) huffman@47192: huffman@47192: lemma power2_eq_imp_eq: huffman@47192: "x\ = y\ \ 0 \ x \ 0 \ y \ x = y" huffman@47192: unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp huffman@47192: huffman@47192: end huffman@47192: huffman@47192: context linordered_ring_strict huffman@47192: begin huffman@47192: huffman@47192: lemma sum_squares_eq_zero_iff: huffman@47192: "x * x + y * y = 0 \ x = 0 \ y = 0" huffman@47192: by (simp add: add_nonneg_eq_0_iff) huffman@47192: huffman@47192: lemma sum_squares_le_zero_iff: huffman@47192: "x * x + y * y \ 0 \ x = 0 \ y = 0" huffman@47192: by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) huffman@47192: huffman@47192: lemma sum_squares_gt_zero_iff: huffman@47192: "0 < x * x + y * y \ x \ 0 \ y \ 0" huffman@47192: by (simp add: not_le [symmetric] sum_squares_le_zero_iff) huffman@47192: haftmann@30996: end haftmann@30996: haftmann@35028: context linordered_idom haftmann@30996: begin huffman@29978: haftmann@30996: lemma power_abs: haftmann@30996: "abs (a ^ n) = abs a ^ n" haftmann@30996: by (induct n) (auto simp add: abs_mult) haftmann@30996: haftmann@30996: lemma abs_power_minus [simp]: haftmann@30996: "abs ((-a) ^ n) = abs (a ^ n)" huffman@35216: by (simp add: power_abs) haftmann@30996: blanchet@35828: lemma zero_less_power_abs_iff [simp, no_atp]: haftmann@30996: "0 < abs a ^ n \ a \ 0 \ n = 0" haftmann@30996: proof (induct n) haftmann@30996: case 0 show ?case by simp haftmann@30996: next haftmann@30996: case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff) huffman@29978: qed huffman@29978: haftmann@30996: lemma zero_le_power_abs [simp]: haftmann@30996: "0 \ abs a ^ n" haftmann@30996: by (rule zero_le_power [OF abs_ge_zero]) haftmann@30996: huffman@47192: lemma zero_le_power2 [simp]: huffman@47192: "0 \ a\" huffman@47192: by (simp add: power2_eq_square) huffman@47192: huffman@47192: lemma zero_less_power2 [simp]: huffman@47192: "0 < a\ \ a \ 0" huffman@47192: by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) huffman@47192: huffman@47192: lemma power2_less_0 [simp]: huffman@47192: "\ a\ < 0" huffman@47192: by (force simp add: power2_eq_square mult_less_0_iff) huffman@47192: huffman@47192: lemma abs_power2 [simp]: huffman@47192: "abs (a\) = a\" huffman@47192: by (simp add: power2_eq_square abs_mult abs_mult_self) huffman@47192: huffman@47192: lemma power2_abs [simp]: huffman@47192: "(abs a)\ = a\" huffman@47192: by (simp add: power2_eq_square abs_mult_self) huffman@47192: huffman@47192: lemma odd_power_less_zero: huffman@47192: "a < 0 \ a ^ Suc (2*n) < 0" huffman@47192: proof (induct n) huffman@47192: case 0 huffman@47192: then show ?case by simp huffman@47192: next huffman@47192: case (Suc n) huffman@47192: have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" huffman@47192: by (simp add: mult_ac power_add power2_eq_square) huffman@47192: thus ?case huffman@47192: by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) huffman@47192: qed haftmann@30996: huffman@47192: lemma odd_0_le_power_imp_0_le: huffman@47192: "0 \ a ^ Suc (2*n) \ 0 \ a" huffman@47192: using odd_power_less_zero [of a n] huffman@47192: by (force simp add: linorder_not_less [symmetric]) huffman@47192: huffman@47192: lemma zero_le_even_power'[simp]: huffman@47192: "0 \ a ^ (2*n)" huffman@47192: proof (induct n) huffman@47192: case 0 huffman@47192: show ?case by simp huffman@47192: next huffman@47192: case (Suc n) huffman@47192: have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" huffman@47192: by (simp add: mult_ac power_add power2_eq_square) huffman@47192: thus ?case huffman@47192: by (simp add: Suc zero_le_mult_iff) huffman@47192: qed haftmann@30996: huffman@47192: lemma sum_power2_ge_zero: huffman@47192: "0 \ x\ + y\" huffman@47192: by (intro add_nonneg_nonneg zero_le_power2) huffman@47192: huffman@47192: lemma not_sum_power2_lt_zero: huffman@47192: "\ x\ + y\ < 0" huffman@47192: unfolding not_less by (rule sum_power2_ge_zero) huffman@47192: huffman@47192: lemma sum_power2_eq_zero_iff: huffman@47192: "x\ + y\ = 0 \ x = 0 \ y = 0" huffman@47192: unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) huffman@47192: huffman@47192: lemma sum_power2_le_zero_iff: huffman@47192: "x\ + y\ \ 0 \ x = 0 \ y = 0" huffman@47192: by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) huffman@47192: huffman@47192: lemma sum_power2_gt_zero_iff: huffman@47192: "0 < x\ + y\ \ x \ 0 \ y \ 0" huffman@47192: unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) haftmann@30996: haftmann@30996: end haftmann@30996: huffman@29978: huffman@47192: subsection {* Miscellaneous rules *} paulson@14348: huffman@47255: lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" huffman@47255: unfolding One_nat_def by (cases m) simp_all huffman@47255: huffman@47192: lemma power2_sum: huffman@47192: fixes x y :: "'a::comm_semiring_1" huffman@47192: shows "(x + y)\ = x\ + y\ + 2 * x * y" huffman@47192: by (simp add: algebra_simps power2_eq_square mult_2_right) haftmann@30996: huffman@47192: lemma power2_diff: huffman@47192: fixes x y :: "'a::comm_ring_1" huffman@47192: shows "(x - y)\ = x\ + y\ - 2 * x * y" huffman@47192: by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) haftmann@30996: haftmann@30996: lemma power_0_Suc [simp]: haftmann@30996: "(0::'a::{power, semiring_0}) ^ Suc n = 0" haftmann@30996: by simp nipkow@30313: haftmann@30996: text{*It looks plausible as a simprule, but its effect can be strange.*} haftmann@30996: lemma power_0_left: haftmann@30996: "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))" haftmann@30996: by (induct n) simp_all haftmann@30996: haftmann@30996: lemma power_eq_0_iff [simp]: haftmann@30996: "a ^ n = 0 \ haftmann@30996: a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \ n \ 0" haftmann@30996: by (induct n) haftmann@30996: (auto simp add: no_zero_divisors elim: contrapos_pp) haftmann@30996: haftmann@36409: lemma (in field) power_diff: haftmann@30996: assumes nz: "a \ 0" haftmann@30996: shows "n \ m \ a ^ (m - n) = a ^ m / a ^ n" haftmann@36409: by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero) nipkow@30313: haftmann@30996: text{*Perhaps these should be simprules.*} haftmann@30996: lemma power_inverse: haftmann@36409: fixes a :: "'a::division_ring_inverse_zero" haftmann@36409: shows "inverse (a ^ n) = inverse a ^ n" haftmann@30996: apply (cases "a = 0") haftmann@30996: apply (simp add: power_0_left) haftmann@30996: apply (simp add: nonzero_power_inverse) haftmann@30996: done (* TODO: reorient or rename to inverse_power *) haftmann@30996: haftmann@30996: lemma power_one_over: haftmann@36409: "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n" haftmann@30996: by (simp add: divide_inverse) (rule power_inverse) haftmann@30996: haftmann@30996: lemma power_divide: haftmann@36409: "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n" haftmann@30996: apply (cases "b = 0") haftmann@30996: apply (simp add: power_0_left) haftmann@30996: apply (rule nonzero_power_divide) haftmann@30996: apply assumption nipkow@30313: done nipkow@30313: huffman@47255: text {* Simprules for comparisons where common factors can be cancelled. *} huffman@47255: huffman@47255: lemmas zero_compare_simps = huffman@47255: add_strict_increasing add_strict_increasing2 add_increasing huffman@47255: zero_le_mult_iff zero_le_divide_iff huffman@47255: zero_less_mult_iff zero_less_divide_iff huffman@47255: mult_le_0_iff divide_le_0_iff huffman@47255: mult_less_0_iff divide_less_0_iff huffman@47255: zero_le_power2 power2_less_0 huffman@47255: nipkow@30313: haftmann@30960: subsection {* Exponentiation for the Natural Numbers *} wenzelm@14577: haftmann@30996: lemma nat_one_le_power [simp]: haftmann@30996: "Suc 0 \ i \ Suc 0 \ i ^ n" haftmann@30996: by (rule one_le_power [of i n, unfolded One_nat_def]) huffman@23305: haftmann@30996: lemma nat_zero_less_power_iff [simp]: haftmann@30996: "x ^ n > 0 \ x > (0::nat) \ n = 0" haftmann@30996: by (induct n) auto paulson@14348: nipkow@30056: lemma nat_power_eq_Suc_0_iff [simp]: haftmann@30996: "x ^ m = Suc 0 \ m = 0 \ x = Suc 0" haftmann@30996: by (induct m) auto nipkow@30056: haftmann@30996: lemma power_Suc_0 [simp]: haftmann@30996: "Suc 0 ^ n = Suc 0" haftmann@30996: by simp nipkow@30056: paulson@14348: text{*Valid for the naturals, but what if @{text"0nat)" haftmann@30996: 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: haftmann@33274: lemma power_dvd_imp_le: haftmann@33274: "i ^ m dvd i ^ n \ (1::nat) < i \ m \ n" haftmann@33274: apply (rule power_le_imp_le_exp, assumption) haftmann@33274: apply (erule dvd_imp_le, simp) haftmann@33274: done haftmann@33274: haftmann@31155: haftmann@31155: subsection {* Code generator tweak *} haftmann@31155: bulwahn@45231: lemma power_power_power [code]: haftmann@31155: "power = power.power (1::'a::{power}) (op *)" haftmann@31155: unfolding power_def power.power_def .. haftmann@31155: haftmann@31155: declare power.power.simps [code] haftmann@31155: haftmann@33364: code_modulename SML haftmann@33364: Power Arith haftmann@33364: haftmann@33364: code_modulename OCaml haftmann@33364: Power Arith haftmann@33364: haftmann@33364: code_modulename Haskell haftmann@33364: Power Arith haftmann@33364: paulson@3390: end