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 -