slightly more specialized name for type class
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago)
changeset 703407383930fc946
parent 70339 e939ea997f5f
child 70341 972c0c744e7c
slightly more specialized name for type class
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
src/HOL/Real_Asymp/Multiseries_Expansion.thy
src/HOL/Set_Interval.thy
src/HOL/String.thy
src/HOL/ex/Bit_Lists.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -277,7 +277,7 @@
     1.4    "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
     1.5    by transfer (simp add: division_segment_int_def)
     1.6  
     1.7 -instance integer :: ring_parity
     1.8 +instance integer :: unique_euclidean_ring_with_nat
     1.9    by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
    1.10  
    1.11  lemma [transfer_rule]:
    1.12 @@ -958,7 +958,7 @@
    1.13  instance natural :: linordered_semidom
    1.14    by (standard; transfer) simp_all
    1.15  
    1.16 -instance natural :: semiring_parity
    1.17 +instance natural :: unique_euclidean_semiring_with_nat
    1.18    by (standard; transfer) simp_all
    1.19  
    1.20  lemma [transfer_rule]:
     2.1 --- a/src/HOL/Divides.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/Divides.thy	Fri Jun 14 08:34:27 2019 +0000
     2.3 @@ -811,7 +811,7 @@
     2.4    and less technical class hierarchy.
     2.5  \<close>
     2.6  
     2.7 -class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
     2.8 +class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
     2.9    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    2.10      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    2.11      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
     3.1 --- a/src/HOL/Groebner_Basis.thy	Fri Jun 14 08:34:27 2019 +0000
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Jun 14 08:34:27 2019 +0000
     3.3 @@ -75,7 +75,7 @@
     3.4  declare mod_eq_dvd_iff[algebra]
     3.5  declare nat_mod_eq_iff[algebra]
     3.6  
     3.7 -context semiring_parity
     3.8 +context unique_euclidean_semiring_with_nat
     3.9  begin
    3.10  
    3.11  declare even_mult_iff [algebra]
    3.12 @@ -83,7 +83,7 @@
    3.13  
    3.14  end
    3.15  
    3.16 -context ring_parity
    3.17 +context unique_euclidean_ring_with_nat
    3.18  begin
    3.19  
    3.20  declare even_minus [algebra]
     4.1 --- a/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
     4.2 +++ b/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
     4.6  
     4.7 -class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring +
     4.8 +class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
     4.9    assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
    4.10      and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
    4.11      and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
    4.12 @@ -424,7 +424,7 @@
    4.13  
    4.14  end
    4.15  
    4.16 -class ring_parity = ring + semiring_parity
    4.17 +class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
    4.18  begin
    4.19  
    4.20  subclass comm_ring_1 ..
    4.21 @@ -456,7 +456,7 @@
    4.22  
    4.23  subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close>
    4.24  
    4.25 -instance nat :: semiring_parity
    4.26 +instance nat :: unique_euclidean_semiring_with_nat
    4.27    by standard (simp_all add: dvd_eq_mod_eq_0)
    4.28  
    4.29  lemma even_Suc_Suc_iff [simp]:
    4.30 @@ -684,7 +684,7 @@
    4.31  
    4.32  subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
    4.33  
    4.34 -instance int :: ring_parity
    4.35 +instance int :: unique_euclidean_ring_with_nat
    4.36    by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
    4.37  
    4.38  lemma even_diff_iff:
    4.39 @@ -762,7 +762,7 @@
    4.40  
    4.41  subsection \<open>Abstract bit operations\<close>
    4.42  
    4.43 -context semiring_parity
    4.44 +context unique_euclidean_semiring_with_nat
    4.45  begin
    4.46  
    4.47  text \<open>The primary purpose of the following operations is
     5.1 --- a/src/HOL/Presburger.thy	Fri Jun 14 08:34:27 2019 +0000
     5.2 +++ b/src/HOL/Presburger.thy	Fri Jun 14 08:34:27 2019 +0000
     5.3 @@ -432,7 +432,7 @@
     5.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     5.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     5.6  
     5.7 -context semiring_parity
     5.8 +context unique_euclidean_semiring_with_nat
     5.9  begin
    5.10  
    5.11  declare even_mult_iff [presburger]
    5.12 @@ -445,7 +445,7 @@
    5.13  
    5.14  end
    5.15  
    5.16 -context ring_parity
    5.17 +context unique_euclidean_ring_with_nat
    5.18  begin
    5.19  
    5.20  declare even_minus [presburger]
     6.1 --- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Fri Jun 14 08:34:27 2019 +0000
     6.2 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Fri Jun 14 08:34:27 2019 +0000
     6.3 @@ -4805,12 +4805,12 @@
     6.4    by auto
     6.5  
     6.6  lemma even_diffI:
     6.7 -  "even a \<Longrightarrow> even b \<Longrightarrow> even (a - b :: 'a :: ring_parity)"
     6.8 +  "even a \<Longrightarrow> even b \<Longrightarrow> even (a - b :: 'a :: unique_euclidean_ring_with_nat)"
     6.9    "odd a \<Longrightarrow> odd b \<Longrightarrow> even (a - b)"
    6.10    by auto
    6.11  
    6.12  lemma odd_diffI:
    6.13 -  "even a \<Longrightarrow> odd b \<Longrightarrow> odd (a - b :: 'a :: ring_parity)"
    6.14 +  "even a \<Longrightarrow> odd b \<Longrightarrow> odd (a - b :: 'a :: unique_euclidean_ring_with_nat)"
    6.15    "odd a \<Longrightarrow> even b \<Longrightarrow> odd (a - b)"
    6.16    by auto
    6.17  
    6.18 @@ -4820,8 +4820,8 @@
    6.19  lemma odd_multI: "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
    6.20    by auto
    6.21  
    6.22 -lemma even_uminusI: "even a \<Longrightarrow> even (-a :: 'a :: ring_parity)"
    6.23 -  and odd_uminusI:  "odd a \<Longrightarrow> odd (-a :: 'a :: ring_parity)"
    6.24 +lemma even_uminusI: "even a \<Longrightarrow> even (-a :: 'a :: unique_euclidean_ring_with_nat)"
    6.25 +  and odd_uminusI:  "odd a \<Longrightarrow> odd (-a :: 'a :: unique_euclidean_ring_with_nat)"
    6.26    by auto
    6.27  
    6.28  lemma odd_powerI: "odd a \<Longrightarrow> odd (a ^ n)"
     7.1 --- a/src/HOL/Set_Interval.thy	Fri Jun 14 08:34:27 2019 +0000
     7.2 +++ b/src/HOL/Set_Interval.thy	Fri Jun 14 08:34:27 2019 +0000
     7.3 @@ -2013,7 +2013,7 @@
     7.4    by (subst sum_subtractf_nat) auto
     7.5  
     7.6  
     7.7 -context semiring_parity
     7.8 +context unique_euclidean_semiring_with_nat
     7.9  begin
    7.10  
    7.11  lemma take_bit_sum:
    7.12 @@ -2272,7 +2272,7 @@
    7.13  
    7.14  end
    7.15  
    7.16 -context semiring_parity
    7.17 +context unique_euclidean_semiring_with_nat
    7.18  begin
    7.19  
    7.20  lemma gauss_sum:
     8.1 --- a/src/HOL/String.thy	Fri Jun 14 08:34:27 2019 +0000
     8.2 +++ b/src/HOL/String.thy	Fri Jun 14 08:34:27 2019 +0000
     8.3 @@ -45,7 +45,7 @@
     8.4  
     8.5  end
     8.6  
     8.7 -context semiring_parity
     8.8 +context unique_euclidean_semiring_with_nat
     8.9  begin
    8.10  
    8.11  definition char_of :: "'a \<Rightarrow> char"
     9.1 --- a/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
     9.2 +++ b/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
     9.3 @@ -25,7 +25,7 @@
     9.4  
     9.5  end
     9.6  
     9.7 -class semiring_bits = semiring_parity +
     9.8 +class semiring_bits = unique_euclidean_semiring_with_nat +
     9.9    assumes half_measure: "a div 2 \<noteq> a \<Longrightarrow> euclidean_size (a div 2) < euclidean_size a"
    9.10    \<comment> \<open>It is not clear whether this could be derived from already existing assumptions.\<close>
    9.11  begin
    9.12 @@ -82,7 +82,7 @@
    9.13    "of_unsigned (bits_of n) = n" for n :: nat
    9.14    using of_unsigned_bits_of_nat [of n, where ?'a = nat] by simp
    9.15  
    9.16 -class ring_bits = ring_parity + semiring_bits
    9.17 +class ring_bits = unique_euclidean_ring_with_nat + semiring_bits
    9.18  begin
    9.19  
    9.20  lemma bits_of_minus_1 [simp]: