*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] \forall versus \And -- also \exists versus \Or*From*: Andrew Gacek <andrew.gacek at gmail.com>*Date*: Tue, 7 Apr 2015 08:51:28 -0500*Cc*: "W. Douglas Maurer" <maurer at gwu.edu>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1504071058580.44791@lxbroy10.informatik.tu-muenchen.de>*References*: <a062007b6d1485c6fc401@192.168.1.20> <alpine.LNX.2.00.1504071058580.44791@lxbroy10.informatik.tu-muenchen.de>

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. -Andrew 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 > beginners. > > > Makarius >

**Follow-Ups**:**Re: [isabelle] \forall versus \And -- also \exists versus \Or***From:*Makarius

**Re: [isabelle] \forall versus \And -- also \exists versus \Or***From:*W. Douglas Maurer

**References**:

- Previous by Date: Re: [isabelle] Modify theorem with equality assumption
- Next by Date: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Previous by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list