src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -59,13 +59,12 @@
 
 axclass field \<subseteq> ring, inverse
   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
-  divide_inverse:      "b \<noteq> 0 ==> a / b = a * inverse b"
+  divide_inverse:      "a / b = a * inverse b"
 
 axclass ordered_field \<subseteq> ordered_ring, field
 
 axclass division_by_zero \<subseteq> zero, inverse
   inverse_zero [simp]: "inverse 0 = 0"
-  divide_zero [simp]: "a / 0 = 0"
 
 
 subsection {* Derived Rules for Addition *}
@@ -595,7 +594,7 @@
 instance ordered_ring \<subseteq> ordered_semiring
 proof
   have "(0::'a) \<le> 1*1" by (rule zero_le_square)
-  thus "(0::'a) < 1" by (simp add: order_le_less ) 
+  thus "(0::'a) < 1" by (simp add: order_le_less) 
 qed
 
 text{*All three types of comparision involving 0 and 1 are covered.*}
@@ -650,7 +649,7 @@
 
 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)"
 apply (insert mult_strict_mono [of 1 m 1 n]) 
-apply (simp add:  order_less_trans [OF zero_less_one]); 
+apply (simp add:  order_less_trans [OF zero_less_one]) 
 done
 
 
@@ -743,24 +742,18 @@
 lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   by (simp add: divide_inverse)
 
-lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
-apply (case_tac "b = 0")
-apply (simp_all add: divide_inverse)
-done
+lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
+by (simp add: divide_inverse)
 
-lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero)
+lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
+by (simp add: divide_inverse)
 
-lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
-by (simp add: divide_inverse_zero)
+lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
+by (simp add: divide_inverse)
 
-lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
+lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
 by (simp add: divide_inverse left_distrib) 
 
-lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
-apply (case_tac "c=0", simp) 
-apply (simp add: nonzero_add_divide_distrib) 
-done
 
 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
       of an ordering.*}
@@ -935,7 +928,7 @@
 
 lemma inverse_divide [simp]:
       "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
-  by (simp add: divide_inverse_zero mult_commute)
+  by (simp add: divide_inverse mult_commute)
 
 lemma nonzero_mult_divide_cancel_left:
   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
@@ -975,23 +968,21 @@
   by (simp add: mult_divide_cancel_left)
 
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
-  by (simp add: divide_inverse [OF not_sym])
+  by (simp add: divide_inverse)
 
-lemma times_divide_eq_right [simp]:
-     "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_assoc)
+lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
+by (simp add: divide_inverse mult_assoc)
 
-lemma times_divide_eq_left [simp]:
-     "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
+by (simp add: divide_inverse mult_ac)
 
 lemma divide_divide_eq_right [simp]:
      "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+by (simp add: divide_inverse mult_ac)
 
 lemma divide_divide_eq_left [simp]:
      "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
-by (simp add: divide_inverse_zero mult_assoc)
+by (simp add: divide_inverse mult_assoc)
 
 
 subsection {* Division and Unary Minus *}
@@ -1005,14 +996,12 @@
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
 by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
-lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp) 
-apply (simp add: nonzero_minus_divide_left) 
-done
+lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
+by (simp add: divide_inverse minus_mult_left [symmetric])
 
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp) 
-by (rule nonzero_minus_divide_right) 
+by (simp add: divide_inverse minus_mult_right [symmetric])
+
 
 text{*The effect is to extract signs from divisions*}
 declare minus_divide_left  [symmetric, simp]
@@ -1028,8 +1017,7 @@
 apply (simp add: nonzero_minus_divide_divide) 
 done
 
-lemma diff_divide_distrib:
-     "(a-b)/(c::'a::{field,division_by_zero}) = a/c - b/c"
+lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
 by (simp add: diff_minus add_divide_distrib) 
 
 
@@ -1236,26 +1224,26 @@
 
 lemma zero_less_divide_iff:
      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
-by (simp add: divide_inverse_zero zero_less_mult_iff)
+by (simp add: divide_inverse zero_less_mult_iff)
 
 lemma divide_less_0_iff:
      "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
       (0 < a & b < 0 | a < 0 & 0 < b)"
-by (simp add: divide_inverse_zero mult_less_0_iff)
+by (simp add: divide_inverse mult_less_0_iff)
 
 lemma zero_le_divide_iff:
      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse_zero zero_le_mult_iff)
+by (simp add: divide_inverse zero_le_mult_iff)
 
 lemma divide_le_0_iff:
      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
-by (simp add: divide_inverse_zero mult_le_0_iff)
+by (simp add: divide_inverse mult_le_0_iff)
 
 lemma divide_eq_0_iff [simp]:
      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse_zero field_mult_eq_0_iff)
+by (simp add: divide_inverse field_mult_eq_0_iff)
 
 
 subsection{*Simplification of Inequalities Involving Literal Divisors*}
@@ -1415,13 +1403,13 @@
 lemma divide_cancel_right [simp]:
      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
 apply (case_tac "c=0", simp) 
-apply (simp add: divide_inverse_zero field_mult_cancel_right) 
+apply (simp add: divide_inverse field_mult_cancel_right) 
 done
 
 lemma divide_cancel_left [simp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
 apply (case_tac "c=0", simp) 
-apply (simp add: divide_inverse_zero field_mult_cancel_left) 
+apply (simp add: divide_inverse field_mult_cancel_left) 
 done
 
 subsection {* Division and the Number One *}
@@ -1669,6 +1657,9 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
+text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
+declare times_divide_eq_left [simp]
+
 ML
 {*
 val add_assoc = thm"add_assoc";
@@ -1809,11 +1800,9 @@
 val right_inverse_eq = thm"right_inverse_eq";
 val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
 val divide_self = thm"divide_self";
-val divide_inverse_zero = thm"divide_inverse_zero";
 val inverse_divide = thm"inverse_divide";
 val divide_zero_left = thm"divide_zero_left";
 val inverse_eq_divide = thm"inverse_eq_divide";
-val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
 val add_divide_distrib = thm"add_divide_distrib";
 val field_mult_eq_0_iff = thm"field_mult_eq_0_iff";
 val field_mult_cancel_right = thm"field_mult_cancel_right";