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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
