# HG changeset patch # User paulson # Date 1391549386 0 # Node ID 3bf50e3cd72716502b6c8408b85e52b551e4fb49 # Parent eadea363deb66e425e786dcf3bfb94587597ea01 removal of "back", etc. diff -r eadea363deb6 -r 3bf50e3cd727 src/HOL/Number_Theory/MiscAlgebra.thy --- 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 \ (inv x = \) = (x = \)" - 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 \ y : carrier R \ x \ y = \ \ x = \ y" - apply (subgoal_tac "\ y = \ \ \ y") - apply (erule ssubst)back - apply (erule subst) - apply (simp_all add: ring_simprules) - 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 \ x = inv x \ x = \ | x = \ \" - 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) \ finite (Units R)" by (rule finite_subset) auto -(* this belongs with MiscAlgebra.thy *) lemma (in monoid) units_of_pow: "x : Units G \ x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n" apply (induct n)