*To*: Alfio Martini <alfio.martini at acm.org>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle: A logic of total functions (?)*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 17 Apr 2015 16:23:42 +0200*In-reply-to*: <CAAPnxw2pFXpLG4sJjgorgKXm-awB2hRu5PymUuTPDZvacCxf-g@mail.gmail.com>*References*: <CAAPnxw2pFXpLG4sJjgorgKXm-awB2hRu5PymUuTPDZvacCxf-g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Dear Alfio,

Andreas On 17/04/15 15:52, Alfio Martini wrote:

Dear Isabelle Users, Taking into account the discussion that follow, I would like to know if my use of the constant "undefined" is correct or justified. I wanted to avoid the option type at all costs and in some of the examples below I would not even know how to use it. To begin with, I wanted to define a paryial recursive function such that the following (informal) specification is satisfied: sumR: int -> int ->_par int -- a partial function to sum the first k integers between -- l and u. It is not defined when l>u. requires l <= u ensures sumI(l,u) = \Sigma_{l<=k<=u} k I came up with the following solution (well I did a pencil and paper proof and have yet to check it with Isabelle/Isar): function sumR:: "int => int => int" where "sumR n n = n" | "n < m ==> sumR n m = m + sumR n (m - 1)"| "n>m ==> sumR n m = undefined" apply atomize_elim apply auto done termination sumR apply (relation "measure (Î(i,N). nat ((N+1) - i))") apply auto done Similarly, the definition of an integer division that satisfies the following specification div:: nat => nat => nat requires n>0 ensures div m n = floor(m/n) can be given by function divV::"nat â nat â nat" where "x < Suc y ==> divV x (Suc y) = 0"| "xâ Suc y ==> divV x (Suc y) = 1 + divV (x - Suc y) (Suc y)"| "divV x 0 = undefined" apply atomize_elim apply auto apply arith done termination by lexicographic_order Then I remembered that primitive recursive definitions allow for non- exaustive patterns. So divV can be given a simpler definition like this: fun divN:: "nat â nat â nat" where "divN x (Suc y) = (if x < Suc y then 0 else 1 + divN (x - Suc y) (Suc y))" In this case, Isabelle prints the following warning, which means to that it uses "undefined" in the internal workings of the primrec package. constants divN :: "nat â nat â nat" Missing patterns in function definition: /\ a. divN a 0 = undefined Looking at previous discussions about this in the mailing list, I found this enlightening explanation from Andreas: A long time ago (before Isabelle2009), "undefined" was called "arbitrary",and "arbitrary" reflected the specification of the element better: it was some element of the type. However, as definitional packages (and some users) used undefined for cases when the desired specification of a constant did not say anything, it got renamed to undefined. But logically, it still is just an arbitrary element of the type. And None would be a very special element of that type. Hope this helps, AndreasThanks for any explanation of my use of "undefined". Best!

**Follow-Ups**:**Re: [isabelle] Isabelle: A logic of total functions (?)***From:*David Cock

**References**:**[isabelle] Isabelle: A logic of total functions (?)***From:*Alfio Martini

- Previous by Date: [isabelle] Isabelle: A logic of total functions (?)
- Next by Date: Re: [isabelle] Isabelle: A logic of total functions (?)
- Previous by Thread: [isabelle] Isabelle: A logic of total functions (?)
- Next by Thread: Re: [isabelle] Isabelle: A logic of total functions (?)
- Cl-isabelle-users April 2015 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