Discussion:
[isabelle] Inequality assumption
Omar Jasim
2016-07-05 15:25:36 UTC
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
Wenda Li
2016-07-05 15:35:34 UTC
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
Post by Omar Jasim
Dear list,
"[|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
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge
Lawrence Paulson
2016-07-05 15:36:42 UTC
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
Post by Omar Jasim
Dear list,
"[|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
Andreas Röhler
2016-07-08 09:58:26 UTC
Post by Lawrence Paulson
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
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.
Lawrence Paulson
2016-07-08 10:23:17 UTC
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
Post by Lawrence Paulson
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
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.
Manuel Eberl
2016-07-05 15:37:17 UTC
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
Post by Omar Jasim
Dear list,
"[|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