# HG changeset patch
# User huffman
# Date 1231437516 28800
# Node ID 54bac26089bd9be92a9deed69d4f777dbbb7038f
# Parent  98ab21b14f09eb612415f4813cc46ecab15d1ccb
clean up division_ring proofs

diff -r 98ab21b14f09 -r 54bac26089bd src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Jan 08 09:12:29 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Thu Jan 08 09:58:36 2009 -0800
@@ -397,67 +397,47 @@
 apply auto
 done
 
-lemma nonzero_inverse_minus_eq:
-  assumes "a \<noteq> 0"
-  shows "inverse (- a) = - inverse a"
-proof -
-  have "- a * inverse (- a) = - a * - inverse a"
-    using assms by simp
-  then show ?thesis unfolding mult_cancel_left using assms by simp 
-qed
-
-lemma nonzero_inverse_inverse_eq:
-  assumes "a \<noteq> 0"
-  shows "inverse (inverse a) = a"
-proof -
-  have "(inverse (inverse a) * inverse a) * a = a" 
-    using assms by (simp add: nonzero_imp_inverse_nonzero)
-  then show ?thesis using assms by (simp add: mult_assoc)
-qed
-
-lemma nonzero_inverse_eq_imp_eq:
-  assumes inveq: "inverse a = inverse b"
-    and anz:  "a \<noteq> 0"
-    and bnz:  "b \<noteq> 0"
-  shows "a = b"
-proof -
-  have "a * inverse b = a * inverse a"
-    by (simp add: inveq)
-  hence "(a * inverse b) * b = (a * inverse a) * b"
-    by simp
-  then show "a = b"
-    by (simp add: mult_assoc anz bnz)
-qed
-
-lemma inverse_1 [simp]: "inverse 1 = 1"
-proof -
-  have "inverse 1 * 1 = 1" 
-    by (rule left_inverse) (rule one_neq_zero)
-  then show ?thesis by simp
-qed
-
 lemma inverse_unique: 
   assumes ab: "a * b = 1"
   shows "inverse a = b"
 proof -
   have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
-  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
-  ultimately show ?thesis by (simp add: mult_assoc [symmetric]) 
+  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
+  ultimately show ?thesis by (simp add: mult_assoc [symmetric])
 qed
 
+lemma nonzero_inverse_minus_eq:
+  "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+  by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+  "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+  by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+  assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+  shows "a = b"
+proof -
+  from `inverse a = inverse b`
+  have "inverse (inverse a) = inverse (inverse b)"
+    by (rule arg_cong)
+  with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
+    by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+  by (rule inverse_unique) simp
+
 lemma nonzero_inverse_mult_distrib: 
-  assumes anz: "a \<noteq> 0"
-    and bnz: "b \<noteq> 0"
+  assumes "a \<noteq> 0" and "b \<noteq> 0"
   shows "inverse (a * b) = inverse b * inverse a"
 proof -
-  have "inverse (a * b) * (a * b) * inverse b = inverse b" 
-    by (simp add: anz bnz)
-  hence "inverse (a * b) * a = inverse b" 
-    by (simp add: mult_assoc bnz)
-  hence "inverse (a * b) * a * inverse a = inverse b * inverse a" 
-    by simp
+  have "a * (b * inverse b) * inverse a = 1"
+    using assms by simp
+  hence "a * b * (inverse b * inverse a) = 1"
+    by (simp only: mult_assoc)
   thus ?thesis
-    by (simp add: mult_assoc anz)
+    by (rule inverse_unique)
 qed
 
 lemma division_ring_inverse_add: