# HG changeset patch
# User Norbert Schirmer <nschirmer@apple.com>
# Date 1657798408 -7200
#      Thu Jul 14 13:33:28 2022 +0200
# Node ID 9b42182c8f290c02bcd38a6b61bbbe2810f0592d
# Parent  787a203a20b6870af5ea7849fdbe946b7ed7cf3a
avoid duplicate fact error on global_interpretation of residues

diff -r 787a203a20b6 -r 9b42182c8f29 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Aug 22 21:37:06 2022 +0200
+++ b/src/HOL/Algebra/Ring.thy	Thu Jul 14 13:33:28 2022 +0200
@@ -292,9 +292,10 @@
 lemma is_monoid: "monoid R"
   by (auto intro!: monoidI m_assoc)
 
+(* Duplicate name.  If needed, use ring_axioms.
 lemma is_ring: "ring R"
   by (rule ring_axioms)
-
+*)
 end
 thm monoid_record_simps
 lemmas ring_record_simps = monoid_record_simps ring.simps
diff -r 787a203a20b6 -r 9b42182c8f29 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Mon Aug 22 21:37:06 2022 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Thu Jul 14 13:33:28 2022 +0200
@@ -98,7 +98,7 @@
 
 \<comment> \<open>the kernel of a ring homomorphism is an ideal\<close>
 lemma (in ring_hom_ring) kernel_is_ideal: "ideal (a_kernel R S h) R"
-  apply (rule idealI [OF R.is_ring])
+  apply (rule idealI [OF R.ring_axioms])
     apply (rule additive_subgroup.a_subgroup[OF additive_subgroup_a_kernel])
    apply (auto simp: a_kernel_def')
   done
diff -r 787a203a20b6 -r 9b42182c8f29 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Mon Aug 22 21:37:06 2022 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jul 14 13:33:28 2022 +0200
@@ -500,12 +500,12 @@
 text \<open>
   Interpretation of lemmas from \<^term>\<open>algebra\<close>.
 \<close>
-
+(*
 lemma (in cring) cring:
   "cring R" ..
-
+*)
 lemma (in UP_cring) UP_algebra:
-  "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
+  "algebra R P" by (auto intro!: algebraI R.cring_axioms UP_cring UP_smult_l_distr UP_smult_r_distr
     UP_smult_assoc1 UP_smult_assoc2)
 
 sublocale UP_cring < algebra R P using UP_algebra .
diff -r 787a203a20b6 -r 9b42182c8f29 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Aug 22 21:37:06 2022 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Jul 14 13:33:28 2022 +0200
@@ -38,7 +38,7 @@
 locale residues =
   fixes m :: int and R (structure)
   assumes m_gt_one: "m > 1"
-  defines "R \<equiv> residue_ring m"
+  defines R_m_def: "R \<equiv> residue_ring m"
 begin
 
 lemma abelian_group: "abelian_group R"
@@ -55,11 +55,11 @@
       by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
   qed
   with m_gt_one show ?thesis
-    by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
+    by (fastforce simp add: R_m_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
 qed
 
 lemma comm_monoid: "comm_monoid R"
-  unfolding R_def residue_ring_def
+  unfolding R_m_def residue_ring_def
   apply (rule comm_monoidI)
     using m_gt_one  apply auto
   apply (metis mod_mult_right_eq mult.assoc mult.commute)
@@ -68,7 +68,7 @@
 
 lemma cring: "cring R"
   apply (intro cringI abelian_group comm_monoid)
-  unfolding R_def residue_ring_def
+  unfolding R_m_def residue_ring_def
   apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq)
   done
 
@@ -87,29 +87,29 @@
 \<close>
 
 lemma res_carrier_eq: "carrier R = {0..m - 1}"
-  by (auto simp: R_def residue_ring_def)
+  by (auto simp: R_m_def residue_ring_def)
 
 lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
-  by (auto simp: R_def residue_ring_def)
+  by (auto simp: R_m_def residue_ring_def)
 
 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
-  by (auto simp: R_def residue_ring_def)
+  by (auto simp: R_m_def residue_ring_def)
 
 lemma res_zero_eq: "\<zero> = 0"
-  by (auto simp: R_def residue_ring_def)
+  by (auto simp: R_m_def residue_ring_def)
 
 lemma res_one_eq: "\<one> = 1"
-  by (auto simp: R_def residue_ring_def units_of_def)
+  by (auto simp: R_m_def residue_ring_def units_of_def)
 
 lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
   using m_gt_one
-  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
+  apply (auto simp add: Units_def R_m_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
   apply (subst (asm) coprime_iff_invertible'_int)
    apply (auto simp add: cong_def)
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
-  using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
+  using m_gt_one unfolding R_m_def a_inv_def m_inv_def residue_ring_def
   apply simp
   apply (rule the_equality)
    apply (simp add: mod_add_right_eq)
@@ -134,16 +134,16 @@
   using insert m_gt_one by auto
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
-  by (auto simp: R_def residue_ring_def mod_simps)
+  by (auto simp: R_m_def residue_ring_def mod_simps)
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
-  by (auto simp: R_def residue_ring_def mod_simps)
+  by (auto simp: R_m_def residue_ring_def mod_simps)
 
 lemma zero_cong: "\<zero> = 0"
-  by (auto simp: R_def residue_ring_def)
+  by (auto simp: R_m_def residue_ring_def)
 
 lemma one_cong: "\<one> = 1 mod m"
-  using m_gt_one by (auto simp: R_def residue_ring_def)
+  using m_gt_one by (auto simp: R_m_def residue_ring_def)
 
 (* FIXME revise algebra library to use 1? *)
 lemma pow_cong: "(x mod m) [^] n = x^n mod m"
@@ -276,7 +276,7 @@
     by (simp add: totient_def totatives_eq card_image)
 qed
 
-lemma (in residues_prime) totient_eq: "totient p = p - 1"
+lemma (in residues_prime) prime_totient_eq: "totient p = p - 1"
   using totient_eq by (simp add: res_prime_units_eq)
 
 lemma (in residues) euler_theorem:
