equal
deleted
inserted
replaced
328 proof |
328 proof |
329 fix z n :: nat |
329 fix z n :: nat |
330 show "z^0 = 1" by simp |
330 show "z^0 = 1" by simp |
331 show "z^(Suc n) = z * (z^n)" by simp |
331 show "z^(Suc n) = z * (z^n)" by simp |
332 qed |
332 qed |
|
333 |
|
334 lemma of_nat_power: |
|
335 "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n" |
|
336 by (induct n, simp_all add: power_Suc) |
333 |
337 |
334 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n" |
338 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n" |
335 by (insert one_le_power [of i n], simp) |
339 by (insert one_le_power [of i n], simp) |
336 |
340 |
337 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)" |
341 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)" |