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

On Tue, 7 Apr 2015, W. Douglas Maurer wrote:

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")

These slightly odd "atomize" and "rulify" things are mainly for internal use of tools to make them work on regular rule statements given by the user. When you write statements yourself, you normally do it the way it works best for you from the start. Then you don't need to apply atomize/rulify at all.

With a little bit of practice, it is easy to know what is best: usually an open rule-format that can be applied readily later on.

This practice is a bit like currying in functional programming: looks odd to totally new users, but is fairly natural after getting used to it.


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