distributivity of partial minus establishes desired properties of dvd in semirings

--- a/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -217,9 +217,7 @@
 
 instance integer :: semiring_numeral_div
   by intro_classes (transfer,
-    fact semiring_numeral_div_class.diff_invert_add1
-    semiring_numeral_div_class.le_add_diff_inverse2
-    semiring_numeral_div_class.mult_div_cancel
+    fact semiring_numeral_div_class.le_add_diff_inverse2
     semiring_numeral_div_class.div_less
     semiring_numeral_div_class.mod_less
     semiring_numeral_div_class.div_positive

--- a/src/HOL/Divides.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Divides.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -548,7 +548,7 @@
 
 subsubsection {* Parity and division *}
 
-class semiring_div_parity = semiring_div + semiring_numeral +
+class semiring_div_parity = comm_semiring_1_diff_distrib + numeral + semiring_div +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   assumes zero_not_eq_two: "0 \<noteq> 2"
@@ -583,19 +583,6 @@
 
 subclass semiring_parity
 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
-  fix a b c
-  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
-    by simp
-next
-  fix a b c
-  assume "(b + c) mod a = 0"
-  with mod_add_eq [of b c a]
-  have "(b mod a + c mod a) mod a = 0"
-    by simp
-  moreover assume "b mod a = 0"
-  ultimately show "c mod a = 0"
-    by simp
-next
   show "1 mod 2 = 1"
     by (fact one_mod_two_eq_one)
 next
@@ -651,11 +638,9 @@
   and less technical class hierarchy.
 *}
 
-class semiring_numeral_div = linordered_semidom + minus + semiring_div +
-  assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
-    and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
-  assumes mult_div_cancel: "b * (a div b) = a - a mod b"
-    and div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
+class semiring_numeral_div = comm_semiring_1_diff_distrib + linordered_semidom + semiring_div +
+  assumes le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
+  assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
@@ -666,9 +651,16 @@
   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
 begin
 
-lemma diff_zero [simp]:
-  "a - 0 = a"
-  by (rule diff_invert_add1 [symmetric]) simp
+lemma mult_div_cancel:
+  "b * (a div b) = a - a mod b"
+proof -
+  have "b * (a div b) + a mod b = a"
+    using mod_div_equality [of a b] by (simp add: ac_simps)
+  then have "b * (a div b) + a mod b - a mod b = a - a mod b"
+    by simp
+  then show ?thesis
+    by simp
+qed
 
 subclass semiring_div_parity
 proof
@@ -713,7 +705,7 @@
     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
   with `w = 1` have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   then show ?P and ?Q
-    by (simp_all add: div mod diff_invert_add1 [symmetric] le_add_diff_inverse2)
+    by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
 qed
 
 lemma divmod_digit_0:
@@ -862,7 +854,7 @@
 
 end
 
-hide_fact (open) diff_invert_add1 le_add_diff_inverse2 diff_zero
+hide_fact (open) le_add_diff_inverse2
   -- {* restore simple accesses for more general variants of theorems *}
 
   

--- a/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -698,7 +698,7 @@
   star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
 
 instance
-  by default (transfer star_inf_def, auto)+
+  by default (transfer, auto)+
 
 end
 
@@ -709,7 +709,7 @@
   star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
 
 instance
-  by default (transfer star_sup_def, auto)+
+  by default (transfer, auto)+
 
 end
 
@@ -850,11 +850,8 @@
 
 declare dvd_def [transfer_refold]
 
