simplify proof
authorhuffman
Sat Sep 03 09:12:19 2011 -0700 (2011-09-03 ago)
changeset 44680761f427ef1ab
parent 44679 a89d0ad8ed20
child 44681 49ef76b4a634
simplify proof
src/HOL/Fields.thy
     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 *}