Email Gateway (Aug 18 2022 at 20:16): Email Gateway (Aug 18 2022 at 20:16):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 20:25):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
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?
Cheers,
Manuel Eberl
Email Gateway (Aug 18 2022 at 20:25):From: Tobias Nipkow <nipkow@in.tum.de>
I believe this is intended: after "have P", "this" should refer to P, but since
P has not been proved at "using", "this" is not defined just yet.
Tobias
Last updated: Apr 26 2024 at 20:16 UTC