Re: [isabelle] Problem with overloading and inductive



Quoting c fe <zehfee at googlemail.com>:

On Mon, Mar 2, 2009 at 12:31 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
[...]
A possible workaround is to use abbreviations for type-specific instances.
For example, if you have a lot of type annotations like "(lifu whatever ::
nat)" in your theory, then you would probably benefit by making a
nat-specific abbreviation, like this:
[...]

But why then use overloading in the first place? If I'm going to use
lifu_nat from your example isn't it almost the same as declaring lifu
and lifu_nat as seperate functions?

I'll give an example from the Isabelle libraries.

The libraries define a polymorphic function "of_nat :: nat => 'a" that can convert from the naturals to any other semiring type. Lots of generic lemmas are proved about it.

The function "int :: nat => int" used to be defined as a separate constant, but now it is defined as an abbreviation for "of_nat :: nat => int". Since it is just an abbreviation, we can use all the lemmas about "of_nat" for reasoning about "int" as well. Back when it was a separate constant, the libraries had two separate versions of each lemma, one for "of_nat" and one for "int".

So if you have any generic lemmas about "lifu", then that might be an argument for using overloading+abbreviations instead of separate constants.

On the other hand, if all of your lemmas about "lifu" are specific to certain types, maybe you would be better off using separate functions. (Unless you think it is really important to have the shared "lifu" syntax.)

- Brian







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