1 (* Title: HOL/IntDiv.thy
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1999 University of Cambridge
6 The division operators div, mod and the divides relation "dvd"
9 IntDiv = IntArith + Recdef +
12 quorem :: "(int*int) * (int*int) => bool"
13 "quorem == %((a,b), (q,r)).
15 (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
17 adjust :: "[int, int, int*int] => int*int"
18 "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b)
21 (** the division algorithm **)
23 (*for the case a>=0, b>0*)
24 consts posDivAlg :: "int*int => int*int"
25 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
27 (if (a<b | b<=Numeral0) then (Numeral0,a)
28 else adjust a b (posDivAlg(a, # 2*b)))"
30 (*for the case a<0, b>0*)
31 consts negDivAlg :: "int*int => int*int"
32 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
34 (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b)
35 else adjust a b (negDivAlg(a, # 2*b)))"
37 (*for the general case b~=0*)
40 negateSnd :: "int*int => int*int"
41 "negateSnd == %(q,r). (q,-r)"
43 (*The full division algorithm considers all possible signs for a, b
44 including the special case a=0, b<0, because negDivAlg requires a<0*)
45 divAlg :: "int*int => int*int"
47 %(a,b). if Numeral0<=a then
48 if Numeral0<=b then posDivAlg (a,b)
49 else if a=Numeral0 then (Numeral0,Numeral0)
50 else negateSnd (negDivAlg (-a,-b))
52 if Numeral0<b then negDivAlg (a,b)
53 else negateSnd (posDivAlg (-a,-b))"
56 int :: "Divides.div" (*avoid clash with 'div' token*)
59 div_def "a div b == fst (divAlg (a,b))"
60 mod_def "a mod b == snd (divAlg (a,b))"