removal of "back", etc.
authorpaulson <lp15@cam.ac.uk>
Tue Feb 04 21:29:46 2014 +0000 (2014-02-04)
changeset 553223bf50e3cd727
parent 55321 eadea363deb6
child 55323 253a029335a2
removal of "back", etc.
src/HOL/Number_Theory/MiscAlgebra.thy
     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)