author paulson Tue, 04 Feb 2014 21:29:46 +0000 changeset 55322 3bf50e3cd727 parent 55321 eadea363deb6 child 55323 253a029335a2
removal of "back", etc.
```--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:28:38 2014 +0000
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Feb 04 21:29:46 2014 +0000
@@ -239,10 +239,7 @@
done

lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
-  apply auto
-  apply (subst Units_inv_inv [symmetric])
-  apply auto
-  done
+by (metis Units_inv_inv inv_one)

(* This goes in FiniteProduct *)
@@ -281,11 +278,7 @@

lemma (in cring) sum_zero_eq_neg:
"x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
-  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
-  apply (erule ssubst)back
-  apply (erule subst)
-  done
+by (metis minus_equality)

(* there's a name conflict -- maybe "domain" should be
"integral_domain" *)
@@ -317,11 +310,7 @@

lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
-  apply (rule square_eq_one)
-  apply auto
-  apply (erule ssubst)back
-  apply (erule Units_r_inv)
-  done
+by (metis Units_closed Units_l_inv square_eq_one)

(*
@@ -334,7 +323,6 @@
"finite (carrier R) \<Longrightarrow> finite (Units R)"
by (rule finite_subset) auto

-(* this belongs with MiscAlgebra.thy *)
lemma (in monoid) units_of_pow:
"x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
apply (induct n)```