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


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.