Email Gateway (Aug 22 2022 at 13:42): Email Gateway (Aug 22 2022 at 13:42):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear list,
I've seen this lemma in Fields theory:
lemma divide_right_mono:
"[|a ≤ b; 0 ≤ c|] ==> a/c ≤ b/c"
by (force simp add: divide_strict_right_mono le_less)
here 0 ≤ c which I think it should be 0 < c as the division cann't done for
zero.
Regards
Omar
Email Gateway (Aug 22 2022 at 13:42):From: Lawrence Paulson <lp15@cam.ac.uk>
We have taken the liberty of extending division with x/0 = 0 precisely so that a great many theorems, including the one you mention, can be proved more generally.
Larry Paulson
Email Gateway (Aug 22 2022 at 13:43):From: Wenda Li <wl302@cam.ac.uk>
Dear Omar,
In Isabelle/HOL, we are having a definition that x/0=0:
assumes inverse_zero [simp]: "inverse 0 = 0"
in this case, divide_right_mono holds as a/0 = b/0 = 0, but whether this
makes sense to mathematician is another question...
Best,
Wenda
Email Gateway (Aug 22 2022 at 13:43):From: Manuel Eberl <eberlm@in.tum.de>
HOL is a total logic, so all functions must be defined for all inputs of
the corresponding type. In Isabelle/HOL, division by zero is therefore
defined to yield zero, and with that, the lemma you cited holds.
Understanding the definitions of the constants involved in a statement
and how they differ from ‘standard’ mathematical definitions is crucial.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:44):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
Hmm, than it would still more useful to replace False by Truth, which
makes Truth and Truth a much more refreshing experience and a happier
world ;)
Well, the nasty thing here IMHO is: dividing by zero might be permitted,
but can't be zero, it's negativ or positiv infinity, resp. |infinity| -
quite different from 0.
Andreas,
not that much surprised.
Email Gateway (Aug 22 2022 at 13:44):From: Lawrence Paulson <lp15@cam.ac.uk>
As virtually everything in Isabelle/HOL is defined rather than postulated, there is no danger of inconsistency. Moreover, extending the domain of a partial function does not affect any statements that are confined to the original domain. We can use any values we please, but in the case of division, the choice of zero is best in that it allows a number of well-known laws to hold unconditionally. An example is (x + y) / z = x/z + y/z.
Larry Paulson
Last updated: Apr 26 2024 at 12:28 UTC