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

How do schematic variables relate to \And quantified variables? I know
that sometimes I need to use 'case' and sometimes 'case_tac' for
example, but it's not clear to me why I can't freely move a variable
from being \And quantified to being schematic and vice-versa.


It looks as though you can always use lemma atomize_all to go back and forth between !! (that is, \And) and ALL, so you can use whichever one you need:
lemma atomize_all [atomize]: (!!x. P x) == Trueprop (ALL x. P x )
proof assume !!x. P x then show ALL x. P x ..
next assume ALL x. P x then show !!x. P x by (rule allE) qed
(section 2.2.17 of "Isabelle/HOL --- Higher-Order Logic")


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.