[isabelle-dev] Problem with transfer method

[Brian Huffman]

On Fri, Sep 27, 2013 at 12:16 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
>> context field_char_0
>> begin
>>
>> …
>>
>> lemma of_rat_minus: "of_rat (- a) = - of_rat a"
>>   apply transfer
>
> the »- _« (name uminus) gets replaced by a bound variable »uminusa«.
> There seems to be a problem with the context here.

The problem here is actually the heuristic that transfer uses to
decide whether or not to generalize over a free variable. Currently
the rule is that all frees are generalized, except for those that
appear in a transfer rule registered in the local context.

In context field_char_0, uminus is a free variable of type "'a => 'a"
which is not mentioned in any transfer rules. The transfer tactic
therefore treats it like any other free variable.

I can see two possible directions for improvement in the heuristic:

1. Always avoid generalizing free variables that are locale
parameters. The problem is that I don't know how to query the context
to find out what they are. (Suggestions, anyone?)

2. Consider the type of the free variable when deciding whether to
generalize. Generalization is not necessary if transfer will not
change the type of the variable. This solution would require careful
design, and would be more work to implement.

For now, you can just use "apply (transfer fixing: uminus)" as a workaround.

- Brian