Re: [isabelle] Can't abbreviate ==> like I want; something to do with prop



On 17.07.2013 06:33, Gottfried Barrow wrote:
abbreviation (input) sequ1233a :: "prop => prop"
("|1')'(2')'(3')'(3a')") where
"sequ1233a == (%x. x)"

The THY and PDF show how I'm using something like that, but I test it
like this:

For testing, try "term" first and see that your syntax works:

    term "|1)(2)(3)(3a) (A ⟹ B)"

theorem "|1)(2)(3)(3a) (A ==> B)"

To understand why your theory command fails, please note that A and B in my term command above have type bool, not prop.

The reason is that the user should never need to care about Trueprop in normal operation. So Isabelle inserts Trueprop automatically if type prop is expected, except if the argument has !! or ==> as an outermost function symbol.

Your debugging attempt shows this:

notation Trueprop("Tr") and "prop"("Pr")

I get the same message with some more information:

Operator: Tr :: bool => prop
Operand: sequ1233a (Tr (A::bool) ==> Tr (B::bool)) :: prop

It typed "sequ1233a (A ==> B)" just fine (note again, A, B :: bool, surrounded by a Tr)). However, another Tr is applied to "sequ1233a (A ==> B)" which then cannot be typed.

You can instruct Isabelle to not insert Trueprop automatically by prefixing it with the PROP syntax:

    theorem "PROP |1)(2)(3)(3a) (A ⟹ B)"
    term "sequ1233ax (PROP A ⟹ PROP B)"


  -- Lars




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