Re: [isabelle] setup_lifting - "no relator for the type" warning



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
context?".

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.

Ondrej





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.