# HG changeset patch
# User haftmann
# Date 1433177962 -7200
# Node ID 838025c6e278d2daed6d1fe4a301a06125f1383b
# Parent  d46de31a50c483faf71434410114d1567f57ea62
implicit partial divison operation in integral domains

diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Divides.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -31,7 +31,13 @@
     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
-subclass semiring_no_zero_divisors ..
+subclass semidom_divide
+proof
+  fix b a
+  assume "b \<noteq> 0"
+  then show "a * b div b = a"
+    using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
+qed simp
 
 lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
   "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
@@ -107,11 +113,13 @@
   "(b * c + a) mod b = a mod b"
   by (simp add: add.commute)
 
-lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
-  using div_mult_self2 [of b 0 a] by simp
-
-lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
-  using div_mult_self1 [of b 0 a] by simp
+lemma div_mult_self1_is_id:
+  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+  by (fact nonzero_mult_divide_cancel_left)
+
+lemma div_mult_self2_is_id:
+  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+  by (fact nonzero_mult_divide_cancel_right)
 
 lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
   using mod_mult_self2 [of 0 b a] by simp
@@ -439,21 +447,21 @@
 next
   assume "b div a = c"
   then have "b div a * a = c * a" by simp
-  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
+  moreover from `a dvd b` have "b div a * a = b" by simp
   ultimately show "b = c * a" by simp
 qed
    
 lemma dvd_div_div_eq_mult:
   assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
   shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
-  using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
+  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
 
 end
 
 class ring_div = comm_ring_1 + semiring_div
 begin
 
-subclass idom ..
+subclass idom_divide ..
 
 text {* Negation respects modular equivalence. *}
 
diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Fields.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -221,7 +221,7 @@
   "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
   by (simp add: divide_diff_eq_iff[symmetric])
 
-lemma divide_zero [simp]:
+lemma division_ring_divide_zero [simp]:
   "a / 0 = 0"
   by (simp add: divide_inverse)
 
@@ -300,18 +300,31 @@
     by (fact field_inverse_zero) 
 qed
 
-subclass idom ..
+subclass idom_divide
+proof
+  fix b a
+  assume "b \<noteq> 0"
+  then show "a * b / b = a"
+    by (simp add: divide_inverse ac_simps)
+next
+  fix a
+  show "a / 0 = 0"
+    by (simp add: divide_inverse)
+qed
 
 text{*There is no slick version using division by zero.*}
 lemma inverse_add:
-  "[| a \<noteq> 0;  b \<noteq> 0 |]
-   ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
-by (simp add: division_ring_inverse_add ac_simps)
+  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
+  by (simp add: division_ring_inverse_add ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_left [simp]:
-assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
-proof -
-  have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
+  assumes [simp]: "c \<noteq> 0"
+  shows "(c * a) / (c * b) = a / b"
+proof (cases "b = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
     by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   also have "... =  a * inverse b * (inverse c * c)"
     by (simp only: ac_simps)
@@ -320,8 +333,8 @@
 qed
 
 lemma nonzero_mult_divide_mult_cancel_right [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
-by (simp add: mult.commute [of _ c])
+  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
+  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
 
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse ac_simps)
@@ -340,33 +353,24 @@
 
 text{*Special Cancellation Simprules for Division*}
 
-lemma nonzero_mult_divide_cancel_right [simp]:
-  "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
-  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
-
-lemma nonzero_mult_divide_cancel_left [simp]:
-  "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
-using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
-
 lemma nonzero_divide_mult_cancel_right [simp]:
-  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
-using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
+  "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
+  using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
 
 lemma nonzero_divide_mult_cancel_left [simp]:
-  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
-using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
+  "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
+  using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
 
 lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
-using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
+  "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
+  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
 
 lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
-  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
-using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
+  "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
+  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
 
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
-  thm field_simps
   by (simp add: field_simps)
 
 lemma frac_eq_eq:
@@ -427,7 +431,7 @@
 
 lemma mult_divide_mult_cancel_left_if [simp]:
   shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
-  by (simp add: mult_divide_mult_cancel_left)
+  by simp
 
 
 text {* Division and Unary Minus *}
diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -1153,10 +1153,29 @@
   shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   using assms by (induct A) (auto simp: no_zero_divisors)
 
-lemma (in field) setprod_diff1:
-  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
-    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
-  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
+lemma (in semidom_divide) setprod_diff1:
+  assumes "finite A" and "f a \<noteq> 0"
+  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
+proof (cases "a \<notin> A")
+  case True then show ?thesis by simp
+next
+  case False with assms show ?thesis
+  proof (induct A rule: finite_induct)
+    case empty then show ?case by simp
+  next
+    case (insert b B)
+    then show ?case
+    proof (cases "a = b")
+      case True with insert show ?thesis by simp
+    next
+      case False with insert have "a \<in> B" by simp
+      def C \<equiv> "B - {a}"
+      with `finite B` `a \<in> B`
+        have *: "B = insert a C" "finite C" "a \<notin> C" by auto
+      with insert show ?thesis by (auto simp add: insert_commute ac_simps)
+    qed
+  qed
+qed
 
 lemma (in field) setprod_inversef: 
   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
diff -r d46de31a50c4 -r 838025c6e278 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -853,6 +853,13 @@
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (semidom) semidom ..
+instance star :: (semidom_divide) semidom_divide
+proof
+  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+    by transfer simp
+  show "\<And>a :: 'a star. divide a 0 = 0"
+    by transfer simp
+qed
 instance star :: (semiring_div) semiring_div
 apply intro_classes
 apply(transfer, rule mod_div_equality)
@@ -865,6 +872,7 @@
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
 instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom .. 
+instance star :: (idom_divide) idom_divide ..
 
 instance star :: (division_ring) division_ring
 apply (intro_classes)
diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Nat.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -1484,6 +1484,14 @@
 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
+lemma of_nat_neq_0 [simp]:
+  "of_nat (Suc n) \<noteq> 0"
+  unfolding of_nat_eq_0_iff by simp
+
+lemma of_nat_0_neq [simp]:
+  "0 \<noteq> of_nat (Suc n)"
+  unfolding of_nat_0_eq_iff by simp  
+  
 end
 
 context linordered_semidom
diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Rings.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -415,33 +415,6 @@
 
 end
 
-class divide =
-  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
-context semiring
-begin
-
-lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
-  by (rule distrib_left distrib_right)+
-
-end
-
-context ring
-begin
-
-lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
-  by (rule left_diff_distrib right_diff_distrib)+
-
-end
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-  
 class semiring_no_zero_divisors = semiring_0 +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 begin
@@ -585,6 +558,46 @@
   \end{itemize}
 *}
 
+class divide =
+  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+context semiring
+begin
+
+lemma [field_simps]:
+  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
+    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
+  by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
+    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
+  by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+class semidom_divide = semidom + divide +
+  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
+  assumes divide_zero [simp]: "divide a 0 = 0"
+begin
+
+lemma nonzero_mult_divide_cancel_left [simp]:
+  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
+  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
+
+end
+
+class idom_divide = idom + semidom_divide
+
 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"