Re: [isabelle] How-to define a object logic
On Sat, 23 Dec 2006, Michael Nedzelsky wrote:
> I try to define the system S_1^0 of modal logic
> One thing which bother me is that the axioms are written like the
> ax_sub1: "PROP is_subst(P,Q,P,Q)"
> instead of simply
> ax_sub1: "is_subst(P,Q,P,Q)"
> Any suggestions and comments are highly welcome.
This is because is_subst yields prop, rather than "o" of the object-logic.
Isabelle requires explicit syntax to indicate this situation -- by default
the system inserts an object-logic judgment. The PROP syntax allows to
input pure propositions, but this markup is absent in output of
applications involving a constant (which is assumed to provide its own
The following declaration introduces a prop predicate with proper concrete
is_subst :: "[o,o,o,o] => prop" ("(1IS'_SUBST/(1'(_,/ _,/ _,/ _')))")
This archive was generated by a fusion of
Pipermail (Mailman edition) and