*To*: Lawrence Paulson <lp15 at cam.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] type error*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Thu, 18 Nov 2010 16:42:25 +0200*In-reply-to*: <D28367C6-EE1E-4086-86AD-2FDDB1A9559F@cam.ac.uk>*References*: <4CE529F2.4060902@abo.fi> <D28367C6-EE1E-4086-86AD-2FDDB1A9559F@cam.ac.uk>*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.12) Gecko/20101027 Lightning/1.0b2 Thunderbird/3.1.6

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

**Follow-Ups**:**Re: [isabelle] type error***From:*Makarius

**References**:**[isabelle] type error***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Higher-order matching against schematic variables
- Next by Date: [isabelle] prooving protocols
- Previous by Thread: [isabelle] type error
- Next by Thread: Re: [isabelle] type error
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list