*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Sun, 4 Oct 2015 11:44:40 -0700*In-reply-to*: <56116E66.7030606@inf.ethz.ch>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com> <561169D0.1020100@inf.ethz.ch> <AEB8C84A-3BCD-4D97-B8C6-006C6345D1CA@inria.fr> <56116E66.7030606@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0

Let's try that again. If you prove: lemma "P x" by(whatever)

lemma "!x. P x"

Dave On 04/10/15 11:22, David Cock wrote:

Grr, sorry, hit send without proofreading. That second one shouldhave beenP x => P y i.e. an *unbound*, not a schematic name.Noam: in your example, it's not clear whether you have an actualschematic, or just an unbound (blue) variable.David On 04/10/15 11:19, Jasmin Blanchette wrote:David,you've just discovered one of Isabelle's most fundamental quirks.As theorems, you're right that they're (logically) equivalent, butthey differ if they appear as assumptions i.e.(!x. P x) => P y holds, but P ?x => P y does not (necessarily) hold.Huh? schematic_lemma "P ?x ==> P y" by assumption Cheers, Jasmin

**Follow-Ups**:**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Alfio Martini

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Larry Paulson

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

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

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Jasmin Blanchette

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

- Previous by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Date: Re: [isabelle] Reverse sorting
- 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