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 example

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

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