Re: [isabelle] Problem with overloading and inductive
Quoting c fe <zehfee at googlemail.com>:
Thanks, that really helped. But it lead to me having to annotated
quite a lot of expressions which made my terms look rather convoluted.
And as I think that those terms are important I want them to look as
comprehensible as possible. So I'm now back to different functions
with the same mixfix syntax and keep getting ambiguous input warnings
but the definitions look ok.
Any time you have functions overloaded to such an extent (i.e.
overloaded with respect to more than one type variable), you are bound
to need a lot of those ugly type annotations.
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:
consts lifu :: "'a => 'b"
lifu_nat :: "'a => nat"
"lifu_nat == lifu"
inductive ind_lifu :: "int list => int => bool"
base: "lifu_nat a = lifu_nat b ==> ind_lifu a b"
Type-specific abbreviations are helpful for output too, since they can
indicate type information that is usually hidden, even when "show
types" is enabled. For example, without the abbreviation lifu_nat, the
command "thm base" would give you no indication of what return type
"lifu" is used at, but with the abbreviation you can tell that it is
used at type nat.
This archive was generated by a fusion of
Pipermail (Mailman edition) and