Re: [isabelle] Abbreviate propositions?
On Sun, 19 Apr 2009, Randy Pollack wrote:
Is there syntax to abbreviate or define propositions?
but I would rather write something about the metalogic like:
Foo :: "sometype => prop
"Foo f == ... ==> ..."
Hopefully the leading universal quantifiers are implicit, and
meta-implication can be used in the body.
You can abbreviate Pure propositions, but there are some snags, because
the concrete syntax layer assumes that prop consts are always
syntactically distinguishable from plain terms. You also need to quantify
Consider the following example:
abbreviation "TRUE == (!!A. PROP A ==> PROP A)"
This defines abstract syntax for TRUE, but only at the term level, without
any embedding into the prop syntax. You can say
prop "PROP TRUE"
but the pretty printer will not print the PROP, because TRUE as a const is
expected to have its own distinguished notation. Of course you can add
that yourself, e.g. like this:
notation TRUE ("TRUE")
Now the literal token "TRUE" is associated with that propositional
constant. As usual with mixfix syntax, you loose "TRUE" as plain
Here is another example of definining a prop const via the locale
locale FALSE = assumes "PROP A"
In a local body free variables are implicitly quantified, and there are
special precautions to embed the constant into prop syntax, such that
prop "PROP FALSE"
works as expected, although it is a bit more cumbersome due to the
mandatory PROP marker.
This archive was generated by a fusion of
Pipermail (Mailman edition) and