Re: [isabelle] universal quantifiers vs. schematic variables



Thanks for that, interesting.

David

On 05/10/15 03:35, Larry Paulson wrote:
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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.