# 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.