Email Gateway (Aug 19 2022 at 11:31): Email Gateway (Aug 19 2022 at 11:31):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 19 2022 at 11:31):From: Lars Noschinski <noschinl@in.tum.de>
Actually, is the PROP syntax documented somewhere? I looked in the index
of the reference manual and the best I could find was the the following
comment in the reference manual in the chapter about inner syntax:
| aprop denotes atomic propositions, which are embedded into regular
| prop by means of an explicit PROP token.
|
| Terms of type prop with non-constant head, e.g. a plain variable, are
| printed in this form. Constants that yield type prop are expected to
| provide their own concrete syntax; otherwise the printed version will
| appear like logic and cannot be parsed again as prop.
-- Lars
Email Gateway (Aug 19 2022 at 11:32):From: Lars Noschinski <noschinl@in.tum.de>
BTW: Searching for PROP in the reference manual, I learned a new trick:
If you want e.g. to apply a rule X: "A ==> B ==> C", but only have the
"B" available as a fact, you can do
from _ and B have "C" apply (rule X)
to skip the first precondition of X and don't need to resort to things like
have "C"
apply (rule X)
prefer 2
apply (fact B)
or
have "C" apply (rule X[OF _ B])
Judging from the few occurrences in Isabelle and the AFP, I guess this
technique is not very well known.
-- Lars
Email Gateway (Aug 19 2022 at 11:32):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Lars,
Thanks for the information about PROP. I experimented with it some, but
I couldn't figure out how to use it with "abbreviation" to not get an error.
All the typing looks right for this:
abbreviation (input) tester :: "prop ⇒ prop" where
"tester x == x"
term "tester (A ==> B)"
(* "A::bool ==> B::bool" :: "prop" *)
--"1" theorem "PROP tester (A ⟹ B)" oops
theorem "tester (A ==> B)"
(* Error *)
Using PROP to turn off all the coercion like with --"1" is not the thing
to do.
Somehow getting around "another Tr is applied to "sequ1233a (A ==> B)"
is the problem. The ==> operator requires I give it a prop, and the
automatic Trueprop requires the abbreviation return it a bool. I can
make my abbreviation "'a => 'a", "prop => prop", and "bool => prop", but
I can't make it "prop => bool".
I've improvised some to get more mileage out of what I have.
Trueprop priority is 5, and ==> priority is 1, so I only have priorities
1, 2, 3, and 4 to use for other notation for ==>. I put the turnstile at
priority 4, and cycle the use of priorities 1, 2, and 3 with other
operators, so I don't have to use parentheses. When I go from 3 to 4, I
have to use parentheses, but 4, 5, and 6 operators can be parentheses
free in their block.
I attached a screen shot. Getting everything to line up is big. Six
levels should be enough for most things.
Regards,
GB
130716_sequ_prop_notation.png
Email Gateway (Aug 19 2022 at 11:32):From: Makarius <makarius@sketis.net>
See isar-ref manual section "7.4 The Pure Syntax". This should be mostly
up-to-date, but it is a long way to go through the manual to find the way
to PROP. (It is rarely needed in regular practice.)
Makarius
Last updated: Apr 16 2024 at 04:18 UTC