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
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and