Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Duplicate fact declaration when interpreting l...

Email Gateway (Dec 11 2022 at 12:54):

From: Asta Halkjær From <andro.from@gmail.com>
Hi everyone,

The following theory produces an error:

theory Scratch imports "HOL-Cardinals.Cardinal_Order_Relation" begin

interpretation wo_rel ‹|UNIV|›
by unfold_locales simp

end

The error is as follows:

Duplicate fact declaration "Scratch.suc_underS" vs. "Scratch.suc_underS"⌂
The above error(s) occurred while activating facts of locale instance
wo_rel "|UNIV|"

In the wo_rel context, suc_underS resolves to a lemma in
HOL/Cardinals/Wellorder_Constructions.thy.
This lemma shadows the lemma suc_underS in HOL/BNF_Wellorder_Relation,
which is what suc_underS resolves to in Wellorder_Constructions.thy just
before the new lemma.
I guess this setup causes trouble when interpreting the locale?

Can I work around it somehow?

Best,
Asta

Email Gateway (Dec 11 2022 at 13:31):

From: Jan van Brügge <jan@vanbruegge.de>
Sorry, this is probably do to my patch to BNFs that is included in Isabelle2022. I had to move some lemmas and definitions from HOL-Cardinals into HOL and apparently missed this when removing the duplicates. CI also did not catch any errors. Maybe hide_fact can help here? I will work on a patch to fix this, but that won't help short-term.

Sorry again,
Jan

Dec 11, 2022 12:54:14 PM Asta Halkjær From <andro.from@gmail.com>:

Email Gateway (Dec 11 2022 at 15:05):

From: Asta Halkjær From <andro.from@gmail.com>
Oh! Thanks for the explanation. Unfortunately I could not make hide_fact
work. It does not seem to affect the locale interpretation machinery.
I've ended up working outside the wo_rel context, prefixing a lot of stuff
with wo_rel and adding [OF foo], foo being my local proof of "wo_rel r",
where necessary.
It is not very pleasant, but fairly mechanical, and it works.

Best,
Asta

Den søn. 11. dec. 2022 kl. 14.30 skrev Jan van Brügge <jan@vanbruegge.de>:

Last updated: Jan 04 2025 at 20:18 UTC