# Re: [isabelle] I need a meta-or

It's a syntax priority problem.

`Trueprop priority is 5, so dealing with the syntax of functions of type
``"prop => prop" and "prop => prop => prop" is tricky:
`
Trueprop :: "bool => prop" ("(_)" 5)
I haven't figured out the rules completely, but it seems I have what I need.

`However, the rules don't make complete sense. For this meta_not_abbr,
``the function form "meta_not_abbr P" gets a coercion error, but notation
``with a priority of 40 works, or even 4:
`
abbreviation (input) meta_not_abbr :: "prop => prop" where
"meta_not_abbr P == (PROP P ==> False)"
notation meta_not_abbr ("~~~ _" 40)
theorem
"meta_not_abbr P" (* coercion error *)
theorem
"(~~~ (~~~ P)) == Trueprop (P)"
by(rule equal_intr_rule, auto simp only:)

`I then have my meta_or_abbr. The function form "meta_or_abbr P Q" also
``gets a coercion error, but infixr notation with priority less than 5
``works, and notation ("mOr _ _") also works:
`
abbreviation (input) meta_or_abbr :: "prop => prop => prop" where
"meta_or_abbr P Q == ((PROP P ==> False) ==> PROP Q)"
notation
meta_or_abbr (infixr "+++" 4) and
meta_or_abbr ("mOr _ _")
theorem
"(P +++ Q +++ R) == Trueprop (P | Q | R)"
by(rule equal_intr_rule, auto simp only:)
theorem
"(mOr P Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)
theorem
"meta_or_abbr P Q" (* coercion error *)
Here are the four connective hybrids. I know why I need one of them:
theorem meta_not:
"(P ==> False) == Trueprop (~P)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_or:
"((P ==> False) ==> Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_and:
"((P ==> (Q ==> False)) ==> False) == Trueprop (P & Q)"
by(rule equal_intr_rule, auto simp only:)
theorem meta_exists:
"((!!x. P x ==> False) ==> False) == Trueprop (? x. P x)"
by(rule equal_intr_rule, auto simp only:)

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