src/HOL/Power.thy
author paulson
Tue Jun 03 10:56:04 1997 +0200 (1997-06-03)
changeset 3390 0c7625196d95
child 4628 0c7e97836e3c
permissions -rw-r--r--
New theory "Power" of exponentiation (and binomial coefficients)
     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 "op ^" nat
    15   "p ^ 0 = 1"
    16   "p ^ (Suc n) = (p::nat) * (p ^ n)"
    17   
    18 primrec "binomial" nat
    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 pred k) + (n choose k))"
    23 
    24 end
    25