src/HOL/Divides.thy
author paulson
Mon Jul 19 15:18:16 1999 +0200 (1999-07-19)
changeset 7029 08d4eb8500dd
parent 6865 5577ffe4c2f1
child 8902 a705822f4e2a
permissions -rw-r--r--
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
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
paulson@6865
    11
(*We use the same sort 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
paulson@6865
    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