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



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")

I get the same message with some more information:

   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
Description: Adobe PDF document



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