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 failure":

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.

Andreas,

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,
GB




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.