# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID 7383930fc94618d9b3e615f4819c3bf1ba71bd70
# Parent  e939ea997f5fc2c99d6525e3f876a7b13c009c28
slightly more specialized name for type class

diff -r e939ea997f5f -r 7383930fc946 src/HOL/Code_Numeral.thy
--- 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]:
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Divides.thy
--- 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"
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Groebner_Basis.thy
--- 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]
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Parity.thy
--- 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
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Presburger.thy
--- 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]
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- 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)"
diff -r e939ea997f5f -r 7383930fc946 src/HOL/Set_Interval.thy
--- 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:
diff -r e939ea997f5f -r 7383930fc946 src/HOL/String.thy
--- 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"
diff -r e939ea997f5f -r 7383930fc946 src/HOL/ex/Bit_Lists.thy
--- 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]: