| author | paulson |
| Fri, 19 Sep 1997 16:12:21 +0200 | |
| changeset 3685 | 5b8c0c8f576e |
| parent 3390 | 0c7625196d95 |
| child 4628 | 0c7e97836e3c |
| 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 |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
12 |
binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50])
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
13 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
14 |
primrec "op ^" nat |
|
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 |
|
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
18 |
primrec "binomial" nat |
|
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) = |
|
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
22 |
(if k = 0 then 1 else (n choose pred k) + (n choose k))" |
|
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 |