author wenzelm Mon, 27 Feb 2012 21:07:00 +0100 changeset 46721 f88b187ad8ca parent 46720 9722171731af child 46722 d0491ab69c84
tuned proofs;
 src/HOL/Algebra/Coset.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/FiniteProduct.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Ring.thy file | annotate | diff | comparison | revisions
```--- 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
@@ -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>)"