*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:02:56 -0700*In-reply-to*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0

Noam,

(!x. P x) => P y holds, but P ?x => P y

David On 04/10/15 10:47, noam neer wrote:

if "P" is a previously defined predicate and I want to prove it always holds, it seems I can do it in two ways. the first uses the universal quantifier as in lemma "!x. P(x)" .... and the second uses schematic variables, as in lemma "P(x)" ... if I'm not mistaken each of these can be used to prove the other, so they are logically equivalent. the only differences I could find were in the way the proved lemmas can be used in proofs, where usually the second formulation is easier to use. my question is if this is indeed the case, and if so why does Isabelle offer two different ways to say the same thing. comparing to the case of --> and ==>, the different arrows are also logically equivalent but they are intended for different situations, but I couldn't find such distinction in the universal case. thanx.

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

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Lars Noschinski

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

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