Re: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?
On 02.09.2014 05:11, Gottfried Barrow wrote:
primrec has the option nonexhaustive, which hides the warning (works for
datatype_new only). Thus, we should add it to this declaration of last.
Thanks for reminding us.
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)"
No, I don't know one. At first I thought that in the latter case
"BarC_get Bar = BarC_get (BarC None)" would not be provable, but
Sledgehammer helped me out: by (metis BarC_get.elims fooD.distinct(1)
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?
However, Nitpick also reported a non-spurious counterexample (empty
assignment), so I'm cc'ing Jasmin.
This archive was generated by a fusion of
Pipermail (Mailman edition) and