--- 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
--- 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. *)
--- 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