# HG changeset patch # User haftmann # Date 1699542712 0 # Node ID 5e6b195eee83a38e3a8962aa27c13e411aadcca1 # Parent ddf255a4ccc3e9c86e8d6a5e6641de185a61a461 slightly less technical formulation of very specific type class diff -r ddf255a4ccc3 -r 5e6b195eee83 NEWS --- a/NEWS Thu Nov 09 15:11:51 2023 +0000 +++ b/NEWS Thu Nov 09 15:11:52 2023 +0000 @@ -18,6 +18,11 @@ * Explicit type class for discrete_linear_ordered_semidom for integral semidomains with a discrete linear order. +* Type class linordered_euclidean_semiring replaces the (rather technical) + type class unique_euclidean_semiring_with_nat; type class + unique_euclidean_ring_with_nat, which barely admits instances other than + isomorphic to int, is discontinued. Minor INCOMPATIBILITY. + *** ML *** diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Archimedean_Field.thy Thu Nov 09 15:11:52 2023 +0000 @@ -412,7 +412,7 @@ lemma floor_divide_of_nat_eq: "\of_nat m / of_nat n\ = of_nat (m div n)" for m n :: nat - by (metis floor_divide_of_int_eq of_int_of_nat_eq unique_euclidean_semiring_with_nat_class.of_nat_div) + by (metis floor_divide_of_int_eq of_int_of_nat_eq linordered_euclidean_semiring_class.of_nat_div) lemma floor_divide_lower: fixes q :: "'a::floor_ceiling" diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Bit_Operations.thy Thu Nov 09 15:11:52 2023 +0000 @@ -2626,7 +2626,7 @@ subsection \Common algebraic structure\ class unique_euclidean_semiring_with_bit_operations = - unique_euclidean_semiring_with_nat + semiring_bit_operations + linordered_euclidean_semiring + semiring_bit_operations begin lemma possible_bit [simp]: diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Code_Numeral.thy Thu Nov 09 15:11:52 2023 +0000 @@ -305,7 +305,7 @@ "division_segment (k :: integer) = (if k \ 0 then 1 else - 1)" by transfer (simp add: division_segment_int_def) -instance integer :: unique_euclidean_ring_with_nat +instance integer :: linordered_euclidean_semiring by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def) instantiation integer :: ring_bit_operations @@ -393,7 +393,7 @@ end -instantiation integer :: unique_euclidean_semiring_with_nat_division +instantiation integer :: linordered_euclidean_semiring_division begin definition divmod_integer :: "num \ num \ integer \ integer" @@ -1065,9 +1065,9 @@ by (simp add: natural_eq_iff) instance natural :: discrete_linordered_semidom - by (standard; transfer) simp_all + by (standard; transfer) (simp_all add: Suc_le_eq) -instance natural :: unique_euclidean_semiring_with_nat +instance natural :: linordered_euclidean_semiring by (standard; transfer) simp_all instantiation natural :: semiring_bit_operations diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Divides.thy Thu Nov 09 15:11:52 2023 +0000 @@ -7,7 +7,7 @@ imports Parity begin -class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + discrete_linordered_semidom + +class unique_euclidean_semiring_numeral = linordered_euclidean_semiring + discrete_linordered_semidom + assumes div_less [no_atp]: "0 \ a \ a < b \ a div b = 0" and mod_less [no_atp]: " 0 \ a \ a < b \ a mod b = a" and div_positive [no_atp]: "0 < b \ b \ a \ a div b > 0" diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Parity.thy Thu Nov 09 15:11:52 2023 +0000 @@ -528,9 +528,9 @@ end -subsection \Special case: euclidean rings containing the natural numbers\ +subsection \Special case: euclidean rings structurally containing the natural numbers\ -class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + +class linordered_euclidean_semiring = discrete_linordered_semidom + 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" @@ -755,7 +755,7 @@ \2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\ proof - have \(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\ (is \?lhs = ?rhs\) - by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex) + by (auto simp add: linorder_class.not_less monoid_mult_class.power_add dest!: le_Suc_ex) then have \of_nat ?lhs = of_nat ?rhs\ by simp then show ?thesis @@ -801,16 +801,13 @@ end -class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat +instance nat :: linordered_euclidean_semiring + by standard simp_all -instance nat :: unique_euclidean_semiring_with_nat - by standard (simp_all add: dvd_eq_mod_eq_0) - -instance int :: unique_euclidean_ring_with_nat +instance int :: linordered_euclidean_semiring by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np) - -context unique_euclidean_semiring_with_nat +context linordered_euclidean_semiring begin subclass semiring_parity @@ -825,7 +822,7 @@ next assume "\ 2 dvd a" have eucl: "euclidean_size (a mod 2) = 1" - proof (rule order_antisym) + proof (rule Orderings.order_antisym) show "euclidean_size (a mod 2) \ 1" using mod_size_less [of 2 a] by simp show "1 \ euclidean_size (a mod 2)" @@ -910,28 +907,21 @@ end -context unique_euclidean_ring_with_nat -begin - -subclass ring_parity .. - lemma minus_1_mod_2_eq [simp]: - "- 1 mod 2 = 1" + \- 1 mod 2 = (1::int)\ by (simp add: mod_2_eq_odd) lemma minus_1_div_2_eq [simp]: - "- 1 div 2 = - 1" + "- 1 div 2 = - (1::int)" proof - - from div_mult_mod_eq [of "- 1" 2] - have "- 1 div 2 * 2 = - 1 * 2" + from div_mult_mod_eq [of "- 1 :: int" 2] + have "- 1 div 2 * 2 = - 1 * (2 :: int)" using add_implies_diff by fastforce then show ?thesis - using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp + using mult_right_cancel [of 2 "- 1 div 2" "- (1 :: int)"] by simp qed -end - -context unique_euclidean_semiring_with_nat +context linordered_euclidean_semiring begin lemma even_mask_div_iff': @@ -957,7 +947,8 @@ moreover from False have \{q. n \ q \ q < m \ q \ n} = {n}\ by auto then have \odd ((\a\{q. n \ q \ q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\ - by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric]) + by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff + linorder_class.not_less mask_eq_sum_exp_nat [symmetric]) ultimately have \odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\ by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all with False show ?thesis @@ -977,7 +968,7 @@ to its positive segments. \ -class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat + +class linordered_euclidean_semiring_division = linordered_euclidean_semiring + fixes divmod :: \num \ num \ 'a \ 'a\ and divmod_step :: \'a \ 'a \ 'a \ 'a \ 'a\ \ \ These are conceptually definitions but force generated code @@ -1021,7 +1012,7 @@ define r s t where \r = (numeral m :: nat)\ \s = (numeral n :: nat)\ \t = 2 * s\ then have *: \numeral m = of_nat r\ \numeral n = of_nat s\ \numeral (num.Bit0 n) = of_nat t\ and \\ s \ r mod s\ - by (simp_all add: not_le) + by (simp_all add: linorder_class.not_le) have t: \2 * (r div t) = r div s - r div s mod 2\ \r mod t = s * (r div s mod 2) + r mod s\ by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Rings.div_mult2_eq \t = 2 * s\) @@ -1122,7 +1113,7 @@ end -instantiation nat :: unique_euclidean_semiring_with_nat_division +instantiation nat :: linordered_euclidean_semiring_division begin definition divmod_nat :: "num \ num \ nat \ nat" @@ -1154,7 +1145,7 @@ \Suc 0 mod numeral (Num.Bit1 n) = 1\ by simp_all -instantiation int :: unique_euclidean_semiring_with_nat_division +instantiation int :: linordered_euclidean_semiring_division begin definition divmod_int :: "num \ num \ int \ int" @@ -1292,23 +1283,23 @@ by auto simproc_setup numeral_divmod - ("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | - "0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | + ("0 div 0 :: 'a :: linordered_euclidean_semiring_division" | "0 mod 0 :: 'a :: linordered_euclidean_semiring_division" | + "0 div 1 :: 'a :: linordered_euclidean_semiring_division" | "0 mod 1 :: 'a :: linordered_euclidean_semiring_division" | "0 div - 1 :: int" | "0 mod - 1 :: int" | - "0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | + "0 div numeral b :: 'a :: linordered_euclidean_semiring_division" | "0 mod numeral b :: 'a :: linordered_euclidean_semiring_division" | "0 div - numeral b :: int" | "0 mod - numeral b :: int" | - "1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | - "1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | + "1 div 0 :: 'a :: linordered_euclidean_semiring_division" | "1 mod 0 :: 'a :: linordered_euclidean_semiring_division" | + "1 div 1 :: 'a :: linordered_euclidean_semiring_division" | "1 mod 1 :: 'a :: linordered_euclidean_semiring_division" | "1 div - 1 :: int" | "1 mod - 1 :: int" | - "1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | + "1 div numeral b :: 'a :: linordered_euclidean_semiring_division" | "1 mod numeral b :: 'a :: linordered_euclidean_semiring_division" | "1 div - numeral b :: int" |"1 mod - numeral b :: int" | "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" | "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" | "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" | - "numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | - "numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | + "numeral a div 0 :: 'a :: linordered_euclidean_semiring_division" | "numeral a mod 0 :: 'a :: linordered_euclidean_semiring_division" | + "numeral a div 1 :: 'a :: linordered_euclidean_semiring_division" | "numeral a mod 1 :: 'a :: linordered_euclidean_semiring_division" | "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" | - "numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | + "numeral a div numeral b :: 'a :: linordered_euclidean_semiring_division" | "numeral a mod numeral b :: 'a :: linordered_euclidean_semiring_division" | "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" | "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" | "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" | @@ -1346,7 +1337,7 @@ subsection \Computing congruences modulo \2 ^ q\\ -context unique_euclidean_semiring_with_nat_division +context linordered_euclidean_semiring_division begin lemma cong_exp_iff_simps: diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Real_Asymp/Multiseries_Expansion.thy --- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Nov 09 15:11:52 2023 +0000 @@ -4805,12 +4805,12 @@ by auto lemma even_diffI: - "even a \ even b \ even (a - b :: 'a :: unique_euclidean_ring_with_nat)" + "even a \ even b \ even (a - b :: int)" "odd a \ odd b \ even (a - b)" by auto lemma odd_diffI: - "even a \ odd b \ odd (a - b :: 'a :: unique_euclidean_ring_with_nat)" + "even a \ odd b \ odd (a - b :: int)" "odd a \ even b \ odd (a - b)" by auto @@ -4820,8 +4820,8 @@ lemma odd_multI: "odd a \ odd b \ odd (a * b)" by auto -lemma even_uminusI: "even a \ even (-a :: 'a :: unique_euclidean_ring_with_nat)" - and odd_uminusI: "odd a \ odd (-a :: 'a :: unique_euclidean_ring_with_nat)" +lemma even_uminusI: "even a \ even (-a :: int)" + and odd_uminusI: "odd a \ odd (-a :: int)" by auto lemma odd_powerI: "odd a \ odd (a ^ n)" diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Thu Nov 09 15:11:51 2023 +0000 +++ b/src/HOL/Set_Interval.thy Thu Nov 09 15:11:52 2023 +0000 @@ -2461,7 +2461,7 @@ end -context unique_euclidean_semiring_with_nat +context linordered_euclidean_semiring begin lemma gauss_sum: