src/HOL/Number_Theory/MiscAlgebra.thy
 changeset 55322 3bf50e3cd727 parent 53374 a14d2a854c02 child 57514 bdc2c6b40bf2
```     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:28:38 2014 +0000
1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:29:46 2014 +0000
1.3 @@ -239,10 +239,7 @@
1.4    done
1.5
1.6  lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
1.7 -  apply auto
1.8 -  apply (subst Units_inv_inv [symmetric])
1.9 -  apply auto
1.10 -  done
1.11 +by (metis Units_inv_inv inv_one)
1.12
1.13
1.14  (* This goes in FiniteProduct *)
1.15 @@ -281,11 +278,7 @@
1.16
1.17  lemma (in cring) sum_zero_eq_neg:
1.18      "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
1.19 -  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
1.20 -  apply (erule ssubst)back
1.21 -  apply (erule subst)
1.22 -  apply (simp_all add: ring_simprules)
1.23 -  done
1.24 +by (metis minus_equality)
1.25
1.26  (* there's a name conflict -- maybe "domain" should be
1.27     "integral_domain" *)
1.28 @@ -317,11 +310,7 @@
1.29
1.30  lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
1.31      x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
1.32 -  apply (rule square_eq_one)
1.33 -  apply auto
1.34 -  apply (erule ssubst)back
1.35 -  apply (erule Units_r_inv)
1.36 -  done
1.37 +by (metis Units_closed Units_l_inv square_eq_one)
1.38
1.39
1.40  (*
1.41 @@ -334,7 +323,6 @@
1.42      "finite (carrier R) \<Longrightarrow> finite (Units R)"
1.43    by (rule finite_subset) auto
1.44
1.45 -(* this belongs with MiscAlgebra.thy *)
1.46  lemma (in monoid) units_of_pow:
1.47      "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
1.48    apply (induct n)
```