(* Title: HOL/Power.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
Also binomial coefficents
*)
Power = Divides +
consts
binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50])
primrec "op ^" nat
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"
primrec "binomial" nat
binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)"
binomial_Suc "(Suc n choose k) =
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
end