Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] When and why interpretation bindings do not ha...

Email Gateway (Aug 23 2022 at 08:43):

From: Shuwei Hu <shuwei.hu@tum.de>
Dear List,

Here is a few minimal illustrations of some really weird behaviors of
locales/interpretations.

theory Scratch imports Main begin
locale L = fixes x begin lemma t: ‹x=x› .. end

interpretation a: L 0 .
thm a.t (* 0 = 0 *)

interpretation b: L 0 .
thm b.t (* DOES NOT EXIST *)

interpretation c: L 1 .
thm c.t (* 1 = 1 *)

interpretation d: L x for x .
thm c.t (* ?x = ?x *)

interpretation e: L 1 .
thm e.t (* DOES NOT EXIST *)
end

The nonexistence of "b.t" is weird but understandable.
The nonexistence of "e.t" is really confusing.

Does anyone know why this happens? Is there any way to avoid this problem?

Thanks,
Shuwei

Email Gateway (Aug 23 2022 at 08:43):

From: Wenda Li <wl302@cam.ac.uk>
Hi Shuwei,

I am no expert on locale interpretation, but to me your examples of b and e are similar, both of which tried to give aliased prefixes of instantiated locales (i.e., L 0 and L 1 respectively).

The command

interpretation b: L 0 .
instantiates the locale L with the same argument as in the previous 'interpretation a: L 0’. Though the instantiation appears successful, it does not introduce new theorems as 'interpretation a: L 0’ did (you can check newly introduced theorems by using the command 'print_theorems’).

One way to counter this situation might be to restrict the scope of the instantiation as demonstrated in the following example:

locale L = fixes x begin lemma t: ‹x=x› .. end

context
begin
interpretation a:L 0 .
thm a.t (* 0 = 0 *)
end
thm a.t (NO LONGER EXIST, AS 'interpretation a:L' IS NOT LONGER EFFECTIVE)

interpretation b:L 0 .
thm b.t (* 0 = 0 *)

Hope this helps,
Wenda

On 19 Mar 2020, at 18:23, Shuwei Hu <shuwei.hu@tum.de> wrote:

Dear List,

Here is a few minimal illustrations of some really weird behaviors of
locales/interpretations.

theory Scratch imports Main begin
locale L = fixes x begin lemma t: ‹x=x› .. end

interpretation a: L 0 .
thm a.t (* 0 = 0 *)

interpretation b: L 0 .
thm b.t (* DOES NOT EXIST *)

interpretation c: L 1 .
thm c.t (* 1 = 1 *)

interpretation d: L x for x .
thm c.t (* ?x = ?x *)

interpretation e: L 1 .
thm e.t (* DOES NOT EXIST *)
end

The nonexistence of "b.t" is weird but understandable.
The nonexistence of "e.t" is really confusing.

Does anyone know why this happens? Is there any way to avoid this problem?

Thanks,
Shuwei
--
Shuwei Hu
TU München
Department of Informatics

Last updated: Nov 21 2024 at 12:39 UTC