src/HOL/Power.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8844 db71c334e854
child 14348 744c868ee0b7
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
077d305615df choose just as an infix
paulson
parents: 5183
diff changeset
    12
  binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
3390
0c7625196d95 New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff changeset
    13
8844
db71c334e854 named "op ^" definitions;
wenzelm
parents: 7843
diff changeset
    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
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4628
diff changeset
    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
0c7e97836e3c *** empty log message ***
wenzelm
parents: 3390
diff changeset
    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