Re: [isabelle] universal quantifiers vs. schematic variables
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
See section 4.
> 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