Minor new lemmas.
authorballarin
Tue Jul 04 11:35:49 2006 +0200 (2006-07-04)
changeset 19981c0f124a0d385
parent 19980 dc17fd6c0908
child 19982 e4d50f8f3722
Minor new lemmas.
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Group.thy
     1.1 --- a/src/HOL/Algebra/CRing.thy	Mon Jul 03 20:03:11 2006 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Tue Jul 04 11:35:49 2006 +0200
     1.3 @@ -55,9 +55,6 @@
     1.4    by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
     1.5  
     1.6  lemma abelian_groupI:
     1.7 -(*
     1.8 -  includes struct R
     1.9 -*)
    1.10    fixes R (structure)
    1.11    assumes a_closed:
    1.12        "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y \<in> carrier R"
    1.13 @@ -167,6 +164,17 @@
    1.14    using comm_group.inv_mult [OF a_comm_group]
    1.15    by (simp add: a_inv_def)
    1.16  
    1.17 +lemma (in abelian_group) minus_equality: 
    1.18 +  "[| x \<in> carrier G; y \<in> carrier G; y \<oplus> x = \<zero> |] ==> \<ominus> x = y" 
    1.19 +  using group.inv_equality [OF a_group] 
    1.20 +  by (auto simp add: a_inv_def) 
    1.21 + 
    1.22 +lemma (in abelian_monoid) minus_unique: 
    1.23 +  "[| x \<in> carrier G; y \<in> carrier G; y' \<in> carrier G;
    1.24 +      y \<oplus> x = \<zero>; x \<oplus> y' = \<zero> |] ==> y = y'" 
    1.25 +  using monoid.inv_unique [OF a_monoid] 
    1.26 +  by (simp add: a_inv_def) 
    1.27 +
    1.28  lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
    1.29  
    1.30  subsection {* Sums over Finite Sets *}
    1.31 @@ -314,9 +322,6 @@
    1.32  subsection {* Basic Facts of Rings *}
    1.33  
    1.34  lemma ringI:
    1.35 -(*
    1.36 -  includes struct R
    1.37 -*)
    1.38    fixes R (structure)
    1.39    assumes abelian_group: "abelian_group R"
    1.40      and monoid: "monoid R"
    1.41 @@ -547,9 +552,6 @@
    1.42        h \<one> = \<one>\<^bsub>S\<^esub>}"
    1.43  
    1.44  lemma ring_hom_memI:
    1.45 -(*
    1.46 -  includes struct R + struct S
    1.47 -*)
    1.48    fixes R (structure) and S (structure)
    1.49    assumes hom_closed: "!!x. x \<in> carrier R ==> h x \<in> carrier S"
    1.50      and hom_mult: "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==>
     2.1 --- a/src/HOL/Algebra/Group.thy	Mon Jul 03 20:03:11 2006 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 04 11:35:49 2006 +0200
     2.3 @@ -90,6 +90,14 @@
     2.4     apply (fast intro: inv_unique, fast)
     2.5    done
     2.6  
     2.7 +lemma (in monoid) Units_l_inv_ex:
     2.8 +  "x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
     2.9 +  by (unfold Units_def) auto
    2.10 +
    2.11 +lemma (in monoid) Units_r_inv_ex:
    2.12 +  "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
    2.13 +  by (unfold Units_def) auto
    2.14 +
    2.15  lemma (in monoid) Units_l_inv:
    2.16    "x \<in> Units G ==> inv x \<otimes> x = \<one>"
    2.17    apply (unfold Units_def m_inv_def, auto)
    2.18 @@ -271,6 +279,14 @@
    2.19    "x \<in> carrier G ==> inv x \<in> carrier G"
    2.20    using Units_inv_closed by simp
    2.21  
    2.22 +lemma (in group) l_inv_ex [simp]:
    2.23 +  "x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
    2.24 +  using Units_l_inv_ex by simp
    2.25 +
    2.26 +lemma (in group) r_inv_ex [simp]:
    2.27 +  "x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
    2.28 +  using Units_r_inv_ex by simp
    2.29 +
    2.30  lemma (in group) l_inv [simp]:
    2.31    "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
    2.32    using Units_l_inv by simp