Re: [isabelle] type error




On 11/18/2010 4:13 PM, Lawrence Paulson wrote:
The following warning should alert you to the problem:

### Additional type variable(s) in specification of disjunctive: 'd
Thank you for your answer. I have figured it out myself finally. I had this
problem before, but I forgot about it.

Wouldn't be better is Isabelle would give an error already when
defining something which depends on an additional type variable?

Best regards,

Viorel Preoteasa
For more information, switch on “show types" and you can locate the occurrence of 'd

Test.disjunctive_def:
   disjunctive TYPE(?'d) (?R::?'a =>  ?'b =>  ?'c) =
   (ALL P::?'d =>  ?'a =>  ?'b. (?R .. SUP P) = SUP (%w::?'d. ?R .. P w))

An implicit type parameter has been generated in order to ensure that this definition is sound. Probably you should make the right hand side of your definition more specific.

Larry Paulson


On 18 Nov 2010, at 13:28, Viorel Preoteasa wrote:

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.