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
```