src/HOL/Power.thy
 author huffman Mon Feb 23 16:25:52 2009 -0800 (2009-02-23) changeset 30079 293b896b9c25 parent 30056 0a35bee25c20 child 30242 aea5d7fa7ef5 permissions -rw-r--r--
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
 paulson@3390 ` 1` ```(* Title: HOL/Power.thy ``` paulson@3390 ` 2` ``` ID: \$Id\$ ``` paulson@3390 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@3390 ` 4` ``` Copyright 1997 University of Cambridge ``` paulson@3390 ` 5` paulson@3390 ` 6` ```*) ``` paulson@3390 ` 7` nipkow@16733 ` 8` ```header{*Exponentiation*} ``` paulson@14348 ` 9` nipkow@15131 ` 10` ```theory Power ``` haftmann@21413 ` 11` ```imports Nat ``` nipkow@15131 ` 12` ```begin ``` paulson@14348 ` 13` haftmann@29608 ` 14` ```class power = ``` haftmann@25062 ` 15` ``` fixes power :: "'a \ nat \ 'a" (infixr "^" 80) ``` haftmann@24996 ` 16` krauss@21199 ` 17` ```subsection{*Powers for Arbitrary Monoids*} ``` paulson@14348 ` 18` haftmann@22390 ` 19` ```class recpower = monoid_mult + power + ``` haftmann@25062 ` 20` ``` assumes power_0 [simp]: "a ^ 0 = 1" ``` haftmann@25062 ` 21` ``` assumes power_Suc: "a ^ Suc n = a * (a ^ n)" ``` paulson@14348 ` 22` krauss@21199 ` 23` ```lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" ``` haftmann@23183 ` 24` ``` by (simp add: power_Suc) ``` paulson@14348 ` 25` paulson@14348 ` 26` ```text{*It looks plausible as a simprule, but its effect can be strange.*} ``` krauss@21199 ` 27` ```lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))" ``` haftmann@23183 ` 28` ``` by (induct n) simp_all ``` paulson@14348 ` 29` paulson@15004 ` 30` ```lemma power_one [simp]: "1^n = (1::'a::recpower)" ``` haftmann@23183 ` 31` ``` by (induct n) (simp_all add: power_Suc) ``` paulson@14348 ` 32` paulson@15004 ` 33` ```lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a" ``` huffman@30079 ` 34` ``` unfolding One_nat_def by (simp add: power_Suc) ``` paulson@14348 ` 35` krauss@21199 ` 36` ```lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n" ``` haftmann@23183 ` 37` ``` by (induct n) (simp_all add: power_Suc mult_assoc) ``` krauss@21199 ` 38` huffman@28131 ` 39` ```lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a" ``` huffman@28131 ` 40` ``` by (simp add: power_Suc power_commutes) ``` huffman@28131 ` 41` paulson@15004 ` 42` ```lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)" ``` haftmann@23183 ` 43` ``` by (induct m) (simp_all add: power_Suc mult_ac) ``` paulson@14348 ` 44` paulson@15004 ` 45` ```lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n" ``` haftmann@23183 ` 46` ``` by (induct n) (simp_all add: power_Suc power_add) ``` paulson@14348 ` 47` krauss@21199 ` 48` ```lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)" ``` haftmann@23183 ` 49` ``` by (induct n) (simp_all add: power_Suc mult_ac) ``` paulson@14348 ` 50` nipkow@25874 ` 51` ```lemma zero_less_power[simp]: ``` paulson@15004 ` 52` ``` "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" ``` paulson@15251 ` 53` ```apply (induct "n") ``` avigad@16775 ` 54` ```apply (simp_all add: power_Suc zero_less_one mult_pos_pos) ``` paulson@14348 ` 55` ```done ``` paulson@14348 ` 56` nipkow@25874 ` 57` ```lemma zero_le_power[simp]: ``` paulson@15004 ` 58` ``` "0 \ (a::'a::{ordered_semidom,recpower}) ==> 0 \ a^n" ``` paulson@14348 ` 59` ```apply (simp add: order_le_less) ``` wenzelm@14577 ` 60` ```apply (erule disjE) ``` nipkow@25874 ` 61` ```apply (simp_all add: zero_less_one power_0_left) ``` paulson@14348 ` 62` ```done ``` paulson@14348 ` 63` nipkow@25874 ` 64` ```lemma one_le_power[simp]: ``` paulson@15004 ` 65` ``` "1 \ (a::'a::{ordered_semidom,recpower}) ==> 1 \ a^n" ``` paulson@15251 ` 66` ```apply (induct "n") ``` paulson@14348 ` 67` ```apply (simp_all add: power_Suc) ``` wenzelm@14577 ` 68` ```apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) ``` wenzelm@14577 ` 69` ```apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) ``` paulson@14348 ` 70` ```done ``` paulson@14348 ` 71` obua@14738 ` 72` ```lemma gt1_imp_ge0: "1 < a ==> 0 \ (a::'a::ordered_semidom)" ``` paulson@14348 ` 73` ``` by (simp add: order_trans [OF zero_le_one order_less_imp_le]) ``` paulson@14348 ` 74` paulson@14348 ` 75` ```lemma power_gt1_lemma: ``` paulson@15004 ` 76` ``` assumes gt1: "1 < (a::'a::{ordered_semidom,recpower})" ``` wenzelm@14577 ` 77` ``` shows "1 < a * a^n" ``` paulson@14348 ` 78` ```proof - ``` wenzelm@14577 ` 79` ``` have "1*1 < a*1" using gt1 by simp ``` wenzelm@14577 ` 80` ``` also have "\ \ a * a^n" using gt1 ``` wenzelm@14577 ` 81` ``` by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le ``` wenzelm@14577 ` 82` ``` zero_le_one order_refl) ``` wenzelm@14577 ` 83` ``` finally show ?thesis by simp ``` paulson@14348 ` 84` ```qed ``` paulson@14348 ` 85` nipkow@25874 ` 86` ```lemma one_less_power[simp]: ``` huffman@24376 ` 87` ``` "\1 < (a::'a::{ordered_semidom,recpower}); 0 < n\ \ 1 < a ^ n" ``` huffman@24376 ` 88` ```by (cases n, simp_all add: power_gt1_lemma power_Suc) ``` huffman@24376 ` 89` paulson@14348 ` 90` ```lemma power_gt1: ``` paulson@15004 ` 91` ``` "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)" ``` paulson@14348 ` 92` ```by (simp add: power_gt1_lemma power_Suc) ``` paulson@14348 ` 93` paulson@14348 ` 94` ```lemma power_le_imp_le_exp: ``` paulson@15004 ` 95` ``` assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a" ``` wenzelm@14577 ` 96` ``` shows "!!n. a^m \ a^n ==> m \ n" ``` wenzelm@14577 ` 97` ```proof (induct m) ``` paulson@14348 ` 98` ``` case 0 ``` wenzelm@14577 ` 99` ``` show ?case by simp ``` paulson@14348 ` 100` ```next ``` paulson@14348 ` 101` ``` case (Suc m) ``` wenzelm@14577 ` 102` ``` show ?case ``` wenzelm@14577 ` 103` ``` proof (cases n) ``` wenzelm@14577 ` 104` ``` case 0 ``` wenzelm@14577 ` 105` ``` from prems have "a * a^m \ 1" by (simp add: power_Suc) ``` wenzelm@14577 ` 106` ``` with gt1 show ?thesis ``` wenzelm@14577 ` 107` ``` by (force simp only: power_gt1_lemma ``` wenzelm@14577 ` 108` ``` linorder_not_less [symmetric]) ``` wenzelm@14577 ` 109` ``` next ``` wenzelm@14577 ` 110` ``` case (Suc n) ``` wenzelm@14577 ` 111` ``` from prems show ?thesis ``` wenzelm@14577 ` 112` ``` by (force dest: mult_left_le_imp_le ``` wenzelm@14577 ` 113` ``` simp add: power_Suc order_less_trans [OF zero_less_one gt1]) ``` wenzelm@14577 ` 114` ``` qed ``` paulson@14348 ` 115` ```qed ``` paulson@14348 ` 116` wenzelm@14577 ` 117` ```text{*Surely we can strengthen this? It holds for @{text "0 (a^m = a^n) = (m=n)" ``` wenzelm@14577 ` 120` ``` by (force simp add: order_antisym power_le_imp_le_exp) ``` paulson@14348 ` 121` paulson@14348 ` 122` ```text{*Can relax the first premise to @{term "0 m < n" ``` wenzelm@14577 ` 126` ```by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] ``` wenzelm@14577 ` 127` ``` power_le_imp_le_exp) ``` paulson@14348 ` 128` paulson@14348 ` 129` paulson@14348 ` 130` ```lemma power_mono: ``` paulson@15004 ` 131` ``` "[|a \ b; (0::'a::{recpower,ordered_semidom}) \ a|] ==> a^n \ b^n" ``` paulson@15251 ` 132` ```apply (induct "n") ``` paulson@14348 ` 133` ```apply (simp_all add: power_Suc) ``` nipkow@25874 ` 134` ```apply (auto intro: mult_mono order_trans [of 0 a b]) ``` paulson@14348 ` 135` ```done ``` paulson@14348 ` 136` paulson@14348 ` 137` ```lemma power_strict_mono [rule_format]: ``` paulson@15004 ` 138` ``` "[|a < b; (0::'a::{recpower,ordered_semidom}) \ a|] ``` wenzelm@14577 ` 139` ``` ==> 0 < n --> a^n < b^n" ``` paulson@15251 ` 140` ```apply (induct "n") ``` nipkow@25874 ` 141` ```apply (auto simp add: mult_strict_mono power_Suc ``` paulson@14348 ` 142` ``` order_le_less_trans [of 0 a b]) ``` paulson@14348 ` 143` ```done ``` paulson@14348 ` 144` paulson@14348 ` 145` ```lemma power_eq_0_iff [simp]: ``` nipkow@30056 ` 146` ``` "(a^n = 0) \ ``` nipkow@30056 ` 147` ``` (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\0)" ``` paulson@15251 ` 148` ```apply (induct "n") ``` nipkow@30056 ` 149` ```apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors) ``` paulson@14348 ` 150` ```done ``` paulson@14348 ` 151` nipkow@30056 ` 152` nipkow@25134 ` 153` ```lemma field_power_not_zero: ``` nipkow@25134 ` 154` ``` "a \ (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \ 0" ``` paulson@14348 ` 155` ```by force ``` paulson@14348 ` 156` paulson@14353 ` 157` ```lemma nonzero_power_inverse: ``` huffman@22991 ` 158` ``` fixes a :: "'a::{division_ring,recpower}" ``` huffman@22991 ` 159` ``` shows "a \ 0 ==> inverse (a ^ n) = (inverse a) ^ n" ``` paulson@15251 ` 160` ```apply (induct "n") ``` huffman@22988 ` 161` ```apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes) ``` huffman@22991 ` 162` ```done (* TODO: reorient or rename to nonzero_inverse_power *) ``` paulson@14353 ` 163` paulson@14348 ` 164` ```text{*Perhaps these should be simprules.*} ``` paulson@14348 ` 165` ```lemma power_inverse: ``` huffman@22991 ` 166` ``` fixes a :: "'a::{division_ring,division_by_zero,recpower}" ``` huffman@22991 ` 167` ``` shows "inverse (a ^ n) = (inverse a) ^ n" ``` huffman@22991 ` 168` ```apply (cases "a = 0") ``` huffman@22991 ` 169` ```apply (simp add: power_0_left) ``` huffman@22991 ` 170` ```apply (simp add: nonzero_power_inverse) ``` huffman@22991 ` 171` ```done (* TODO: reorient or rename to inverse_power *) ``` paulson@14348 ` 172` avigad@16775 ` 173` ```lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = ``` avigad@16775 ` 174` ``` (1 / a)^n" ``` avigad@16775 ` 175` ```apply (simp add: divide_inverse) ``` avigad@16775 ` 176` ```apply (rule power_inverse) ``` avigad@16775 ` 177` ```done ``` avigad@16775 ` 178` wenzelm@14577 ` 179` ```lemma nonzero_power_divide: ``` paulson@15004 ` 180` ``` "b \ 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)" ``` paulson@14353 ` 181` ```by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) ``` paulson@14353 ` 182` wenzelm@14577 ` 183` ```lemma power_divide: ``` paulson@15004 ` 184` ``` "(a/b) ^ n = ((a::'a::{field,division_by_zero,recpower}) ^ n / b ^ n)" ``` paulson@14353 ` 185` ```apply (case_tac "b=0", simp add: power_0_left) ``` wenzelm@14577 ` 186` ```apply (rule nonzero_power_divide) ``` wenzelm@14577 ` 187` ```apply assumption ``` paulson@14353 ` 188` ```done ``` paulson@14353 ` 189` paulson@15004 ` 190` ```lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n" ``` paulson@15251 ` 191` ```apply (induct "n") ``` paulson@14348 ` 192` ```apply (auto simp add: power_Suc abs_mult) ``` paulson@14348 ` 193` ```done ``` paulson@14348 ` 194` paulson@24286 ` 195` ```lemma zero_less_power_abs_iff [simp,noatp]: ``` paulson@15004 ` 196` ``` "(0 < (abs a)^n) = (a \ (0::'a::{ordered_idom,recpower}) | n=0)" ``` paulson@14353 ` 197` ```proof (induct "n") ``` paulson@14353 ` 198` ``` case 0 ``` paulson@14353 ` 199` ``` show ?case by (simp add: zero_less_one) ``` paulson@14353 ` 200` ```next ``` paulson@14353 ` 201` ``` case (Suc n) ``` haftmann@25231 ` 202` ``` show ?case by (auto simp add: prems power_Suc zero_less_mult_iff ``` haftmann@25231 ` 203` ``` abs_zero) ``` paulson@14353 ` 204` ```qed ``` paulson@14353 ` 205` paulson@14353 ` 206` ```lemma zero_le_power_abs [simp]: ``` paulson@15004 ` 207` ``` "(0::'a::{ordered_idom,recpower}) \ (abs a)^n" ``` huffman@22957 ` 208` ```by (rule zero_le_power [OF abs_ge_zero]) ``` paulson@14353 ` 209` huffman@28131 ` 210` ```lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring_1,recpower}) ^ n" ``` huffman@28131 ` 211` ```proof (induct n) ``` huffman@28131 ` 212` ``` case 0 show ?case by simp ``` huffman@28131 ` 213` ```next ``` huffman@28131 ` 214` ``` case (Suc n) then show ?case ``` huffman@28131 ` 215` ``` by (simp add: power_Suc2 mult_assoc) ``` paulson@14348 ` 216` ```qed ``` paulson@14348 ` 217` paulson@14348 ` 218` ```text{*Lemma for @{text power_strict_decreasing}*} ``` paulson@14348 ` 219` ```lemma power_Suc_less: ``` paulson@15004 ` 220` ``` "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|] ``` paulson@14348 ` 221` ``` ==> a * a^n < a^n" ``` paulson@15251 ` 222` ```apply (induct n) ``` wenzelm@14577 ` 223` ```apply (auto simp add: power_Suc mult_strict_left_mono) ``` paulson@14348 ` 224` ```done ``` paulson@14348 ` 225` paulson@14348 ` 226` ```lemma power_strict_decreasing: ``` paulson@15004 ` 227` ``` "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|] ``` paulson@14348 ` 228` ``` ==> a^N < a^n" ``` wenzelm@14577 ` 229` ```apply (erule rev_mp) ``` paulson@15251 ` 230` ```apply (induct "N") ``` wenzelm@14577 ` 231` ```apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) ``` wenzelm@14577 ` 232` ```apply (rename_tac m) ``` paulson@14348 ` 233` ```apply (subgoal_tac "a * a^m < 1 * a^n", simp) ``` wenzelm@14577 ` 234` ```apply (rule mult_strict_mono) ``` nipkow@25874 ` 235` ```apply (auto simp add: zero_less_one order_less_imp_le) ``` paulson@14348 ` 236` ```done ``` paulson@14348 ` 237` paulson@14348 ` 238` ```text{*Proof resembles that of @{text power_strict_decreasing}*} ``` paulson@14348 ` 239` ```lemma power_decreasing: ``` paulson@15004 ` 240` ``` "[|n \ N; 0 \ a; a \ (1::'a::{ordered_semidom,recpower})|] ``` paulson@14348 ` 241` ``` ==> a^N \ a^n" ``` wenzelm@14577 ` 242` ```apply (erule rev_mp) ``` paulson@15251 ` 243` ```apply (induct "N") ``` wenzelm@14577 ` 244` ```apply (auto simp add: power_Suc le_Suc_eq) ``` wenzelm@14577 ` 245` ```apply (rename_tac m) ``` paulson@14348 ` 246` ```apply (subgoal_tac "a * a^m \ 1 * a^n", simp) ``` wenzelm@14577 ` 247` ```apply (rule mult_mono) ``` nipkow@25874 ` 248` ```apply (auto simp add: zero_le_one) ``` paulson@14348 ` 249` ```done ``` paulson@14348 ` 250` paulson@14348 ` 251` ```lemma power_Suc_less_one: ``` paulson@15004 ` 252` ``` "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1" ``` wenzelm@14577 ` 253` ```apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) ``` paulson@14348 ` 254` ```done ``` paulson@14348 ` 255` paulson@14348 ` 256` ```text{*Proof again resembles that of @{text power_strict_decreasing}*} ``` paulson@14348 ` 257` ```lemma power_increasing: ``` paulson@15004 ` 258` ``` "[|n \ N; (1::'a::{ordered_semidom,recpower}) \ a|] ==> a^n \ a^N" ``` wenzelm@14577 ` 259` ```apply (erule rev_mp) ``` paulson@15251 ` 260` ```apply (induct "N") ``` wenzelm@14577 ` 261` ```apply (auto simp add: power_Suc le_Suc_eq) ``` paulson@14348 ` 262` ```apply (rename_tac m) ``` paulson@14348 ` 263` ```apply (subgoal_tac "1 * a^n \ a * a^m", simp) ``` wenzelm@14577 ` 264` ```apply (rule mult_mono) ``` nipkow@25874 ` 265` ```apply (auto simp add: order_trans [OF zero_le_one]) ``` paulson@14348 ` 266` ```done ``` paulson@14348 ` 267` paulson@14348 ` 268` ```text{*Lemma for @{text power_strict_increasing}*} ``` paulson@14348 ` 269` ```lemma power_less_power_Suc: ``` paulson@15004 ` 270` ``` "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n" ``` paulson@15251 ` 271` ```apply (induct n) ``` wenzelm@14577 ` 272` ```apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) ``` paulson@14348 ` 273` ```done ``` paulson@14348 ` 274` paulson@14348 ` 275` ```lemma power_strict_increasing: ``` paulson@15004 ` 276` ``` "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N" ``` wenzelm@14577 ` 277` ```apply (erule rev_mp) ``` paulson@15251 ` 278` ```apply (induct "N") ``` wenzelm@14577 ` 279` ```apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) ``` paulson@14348 ` 280` ```apply (rename_tac m) ``` paulson@14348 ` 281` ```apply (subgoal_tac "1 * a^n < a * a^m", simp) ``` wenzelm@14577 ` 282` ```apply (rule mult_strict_mono) ``` nipkow@25874 ` 283` ```apply (auto simp add: order_less_trans [OF zero_less_one] order_less_imp_le) ``` paulson@14348 ` 284` ```done ``` paulson@14348 ` 285` nipkow@25134 ` 286` ```lemma power_increasing_iff [simp]: ``` nipkow@25134 ` 287` ``` "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \ b ^ y) = (x \ y)" ``` nipkow@25134 ` 288` ```by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) ``` paulson@15066 ` 289` paulson@15066 ` 290` ```lemma power_strict_increasing_iff [simp]: ``` nipkow@25134 ` 291` ``` "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)" ``` nipkow@25134 ` 292` ```by (blast intro: power_less_imp_less_exp power_strict_increasing) ``` paulson@15066 ` 293` paulson@14348 ` 294` ```lemma power_le_imp_le_base: ``` nipkow@25134 ` 295` ```assumes le: "a ^ Suc n \ b ^ Suc n" ``` nipkow@25134 ` 296` ``` and ynonneg: "(0::'a::{ordered_semidom,recpower}) \ b" ``` nipkow@25134 ` 297` ```shows "a \ b" ``` nipkow@25134 ` 298` ```proof (rule ccontr) ``` nipkow@25134 ` 299` ``` assume "~ a \ b" ``` nipkow@25134 ` 300` ``` then have "b < a" by (simp only: linorder_not_le) ``` nipkow@25134 ` 301` ``` then have "b ^ Suc n < a ^ Suc n" ``` nipkow@25134 ` 302` ``` by (simp only: prems power_strict_mono) ``` nipkow@25134 ` 303` ``` from le and this show "False" ``` nipkow@25134 ` 304` ``` by (simp add: linorder_not_less [symmetric]) ``` nipkow@25134 ` 305` ```qed ``` wenzelm@14577 ` 306` huffman@22853 ` 307` ```lemma power_less_imp_less_base: ``` huffman@22853 ` 308` ``` fixes a b :: "'a::{ordered_semidom,recpower}" ``` huffman@22853 ` 309` ``` assumes less: "a ^ n < b ^ n" ``` huffman@22853 ` 310` ``` assumes nonneg: "0 \ b" ``` huffman@22853 ` 311` ``` shows "a < b" ``` huffman@22853 ` 312` ```proof (rule contrapos_pp [OF less]) ``` huffman@22853 ` 313` ``` assume "~ a < b" ``` huffman@22853 ` 314` ``` hence "b \ a" by (simp only: linorder_not_less) ``` huffman@22853 ` 315` ``` hence "b ^ n \ a ^ n" using nonneg by (rule power_mono) ``` huffman@22853 ` 316` ``` thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less) ``` huffman@22853 ` 317` ```qed ``` huffman@22853 ` 318` paulson@14348 ` 319` ```lemma power_inject_base: ``` wenzelm@14577 ` 320` ``` "[| a ^ Suc n = b ^ Suc n; 0 \ a; 0 \ b |] ``` paulson@15004 ` 321` ``` ==> a = (b::'a::{ordered_semidom,recpower})" ``` paulson@14348 ` 322` ```by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) ``` paulson@14348 ` 323` huffman@22955 ` 324` ```lemma power_eq_imp_eq_base: ``` huffman@22955 ` 325` ``` fixes a b :: "'a::{ordered_semidom,recpower}" ``` huffman@22955 ` 326` ``` shows "\a ^ n = b ^ n; 0 \ a; 0 \ b; 0 < n\ \ a = b" ``` huffman@22955 ` 327` ```by (cases n, simp_all, rule power_inject_base) ``` huffman@22955 ` 328` huffman@29978 ` 329` ```text {* The divides relation *} ``` huffman@29978 ` 330` huffman@29978 ` 331` ```lemma le_imp_power_dvd: ``` huffman@29978 ` 332` ``` fixes a :: "'a::{comm_semiring_1,recpower}" ``` huffman@29978 ` 333` ``` assumes "m \ n" shows "a^m dvd a^n" ``` huffman@29978 ` 334` ```proof ``` huffman@29978 ` 335` ``` have "a^n = a^(m + (n - m))" ``` huffman@29978 ` 336` ``` using `m \ n` by simp ``` huffman@29978 ` 337` ``` also have "\ = a^m * a^(n - m)" ``` huffman@29978 ` 338` ``` by (rule power_add) ``` huffman@29978 ` 339` ``` finally show "a^n = a^m * a^(n - m)" . ``` huffman@29978 ` 340` ```qed ``` huffman@29978 ` 341` huffman@29978 ` 342` ```lemma power_le_dvd: ``` huffman@29978 ` 343` ``` fixes a b :: "'a::{comm_semiring_1,recpower}" ``` huffman@29978 ` 344` ``` shows "a^n dvd b \ m \ n \ a^m dvd b" ``` huffman@29978 ` 345` ``` by (rule dvd_trans [OF le_imp_power_dvd]) ``` huffman@29978 ` 346` paulson@14348 ` 347` paulson@14348 ` 348` ```subsection{*Exponentiation for the Natural Numbers*} ``` paulson@3390 ` 349` haftmann@25836 ` 350` ```instantiation nat :: recpower ``` haftmann@25836 ` 351` ```begin ``` haftmann@21456 ` 352` haftmann@25836 ` 353` ```primrec power_nat where ``` haftmann@25836 ` 354` ``` "p ^ 0 = (1\nat)" ``` haftmann@25836 ` 355` ``` | "p ^ (Suc n) = (p\nat) * (p ^ n)" ``` wenzelm@14577 ` 356` haftmann@25836 ` 357` ```instance proof ``` paulson@14438 ` 358` ``` fix z n :: nat ``` paulson@14348 ` 359` ``` show "z^0 = 1" by simp ``` paulson@14348 ` 360` ``` show "z^(Suc n) = z * (z^n)" by simp ``` paulson@14348 ` 361` ```qed ``` paulson@14348 ` 362` haftmann@25836 ` 363` ```end ``` haftmann@25836 ` 364` huffman@23305 ` 365` ```lemma of_nat_power: ``` huffman@23305 ` 366` ``` "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n" ``` huffman@23431 ` 367` ```by (induct n, simp_all add: power_Suc of_nat_mult) ``` huffman@23305 ` 368` huffman@30079 ` 369` ```lemma nat_one_le_power [simp]: "Suc 0 \ i ==> Suc 0 \ i^n" ``` huffman@30079 ` 370` ```by (rule one_le_power [of i n, unfolded One_nat_def]) ``` paulson@14348 ` 371` nipkow@25162 ` 372` ```lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)" ``` haftmann@21413 ` 373` ```by (induct "n", auto) ``` paulson@14348 ` 374` nipkow@30056 ` 375` ```lemma nat_power_eq_Suc_0_iff [simp]: ``` nipkow@30056 ` 376` ``` "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)" ``` nipkow@30056 ` 377` ```by (induct_tac m, auto) ``` nipkow@30056 ` 378` nipkow@30056 ` 379` ```lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0" ``` nipkow@30056 ` 380` ```by simp ``` nipkow@30056 ` 381` paulson@14348 ` 382` ```text{*Valid for the naturals, but what if @{text"0nat)" ``` haftmann@21413 ` 387` ``` assumes less: "i^m < i^n" ``` haftmann@21413 ` 388` ``` shows "m < n" ``` haftmann@21413 ` 389` ```proof (cases "i = 1") ``` haftmann@21413 ` 390` ``` case True with less power_one [where 'a = nat] show ?thesis by simp ``` haftmann@21413 ` 391` ```next ``` haftmann@21413 ` 392` ``` case False with nonneg have "1 < i" by auto ``` haftmann@21413 ` 393` ``` from power_strict_increasing_iff [OF this] less show ?thesis .. ``` haftmann@21413 ` 394` ```qed ``` paulson@14348 ` 395` ballarin@17149 ` 396` ```lemma power_diff: ``` ballarin@17149 ` 397` ``` assumes nz: "a ~= 0" ``` ballarin@17149 ` 398` ``` shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)" ``` ballarin@17149 ` 399` ``` by (induct m n rule: diff_induct) ``` ballarin@17149 ` 400` ``` (simp_all add: power_Suc nonzero_mult_divide_cancel_left nz) ``` ballarin@17149 ` 401` ballarin@17149 ` 402` paulson@14348 ` 403` ```text{*ML bindings for the general exponentiation theorems*} ``` paulson@14348 ` 404` ```ML ``` paulson@14348 ` 405` ```{* ``` paulson@14348 ` 406` ```val power_0 = thm"power_0"; ``` paulson@14348 ` 407` ```val power_Suc = thm"power_Suc"; ``` paulson@14348 ` 408` ```val power_0_Suc = thm"power_0_Suc"; ``` paulson@14348 ` 409` ```val power_0_left = thm"power_0_left"; ``` paulson@14348 ` 410` ```val power_one = thm"power_one"; ``` paulson@14348 ` 411` ```val power_one_right = thm"power_one_right"; ``` paulson@14348 ` 412` ```val power_add = thm"power_add"; ``` paulson@14348 ` 413` ```val power_mult = thm"power_mult"; ``` paulson@14348 ` 414` ```val power_mult_distrib = thm"power_mult_distrib"; ``` paulson@14348 ` 415` ```val zero_less_power = thm"zero_less_power"; ``` paulson@14348 ` 416` ```val zero_le_power = thm"zero_le_power"; ``` paulson@14348 ` 417` ```val one_le_power = thm"one_le_power"; ``` paulson@14348 ` 418` ```val gt1_imp_ge0 = thm"gt1_imp_ge0"; ``` paulson@14348 ` 419` ```val power_gt1_lemma = thm"power_gt1_lemma"; ``` paulson@14348 ` 420` ```val power_gt1 = thm"power_gt1"; ``` paulson@14348 ` 421` ```val power_le_imp_le_exp = thm"power_le_imp_le_exp"; ``` paulson@14348 ` 422` ```val power_inject_exp = thm"power_inject_exp"; ``` paulson@14348 ` 423` ```val power_less_imp_less_exp = thm"power_less_imp_less_exp"; ``` paulson@14348 ` 424` ```val power_mono = thm"power_mono"; ``` paulson@14348 ` 425` ```val power_strict_mono = thm"power_strict_mono"; ``` paulson@14348 ` 426` ```val power_eq_0_iff = thm"power_eq_0_iff"; ``` nipkow@25134 ` 427` ```val field_power_eq_0_iff = thm"power_eq_0_iff"; ``` paulson@14348 ` 428` ```val field_power_not_zero = thm"field_power_not_zero"; ``` paulson@14348 ` 429` ```val power_inverse = thm"power_inverse"; ``` paulson@14353 ` 430` ```val nonzero_power_divide = thm"nonzero_power_divide"; ``` paulson@14353 ` 431` ```val power_divide = thm"power_divide"; ``` paulson@14348 ` 432` ```val power_abs = thm"power_abs"; ``` paulson@14353 ` 433` ```val zero_less_power_abs_iff = thm"zero_less_power_abs_iff"; ``` paulson@14353 ` 434` ```val zero_le_power_abs = thm "zero_le_power_abs"; ``` paulson@14348 ` 435` ```val power_minus = thm"power_minus"; ``` paulson@14348 ` 436` ```val power_Suc_less = thm"power_Suc_less"; ``` paulson@14348 ` 437` ```val power_strict_decreasing = thm"power_strict_decreasing"; ``` paulson@14348 ` 438` ```val power_decreasing = thm"power_decreasing"; ``` paulson@14348 ` 439` ```val power_Suc_less_one = thm"power_Suc_less_one"; ``` paulson@14348 ` 440` ```val power_increasing = thm"power_increasing"; ``` paulson@14348 ` 441` ```val power_strict_increasing = thm"power_strict_increasing"; ``` paulson@14348 ` 442` ```val power_le_imp_le_base = thm"power_le_imp_le_base"; ``` paulson@14348 ` 443` ```val power_inject_base = thm"power_inject_base"; ``` paulson@14348 ` 444` ```*} ``` wenzelm@14577 ` 445` paulson@14348 ` 446` ```text{*ML bindings for the remaining theorems*} ``` paulson@14348 ` 447` ```ML ``` paulson@14348 ` 448` ```{* ``` paulson@14348 ` 449` ```val nat_one_le_power = thm"nat_one_le_power"; ``` paulson@14348 ` 450` ```val nat_power_less_imp_less = thm"nat_power_less_imp_less"; ``` paulson@14348 ` 451` ```val nat_zero_less_power_iff = thm"nat_zero_less_power_iff"; ``` paulson@14348 ` 452` ```*} ``` paulson@3390 ` 453` paulson@3390 ` 454` ```end ```