*To*: noam neer <noamneer at gmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sun, 4 Oct 2015 20:24:40 +0200*In-reply-to*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

Hi, > 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. first of all, your assessment is correct. Nitpicking: In the second formulation, you use the free variable 'x', which â after proving the lemma â gets generalized to a schematic variable. You can recognize schematic variables by the prefixed question mark (e.g. '?x'). > 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. I don't have an insight into the early history of Isabelle. I have the understanding that the notion of schematic has been there for a long time. The only explanation I can offer is that schematic variables can be easily instantiated. For example, if you have the theorem 'P ?x', you can substitute '?x' by something arbitrary, without having to know about the universal quantifier. In the explicitly-quantified case (be it HOL quantification or Pure quantification), the 'x' would be a bound variable and you would need to know more. Essentially, schematic variables allow for easy *outermost* quantification. Cheers Lars

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

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

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

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