Re: [isabelle] Referring to "this" in "from" and "using"



On Fri, 15 Jun 2012, Manuel Eberl wrote:

I noticed that the following works:
note A
from B[OF this] have C

Whereas this does not:
note A
have C using B[OF this]

The error message is "Unknown fact 'this'".

Is this intended behaviour, and if yes, why?

The question is how far does the implicit scope of "this" reach. The Isar proof language is based on an alternation of facts and goals, i.e. you "state" things in forward mode and then "prove" things in backward mode.

When you claim a new goal, you are already one step after the last fact, so the "this" binding is removed, and thus unavailable in a 'using' command.

In principle one could do otherwhise. There are many degrees of freedom in the design space. By re-adjusting them you would get a slightly different language, with slightly different style of expression. Its a bit like English vs. French vs. German vs. Italien -- basically the same thing, but slightly different here and there ...


	Makarius





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