Email Gateway (Aug 18 2022 at 13:24): Email Gateway (Aug 18 2022 at 13:24):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Is there syntax to abbreviate or define propositions? E.g. I can
write:
abbreviation
Foo :: "sometype => bool
where
"Foo f == \<forall> X Y. ... --> ..."
but I would rather write something about the metalogic like:
abbreviation
Foo :: "sometype => prop
where
"Foo f == ... ==> ..."
Hopefully the leading universal quantifiers are implicit, and
meta-implication can be used in the body.
Thanks,
Randy
Email Gateway (Aug 18 2022 at 13:24):From: Makarius <makarius@sketis.net>
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
explicitly.
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
identifier.
Here is another example of definining a prop const via the locale
mechanism:
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.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC