Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with "additional type variables" in a ...

view this post on Zulip Email Gateway (Aug 22 2022 at 13:17):

From: Makarius <makarius@sketis.net>
See the "implementation" manual section "2.3.2 Auxiliary connectives";
it also refers to Section 2.2 about "hidden polymorphism", which is the
problem being solved here. Section "2.3.3 Sort hypotheses" is also related.

There is a much longer story behind all that, going back to early
versions of Gordon-style HOL that allowed such "hidden polymorphism" in
definitions that were not definitions. That caused a total existence
failure of the logic.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 13:25):

From: Lars-Henrik Eriksson <lhe@it.uu.se>
Hi,

I'm having a problem with Isabelle 2016 which I've minimised to the following file. There seems to be something particular in how Isabelle handles types appearing in a definition but not in any arguments to the thing being defined.

theory Test
imports
HOL
begin

definition foo :: "bool" ("f" 50) where
"foo ≡ ∀x :: 'a. True"

abbreviation bar :: "bool" where
"bar ≡ foo"

lemma "foo"
sorry
end

The definition gives the output

consts
foo :: "bool"
Additional type variable(s) in specification of "foo": 'a
Dropping mixfix syntax ("foo" [] 50)

The abbreviation and lemma both give the output

Type unification failed: Clash of types "_ ⇒ _" and "bool"

Type error in application: incompatible operand type

Operator: op ≡ bar :: bool ⇒ prop
Operand: foo :: ??'a itself ⇒ bool

Why is the mixfix syntax dropped?
Why has foo -- which was defined to be a constant and this was confirmed by the output -- become a function?

Is there a way to get the mixfix syntax and abbreviation to work?

Thanks,

Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden

view this post on Zulip Email Gateway (Aug 22 2022 at 13:26):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Lars-Henrik,

The problem is the implicit type ‘a in the definition of foo. To this end, Isabelle inserts a
dummy argument in the definition of foo of type (‘a itself). So your definition becomes

definition foo' :: "'a itself ⇒ bool" where
"foo' _ ≡ ∀ x :: 'a. True”

you also see this definition, if you perform a “print_theorems” after your definition of “foo”.

Hope this helps,
René

Last updated: Apr 26 2024 at 12:28 UTC