src/HOL/Power.thy
author berghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 5183 89f162de39cf
parent 4628 0c7e97836e3c
child 7843 077d305615df
permissions -rw-r--r--
Adapted to new datatype package.
     1 (*  Title:      HOL/Power.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
     7 Also binomial coefficents
     8 *)
     9 
    10 Power = Divides + 
    11 consts
    12   binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
    13 
    14 primrec
    15   "p ^ 0 = 1"
    16   "p ^ (Suc n) = (p::nat) * (p ^ n)"
    17   
    18 primrec
    19   binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
    20 
    21   binomial_Suc "(Suc n choose k) =
    22                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
    23 
    24 end
    25