| author | wenzelm |
| Thu, 12 Feb 1998 17:53:05 +0100 | |
| changeset 4628 | 0c7e97836e3c |
| parent 3390 | 0c7625196d95 |
| child 5183 | 89f162de39cf |
| permissions | -rw-r--r-- |
| paulson@3390 | 1 |
(* Title: HOL/Power.thy |
| paulson@3390 | 2 |
ID: $Id$ |
| paulson@3390 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| paulson@3390 | 4 |
Copyright 1997 University of Cambridge |
| paulson@3390 | 5 |
|
| paulson@3390 | 6 |
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat |
| paulson@3390 | 7 |
Also binomial coefficents |
| paulson@3390 | 8 |
*) |
| paulson@3390 | 9 |
|
| paulson@3390 | 10 |
Power = Divides + |
| paulson@3390 | 11 |
consts |
| paulson@3390 | 12 |
binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50])
|
| paulson@3390 | 13 |
|
| paulson@3390 | 14 |
primrec "op ^" nat |
| paulson@3390 | 15 |
"p ^ 0 = 1" |
| paulson@3390 | 16 |
"p ^ (Suc n) = (p::nat) * (p ^ n)" |
| paulson@3390 | 17 |
|
| paulson@3390 | 18 |
primrec "binomial" nat |
| paulson@3390 | 19 |
binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)" |
| paulson@3390 | 20 |
|
| paulson@3390 | 21 |
binomial_Suc "(Suc n choose k) = |
| wenzelm@4628 | 22 |
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
| paulson@3390 | 23 |
|
| paulson@3390 | 24 |
end |
| paulson@3390 | 25 |