[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)"
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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.