src/ZF/Integ/IntDiv.thy
changeset 9578 ab26d6c8ebfe
child 9883 c1c8647af477
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Integ/IntDiv.thy	Fri Aug 11 13:27:17 2000 +0200
     1.3 @@ -0,0 +1,62 @@
     1.4 +(*  Title:      ZF/IntDiv.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +The division operators div, mod
    1.10 +*)
    1.11 +
    1.12 +IntDiv = IntArith + 
    1.13 +
    1.14 +constdefs
    1.15 +  quorem :: "[i,i] => o"
    1.16 +    "quorem == %<a,b> <q,r>.
    1.17 +                      a = b$*q $+ r &
    1.18 +                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
    1.19 +
    1.20 +  adjust :: "[i,i,i] => i"
    1.21 +    "adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
    1.22 +                            else <#2$*q,r>"
    1.23 +
    1.24 +(**
    1.25 +(** the division algorithm **)
    1.26 +
    1.27 +(*for the case a>=0, b>0*)
    1.28 +consts posDivAlg :: "int*int => int*int"
    1.29 +recdef posDivAlg "inv_image less_than (%<a,b>. nat(a $- b $+ #1))"
    1.30 +    "posDivAlg <a,b> =
    1.31 +       (if (a$<b | b$<=#0) then <#0,a>
    1.32 +        else adjust a b (posDivAlg<a,#2$*b>))"
    1.33 +
    1.34 +(*for the case a<0, b>0*)
    1.35 +consts negDivAlg :: "int*int => int*int"
    1.36 +recdef negDivAlg "inv_image less_than (%<a,b>. nat(- a $- b))"
    1.37 +    "negDivAlg <a,b> =
    1.38 +       (if (#0$<=a$+b | b$<=#0) then <#-1,a$+b>
    1.39 +        else adjust a b (negDivAlg<a,#2$*b>))"
    1.40 +
    1.41 +(*for the general case b~=0*)
    1.42 +
    1.43 +constdefs
    1.44 +  negateSnd :: "int*int => int*int"
    1.45 +    "negateSnd == %<q,r>. <q,-r>"
    1.46 +
    1.47 +  (*The full division algorithm considers all possible signs for a, b
    1.48 +    including the special case a=0, b<0, because negDivAlg requires a<0*)
    1.49 +  divAlg :: "int*int => int*int"
    1.50 +    "divAlg ==
    1.51 +       %<a,b>. if #0$<=a then
    1.52 +                  if #0$<=b then posDivAlg <a,b>
    1.53 +                  else if a=#0 then <#0,#0>
    1.54 +                       else negateSnd (negDivAlg <-a,-b>)
    1.55 +               else 
    1.56 +                  if #0$<b then negDivAlg <a,b>
    1.57 +                  else         negateSnd (posDivAlg <-a,-b>)"
    1.58 +
    1.59 +defs
    1.60 +  div_def   "a div b == fst (divAlg <a,b>)"
    1.61 +  mod_def   "a mod b == snd (divAlg <a,b>)"
    1.62 +
    1.63 +**)
    1.64 +
    1.65 +end