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

Hi Gottfried,

On 02.09.2014 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)"
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.

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?
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) fooD.inject option.distinct(1)).

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