Re: [isabelle] \forall versus \And -- also \exists versus \Or
On Tue, 7 Apr 2015, Andrew Gacek wrote:
How do schematic variables relate to \And quantified variables?
The Pure quantifier !!x. B x provides a local context to B x inside the
language of propositions. When you positively establish !!x. B x as a
fact, the system puts it into a standard form B ?x with schematic x. There
is normally no choice here: if facts with outermost !!x. B x persist,
something is usually wrong somewhere.
Negatively, on the assumption side, the !! quantier is not optional,
according to how the logic works.
but it's not clear to me why I can't freely move a variable
from being \And quantified to being schematic and vice-versa.
To develop an intuition about quantifier scoping rules, I recommend to
prove or disprove propositions involving ALL and --> in FOL or HOL (!) and
let "blast" or "iprover" or something else work on that. Then you
transfer the results mentally to !! and ==> in Pure.
I know that sometimes I need to use 'case' and sometimes 'case_tac' for
That is a slightly different situation. If you have a subgoal with local
!! quantification, these goal parameters are not part of the proof
context, so you can't refer to them directly.
Nonetheless case_tac and friends do that unofficially, and until
Isabelle2014 in a rather messy way. In Isabelle2015 this will be much
better, with extra colors to indicate the hidden goal scope that is
As part of the Eisbach project, these old dark corners of the system have
become a bit lighter, and we might even get rid of rule_tac, case_tac etc.
eventually. They are stemming from very ancient times, before the proof
context was fully understood.
This archive was generated by a fusion of
Pipermail (Mailman edition) and