Email Gateway (Dec 11 2022 at 12:54): 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: Apr 19 2024 at 20:15 UTC