[isabelle] type error



Hello,

I have the following theory. At theorem test I get the following error:

*** Type unification failed: Clash of types "fun" and "bool"
*** Type error in application: Incompatible operand type
***
*** Operator:  Trueprop :: bool => prop
*** Operand: disjunctive (R::??'d::type itself) :: (??'a::type => ??'b::complete_lattice => ??'c::complete_lattice) => bool
***
*** At command "theorem".

Could someone help me?

Best regards,

Viorel

theory Test
imports Main Lattice_Syntax
begin

abbreviation
SUP1_syntax :: "('a => 'b::complete_lattice) => 'b" ("(SUP _)" [1000] 1000)
  where "SUP P == SUPR UNIV P"

definition apply_fun::"('a=>'b=>'c)=>('a=>'b)=>'a=>'c" (infixl ".." 5) where
  "(A .. B) = (% x . (A x) (B x))";

definition
"(disjunctive R) = (! P . (R .. (SUP P)) = (SUP (% w . (R .. (P w)))))";

theorem test: "disjunctive R";






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