Re: [isabelle] Isabelle: A logic of total functions (?)

Dear Alfio,

Your usage of undefined matches the usual conventions in Isabelle/HOL specification tools. Whether it accurately models your specification depends on your understanding of the specification. Nowadays in HOL, we are normally happy if we get a any function definition that satisfies the specification. However, many packages internally refine the specification. For example, you can prove that sumR evaluates to the same value for all intervals (l,r) with r < l (but you don't know which one).

If you wanted to model say a hardware instruction of a processor with under-specified behaviour, then this usage of undefined is probably not faithful, because the result of executing the instructor for r < l may probably depend on l, r, the weather and whatever else. So it really depends on what you are trying to define and do.


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
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
termination sumR
apply (relation "measure (Î(i,N). nat ((N+1) - i))")

apply auto

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

   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,

Thanks for any explanation of my use of "undefined".


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