Re: [isabelle] universal quantifiers vs. schematic variables
Let's try that again.
If you prove:
lemma "P x"
then (assuming x was completely unbound at that point), you've obviously
done something at least as hard as proving
lemma "!x. P x"
i.e. proving something about a concrete x, without assuming anything in
particular about it, and thus your proof could in principle be reapplied
to any other concrete value. 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
In summary, propositions with schematics are a *bit* like universally
quantified formulae, but not quite. The semantics get more complicated
when a given schematic appears multiple times e.g. in assumption and
conclusions. In that case, by instantiating a schematic, you're making
a (potentially unsafe) *choice* in your proof - you may end up in an
unprovable state, even for a true theorem.
Larry could presumably shine more light on the design decisions here,
but schematics are (as far as I understand) a more fundamental part of
the term rewriting system, with something more of an "operational"
semantics i.e. it does what it does, while "!" is the quantifier of
Pure, with a specific logical interpretation.
On 04/10/15 11:22, David Cock wrote:
Grr, sorry, hit send without proofreading. That second one should
P x => P y
i.e. an *unbound*, not a schematic name.
Noam: in your example, it's not clear whether you have an actual
schematic, or just an unbound (blue) variable.
On 04/10/15 11:19, Jasmin Blanchette wrote:
you've just discovered one of Isabelle's most fundamental quirks.
As theorems, you're right that they're (logically) equivalent, but
they differ if they appear as assumptions i.e.
(!x. P x) => P y
P ?x => P y
does not (necessarily) hold.
schematic_lemma "P ?x ==> P y"
This archive was generated by a fusion of
Pipermail (Mailman edition) and