[isabelle-dev] Problem with transfer method

[Makarius]

On Mon, 30 Sep 2013, Brian Huffman wrote:

> 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?)

Locale parameters are just one example of regular "fixed variables". 
"Free variables" don't really exist within the logical context, this is 
only an intermediate phase of certain syntax mechanisms (e.g. "auto fix").

According to the normal context discipline, free variables are always 
fixed, like a local const.  We have a few tools that violate that 
principle and consequently cause confusion, e.g. the Simplifier. There 
are sometimes historical reasons for that, and little hope for reforms.

Is this also the case for transfer?


The "for" notation routinely helps in situations where users need to 
indicate an adhoc context extension to make frees essentially arbitrary, 
instead of fixed.  E.g. see the "ind_cases" method or the "lemmas" 
command.  The "induct" method has its own way to make a context of fixes 
explicit.


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

That looks like the complement of a regular "for" context, e.g. as seen in 
"ind_cases".  Such a positive form of indicating the context has the 
advantage of compositionality -- it allows the enclosing context to be 
extended later.


 	Makarius