--- a/src/HOL/Parity.thy Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Parity.thy Mon Mar 23 19:05:14 2015 +0100
@@ -11,13 +11,15 @@
subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
-class semiring_parity = semiring_dvd + semiring_numeral +
+class semiring_parity = comm_semiring_1_diff_distrib + numeral +
assumes odd_one [simp]: "\<not> 2 dvd 1"
assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
begin
+subclass semiring_numeral ..
+
abbreviation even :: "'a \<Rightarrow> bool"
where
"even a \<equiv> 2 dvd a"
@@ -97,9 +99,11 @@
end
-class ring_parity = comm_ring_1 + semiring_parity
+class ring_parity = ring + semiring_parity
begin
+subclass comm_ring_1 ..
+
lemma even_minus [simp]:
"even (- a) \<longleftrightarrow> even a"
by (fact dvd_minus_iff)