src/HOL/Hoare/Arith2.thy
author berghofe
Tue Jun 25 13:11:29 1996 +0200 (1996-06-25)
changeset 1824 44254696843a
parent 1558 9c6ebfab4e05
child 3372 6e472c8f0011
permissions -rw-r--r--
Changed argument order of nat_rec.
clasohm@1476
     1
(*  Title:      HOL/Hoare/Arith2.thy
nipkow@1335
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Norbert Galm
nipkow@1335
     4
    Copyright   1995 TUM
nipkow@1335
     5
nipkow@1335
     6
More arithmetic.
nipkow@1335
     7
*)
nipkow@1335
     8
nipkow@1335
     9
Arith2 = Arith +
nipkow@1335
    10
clasohm@1558
    11
constdefs
clasohm@1558
    12
  divides :: [nat, nat] => bool                             (infixl 70)
clasohm@1558
    13
  "x divides n == 0<n & 0<x & (n mod x) = 0"
clasohm@1558
    14
clasohm@1476
    15
  cd      :: [nat, nat, nat] => bool
clasohm@1558
    16
  "cd x m n  == x divides m & x divides n"
nipkow@1335
    17
clasohm@1558
    18
  gcd     :: [nat, nat] => nat
clasohm@1558
    19
  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
nipkow@1335
    20
clasohm@1558
    21
  pow     :: [nat, nat] => nat                              (infixl 75)
berghofe@1824
    22
  "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
clasohm@1558
    23
clasohm@1558
    24
  fac     :: nat => nat
berghofe@1824
    25
  "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
nipkow@1335
    26
nipkow@1335
    27
end