refactor(library/data/nat): move nat.comm_semiring to separate file

library/data/nat/basic.lean

@@ -7,10 +7,8 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
 
 Basic operations on the natural numbers.
 -/
-
+import logic.connectives data.num algebra.binary
-import logic.connectives data.num algebra.binary algebra.ring
+open binary eq.ops
-
-open eq.ops binary
 
 namespace nat
 
@@ -288,44 +286,4 @@ cases_on n
              ... = succ n' * m' + succ n' : mul_succ
              ... = succ (succ n' * m' + n') : add_succ)⁻¹)
           !succ_ne_zero))
-
-section
-  open [classes] algebra
-
-  protected definition comm_semiring [instance] : algebra.comm_semiring nat :=
-  algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
-    mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
-    zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
-end
-
-section port_algebra
-  theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
-  theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
-
-  definition dvd (a b : ℕ) : Prop := algebra.dvd a b
-  infix `|` := dvd
-  theorem dvd.intro : ∀{a b c : ℕ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
-  theorem dvd.ex : ∀{a b : ℕ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
-  theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
-    @algebra.dvd.elim _ _
-  theorem dvd.refl : ∀a : ℕ, a | a := algebra.dvd.refl
-  theorem dvd.trans : ∀{a b c : ℕ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _
-  theorem eq_zero_of_zero_dvd : ∀{a : ℕ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
-  theorem dvd_zero : ∀a : ℕ, a | 0 := algebra.dvd_zero
-  theorem one_dvd : ∀a : ℕ, 1 | a := algebra.one_dvd
-  theorem dvd_mul_right : ∀a b : ℕ, a | a * b := algebra.dvd_mul_right
-  theorem dvd_mul_left : ∀a b : ℕ, a | b * a := algebra.dvd_mul_left
-  theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | b * c :=
-    @algebra.dvd_mul_of_dvd_left _ _
-  theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | c * b :=
-    @algebra.dvd_mul_of_dvd_right _ _
-  theorem mul_dvd_mul : ∀{a b c d : ℕ}, a | b → c | d → a * c | b * d :=
-    @algebra.mul_dvd_mul _ _
-  theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, a * b | c → a | c :=
-    @algebra.dvd_of_mul_right_dvd _ _
-  theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, a * b | c → b | c :=
-    @algebra.dvd_of_mul_left_dvd _ _
-  theorem dvd_add : ∀{a b c : ℕ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _
-end port_algebra
-
 end nat

library/data/nat/comm_semiring.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.nat.algebra
+Authors: Jeremy Avigad
+
+nat is a comm_semiring
+-/
+import data.nat.basic algebra.binary algebra.ring
+open binary
+
+namespace nat
+section
+  open [classes] algebra
+
+  protected definition comm_semiring [instance] : algebra.comm_semiring nat :=
+  algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
+    mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
+    zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
+end
+
+section port_algebra
+  theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
+  theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
+
+  definition dvd (a b : ℕ) : Prop := algebra.dvd a b
+  infix `|` := dvd
+  theorem dvd.intro : ∀{a b c : ℕ} (H : a * b = c), a | c := @algebra.dvd.intro _ _
+  theorem dvd.ex : ∀{a b : ℕ} (H : a | b), ∃c, a * c = b := @algebra.dvd.ex _ _
+  theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a | b) (H₂ : ∀c, a * c = b → P), P :=
+    @algebra.dvd.elim _ _
+  theorem dvd.refl : ∀a : ℕ, a | a := algebra.dvd.refl
+  theorem dvd.trans : ∀{a b c : ℕ} (H₁ : a | b) (H₂ : b | c), a | c := @algebra.dvd.trans _ _
+  theorem eq_zero_of_zero_dvd : ∀{a : ℕ} (H : 0 | a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
+  theorem dvd_zero : ∀a : ℕ, a | 0 := algebra.dvd_zero
+  theorem one_dvd : ∀a : ℕ, 1 | a := algebra.one_dvd
+  theorem dvd_mul_right : ∀a b : ℕ, a | a * b := algebra.dvd_mul_right
+  theorem dvd_mul_left : ∀a b : ℕ, a | b * a := algebra.dvd_mul_left
+  theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | b * c :=
+    @algebra.dvd_mul_of_dvd_left _ _
+  theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : a | b) (c : ℕ), a | c * b :=
+    @algebra.dvd_mul_of_dvd_right _ _
+  theorem mul_dvd_mul : ∀{a b c d : ℕ}, a | b → c | d → a * c | b * d :=
+    @algebra.mul_dvd_mul _ _
+  theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, a * b | c → a | c :=
+    @algebra.dvd_of_mul_right_dvd _ _
+  theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, a * b | c → b | c :=
+    @algebra.dvd_of_mul_left_dvd _ _
+  theorem dvd_add : ∀{a b c : ℕ}, a | b → a | c → a | b + c := @algebra.dvd_add _ _
+end port_algebra
+end nat

library/data/nat/default.lean

@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import .basic .order .sub .div .bquant
+import .basic .order .sub .div .bquant .comm_semiring

library/data/nat/div.lean

@@ -8,7 +8,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Definitions of div, mod, and gcd on the natural numbers.
 -/
 
-import data.nat.sub logic
+import data.nat.sub data.nat.comm_semiring logic
 import algebra.relation
 import tools.fake_simplifier