Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Some facts are not available in the int context

Email Gateway (Dec 16 2022 at 10:55):

From: Emin Karayel <me@eminkarayel.de>
Dear all,

There is a global interpretation for the ring locale of the structure Z:

interpretation int: "domain" 𝒵
(in line 136 HOL-Algebra.IntRing) - Note that domain is a sublocale of ring.

This should mean that a lemma in the context of ring will be available with
the namespace int. For most facts in ring this seems to be true (e.g.
int.a_assoc).

However, this doesn't work for facts defined in
HOL-Algebra.Chinese_Remainder. Example: The following facts are not found
and I can't explain why?
thm int.canonical_proj_ring_hom
thm int.canonical_proj_is_surj

I also checked and this seems to be specific to the int interpretation. For
example:

theory Scratch
imports "HOL-Algebra.Chinese_Remainder" "HOL-Algebra.IntRing"
begin

interpretation q: domain "ZFact 5"
using ZFact_prime_is_domain by simp

Then the following are available facts (as expected):
thm q.canonical_proj_is_surj
thm q.canonical_proj_ring_hom

Thanks a lot for any help/insights,
Emin

Last updated: Apr 20 2024 at 01:05 UTC