Email Gateway (Dec 05 2023 at 21:59): Email Gateway (Dec 05 2023 at 21:59):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am a bit afraid to ask, but are the datatype definitions in the following theory
expected to work?
theory Barf
imports Main
begin
locale L =
fixes N :: "'x list"
assumes "N = []"
begin
datatype ('a, 'b) foo =
Null
| MkArr ‹'a ⇒ 'b› ‹'a ⇒ 'b› ‹'a ⇒ 'b›
end
locale M
begin
datatype 'a bar =
Null
| MkArr 'a 'a "('a, 'a) L.foo"
end
end
When I check this theory, the second datatype definition produces the errors below,
which are pretty much incomprehensible to me. The presence of the assumption in
locale M seems to be an essential ingredient in the failure.
These (but a little more involved) were the datatype definitions I wanted to write.
I will work around this issue if necessary, but I figure it would be useful to have an
idea about why what I wanted to do doesn't fly.
Thanks!
- Gene Stark
Email Gateway (Dec 05 2023 at 23:27):From: Manuel Eberl <manuel@pruvisto.org>
One of the datatype experts might be able to answer that question better
than I can, but honestly I'm baffled that the "datatype" command (and
"typedef", too, apparently) works inside a locale context at all. I
don't really see what the point of that would be, since you can refer
neither to variables nor type variables fixed by the locale. So why not
just declare the datatype outside the locale context?
My guess would be that "datatype" was never meant to work inside a
locale context and is therefore quite brittle when used there. But
that's just a guess.
Manuel
Email Gateway (Dec 06 2023 at 00:05):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I can well understand what you are saying, though if datatypes were not intended to work within a locale,
the system probably should have been constructed to reject such uses at a higher level than having the
proof tactics fail, generate unhandled ML exceptions, and so on.
I have been using datatypes within locales basically for modularity reasons. I like the idea that the
type names are localized to the locales to which they belong. I was surprised when I first tried it and
it worked, but I just assumed that someone had been busy improving things, so I took advantage of it.
Email Gateway (Dec 06 2023 at 00:51):From: Wenda Li <wenda.li@ed.ac.uk>
I hope we can have types properly defined inside a locale some day in the future though :-)
Wenda
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
Email Gateway (Dec 07 2023 at 07:05):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Gene, all,
The support of datatype in locales is somewhat more limited than what you can do on the top-level, in particular when you start mixing datatypes from different locales.
First, there is the limitation that datatype inherits from typedef: the new type cannot depend on the locally fixed constants and types. Perhaps this is what would be needed for Wenda's “can have types properly defined”, but as of today we don’t have such typedefs (except when using HOL-Types_To_Sets, at a cost of an axiom—the datatype command is not integrated with Types_To_Sets at all).
Second, after you define you type foo in the locale L, all theorems related to foo are annotated with L’s assumption (see e.g., L.foo.induct outside of the locale). The subsequent datatype command (for bar) cannot handle datatypes with such assumptions, which is why you seeing these tactic failures. (Ideally these low-level errors should be hidden from the user.)
So the workaround suggested by Manuel to define foo outside of L is one solution. Another would be to interpret L in M: after adding
interpretation L: L "[]" by standard simp
before datatype ‘a foo in M makes the datatype command succeed.
Best wishes,
Dmitriy
Last updated: Apr 28 2024 at 20:16 UTC