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

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

lemma atomize_all [atomize]: (!!x. P x) == Trueprop (ALL x. P x ) proof assume !!x. P x then show ALL x. P x .. next assume ALL x. P x then show !!x. P x by (rule allE) qed (section 2.2.17 of "Isabelle/HOL --- Higher-Order Logic") -Douglas -- Prof. W. Douglas Maurer Washington, DC 20052, USA Department of Computer Science Tel. (1-202)994-5921 The George Washington University Fax (1-202)994-4875

**Follow-Ups**:

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

**Re: [isabelle] \forall versus \And -- also \exists versus \Or***From:*Andrew Gacek

- Previous by Date: Re: [isabelle] Local_Theory.map_naming in locales
- Next by Date: [isabelle] [Isabelle] how to translate this into Isabelle language to prove the this
- 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