generalized
authorhaftmann
Tue Mar 20 09:27:39 2018 +0000 (14 months ago)
changeset 67905fe0f4eeceeb7
parent 67904 465f43a9f780
child 67906 9cc32b18c785
generalized
src/HOL/Code_Numeral.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Mar 19 19:24:45 2018 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Mar 20 09:27:39 2018 +0000
     1.3 @@ -889,6 +889,9 @@
     1.4    "division_segment (n::natural) = 1"
     1.5    by (simp add: natural_eq_iff)
     1.6  
     1.7 +instance natural :: linordered_semidom
     1.8 +  by (standard; transfer) simp_all
     1.9 +
    1.10  instance natural :: semiring_parity
    1.11    by (standard; transfer) simp_all
    1.12  
     2.1 --- a/src/HOL/Parity.thy	Mon Mar 19 19:24:45 2018 +0100
     2.2 +++ b/src/HOL/Parity.thy	Tue Mar 20 09:27:39 2018 +0000
     2.3 @@ -11,7 +11,7 @@
     2.4  
     2.5  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
     2.6  
     2.7 -class semiring_parity = linordered_semidom + unique_euclidean_semiring +
     2.8 +class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring +
     2.9    assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
    2.10      and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
    2.11      and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"