Re: [isabelle] Inequality assumption



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


On 05/07/16 17:22, Omar Jasim wrote:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.