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

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Can't abbreviate ==> like I want; something to do with prop
• From: Gottfried Barrow <gottfried.barrow at gmx.com>
• Date: Tue, 16 Jul 2013 23:33:17 -0500
• User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

```Hi,

I've set up some notation that corresponds to sequent proof diagrams.

The attached THY and PDF show how what I explain here fits in.

```
The notation is mostly notation for ==>, with different priorities. Because ==> is infix, I need some dummy notation to start off a new line, which I partially have, but it doesn't work when I need something in parenthesis, like (A ==> B).
```
An abbreviation which does work looks like this:

abbreviation (input) sequ1 :: "'a => 'a" ("|1')") where
"sequ1 x == x"

theorem "|1) A ==> B" oops

```
To try and make the above work with (A ==> B), I define an abbreviation like this:
```
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:
```
theorem "|1)(2)(3)(3a) (A ==> B)"

I get this type of error:

Type error in application: incompatible operand type

Operator:  Trueprop :: bool => prop
Operand:   sequ1233a (A::bool ==> B::bool) :: prop

```
I know there is some automatic coercion with Trueprop going on, so I use this to see what Trueprop is up to:
```
notation Trueprop("Tr") and "prop"("Pr")

Operator:  Tr :: bool => prop
Operand:   sequ1233a (Tr (A::bool) ==> Tr (B::bool)) :: prop

```
For some reason the return value of my function sequ1233a is not the right type. I try to change it to type (bool => bool), but that doesn't fix it. I try type (prop => bool) , but that causes an abbreviation error.
```
```
If someone can tell me how to fix that, then I can get rid of the use of (*...*) in my diagrams.
```
Thanks,
GB

```
```(*--{*\<^isub>`\<langle>``*)
theory i130716_sequ_prop_notation
imports Complex_Main
begin

(*\<^isub>^Trueprop\<^isub>_ priority is 5, so the priority for the meta-implication notation
cannot be higher than 4 without causing errors due to the automatic coercion
that occurs from \<^isub>^bool\<^isub>_ to \<^isub>^prop\<^isub>_.*)
notation ==> (infixr "\<bar>\<bar>" 1)
notation ==> (infixr "[1>" 1)
notation ==> (infixr "[1')" 1)
notation ==> (infixr "[1')'(2')" 1)
notation ==> (infixr "[1')'(2')'(3')" 1)

notation ==> (infixr "||" 2)
notation ==> (infixr "[2>" 2)
notation ==> (infixr "[2')" 2)
notation ==> (infixr "[2')'(3')" 2)

notation ==> (infixr "[3>" 3)
notation ==> (infixr "[3')" 3)
notation ==> (infixr "[3a>" 3)
notation ==> (infixr "[3a')" 3)

notation ==> (infixr "\<cedilla>" 4)
notation ==> (infixr "\<turnstile>" 4)

abbreviation (input) sequ1 :: "'a \<Rightarrow> 'a" ("|1')") where
"sequ1 x == x"
abbreviation (input) sequ12 :: "'a \<Rightarrow> 'a" ("|1')'(2')") where
"sequ12 x == x"
abbreviation (input) sequ123 :: "'a \<Rightarrow> 'a" ("|1')'(2')'(3')") where
"sequ123 x == x"
abbreviation (input) sequ2 :: "'a \<Rightarrow> 'a" ("|2')") where
"sequ2 x == x"
abbreviation (input) sequ3 :: "'a \<Rightarrow> 'a" ("|3')") where
"sequ3 x == x"
abbreviation (input) sequ3a :: "'a \<Rightarrow> 'a" ("|3a')") where
"sequ3a x == x"

abbreviation (input) sequ1233a :: "prop \<Rightarrow> prop" ("|1')'(2')'(3')'(3a')") where
"sequ1233a == (\<lambda>x. x)"

notation Trueprop("Tr") and "prop"("Pr")

theorem "|1) A \<Longrightarrow> B" oops

theorem "|1)(2)(3)(3a) (A \<Longrightarrow> B)"
(*Type unification failed: Clash of types "prop" and "bool"
Type error in application: incompatible operand type
Operator:  Tr :: bool \<Rightarrow> prop
Operand:   sequ1233a (Tr (A\<Colon>bool) \<Longrightarrow> Tr (B\<Colon>bool)) :: prop
Local coercion insertion on the operand failed:
"prop" is not a subtype of "bool"
Now trying to infer coercions globally.
Coercion inference failed:
"prop" is not a subtype of "bool"*)

theorem
(*|1)(2)(3*)"(
|3a) A \<and> B \<longrightarrow> C\<cedilla> A\<cedilla> B \<turnstile> A
[3a) A \<and> B \<longrightarrow> C\<cedilla> A\<cedilla> B \<turnstile> B
[3a> A \<and> B \<longrightarrow> C\<cedilla> A\<cedilla> B \<turnstile> A \<and> B
)[3) C\<cedilla> A\<cedilla> B \<turnstile> C
[3> A \<and> B \<longrightarrow> C\<cedilla> A \<turnstile> B \<longrightarrow> C
[2> A \<and> B \<longrightarrow> C\<cedilla> A \<turnstile> B \<longrightarrow> C
[1> A \<and> B \<longrightarrow> C \<turnstile> A \<longrightarrow> (B \<longrightarrow> C)"
by(auto)

theorem
"|1) B \<and> A \<turnstile> B \<and> A
[1)(2)(3) A \<and> B \<turnstile> C
[3> A \<and> B \<longrightarrow> C
[2)(3) A \<turnstile> A
[3) B \<turnstile> B
[3> A\<cedilla> B \<turnstile> A \<and> B
[2> A\<cedilla> B \<turnstile> C
[1> B \<and> A \<turnstile> C"
by(auto)

(******************************************************************************)
end
(******************************************************************************)
(*``\<rangle>\<^isub>`*}*)

```

Attachment: i130716_sequ_prop_notation.pdf