author ballarin Tue, 04 Jul 2006 11:35:49 +0200 changeset 19981 c0f124a0d385 parent 19980 dc17fd6c0908 child 19982 e4d50f8f3722
Minor new lemmas.
 src/HOL/Algebra/CRing.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Group.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Algebra/CRing.thy	Mon Jul 03 20:03:11 2006 +0200
+++ b/src/HOL/Algebra/CRing.thy	Tue Jul 04 11:35:49 2006 +0200
@@ -55,9 +55,6 @@
by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)

lemma abelian_groupI:
-(*
-  includes struct R
-*)
fixes R (structure)
assumes a_closed:
"!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
@@ -167,6 +164,17 @@
using comm_group.inv_mult [OF a_comm_group]

+lemma (in abelian_group) minus_equality:
+  "[| x \<in> carrier G; y \<in> carrier G; y \<oplus> x = \<zero> |] ==> \<ominus> x = y"
+  using group.inv_equality [OF a_group]
+  by (auto simp add: a_inv_def)
+
+lemma (in abelian_monoid) minus_unique:
+  "[| x \<in> carrier G; y \<in> carrier G; y' \<in> carrier G;
+      y \<oplus> x = \<zero>; x \<oplus> y' = \<zero> |] ==> y = y'"
+  using monoid.inv_unique [OF a_monoid]
+
lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm

subsection {* Sums over Finite Sets *}
@@ -314,9 +322,6 @@
subsection {* Basic Facts of Rings *}

lemma ringI:
-(*
-  includes struct R
-*)
fixes R (structure)
assumes abelian_group: "abelian_group R"
and monoid: "monoid R"
@@ -547,9 +552,6 @@
h \<one> = \<one>\<^bsub>S\<^esub>}"

lemma ring_hom_memI:
-(*
-  includes struct R + struct S
-*)
fixes R (structure) and S (structure)
assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>```
```--- a/src/HOL/Algebra/Group.thy	Mon Jul 03 20:03:11 2006 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jul 04 11:35:49 2006 +0200
@@ -90,6 +90,14 @@
apply (fast intro: inv_unique, fast)
done

+lemma (in monoid) Units_l_inv_ex:
+  "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
+  by (unfold Units_def) auto
+
+lemma (in monoid) Units_r_inv_ex:
+  "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
+  by (unfold Units_def) auto
+
lemma (in monoid) Units_l_inv:
"x \<in> Units G ==> inv x \<otimes> x = \<one>"
apply (unfold Units_def m_inv_def, auto)
@@ -271,6 +279,14 @@
"x \<in> carrier G ==> inv x \<in> carrier G"
using Units_inv_closed by simp

+lemma (in group) l_inv_ex [simp]:
+  "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
+  using Units_l_inv_ex by simp
+
+lemma (in group) r_inv_ex [simp]:
+  "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
+  using Units_r_inv_ex by simp
+
lemma (in group) l_inv [simp]:
"x \<in> carrier G ==> inv x \<otimes> x = \<one>"
using Units_l_inv by simp```