--- a/src/HOL/Code_Numeral.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Fri Jun 14 08:34:27 2019 +0000
@@ -277,7 +277,7 @@
"division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
by transfer (simp add: division_segment_int_def)
-instance integer :: ring_parity
+instance integer :: unique_euclidean_ring_with_nat
by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
lemma [transfer_rule]:
@@ -958,7 +958,7 @@
instance natural :: linordered_semidom
by (standard; transfer) simp_all
-instance natural :: semiring_parity
+instance natural :: unique_euclidean_semiring_with_nat
by (standard; transfer) simp_all
lemma [transfer_rule]:
--- a/src/HOL/Divides.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Divides.thy Fri Jun 14 08:34:27 2019 +0000
@@ -811,7 +811,7 @@
and less technical class hierarchy.
\<close>
-class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
--- a/src/HOL/Groebner_Basis.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Groebner_Basis.thy Fri Jun 14 08:34:27 2019 +0000
@@ -75,7 +75,7 @@
declare mod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
declare even_mult_iff [algebra]
@@ -83,7 +83,7 @@
end
-context ring_parity
+context unique_euclidean_ring_with_nat
begin
declare even_minus [algebra]
--- a/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000
@@ -11,7 +11,7 @@
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
-class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring +
+class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
@@ -424,7 +424,7 @@
end
-class ring_parity = ring + semiring_parity
+class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
begin
subclass comm_ring_1 ..
@@ -456,7 +456,7 @@
subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close>
-instance nat :: semiring_parity
+instance nat :: unique_euclidean_semiring_with_nat
by standard (simp_all add: dvd_eq_mod_eq_0)
lemma even_Suc_Suc_iff [simp]:
@@ -684,7 +684,7 @@
subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
-instance int :: ring_parity
+instance int :: unique_euclidean_ring_with_nat
by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
lemma even_diff_iff:
@@ -762,7 +762,7 @@
subsection \<open>Abstract bit operations\<close>
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
text \<open>The primary purpose of the following operations is
--- a/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000
@@ -432,7 +432,7 @@
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
declare even_mult_iff [presburger]
@@ -445,7 +445,7 @@
end
-context ring_parity
+context unique_euclidean_ring_with_nat
begin
declare even_minus [presburger]
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Fri Jun 14 08:34:27 2019 +0000
@@ -4805,12 +4805,12 @@
by auto
lemma even_diffI:
- "even a \<Longrightarrow> even b \<Longrightarrow> even (a - b :: 'a :: ring_parity)"
+ "even a \<Longrightarrow> even b \<Longrightarrow> even (a - b :: 'a :: unique_euclidean_ring_with_nat)"
"odd a \<Longrightarrow> odd b \<Longrightarrow> even (a - b)"
by auto
lemma odd_diffI:
- "even a \<Longrightarrow> odd b \<Longrightarrow> odd (a - b :: 'a :: ring_parity)"
+ "even a \<Longrightarrow> odd b \<Longrightarrow> odd (a - b :: 'a :: unique_euclidean_ring_with_nat)"
"odd a \<Longrightarrow> even b \<Longrightarrow> odd (a - b)"
by auto
@@ -4820,8 +4820,8 @@
lemma odd_multI: "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
by auto
-lemma even_uminusI: "even a \<Longrightarrow> even (-a :: 'a :: ring_parity)"
- and odd_uminusI: "odd a \<Longrightarrow> odd (-a :: 'a :: ring_parity)"
+lemma even_uminusI: "even a \<Longrightarrow> even (-a :: 'a :: unique_euclidean_ring_with_nat)"
+ and odd_uminusI: "odd a \<Longrightarrow> odd (-a :: 'a :: unique_euclidean_ring_with_nat)"
by auto
lemma odd_powerI: "odd a \<Longrightarrow> odd (a ^ n)"
--- a/src/HOL/Set_Interval.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Set_Interval.thy Fri Jun 14 08:34:27 2019 +0000
@@ -2013,7 +2013,7 @@
by (subst sum_subtractf_nat) auto
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
lemma take_bit_sum:
@@ -2272,7 +2272,7 @@
end
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
lemma gauss_sum:
--- a/src/HOL/String.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/String.thy Fri Jun 14 08:34:27 2019 +0000
@@ -45,7 +45,7 @@
end
-context semiring_parity
+context unique_euclidean_semiring_with_nat
begin
definition char_of :: "'a \<Rightarrow> char"
--- a/src/HOL/ex/Bit_Lists.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy Fri Jun 14 08:34:27 2019 +0000
@@ -25,7 +25,7 @@
end
-class semiring_bits = semiring_parity +
+class semiring_bits = unique_euclidean_semiring_with_nat +
assumes half_measure: "a div 2 \<noteq> a \<Longrightarrow> euclidean_size (a div 2) < euclidean_size a"
\<comment> \<open>It is not clear whether this could be derived from already existing assumptions.\<close>
begin
@@ -82,7 +82,7 @@
"of_unsigned (bits_of n) = n" for n :: nat
using of_unsigned_bits_of_nat [of n, where ?'a = nat] by simp
-class ring_bits = ring_parity + semiring_bits
+class ring_bits = unique_euclidean_ring_with_nat + semiring_bits
begin
lemma bits_of_minus_1 [simp]: