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"
"sequ1233a == (%x. x)"
The THY and PDF show how I'm using something like that, but I test it
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
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)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and