src/HOL/Hoare/Arith2.thy
author clasohm
Wed Nov 29 17:01:41 1995 +0100 (1995-11-29)
changeset 1374 5e407f2a3323
parent 1335 5e1c0540f285
child 1476 608483c2122a
permissions -rw-r--r--
removed quotes from consts and syntax sections
nipkow@1335
     1
(*  Title: 	HOL/Hoare/Arith2.thy
nipkow@1335
     2
    ID:         $Id$
nipkow@1335
     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
nipkow@1335
    11
consts
clasohm@1374
    12
  divides :: [nat, nat] => bool			(infixl 70)
clasohm@1374
    13
  cd	  :: [nat, nat, nat] => bool
clasohm@1374
    14
  gcd	  :: [nat, nat] => nat
nipkow@1335
    15
clasohm@1374
    16
  pow	  :: [nat, nat] => nat			(infixl 75)
clasohm@1374
    17
  fac	  :: nat => nat
nipkow@1335
    18
nipkow@1335
    19
defs
nipkow@1335
    20
  divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
nipkow@1335
    21
  cd_def	"cd x m n  == x divides m & x divides n"
nipkow@1335
    22
  gcd_def	"gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
nipkow@1335
    23
nipkow@1335
    24
  pow_def	"m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
nipkow@1335
    25
  fac_def	"fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
nipkow@1335
    26
nipkow@1335
    27
end