-instance star :: (semiring_dvd) semiring_dvd
-apply intro_classes
-apply(transfer, rule dvd_add_times_triv_left_iff)
-apply(transfer, erule (1) dvd_addD)
-done
+instance star :: (comm_semiring_1_diff_distrib) comm_semiring_1_diff_distrib
+by intro_classes (transfer, fact right_diff_distrib')
 
 instance star :: (no_zero_divisors) no_zero_divisors
 by (intro_classes, transfer, rule no_zero_divisors)
@@ -1040,18 +1037,16 @@
 
 instance star :: (semiring_numeral_div) semiring_numeral_div
 apply intro_classes
-apply(transfer, erule semiring_numeral_div_class.diff_invert_add1)
-apply(transfer, erule semiring_numeral_div_class.le_add_diff_inverse2)
-apply(transfer, rule semiring_numeral_div_class.mult_div_cancel)
-apply(transfer, erule (1) semiring_numeral_div_class.div_less)
-apply(transfer, erule (1) semiring_numeral_div_class.mod_less)
-apply(transfer, erule (1) semiring_numeral_div_class.div_positive)
-apply(transfer, erule semiring_numeral_div_class.mod_less_eq_dividend)
-apply(transfer, erule semiring_numeral_div_class.pos_mod_bound)
-apply(transfer, erule semiring_numeral_div_class.pos_mod_sign)
-apply(transfer, erule semiring_numeral_div_class.mod_mult2_eq)
-apply(transfer, erule semiring_numeral_div_class.div_mult2_eq)
-apply(transfer, rule discrete)
+apply(transfer, fact semiring_numeral_div_class.le_add_diff_inverse2)
+apply(transfer, fact semiring_numeral_div_class.div_less)
+apply(transfer, fact semiring_numeral_div_class.mod_less)
+apply(transfer, fact semiring_numeral_div_class.div_positive)
+apply(transfer, fact semiring_numeral_div_class.mod_less_eq_dividend)
+apply(transfer, fact semiring_numeral_div_class.pos_mod_bound)
+apply(transfer, fact semiring_numeral_div_class.pos_mod_sign)
+apply(transfer, fact semiring_numeral_div_class.mod_mult2_eq)
+apply(transfer, fact semiring_numeral_div_class.div_mult2_eq)
+apply(transfer, fact discrete)
 done
 
 subsection {* Finite class *}

--- a/src/HOL/NSA/transfer.ML	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/NSA/transfer.ML	Mon Mar 23 19:05:14 2015 +0100
@@ -68,7 +68,7 @@
   in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
 
 fun transfer_tac ctxt ths =
-    SUBGOAL (fn (t,i) =>
+    SUBGOAL (fn (t, _) =>
         (fn th =>
             let
               val tr = transfer_thm_of ctxt ths t

--- a/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -366,12 +366,20 @@
 
 text {* Difference distributes over multiplication *}
 
-lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
-by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
-
-lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
-by (simp add: diff_mult_distrib mult.commute [of k])
-  -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
+instance nat :: comm_semiring_1_diff_distrib
+proof
+  fix k m n :: nat
+  show "k * ((m::nat) - n) = (k * m) - (k * n)"
+    by (induct m n rule: diff_induct) simp_all
+qed
+
+lemma diff_mult_distrib:
+  "((m::nat) - n) * k = (m * k) - (n * k)"
+  by (fact left_diff_distrib')
+  
+lemma diff_mult_distrib2:
+  "k * ((m::nat) - n) = (k * m) - (k * n)"
+  by (fact right_diff_distrib')
 
 
 subsubsection {* Multiplication *}
@@ -1876,48 +1884,6 @@
 
 subsection {* The divides relation on @{typ nat} *}
 
-instance nat :: semiring_dvd
-proof
-  fix m n q :: nat
-  show "m dvd q * m + n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
-  proof
-    assume ?Q then show ?P by simp
-  next
-    assume ?P then obtain d where *: "q * m + n = m * d" ..
-    show ?Q
-    proof (cases "n = 0")
-      case True then show ?Q by simp
-    next
-      case False
-      with * have "q * m < m * d"
-        using less_add_eq_less [of 0 n "q * m" "m * d"] by simp
-      then have "q \<le> d" by (auto intro: ccontr simp add: mult.commute [of m])
-      with * [symmetric] have "n = m * (d - q)"
-        by (simp add: diff_mult_distrib2 mult.commute [of m])
-      then show ?Q ..
-    qed
-  qed
-  assume "m dvd n + q" and "m dvd n"
-  show "m dvd q"
-  proof -
-    from `m dvd n` obtain d where "n = m * d" ..
-    moreover from `m dvd n + q` obtain e where "n + q = m * e" ..
-    ultimately have *: "m * d + q = m * e" by simp
-    show "m dvd q"
-    proof (cases "q = 0")
-      case True then show ?thesis by simp
-    next
-      case False
-      with * have "m * d < m * e"
-        using less_add_eq_less [of 0 q "m * d" "m * e"] by simp
-      then have "d \<le> e" by (auto intro: ccontr)
-      with * have "q = m * (e - d)"
-        by (simp add: diff_mult_distrib2)
-      then show ?thesis ..
-    qed
-  qed
-qed
-
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
 unfolding dvd_def by simp
 

--- a/src/HOL/Number_Theory/Cong.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -443,7 +443,7 @@
   apply (erule ssubst)
   apply (subst zmod_zmult2_eq)
   apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
-  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
+  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+
   done
 
 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"

--- a/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Parity.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -11,13 +11,15 @@
 
 subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
 
-class semiring_parity = semiring_dvd + semiring_numeral +
+class semiring_parity = comm_semiring_1_diff_distrib + numeral +
   assumes odd_one [simp]: "\<not> 2 dvd 1"
   assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
   assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
   assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
 begin
 
+subclass semiring_numeral ..
+
 abbreviation even :: "'a \<Rightarrow> bool"
 where
   "even a \<equiv> 2 dvd a"
@@ -97,9 +99,11 @@
 
 end
 
-class ring_parity = comm_ring_1 + semiring_parity
+class ring_parity = ring + semiring_parity
 begin
 
+subclass comm_ring_1 ..
+
 lemma even_minus [simp]:
   "even (- a) \<longleftrightarrow> even a"
   by (fact dvd_minus_iff)

--- a/src/HOL/Rings.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Rings.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -228,35 +228,6 @@
 
 end
 
-class semiring_dvd = comm_semiring_1 +
-  assumes dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
-  assumes dvd_addD: "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
-begin
-
-lemma dvd_add_times_triv_right_iff [simp]:
-  "a dvd b + c * a \<longleftrightarrow> a dvd b"
-  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
-
-lemma dvd_add_triv_left_iff [simp]:
-  "a dvd a + b \<longleftrightarrow> a dvd b"
-  using dvd_add_times_triv_left_iff [of a 1 b] by simp
-
-lemma dvd_add_triv_right_iff [simp]:
-  "a dvd b + a \<longleftrightarrow> a dvd b"
-  using dvd_add_times_triv_right_iff [of a b 1] by simp
-
-lemma dvd_add_right_iff:
-  assumes "a dvd b"
-  shows "a dvd b + c \<longleftrightarrow> a dvd c"
-  using assms by (auto dest: dvd_addD)
-
-lemma dvd_add_left_iff:
-  assumes "a dvd c"
-  shows "a dvd b + c \<longleftrightarrow> a dvd b"
-  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
-
-end
-
 class no_zero_divisors = zero + times +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 begin
@@ -293,6 +264,65 @@
 
 end
 
+class comm_semiring_1_diff_distrib = comm_semiring_1_cancel +
+  assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c"
+begin
+
+lemma left_diff_distrib' [algebra_simps]:
+  "(b - c) * a = b * a - c * a"
+  by (simp add: algebra_simps)
+
+lemma dvd_add_times_triv_left_iff [simp]:
+  "a dvd c * a + b \<longleftrightarrow> a dvd b"
+proof -
+  have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
+  proof
+    assume ?Q then show ?P by simp
+  next
+    assume ?P
+    then obtain d where "a * c + b = a * d" ..
+    then have "a * c + b - a * c = a * d - a * c" by simp
+    then have "b = a * d - a * c" by simp
+    then have "b = a * (d - c)" by (simp add: algebra_simps) 
+    then show ?Q ..
+  qed
+  then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps)
+qed
+
+lemma dvd_add_times_triv_right_iff [simp]:
+  "a dvd b + c * a \<longleftrightarrow> a dvd b"
+  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
+
+lemma dvd_add_triv_left_iff [simp]:
+  "a dvd a + b \<longleftrightarrow> a dvd b"
+  using dvd_add_times_triv_left_iff [of a 1 b] by simp
+
+lemma dvd_add_triv_right_iff [simp]:
+  "a dvd b + a \<longleftrightarrow> a dvd b"
+  using dvd_add_times_triv_right_iff [of a b 1] by simp
+
+lemma dvd_add_right_iff:
+  assumes "a dvd b"
+  shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then obtain d where "b + c = a * d" ..
+  moreover from `a dvd b` obtain e where "b = a * e" ..
+  ultimately have "a * e + c = a * d" by simp
+  then have "a * e + c - a * e = a * d - a * e" by simp
+  then have "c = a * d - a * e" by simp
+  then have "c = a * (d - e)" by (simp add: algebra_simps)
+  then show ?Q ..
+next
+  assume ?Q with assms show ?P by simp
+qed
+
+lemma dvd_add_left_iff:
+  assumes "a dvd c"
+  shows "a dvd b + c \<longleftrightarrow> a dvd b"
+  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
+
+end
+
 class ring = semiring + ab_group_add
 begin
 
@@ -370,27 +400,8 @@
 subclass ring_1 ..
 subclass comm_semiring_1_cancel ..
 
-subclass semiring_dvd
-proof
-  fix a b c
-  show "a dvd c * a + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
-  proof
-    assume ?Q then show ?P by simp
-  next
-    assume ?P then obtain d where "c * a + b = a * d" ..
-    then have "b = a * (d - c)" by (simp add: algebra_simps)
-    then show ?Q ..
-  qed
-  assume "a dvd b + c" and "a dvd b"
-  show "a dvd c"
-  proof -
-    from `a dvd b` obtain d where "b = a * d" ..
-    moreover from `a dvd b + c` obtain e where "b + c = a * e" ..
-    ultimately have "a * d + c = a * e" by simp
-    then have "c = a * (e - d)" by (simp add: algebra_simps)
-    then show "a dvd c" ..
-  qed
-qed
+subclass comm_semiring_1_diff_distrib
+  by unfold_locales (simp add: algebra_simps)
 
 lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
 proof
@@ -1265,4 +1276,3 @@
   code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-