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
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.

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


	Makarius


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