Re: [isabelle] Reason not to use "undefined" with "fun", instead of leaving cases undefined?
Dmitriy (and Andreas),
On 14-09-02 01:01, Dmitriy Traytel 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.
And from your "Re: [isabelle] selector name in datatype_new causes proof
if no selector is specified for datatypes, there will be none
generated (a recent policy change)...
With "nonexhaustive", and with being able to define selector's in the
datatype definition, those two will get rid of most warnings that can
come from using underspecified functions. I switched my use of a "fun"
to an "abbreviation", which doesn't warn me about "the None", so that
gives me another way to get rid of warnings.
I kept using the query panel to try and find the "getter" functions for
a datatype, but I didn't see anything, so your comment above was useful,
and in going to look at "the" again, as an underspecified function, I
saw that it is now defined in the datatype defintion, which showed me
how to define a getter.
On 14-09-02 01:17, Andreas Lochbihler wrote:
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.
I don't exactly know what "pay attention to this" means in regards to
"primrec", but I guess it means if I'm having proof problems when using
"primrec" and "undefined", then I can try to see if switching to "fun"
helps, since "fun" is doing what I'm doing".
However, from a modelling perspective, it can make a difference.
Modelling and semantics learning always stays at the end of the line,
but I worked through your example, and it reminded me how "undefined" is
concrete, in regards to existence and uniqueness for a particular type.
Thanks to the both of you,
This archive was generated by a fusion of
Pipermail (Mailman edition) and