src/HOL/Divides.thy
 changeset 59833 ab828c2c5d67 parent 59816 034b13f4efae child 60352 d46de31a50c4
```     1.1 --- a/src/HOL/Divides.thy	Sat Mar 28 20:43:19 2015 +0100
1.2 +++ b/src/HOL/Divides.thy	Sat Mar 28 21:32:48 2015 +0100
1.3 @@ -18,7 +18,7 @@
1.4
1.5  subsection {* Abstract division in commutative semirings. *}
1.6
1.7 -class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
1.8 +class semiring_div = semidom + div +
1.9    assumes mod_div_equality: "a div b * b + a mod b = a"
1.10      and div_by_0 [simp]: "a div 0 = 0"
1.11      and div_0 [simp]: "0 div a = 0"
1.12 @@ -445,10 +445,10 @@
1.13
1.14  end
1.15
1.16 -class ring_div = semiring_div + comm_ring_1
1.17 +class ring_div = comm_ring_1 + semiring_div
1.18  begin
1.19
1.20 -subclass ring_1_no_zero_divisors ..
1.21 +subclass idom ..
1.22
1.23  text {* Negation respects modular equivalence. *}
1.24
1.25 @@ -548,7 +548,7 @@
1.26
1.27  subsubsection {* Parity and division *}
1.28
1.29 -class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div +
1.30 +class semiring_div_parity = semiring_div + comm_semiring_1_diff_distrib + numeral +
1.31    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
1.32    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
1.33    assumes zero_not_eq_two: "0 \<noteq> 2"
1.34 @@ -638,7 +638,7 @@
1.35    and less technical class hierarchy.
1.36  *}
1.37
1.38 -class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div +
1.39 +class semiring_numeral_div = semiring_div + comm_semiring_1_diff_distrib + linordered_semidom +
1.40    assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
1.41    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
1.42      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
1.43 @@ -2849,4 +2849,3 @@
1.44    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
1.45
1.46  end
1.47 -
```