src/ZF/Integ/IntDiv.thy
author paulson
Thu Sep 07 17:36:37 2000 +0200 (2000-09-07)
changeset 9883 c1c8647af477
parent 9578 ab26d6c8ebfe
child 9955 6ed42bcba707
permissions -rw-r--r--
a number of new theorems
paulson@9578
     1
(*  Title:      ZF/IntDiv.thy
paulson@9578
     2
    ID:         $Id$
paulson@9578
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9578
     4
    Copyright   1999  University of Cambridge
paulson@9578
     5
paulson@9578
     6
The division operators div, mod
paulson@9578
     7
*)
paulson@9578
     8
paulson@9578
     9
IntDiv = IntArith + 
paulson@9578
    10
paulson@9578
    11
constdefs
paulson@9578
    12
  quorem :: "[i,i] => o"
paulson@9578
    13
    "quorem == %<a,b> <q,r>.
paulson@9578
    14
                      a = b$*q $+ r &
paulson@9578
    15
                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
paulson@9578
    16
paulson@9578
    17
  adjust :: "[i,i,i] => i"
paulson@9578
    18
    "adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
paulson@9578
    19
                            else <#2$*q,r>"
paulson@9578
    20
paulson@9578
    21
paulson@9578
    22
end