Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Porting to 2009: Duplicate facts on locale int...


view this post on Zulip Email Gateway (Aug 18 2022 at 13:25):

From: Peter Lammich <peter.lammich@uni-muenster.de>
I get a "duplicate fact"-error error when trying to interpret a locale
that imports a fact with the same name from different locales:
In Isabelle2007 this worked well, and I frequently use it. Do I have to
rename all those lemmas to make their names unique, or
is there a simpler way to convert ?

Here follows a toy-example that illustrates the problem:

locale B =
assumes Y: "True"
begin
lemma A: True ..
end

locale C =
assumes Z: "True"
begin
lemma A: True ..
end

locale D = B + C
begin
lemma A: "True" ..
end

interpretation x: D
apply (unfold_locales)
apply simp
done

*** Duplicate fact "Scratch.x.A"
*** At command "done".

Many thanks for any hints,
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 13:25):

From: Makarius <makarius@sketis.net>
Formerly there were more implicit (strange) prefixes in locale import
expressions. Instead, the user can now add explicit qualifiers. For
example, this is how to keep the name spaces of B and C separate in the
merge:

locale D = b: B + c: C
begin
...

Makarius


Last updated: Nov 21 2024 at 12:39 UTC