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"

abbreviation
  lifu_nat :: "'a => nat"
where
  "lifu_nat == lifu"

inductive ind_lifu :: "int list => int => bool"
where
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.

- Brian







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