*To*: "mnfrd.krbr at gmail.com" <mnfrd.krbr at gmail.com>*Subject*: Re: [isabelle] 1/0 = 0?*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Tue, 27 Feb 2018 11:28:58 +0000*Accept-language*: de-DE, de-AT, en-US*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAHm1DC59d6OU52bzXhN9M8Mq9BoZfnSE61V0HPnZfEC7qv0Y0w@mail.gmail.com>*References*: <CAHm1DC59d6OU52bzXhN9M8Mq9BoZfnSE61V0HPnZfEC7qv0Y0w@mail.gmail.com>*Thread-index*: AQHTr7sELmw5E2uInUObyT0kL3xGe6O4DBcA*Thread-topic*: [isabelle] 1/0 = 0?

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, René > Am 27.02.2018 um 12:02 schrieb Manfred Kerber <mnfrd.krbr at gmail.com>: > > 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 >

**References**:**[isabelle] 1/0 = 0?***From:*Manfred Kerber

- Previous by Date: [isabelle] 1/0 = 0?
- Next by Date: Re: [isabelle] Vector transpose
- Previous by Thread: [isabelle] 1/0 = 0?
- Next by Thread: Re: [isabelle] 1/0 = 0?
- Cl-isabelle-users February 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list