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?
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.