Stream: Beginner Questions

Topic: Multiple types of division for integers in the same Theory

Nils Buchholz (Feb 06 2024 at 13:17):

Is it possible to use both Isabelles F-Division and the euclidean division for Integers in the same theory?
Or would this require redefining one of the two as a separate function?

Manuel Eberl (Feb 09 2024 at 11:21):

What is "F-division"?

Nils Buchholz (Feb 11 2024 at 12:32):

Division that always rounds down.
So 5/2 = 2 and -5/2 = -3 etc.

Manuel Eberl (Feb 16 2024 at 11:39):

That's what Isabelle/HOL's normal div operator already does.

Manuel Eberl (Feb 16 2024 at 11:40):

I assume the alternative would be to always round to 0? We don't have one like that, I think. If you want that you'll have to define one yourself and it will be separate from the normal one.

Manuel Eberl (Feb 16 2024 at 11:41):

Of course you are then free to introduce whatever kind of notation you want for that operator, e.g. $\text{div}_0$.

Last updated: Dec 21 2024 at 16:20 UTC