Re: [isabelle] universal quantifiers vs. schematic variables

You'll probably get answers from more knowledgable persons than I, but 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

holds, but

P ?x => P y

does not (necessarily) hold. In the second case, you know that P holds for some (particular, unspecified) x, but you don't know whether that is equal to y.


On 04/10/15 10:47, noam neer wrote:
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. my question is if this is indeed the case,
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.


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