src/HOL/Divides.thy
author wenzelm
Sun May 21 14:49:28 2000 +0200 (2000-05-21)
changeset 8902 a705822f4e2a
parent 7029 08d4eb8500dd
child 8961 b547482dd127
permissions -rw-r--r--
replaced {{ }} by { };
paulson@3366
     1
(*  Title:      HOL/Divides.thy
paulson@3366
     2
    ID:         $Id$
paulson@3366
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6865
     4
    Copyright   1999  University of Cambridge
paulson@3366
     5
paulson@3366
     6
The division operators div, mod and the divides relation "dvd"
paulson@3366
     7
*)
paulson@3366
     8
paulson@3366
     9
Divides = Arith +
paulson@3366
    10
wenzelm@8902
    11
(*We use the same class for div and mod;
paulson@6865
    12
  moreover, dvd is defined whenever multiplication is*)
paulson@6865
    13
axclass
paulson@6865
    14
  div < term
paulson@6865
    15
paulson@6865
    16
instance
wenzelm@8902
    17
  nat :: div
paulson@6865
    18
paulson@3366
    19
consts
paulson@6865
    20
  div  :: ['a::div, 'a]  => 'a          (infixl 70)
paulson@6865
    21
  mod  :: ['a::div, 'a]  => 'a          (infixl 70)
paulson@6865
    22
  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
paulson@3366
    23
paulson@3366
    24
paulson@6865
    25
(*Remainder and quotient are defined here by algorithms and later proved to
paulson@6865
    26
  satisfy the traditional definition (theorem mod_div_equality)
paulson@6865
    27
*)
paulson@3366
    28
defs
paulson@6865
    29
paulson@3366
    30
  mod_def   "m mod n == wfrec (trancl pred_nat)
paulson@7029
    31
                          (%f j. if j<n | n=0 then j else f (j-n)) m"
paulson@6865
    32
paulson@3366
    33
  div_def   "m div n == wfrec (trancl pred_nat) 
paulson@7029
    34
                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
paulson@3366
    35
paulson@6865
    36
(*The definition of dvd is polymorphic!*)
paulson@3366
    37
  dvd_def   "m dvd n == EX k. n = m*k"
paulson@3366
    38
paulson@3366
    39
end