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:

 abbreviation
   Foo :: "sometype => prop
 where
   "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 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






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