Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Duplicate Fact Declaration Because of Name Man...

Email Gateway (May 10 2023 at 07:14):

From: Tjark Weber <tjark.weber@it.uu.se>
I have defined a quotient type

quotient_type Q = ...

This definition generates a theorem named abs_Q_def (among others).

Next, I would like to make this type an instance of the class abs (from
Groups.thy). I tried to proceed as follows:

instantiation Q :: abs
begin

definition abs_Q :: "Q ⇒ Q" where "abs_Q ≡ ..."

instance ...

end

However, the definition fails with an error message

Duplicate fact declaration "Scratch.abs_Q_def" vs.
"Scratch.abs_Q_def"

Is there a workaround/solution?

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (May 10 2023 at 07:47):

From: Manuel Eberl <manuel@pruvisto.org>
The problem here is really just the theorem names, not the constants
themselves. I can think of three possible workarounds:

1. give the definition theorem in the instance a different name:

instantiation Q :: abs
    begin
    definition abs_Q :: "Q ⇒ Q" where
      abs_Q_def': "abs_Q Q = Q"
    instance ..
    end

2. pick custom names for the abs/rep morphisms:

quotient_type Q = "int set" / "(=)"
      morphisms foo bar
      sorry

(curiously, this does not affect the "real" morphisms behind the scenes;
those are still called Abs_Q/Rep_Q)

3. do the instantiation in a different theory from the one that you are
   doing the typedef in. That way the fully-qualified names of the theorems
   are different.

Manuel

Last updated: Jan 04 2025 at 20:18 UTC