[isabelle] Export from class target fails to replace operations
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)"
theory ScratchA imports Scratch "~~/src/HOL/Number_Theory/Euclidean_Algorithm" begin
lemma (in euclidean_ring) lem: "b â 0 â fractrel (a, b) (a, b)" sorry
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and