Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locales: Interpretation changes behaviour of l...


view this post on Zulip Email Gateway (Aug 22 2022 at 11:33):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I ran into the following unexpected behaviour with locales:

theory Scratch
imports Main
begin

locale A begin
definition "name ≡ True"
end

interpretation foo!: A by (unfold_locales) (* If this line is
removed, everything works as expected. *)

locale B = A +
assumes "name" (* Name is a FREE VARIABLE here*)

end

When defining locale B, I would have expected "name" to reference to the
definition in A. However, if there is an interpretation of A before,
"name" is a free variable in the definition of B, and I have no idea how
to access "name" from A?

Questions:

1. Is this the correct behaviour?
2. How to correctly reference "name" from A, in the definition of B?

view this post on Zulip Email Gateway (Aug 22 2022 at 11:34):

From: Peter Lammich <lammich@in.tum.de>
This was a boiled down example. The original example had a parameter, and i
used the interpretation to get code theorems for the constants defined in this
locale.

Enviado atraves de Huawei Mobile

\-------- Originalnachricht --------


Last updated: Mar 28 2024 at 12:29 UTC