src/HOL/Parity.thy
 changeset 59816 034b13f4efae parent 58889 5b7a9633cfa8 child 60343 063698416239
```     1.1 --- a/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
1.2 +++ b/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
1.3 @@ -11,13 +11,15 @@
1.4
1.5  subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
1.6
1.7 -class semiring_parity = semiring_dvd + semiring_numeral +
1.8 +class semiring_parity = comm_semiring_1_diff_distrib + numeral +
1.9    assumes odd_one [simp]: "\<not> 2 dvd 1"
1.10    assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
1.11    assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
1.12    assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
1.13  begin
1.14
1.15 +subclass semiring_numeral ..
1.16 +
1.17  abbreviation even :: "'a \<Rightarrow> bool"
1.18  where
1.19    "even a \<equiv> 2 dvd a"
1.20 @@ -97,9 +99,11 @@
1.21
1.22  end
1.23
1.24 -class ring_parity = comm_ring_1 + semiring_parity
1.25 +class ring_parity = ring + semiring_parity
1.26  begin
1.27
1.28 +subclass comm_ring_1 ..
1.29 +
1.30  lemma even_minus [simp]:
1.31    "even (- a) \<longleftrightarrow> even a"
1.32    by (fact dvd_minus_iff)
```