src/ZF/Integ/IntDiv.thy
author paulson
Fri Aug 11 13:27:17 2000 +0200 (2000-08-11)
changeset 9578 ab26d6c8ebfe
child 9883 c1c8647af477
permissions -rw-r--r--
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
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
(** the division algorithm **)
paulson@9578
    23
paulson@9578
    24
(*for the case a>=0, b>0*)
paulson@9578
    25
consts posDivAlg :: "int*int => int*int"
paulson@9578
    26
recdef posDivAlg "inv_image less_than (%<a,b>. nat(a $- b $+ #1))"
paulson@9578
    27
    "posDivAlg <a,b> =
paulson@9578
    28
       (if (a$<b | b$<=#0) then <#0,a>
paulson@9578
    29
        else adjust a b (posDivAlg<a,#2$*b>))"
paulson@9578
    30
paulson@9578
    31
(*for the case a<0, b>0*)
paulson@9578
    32
consts negDivAlg :: "int*int => int*int"
paulson@9578
    33
recdef negDivAlg "inv_image less_than (%<a,b>. nat(- a $- b))"
paulson@9578
    34
    "negDivAlg <a,b> =
paulson@9578
    35
       (if (#0$<=a$+b | b$<=#0) then <#-1,a$+b>
paulson@9578
    36
        else adjust a b (negDivAlg<a,#2$*b>))"
paulson@9578
    37
paulson@9578
    38
(*for the general case b~=0*)
paulson@9578
    39
paulson@9578
    40
constdefs
paulson@9578
    41
  negateSnd :: "int*int => int*int"
paulson@9578
    42
    "negateSnd == %<q,r>. <q,-r>"
paulson@9578
    43
paulson@9578
    44
  (*The full division algorithm considers all possible signs for a, b
paulson@9578
    45
    including the special case a=0, b<0, because negDivAlg requires a<0*)
paulson@9578
    46
  divAlg :: "int*int => int*int"
paulson@9578
    47
    "divAlg ==
paulson@9578
    48
       %<a,b>. if #0$<=a then
paulson@9578
    49
                  if #0$<=b then posDivAlg <a,b>
paulson@9578
    50
                  else if a=#0 then <#0,#0>
paulson@9578
    51
                       else negateSnd (negDivAlg <-a,-b>)
paulson@9578
    52
               else 
paulson@9578
    53
                  if #0$<b then negDivAlg <a,b>
paulson@9578
    54
                  else         negateSnd (posDivAlg <-a,-b>)"
paulson@9578
    55
paulson@9578
    56
defs
paulson@9578
    57
  div_def   "a div b == fst (divAlg <a,b>)"
paulson@9578
    58
  mod_def   "a mod b == snd (divAlg <a,b>)"
paulson@9578
    59
paulson@9578
    60
**)
paulson@9578
    61
paulson@9578
    62
end