*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 05 Oct 2015 07:55:44 +0200*In-reply-to*: <561169D0.1020100@inf.ethz.ch>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com> <561169D0.1020100@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0

On 04.10.2015 20:02, David Cock wrote: > Noam, > You'll probably get answers from more knowledgable persons than I, but > you've just discovered one of Isabelle's most fundamental quirks. As > theorems, you're right that they're (logically) equivalent, but they > differ if they appear as assumptions i.e. Schematic variables are equivalent to outermost universal quantifiers. > (!x. P x) => P y > holds, but > > P ?x => P y That is, the theorem "P ?x ==> P y" is equivalent to the theorem "!!x. P x ==> P y" which is equivalent (in HOL) to "(?x. P x) ==> P y". -- Lars

**References**:**[isabelle] universal quantifiers vs. schematic variables***From:*noam neer

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

- Previous by Date: [isabelle] 2nd CfP MILS Prague 19 Jan 2016
- Next by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Previous by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Cl-isabelle-users October 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