Re: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?
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
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