Email Gateway (Aug 22 2022 at 12:11): Email Gateway (Aug 22 2022 at 12:11):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
In Isabelle2015, I had the following datatype:
datatype ('a::len0) wordinterval = WordInterval
"('a::len0) word" --"start (inclusive)"
"('a::len0) word" --"end (inclusive)"
| RangeUnion "'a wordinterval" "'a
wordinterval"
With Isabelle2016-RC0, I get the following error:
Type definition with open dependencies, use "typedef (overloaded)" or
enable configuration option "typedef_overloaded" in the context.
Type: ('a, 'b) wordinterval_pre_wordinterval
Deps: len_of('a)
The error(s) above occurred in typedef
"wordinterval.wordinterval_pre_wordinterval"
The news describes this behavior for typedef. But how do I translate
my datatype to Isabelle2016?
Is typedef (overloaded) dangerous?
As an ordinary user, who does not dig into Isabelle internals too
much, trying to define a datatype and getting an error about typedef
is confusing.
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:13):From: Makarius <makarius@sketis.net>
The NEWS file says "This provides extra robustness in theory
construction."
The isar-ref manual says:
Recent clarification of overloading in the HOL logic proper @{cite
"Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of
constant definitions versus type definitions may be understood
uniformly. This requires an interpretation of Isabelle/HOL that
substantially reforms the set-theoretic model of A. Pitts @{cite
"pitts93"}, by taking a schematic view on polymorphism and interpreting
only ground types in the set-theoretic sense of HOL88. Moreover,
type-constructors may be explicitly overloaded, e.g.\ by making the
subset depend on type-class parameters (cf.\ \secref{sec:class}). This
is semantically like a dependent type: the meaning relies on the
operations provided by different type-class instances.
So it goes beyond the classic understanding of the HOL logic, i.e. the one
of HOL4 or HOL-Light.
There is nothing wrong with that. The extra option merely makes clear,
where the transition happens, for applications that need extreme forms of
reliability (e.g. by translation to OpenTheory or other HOL systems).
Makarius
Last updated: Apr 26 2024 at 20:16 UTC