[isabelle] \forall versus \And -- also \exists versus \Or

(1) I am having trouble understanding why Isar permits both \forall and \And, seeing that they appear to do exactly the same thing. I understand that \And is for the statement of a theorem or lemma, and is not supposed to be used in a proof. But what would happen if we used \forall in the statement of a lemma, rather than \And? How would this affect the rest of the proof? (2) Am I to understand that, just as \And is the universal quantifier at the meta-level, \Or is the existential quantifier at the meta-level? Certainly \Or x. P(x) appears to do the same thing as \exists x. P(x) . Further confusing me here is that a number of example Isar proof statements do use \exists instead of \Or, such as lemma assumes Pf: "\exists x. P(f x)" shows "\exists y. P y" (p. 10 of "A Tutorial Introduction To Structured Isar Proofs"). (3) In Whats In Main, under Orderings, under Syntax, there is given some syntax for \forall and for \exists, such as \forall x \leq y. P \equiv \forall x. x \leq y --> P . There are eight rules given here, four for \forall and four for \exists . Do these rules also work for \And and \Or ? (4) Am I understanding correctly that \And applied to the null set is True, while \Or applied to the null set is False?

Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875

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