src/HOL/Hoare/Arith2.thy
author clasohm
Fri, 08 Mar 1996 13:11:09 +0100
changeset 1558 9c6ebfab4e05
parent 1476 608483c2122a
child 1824 44254696843a
permissions -rw-r--r--
added constdefs section
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
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
More arithmetic.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
Arith2 = Arith +
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    11
constdefs
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    12
  divides :: [nat, nat] => bool                             (infixl 70)
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    13
  "x divides n == 0<n & 0<x & (n mod x) = 0"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    14
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
    15
  cd      :: [nat, nat, nat] => bool
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    16
  "cd x m n  == x divides m & x divides n"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    18
  gcd     :: [nat, nat] => nat
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    19
  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    21
  pow     :: [nat, nat] => nat                              (infixl 75)
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    22
  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    23
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    24
  fac     :: nat => nat
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    25
  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
end