src/HOL/Hoare/Arith2.thy
author wenzelm
Fri, 10 Oct 1997 19:02:28 +0200
changeset 3842 b55686a7b22c
parent 3372 6e472c8f0011
child 4359 6f2986464280
permissions -rw-r--r--
fixed dots;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     1
(*  Title:      HOL/Hoare/Arith2.thy
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     3
    Author:     Norbert Galm
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
3372
6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents: 1824
diff changeset
     6
More arithmetic.  Much of this duplicates ex/Primes.
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
3372
6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents: 1824
diff changeset
     9
Arith2 = Divides +
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    11
constdefs
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    12
  cd      :: [nat, nat, nat] => bool
3372
6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents: 1824
diff changeset
    13
  "cd x m n  == x dvd m & x dvd n"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    14
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    15
  gcd     :: [nat, nat] => nat
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    16
  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    18
  pow     :: [nat, nat] => nat                              (infixl 75)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3372
diff changeset
    19
  "m pow n     == nat_rec (Suc 0) (%u v. m*v) n"
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    20
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    21
  fac     :: nat => nat
1824
44254696843a Changed argument order of nat_rec.
berghofe
parents: 1558
diff changeset
    22
  "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    23
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
end