*To*: "W. Douglas Maurer" <maurer at gwu.edu>*Subject*: Re: [isabelle] \forall versus \And -- also \exists versus \Or*From*: Makarius <makarius at sketis.net>*Date*: Fri, 17 Apr 2015 00:08:06 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <a062007b9d149e43ad72c@[192.168.1.20]>*References*: <a062007b6d1485c6fc401@192.168.1.20> <alpine.LNX.2.00.1504071058580.44791@lxbroy10.informatik.tu-muenchen.de> <CAHgzvFgCLJoSNv5G4q5T6+cuBfZuf2ggETgYBdinm4Yy-TE3Wg@mail.gmail.com> <a062007b9d149e43ad72c@[192.168.1.20]>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 7 Apr 2015, W. Douglas Maurer wrote:

It looks as though you can always use lemma atomize_all to go back and forthbetween !! (that is, \And) and ALL, so you can use whichever one you need: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")

Makarius

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

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

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

- Previous by Date: Re: [isabelle] Strange simplifier behaviour
- Next by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Previous by Thread: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Next by Thread: Re: [isabelle] Local_Theory.map_naming in locales
- 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