src/HOL/Hoare/Arith2.thy
author nipkow
Fri, 17 Nov 1995 09:04:10 +0100
changeset 1335 5e1c0540f285
child 1374 5e407f2a3323
permissions -rw-r--r--
New directory. Hoare logic according to Mike Gordon.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/Hoare/Arith2.thy
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     3
    Author: 	Norbert Galm
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
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
consts
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    12
  divides :: "[nat, nat] => bool"			(infixl 70)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    13
  cd	  :: "[nat, nat, nat] => bool"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    14
  gcd	  :: "[nat, nat] => nat"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    15
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    16
  pow	  :: "[nat, nat] => nat"			(infixl 75)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    17
  fac	  :: "nat => nat"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
defs
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
  divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    21
  cd_def	"cd x m n  == x divides m & x divides n"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    22
  gcd_def	"gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    23
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
  pow_def	"m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    25
  fac_def	"fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
end