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


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.

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.

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.


Attachment: 130716_sequ_prop_notation.png
Description: PNG image

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