Re: [isabelle] setup_lifting - "no relator for the type" warning
On Thu, 24 Jan 2013, Ondřej Kunčar wrote:
On 01/24/2013 04:31 PM, John Wickerson wrote:
Thanks again, Ondrej.
I have one further question on this topic, which can be summarised as
"How can I make the transfer method work properly inside a
In more detail: suppose I'm working inside a context that gives me
the assumption "P f" for some fixed f. I write a lemma involving f,
and begin the proof by applying the transfer method. The transfer
method *generalises* f, and thus loses the fact that P holds for it.
Just citing from The Isabelle/Isar Reference Manual:
Goals are generalized over all free variables by default; this is necessary
for variables whose types change, but can be overridden for specific
variables with e.g. transfer fixing: x y z.
I've occasionally seen this from a distance, but did not look more closely
(and right now I am also busy with the Isabelle2013 release).
Historically, the treatment of Free variables as arbitrary might stem from
the original HOL4 version of the quotient mechanism by Peter Homeier, when
it was ported to Isabelle/HOL for the first time. But Isabelle has a
clear notion of "fixed variable" within a context, which act as local
constants by default. So the above exception declaration via "fixing"
looks more like a hot fix.
A more standard way in Isabelle is to leave things as fixed as they are
already in the context, unless the users says differenly by augmenting the
"eigen context" of some language element. The "ind_cases" proof method is
an example for that, it uses the "for" syntax for that. (The same "for"
notation helped out in many conceptually difficult situations in locale
expressions some years ago.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and