| author | paulson |
| Fri, 24 Jan 2003 18:13:59 +0100 | |
| changeset 13786 | ab8f39f48a6f |
| parent 8844 | db71c334e854 |
| child 14348 | 744c868ee0b7 |
| permissions | -rw-r--r-- |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Power.thy |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
5 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
6 |
The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
7 |
Also binomial coefficents |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
8 |
*) |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
9 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
10 |
Power = Divides + |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
11 |
consts |
| 7843 | 12 |
binomial :: "[nat,nat] => nat" (infixl "choose" 65) |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
13 |
|
| 8844 | 14 |
primrec (power) |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
15 |
"p ^ 0 = 1" |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
16 |
"p ^ (Suc n) = (p::nat) * (p ^ n)" |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
17 |
|
| 5183 | 18 |
primrec |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
19 |
binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)" |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
20 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
21 |
binomial_Suc "(Suc n choose k) = |
| 4628 | 22 |
(if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
23 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
24 |
end |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
25 |