Stream: General

Topic: Duplicate fact declaration when interpreting wo_rel

Asta Halkjær From (Aug 28 2024 at 13:47):

Hi,

I asked this question on the mailing list a while back, but it seemingly wasn't fixed, so I'm going to ask again for a workaround.

The following theory gives the error:

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

theory Scratch imports "HOL-Cardinals.Cardinal_Order_Relation" begin

interpretation wo_rel ‹|UNIV|›
  by unfold_locales simp

end

As far as I can tell, the error occurs because both HOL/Cardinals/Wellorder_Constructions.thy and HOL/BNF_Wellorder_Relation include lemmas "suc_underS" for wo_rel. I tried to hide_fact wo_rel.suc_underS twice before the interpretation, but it doesn't make the error go away.

Any hints?

Best,
Asta

Old post: https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2022-12/msg00012.html

Mathias Fleury (Aug 28 2024 at 13:59):

As far as I know there is no way in Isabelle to delete theorems (even private does not do that), so I do not think that you have any solution.
Please ask again on the mailing so that this gets fixed.

Jan van Brügge (Aug 28 2024 at 14:56):

Oh I thought I did submit my fix already, sorry about that. Will set myself a reminder for when I finally get access to the testing infrastructure myself

Asta Halkjær From (Aug 28 2024 at 14:58):

Thanks, Jan!

Asta Halkjær From (Feb 04 2025 at 10:46):

This is fixed in Isabelle2025-RC1 :octopus:

Jan van Brügge (Feb 04 2025 at 21:43):

Yes, I submitted a patch now

Jan van Brügge (Feb 04 2025 at 21:44):

Turns out it was not actually my fault, this bug had to be much older than my change

Last updated: Feb 28 2025 at 08:24 UTC