*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Isabelle: A logic of total functions (?)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Fri, 17 Apr 2015 10:52:43 -0300*Sender*: alfio.martini at gmail.com

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, > Andreas Thanks for any explanation of my use of "undefined". Best! -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

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

- Previous by Date: [isabelle] Changing definition of finprod
- Next by Date: Re: [isabelle] Isabelle: A logic of total functions (?)
- Previous by Thread: [isabelle] Changing definition of finprod
- 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