# HG changeset patch
# User wenzelm
# Date 1330373220 -3600
# Node ID f88b187ad8caa314338432fd74cd6b80c7f52b6b
# Parent  9722171731af4430a8457dd88fd6bf04af477462
tuned proofs;

diff -r 9722171731af -r f88b187ad8ca src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Feb 27 20:55:30 2012 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Feb 27 21:07:00 2012 +0100
@@ -232,7 +232,7 @@
   also from carr
       have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc)
   also from carr
-      have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv)
+      have "\<dots> = x' \<otimes> \<one>" by simp
   also from carr
       have "\<dots> = x'" by simp
   finally
@@ -520,8 +520,7 @@
 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
 apply (rule_tac x = x in bexI)
 apply (rule bexI [of _ "\<one>"])
-apply (auto simp add: subgroup.m_closed subgroup.one_closed
-                      r_one subgroup.subset [THEN subsetD])
+apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
 done
 
 
@@ -612,7 +611,7 @@
       fix x y
       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
          and "inv x \<otimes> y \<in> H"
-      hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
+      hence "inv (inv x \<otimes> y) \<in> H" by simp
       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
     qed
   next
@@ -722,7 +721,7 @@
   assume abrcong: "(a, b) \<in> rcong H"
     and ccarr: "c \<in> carrier G"
 
-  from ccarr have "c \<in> Units G" by (simp add: Units_eq)
+  from ccarr have "c \<in> Units G" by simp
   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
 
   from abrcong
diff -r 9722171731af -r f88b187ad8ca src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 20:55:30 2012 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Feb 27 21:07:00 2012 +0100
@@ -190,7 +190,7 @@
 lemma (in LCD) foldD_closed [simp]:
   "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
 proof (induct set: finite)
-  case empty then show ?case by (simp add: foldD_empty)
+  case empty then show ?case by simp
 next
   case insert then show ?case by (simp add: foldD_insert)
 qed
@@ -328,7 +328,7 @@
            apply fast
           apply fast
          apply assumption
-        apply (fastforce intro: m_closed)
+        apply fastforce
        apply simp+
    apply fast
   apply (auto simp add: finprod_def)
@@ -372,14 +372,13 @@
      finprod G g A \<otimes> finprod G g B"
 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
 proof (induct set: finite)
-  case empty then show ?case by (simp add: finprod_closed)
+  case empty then show ?case by simp
 next
   case (insert a A)
   then have a: "g a \<in> carrier G" by fast
   from insert have A: "g \<in> A -> carrier G" by fast
   from insert A a show ?case
-    by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
-          Int_mono2) 
+    by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) 
 qed
 
 lemma finprod_Un_disjoint:
@@ -387,7 +386,7 @@
       g \<in> A -> carrier G; g \<in> B -> carrier G |]
    ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   apply (subst finprod_Un_Int [symmetric])
-      apply (auto simp add: finprod_closed)
+      apply auto
   done
 
 lemma finprod_multf:
@@ -498,9 +497,8 @@
   assumes fin: "finite A"
     shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
         inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
-  using fin apply induct
-  apply (auto simp add: finprod_insert Pi_def)
-done
+  using fin
+  by induct (auto simp add: Pi_def)
 
 lemma finprod_const:
   assumes fin [simp]: "finite A"
@@ -512,7 +510,7 @@
   apply auto
   apply (subst m_comm)
   apply auto
-done
+  done
 
 (* The following lemma was contributed by Jesus Aransay. *)
 
diff -r 9722171731af -r f88b187ad8ca src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Feb 27 20:55:30 2012 +0100
+++ b/src/HOL/Algebra/Ring.thy	Mon Feb 27 21:07:00 2012 +0100
@@ -259,16 +259,12 @@
 
 context ring begin
 
-lemma is_abelian_group:
-  "abelian_group R"
-  ..
+lemma is_abelian_group: "abelian_group R" ..
 
-lemma is_monoid:
-  "monoid R"
+lemma is_monoid: "monoid R"
   by (auto intro!: monoidI m_assoc)
 
-lemma is_ring:
-  "ring R"
+lemma is_ring: "ring R"
   by (rule ring_axioms)
 
 end
@@ -444,12 +440,13 @@
       show "\<one> = \<zero>" by simp
 qed
 
-lemma carrier_one_zero:
-  shows "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
-  by (rule, erule one_zeroI, erule one_zeroD)
+lemma carrier_one_zero: "(carrier R = {\<zero>}) = (\<one> = \<zero>)"
+  apply rule
+   apply (erule one_zeroI)
+  apply (erule one_zeroD)
+  done
 
-lemma carrier_one_not_zero:
-  shows "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
+lemma carrier_one_not_zero: "(carrier R \<noteq> {\<zero>}) = (\<one> \<noteq> \<zero>)"
   by (simp add: carrier_one_zero)
 
 end
@@ -571,7 +568,7 @@
     from bcarr
     have "b = \<one> \<otimes> b" by algebra
     also from aUnit acarr
-    have "... = (inv a \<otimes> a) \<otimes> b" by (simp add: Units_l_inv)
+    have "... = (inv a \<otimes> a) \<otimes> b" by simp
     also from acarr bcarr aUnit[THEN Units_inv_closed]
     have "... = (inv a) \<otimes> (a \<otimes> b)" by algebra
     also from ab and acarr bcarr aUnit