author huffman Sat Sep 03 09:12:19 2011 -0700 (2011-09-03 ago) changeset 44680 761f427ef1ab parent 44679 a89d0ad8ed20 child 44681 49ef76b4a634
simplify proof
 src/HOL/Fields.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Fields.thy	Sat Sep 03 08:01:49 2011 -0700
1.2 +++ b/src/HOL/Fields.thy	Sat Sep 03 09:12:19 2011 -0700
1.3 @@ -207,18 +207,6 @@
1.4    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
1.5  qed
1.6
1.7 -lemma inverse_eq_imp_eq:
1.8 -  "inverse a = inverse b \<Longrightarrow> a = b"
1.9 -apply (cases "a=0 | b=0")
1.10 - apply (force dest!: inverse_zero_imp_zero
1.11 -              simp add: eq_commute [of "0::'a"])
1.12 -apply (force dest!: nonzero_inverse_eq_imp_eq)
1.13 -done
1.14 -
1.15 -lemma inverse_eq_iff_eq [simp]:
1.16 -  "inverse a = inverse b \<longleftrightarrow> a = b"
1.17 -  by (force dest!: inverse_eq_imp_eq)
1.18 -
1.19  lemma inverse_inverse_eq [simp]:
1.20    "inverse (inverse a) = a"
1.21  proof cases
1.22 @@ -228,6 +216,14 @@
1.23    thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
1.24  qed
1.25
1.26 +lemma inverse_eq_imp_eq:
1.27 +  "inverse a = inverse b \<Longrightarrow> a = b"
1.28 +  by (drule arg_cong [where f="inverse"], simp)
1.29 +
1.30 +lemma inverse_eq_iff_eq [simp]:
1.31 +  "inverse a = inverse b \<longleftrightarrow> a = b"
1.32 +  by (force dest!: inverse_eq_imp_eq)
1.33 +
1.34  end
1.35
1.36  subsection {* Fields *}
```