Email Gateway (Aug 18 2022 at 16:35): Email Gateway (Aug 18 2022 at 16:35):From: Victor Porton <porton@narod.ru>
The following theory does not verify. I consider this a bug of Isabelle 2009-2.
<<<<
theory test
imports Main_ZF
begin
locale loc =
fixes "x"
interpretation inter: loc "0" .
definition "a == inter.x"
end
>
To work around of this it may be used:
<<<<
theory test
imports Main_ZF
begin
locale loc =
fixes "x"
begin
definition "x1 == x"
end
interpretation inter: loc "0" .
definition "a == inter.x1"
end
>
Is it really a bug or just my misunderstanding of how Isabelle works? At least this is counter-intuitive.
Email Gateway (Aug 18 2022 at 16:35):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Dec 21, 2010 at 2:52 PM, Victor Porton <porton@narod.ru> wrote:
The following theory does not verify. I consider this a bug of Isabelle 2009-2.
locale loc =
fixes "x"interpretation inter: loc "0" .
definition "a == inter.x"
You might call this a "feature request" rather than a "bug report".
The locale tutorial says that qualified names are generated for
definitions in a locale, but it says nothing about generating
qualified names for the parameters of the locale.
Anyway, considered as a feature request, this actually seems pretty
reasonable to me. And it seems like it wouldn't be too hard to
implement.
locale loc =
fixes "x"
begindefinition "x1 == x"
end
interpretation inter: loc "0" .
definition "a == inter.x1"
Currently, the locale interpretation above introduces "inter.x1" as an
input abbreviation for "loc.x1 0". We could also introduce "inter.x"
as an input-only abbreviation for "0".
I don't think such a feature would cause any backward-compatibility
problems. Does anyone have any objections or other comments?
Last updated: Apr 20 2024 at 08:16 UTC