Email Gateway (Aug 22 2022 at 11:23): Email Gateway (Aug 22 2022 at 11:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the type class implementation,
I have the following problem. In one theory, a constant (fractrel) is defined in the
target of a type class (idom) and the definition depends on some of the parameters of the
type class. In another theory, a subclass (euclidean_ring) of this type class is defined.
In a third theory, which imports both theories, I prove in the type class target of the
subclass a lemma which refers to the constant fractrel.
After having left the type class target, I found that the theorem is not exported
correctly. The theorem refers to the foundational constant "idom.fractrel ..." rather than
the overloaded constant "fractrel".
Here is a minimal example:
theory Scratch imports Main begin
definition (in idom) fractrel :: "'a × 'a ⇒ 'a * 'a ⇒ bool"
where "fractrel = (λx y. fst x * snd y = fst y * snd x)"
end
theory ScratchA imports Scratch "~~/src/HOL/Number_Theory/Euclidean_Algorithm" begin
lemma (in euclidean_ring) lem: "b ≠ 0 ⟹ fractrel (a, b) (a, b)" sorry
thm lem
end
The "thm lem" command outputs
?b ≠ 0 ⟹ idom.fractrel op * (?a, ?b) (?a, ?b)
but it should be
?b ≠ 0 ⟹ fractrel (?a, ?b) (?a, ?b)
Obviously, lem in the current form is unusable, because "idom.fractrel op *" and
"fractrel" do not unify. What is going on here or am I doing something wrong? How do I get
the theorem I'd like to have?
Best,
Andreas
PS: In my actual use case, the lemma lem refers to a constant defined in the context of
euclidean_ring, so I cannot just move it to the target idom, where the export from the
context works as expected. Also, the definition of fractrel should be in some other theory
than the lemma; if they were in the same, the export works again as expected.
Email Gateway (Aug 22 2022 at 11:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Indeed strange. The mixin in the corresponding class seems somehow get
lost on theory merge. It will take more rounds of investigation to find
out what is going wrong here.
You can help yourself by introducing a new auxiliary class, cf. B.thy.
Florian
A.thy
B.thy
C.thy
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC