[isabelle] Inequality assumption

[Omar Jasim]

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]

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

[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

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]

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]

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]

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