# HG changeset patch
# User huffman
# Date 1315066339 25200
# Node ID 761f427ef1ab3fa8b162508508a08167965c543f
# Parent  a89d0ad8ed203cb74174037a760080123d5207bd
simplify proof

diff -r a89d0ad8ed20 -r 761f427ef1ab src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Sep 03 08:01:49 2011 -0700
+++ b/src/HOL/Fields.thy	Sat Sep 03 09:12:19 2011 -0700
@@ -207,18 +207,6 @@
   thus ?thesis by (simp add: nonzero_inverse_minus_eq)
 qed
 
-lemma inverse_eq_imp_eq:
-  "inverse a = inverse b \<Longrightarrow> a = b"
-apply (cases "a=0 | b=0") 
- apply (force dest!: inverse_zero_imp_zero
-              simp add: eq_commute [of "0::'a"])
-apply (force dest!: nonzero_inverse_eq_imp_eq) 
-done
-
-lemma inverse_eq_iff_eq [simp]:
-  "inverse a = inverse b \<longleftrightarrow> a = b"
-  by (force dest!: inverse_eq_imp_eq)
-
 lemma inverse_inverse_eq [simp]:
   "inverse (inverse a) = a"
 proof cases
@@ -228,6 +216,14 @@
   thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
 qed
 
+lemma inverse_eq_imp_eq:
+  "inverse a = inverse b \<Longrightarrow> a = b"
+  by (drule arg_cong [where f="inverse"], simp)
+
+lemma inverse_eq_iff_eq [simp]:
+  "inverse a = inverse b \<longleftrightarrow> a = b"
+  by (force dest!: inverse_eq_imp_eq)
+
 end
 
 subsection {* Fields *}