Re: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?

Dear Gottfried,

Technically, you do not change the internal construction at all if you add the missing cases with undefined on the right-hand side. The function package does the same internally. With primrec, it is slightly different, because primrec internally abstracts over the other parameters and then uses undefined with a function type rather than the parameters. So, if you pay attention to this, you do not change what you can prove in Isabelle about your definitions.

However, from a modelling perspective, it can make a difference. Say, you write the following definition:

fun nth :: "nat => 'a list => 'a" where
  "nth 0 (x # xs) = x"
| "nth (Suc n) (x # xs) = nth n xs"
| "nth n [] = undefined"

Then the last equation is part of the specification that fun exports for regular usage. From a modelling point of view, all your theorems about nth then only apply to the real world if whenever you access a list (think array) beyond its end, you get the same back no matter how far you reach beyond the end. If you want to model array access in memory, this is clearly unrealistic. Instead, if you omit the last equation (and do not pierce the veil of abstraction that fun provides you - but there is currently no way to express this in Isabelle), then you don't have this assumption about nth in your model.


On 02/09/14 05:11, Gottfried Barrow wrote:

The canonical way in the HOL sources, when there's no need for a total function, is to not
cover all the cases, like "last", which is not covered for []:

   primrec last :: "'a list => 'a" where
     "last (x # xs) = (if xs = [] then x else last xs)"

I've been doing that kind of thing, but it occurred to me that I could put "undefined" to
good use, to get rid of the warnings, like this:

   datatype fooD = Bar | BarC "nat option"

   fun BarC_get :: "fooD => nat" where
     "BarC_get Bar = undefined"
    |"BarC_get (BarC None) = undefined"
    |"BarC_get (BarC (Some n)) = n"

Instead of like the above:

   fun BarC_get2 :: "fooD => nat" where
     "BarC_get2 (BarC (Some n)) = n"

Is there some, good, mysterious reason why I shouldn't do this to get rid of the warnings?


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