Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] type error

Email Gateway (Aug 18 2022 at 16:29):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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";

Email Gateway (Aug 18 2022 at 16:29):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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";

Email Gateway (Aug 18 2022 at 16:30):

From: Makarius <makarius@sketis.net>
This problem of "hidden polymorphism" is notorious since very early
versions of Gordon-style HOL. After several years of spurious crashes in
Isabelle, we are now in the state where the infrastructure is able to
treat it robustly in most situations, despite remaining surprises as
experienced above.

The deeper problem here is that it depends on the context of a
specification if a locally fixed type variable is really "polymorphic" and
thus leads to extra TYPE arguments, or not. In general it is not an error.

Warnings are traditionally hardly visible in Proof General interaction.
This is about to improve very soon in the editor view.

Makarius

Last updated: Apr 25 2024 at 16:19 UTC