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