src/HOL/Power.thy
changeset 25836 f7771e4f7064
parent 25231 1aa9c8f022d0
child 25874 14819a95cf75
     1.1 --- a/src/HOL/Power.thy	Sat Jan 05 09:16:11 2008 +0100
     1.2 +++ b/src/HOL/Power.thy	Sat Jan 05 09:16:27 2008 +0100
     1.3 @@ -323,19 +323,21 @@
     1.4  
     1.5  subsection{*Exponentiation for the Natural Numbers*}
     1.6  
     1.7 -instance nat :: power ..
     1.8 +instantiation nat :: recpower
     1.9 +begin
    1.10  
    1.11 -primrec (power)
    1.12 -  "p ^ 0 = 1"
    1.13 -  "p ^ (Suc n) = (p::nat) * (p ^ n)"
    1.14 +primrec power_nat where
    1.15 +  "p ^ 0 = (1\<Colon>nat)"
    1.16 +  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
    1.17  
    1.18 -instance nat :: recpower
    1.19 -proof
    1.20 +instance proof
    1.21    fix z n :: nat
    1.22    show "z^0 = 1" by simp
    1.23    show "z^(Suc n) = z * (z^n)" by simp
    1.24  qed
    1.25  
    1.26 +end
    1.27 +
    1.28  lemma of_nat_power:
    1.29    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    1.30  by (induct n, simp_all add: power_Suc of_nat_mult)