[isabelle-dev] Problem with transfer method
makarius at sketis.net
Mon Sep 30 23:34:14 CEST 2013
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
> For now, you can just use "apply (transfer fixing: uminus)" as a
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
More information about the isabelle-dev