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

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,
> Andreas

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

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

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