isabelle

Is 1 / 0 = 0 according to Isabelle?


The following lemma:

lemma "(1::real) / 0 = 0" by simp

goes through because of theorem division_ring_divide_zero

I find this very disturbing since if I want to show that some fraction is non-zero I have to show that the numerator is non-zero AND the denominator is non-zero, which might make sense but confuses two different problems into one.

Is there a way of separating the well-definition of a fraction and its non-zeroness?


Solution

  • Isabelle/HOL is a logic of total functions, so there is no built-in notion of a fraction or any other function application being undefined. That is, a / b is defined for all a and b, and it returns their quotient except when b is zero. But then it still has a value.

    In the library, the decision was made to complete the function in such a way that x / 0 = 0. This decision simplifies many proofs, since you have to deal with less side conditions. Unfortunately it also sometimes confuses people who expect something else.