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)