# HG changeset patch
# User ballarin
# Date 1152005749 -7200
# Node ID c0f124a0d3857fce7a053289302432a561c9049c
# Parent  dc17fd6c09087c1e6b66bd8a93341b6293defb1a
Minor new lemmas.

diff -r dc17fd6c0908 -r c0f124a0d385 src/HOL/Algebra/CRing.thy
--- 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]
   by (simp add: a_inv_def)
 
+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] 
+  by (simp add: a_inv_def) 
+
 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 |] ==>
diff -r dc17fd6c0908 -r c0f124a0d385 src/HOL/Algebra/Group.thy
--- 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