Re: [isabelle] \forall versus \And -- also \exists versus \Or
How do schematic variables relate to \And quantified variables? I know
that sometimes I need to use 'case' and sometimes 'case_tac' for
example, 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.
On Tue, Apr 7, 2015 at 4:07 AM, Makarius <makarius at sketis.net> wrote:
> On Mon, 6 Apr 2015, W. Douglas Maurer wrote:
>> (1) I am having trouble understanding why Isar permits both \forall and
>> \And, seeing that they appear to do exactly the same thing. I understand
>> that \And is for the statement of a theorem or lemma, and is not supposed to
>> be used in a proof. But what would happen if we used \forall in the
>> statement of a lemma, rather than \And? How would this affect the rest of
>> the proof?
> You should not think of !! as the same as ALL, and ==> as the same as
> --> etc.
> Just a few notes on this, to overcome common misunderstandings.
> * Isabelle/Pure is minimal higher-order logic with connectives !! and ==>
> used to describe natural deduction rules declaratively. The
> Isabelle/Isar proof languages uses the same rule format to produce
> structured proofs. These concepts are integral to Isabelle, and big
> assets of its approach; schematic variables also belong here.
> * Isabelle/HOL is full higher-order logic with the whole zoo of
> connectives (ALL, EX, -->, <-->, ~ etc.) and much more, to work with
> applications. HOL statements may occur in Pure rules naturally.
> * The view of Pure as "meta-logic" and HOL as "object-logic" is OK in the
> historical understanding of Isabelle as "logical framework" to declare
> other logics, but it has little practical relevance today.
> * The view of Pure as "rule framework for structured reasoning" is very
> relevant today. It is the canonical way how I usually explain that to
This archive was generated by a fusion of
Pipermail (Mailman edition) and