Re: [isabelle] 1/0 = 0?


that makes me some headache. IMHO the freedom of model making is limited. The task is to represent reality. We know what happens when the quotient goes towards zero. From there don't see any reason why to assume zero as result. This looks like a false positive and might make results unreliable. There should be better ways to deal with.

Andreas Röhler

On 03.03.2018 15:40, Tobias Nipkow wrote:
Programming languages and logics are closely related but not identical. The same operator may have different meanings in both, although it looks the same, eg "/". This just means you cannot translate operators verbatim (in both directions) but have to take their semantics into account. Thus "/" in Isabelle/HOL is not translated into "/" in (for example) ML but into a modified version that obeys "1/0 = 0".


On 02/03/2018 13:42, Manfred Kerber wrote:
Dear All,

Many thanks for all your answers; they are very helpful. Yes, I
understand the statement and agree with it that we are free in
defining concepts and that we should do so with the properties we want
to get in mind. As somebody who is interested in the extraction of
code, I am also concerned with the relationship of the Isabelle
definition and that in a programming language. Should it be a goal to
have definitions for partial functions such as division that are close
to the ones taken in programming languages? Or can we convincingly
defend a design decision for 1/0 = 0 to programming language people
who could have also gone the route of defining 1/0 as 0, but had very
good reasons not to do this and are more willing to accept a crash
than the answer 0? Or do we have to accept that Isabelle is for such
cases different from standard programming languages and argue that we
best avoid such expressions?

Best wishes

On 27 February 2018 at 23:58,  <Michael.Norrish at> wrote:

There is a spectrum of possibilities here.

At one end you have the attitude that takes OpenTheory to leave n - m undefined on the natural numbers when m > n (and pre 0 also undefined). At the other, you can try to give "reasonable" values to everything.

Note that if you want to have things be ‘properly’ unspecified, you would definitely take René’s second approach: that consequence (5/0 = 3/0) is horrid.

As with all definitions, the question is what consequences you want to be true.


On 27/2/18, 22:32, "cl-isabelle-users-bounces at on behalf of Thiemann, Rene" <cl-isabelle-users-bounces at on behalf of Rene.Thiemann at> wrote:

     Dear Manfred,

     I did not look in the history on why it was defined like this but just make
     some comments.

     As you already said, Isabelle is a logic of total function, so you have to totally specify      division. Therefore, there also is a special constant “undefined” of each type      which stands for some arbitrary fixed value of that type. So, “undefined :: real”      is a real number, but we don’t know whether it is 0, 1, pi, e, or ….

     So in principle, you could define division as
       “x / y = (if y = 0 then undefined else THE-unique z such that y * z = x)”

     As a consequence, several nice equalities now get preconditions.
     For instance, the current lemma times_divide_eq_left

     "b / c * a = b * a / c”

     with the above definition will only be provable if c is not 0.

     This will definitely make formal proofs more verbose, because one now
     has to keep track that all divisions are not by 0.

     And on the contrary, even if you define “x / y” as above, then you still will be able to prove      that “5 / 0 = 2 / 0” since both sides simplify to the same constant “undefined”.

     So even “undefined” behaviour is fully specified and can be exploited for proofs.      (though you can also define “x / y = (if y = 0 then undefined x else …)” where       then “5 / 0 = 2 / 0” simplifies to “undefined 5 = undefined 2” which as far as       I know impossible to proof or to disprove; here, “undefined” is a fixed function
      of type real to real.).

     I hope this clarifies the situation a bit,

     > Am 27.02.2018 um 12:02 schrieb Manfred Kerber <mnfrd.krbr at>:
     > Hi,
     > I was recently confused about expressions such as value "(1::nat)/0"
     > for which I get the result 0 :: real.
     > I understand that the logic used in Isabelle/HOL is total. However, I      > thought that usually partiality is approximated by leaving the value      > of expressions such as 1/0 as unspecified. What is the reason that
     > this seems not to be the case for 1/0?
     > Kind regards
     > Manfred

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