--- a/NEWS Wed Aug 24 06:21:06 2022 +0000
+++ b/NEWS Wed Aug 24 08:22:13 2022 +0000
@@ -44,6 +44,14 @@
*** HOL ***
+* HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
+
+ is_ring ~> ring_axioms
+ cring ~> cring_axioms
+ R_def ~> R_m_def
+
+INCOMPATIBILITY.
+
* Moved auxiliary computation constant "divmod_nat" to theory
"Euclidean_Division". Minor INCOMPATIBILITY.
--- a/src/HOL/Algebra/Ideal_Product.thy Wed Aug 24 06:21:06 2022 +0000
+++ b/src/HOL/Algebra/Ideal_Product.thy Wed Aug 24 08:22:13 2022 +0000
@@ -49,7 +49,7 @@
assumes "ideal I R" "ideal J R"
shows "ideal (I \<cdot> J) R"
proof (rule idealI)
- show "ring R" using is_ring .
+ show "ring R" using ring_axioms .
next
show "subgroup (I \<cdot> J) (add_monoid R)"
unfolding subgroup_def
--- a/src/HOL/Algebra/Ring.thy Wed Aug 24 06:21:06 2022 +0000
+++ b/src/HOL/Algebra/Ring.thy Wed Aug 24 08:22:13 2022 +0000
@@ -292,10 +292,8 @@
lemma is_monoid: "monoid R"
by (auto intro!: monoidI m_assoc)
-lemma is_ring: "ring R"
- by (rule ring_axioms)
+end
-end
thm monoid_record_simps
lemmas ring_record_simps = monoid_record_simps ring.simps
--- a/src/HOL/Algebra/RingHom.thy Wed Aug 24 06:21:06 2022 +0000
+++ b/src/HOL/Algebra/RingHom.thy Wed Aug 24 08:22:13 2022 +0000
@@ -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
--- a/src/HOL/Algebra/UnivPoly.thy Wed Aug 24 06:21:06 2022 +0000
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Aug 24 08:22:13 2022 +0000
@@ -501,11 +501,8 @@
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 .
--- a/src/HOL/Number_Theory/Residues.thy Wed Aug 24 06:21:06 2022 +0000
+++ b/src/HOL/Number_Theory/Residues.thy Wed Aug 24 08:22:13 2022 +0000
@@ -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: