Re: [mizar] Integer division and modulus/remainder in Mizar

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

On Tue, 5 Aug 2008, John Harrison wrote:

> I'm curious how Mizar defines division and modulus of integers where
> one or both arguments are negative.
>
> This is a well-known area where programming languages disagree or are
> undefined, so I'm doing a little survey of some of the world's leading
> theorem provers to see if there is a consensus there.
>
> John.

Dear John,

in Mizar Mathematical Library division and modulus of integers are defined 
as follows:

definition
  let i1,i2 be Integer;
  func i1 div i2 -> Integer equals
:: INT_1:def 7
  [\ i1 / i2 /];
end;

that is 'div' is the floor of frac and then

definition
  let i1,i2 be Integer;
  func i1 mod i2 -> Integer equals
:: INT_1:def 8
  i1 - (i1 div i2) * i2 if i2 <> 0
  otherwise 0;
end;

All details can be found at

http://merak.pb.bialystok.pl/mml/current/int_1.html

Best regards
Artur