*To*: David Cock <david.cock at inf.ethz.ch>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Mon, 5 Oct 2015 11:35:24 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <56117398.3070207@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> <56117398.3070207@inf.ethz.ch>

The nice thing is that what appears to be different behaviours is different aspects of one single operation, namely higher-order Horn clause resolution. Some historical details are available in my 1989 paper The Foundation of a Generic Theorem Prover http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf See section 4. Larry Paulson > On 4 Oct 2015, at 19:44, David Cock <david.cock at inf.ethz.ch> wrote: > > Isabelle "knows" this, and thus transparently lifts your result to the schematic lemma "P ?x", ie. a lemma with a named hole where x should be. That hole can be filled with whatever you like, and so, as Jasmin pointed out, you've effectively got a universally quantified result. > > Schematics in the conclusion (e.g. in a subgoal) can work differently. If at some point you end up with a subgoal of the form "P ?x", you can prove it by substituting a *particular* x that satisfies (P x). For example, you can prove "?x = (0::nat)" with "by(refl)" (i.e. substituting 0), but that proof obviously *doesn't* generalise to all possible substitutions.

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

**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

**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] 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