src/HOL/Divides.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 10789 260fa2c67e3e
child 13152 2a54f99b44b3
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
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
nipkow@10214
     9
Divides = NatArith +
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
wenzelm@12338
    14
  div < type
paulson@6865
    15
paulson@8961
    16
instance  nat :: div
paulson@8961
    17
instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
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)
nipkow@10789
    22
  dvd  :: ['a::times, 'a] => bool       (infixl 50) 
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@10559
    39
(*This definition helps prove the harder properties of div and mod.
paulson@10559
    40
  It is copied from IntDiv.thy; should it be overloaded?*)
paulson@10559
    41
constdefs
paulson@10559
    42
  quorem :: "(nat*nat) * (nat*nat) => bool"
paulson@10559
    43
    "quorem == %((a,b), (q,r)).
paulson@10559
    44
                      a = b*q + r &
paulson@10559
    45
                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
paulson@10559
    46
paulson@3366
    47
end