Unit_inv_l, Unit_inv_r made [simp].

--- a/src/HOL/Algebra/Coset.thy	Tue Jul 29 16:16:10 2008 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Jul 29 16:17:13 2008 +0200
@@ -621,7 +621,8 @@
       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
 	 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
-      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv) 
+      hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
+	by (simp add: m_assoc del: r_inv Units_r_inv) 
       thus "inv x \<otimes> z \<in> H" by simp
     qed
   qed

--- a/src/HOL/Algebra/Group.thy	Tue Jul 29 16:16:10 2008 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Jul 29 16:17:13 2008 +0200
@@ -77,6 +77,27 @@
   finally show ?thesis .
 qed
 
+lemma (in monoid) Units_m_closed [intro, simp]:
+  assumes x: "x \<in> Units G" and y: "y \<in> Units G"
+  shows "x \<otimes> y \<in> Units G"
+proof -
+  from x obtain x' where x: "x \<in> carrier G" "x' \<in> carrier G" and xinv: "x \<otimes> x' = \<one>" "x' \<otimes> x = \<one>"
+    unfolding Units_def by fast
+  from y obtain y' where y: "y \<in> carrier G" "y' \<in> carrier G" and yinv: "y \<otimes> y' = \<one>" "y' \<otimes> y = \<one>"
+    unfolding Units_def by fast
+  from x y xinv yinv have "y' \<otimes> (x' \<otimes> x) \<otimes> y = \<one>" by simp
+  moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
+  moreover note x y
+  ultimately show ?thesis unfolding Units_def
+    -- "Must avoid premature use of @{text hyp_subst_tac}."
+    apply (rule_tac CollectI)
+    apply (rule)
+    apply (fast)
+    apply (rule bexI [where x = "y' \<otimes> x'"])
+    apply (auto simp: m_assoc)
+    done
+qed
+
 lemma (in monoid) Units_one_closed [intro, simp]:
   "\<one> \<in> Units G"
   by (unfold Units_def) auto
@@ -96,14 +117,14 @@
   "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
   by (unfold Units_def) auto
 
-lemma (in monoid) Units_l_inv:
+lemma (in monoid) Units_l_inv [simp]:
   "x \<in> Units G ==> inv x \<otimes> x = \<one>"
   apply (unfold Units_def m_inv_def, auto)
   apply (rule theI2, fast)
    apply (fast intro: inv_unique, fast)
   done
 
-lemma (in monoid) Units_r_inv:
+lemma (in monoid) Units_r_inv [simp]:
   "x \<in> Units G ==> x \<otimes> inv x = \<one>"
   apply (unfold Units_def m_inv_def, auto)
   apply (rule theI2, fast)
@@ -126,7 +147,7 @@
   assume eq: "x \<otimes> y = x \<otimes> z"
     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
-    by (simp add: m_assoc Units_closed)
+    by (simp add: m_assoc Units_closed del: Units_l_inv)
   with G show "y = z" by (simp add: Units_l_inv)
 next
   assume eq: "y = z"
@@ -138,9 +159,8 @@
   "x \<in> Units G ==> inv (inv x) = x"
 proof -
   assume x: "x \<in> Units G"
-  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
-    by (simp add: Units_l_inv Units_r_inv)
-  with x show ?thesis by (simp add: Units_closed)
+  then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by simp
+  with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv)
 qed
 
 lemma (in monoid) inv_inj_on_Units:
@@ -187,6 +207,13 @@
   "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
   by (induct m) (simp, simp add: nat_pow_mult add_commute)
 
+
+(* Jacobson defines submonoid here. *)
+(* Jacobson defines the order of a monoid here. *)
+
+
+subsection {* Groups *}
+
 text {*
   A group is a monoid all of whose elements are invertible.
 *}
@@ -194,7 +221,6 @@
 locale group = monoid +
   assumes Units: "carrier G <= Units G"
 
-
 lemma (in group) is_group: "group G" by (rule group_axioms)
 
 theorem groupI:
@@ -254,12 +280,10 @@
   qed
   then have carrier_subset_Units: "carrier G <= Units G"
     by (unfold Units_def) fast
-  show ?thesis
-    by (fast intro!: group.intro monoid.intro group_axioms.intro
-      carrier_subset_Units intro: prems r_one)
+  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
 qed
 
-lemma (in monoid) monoid_groupI:
+lemma (in monoid) group_l_invI:
   assumes l_inv_ex:
     "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
   shows "group G"
@@ -313,7 +337,7 @@
   assume eq: "y \<otimes> x = z \<otimes> x"
     and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
-    by (simp add: m_assoc [symmetric] del: r_inv)
+    by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
   with G show "y = z" by simp
 next
   assume eq: "y = z"
@@ -324,7 +348,7 @@
 lemma (in group) inv_one [simp]:
   "inv \<one> = \<one>"
 proof -
-  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
+  have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv)
   moreover have "... = \<one>" by simp
   finally show ?thesis .
 qed
@@ -343,7 +367,7 @@
   assume G: "x \<in> carrier G"  "y \<in> carrier G"
   then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
     by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
-  with G show ?thesis by (simp del: l_inv)
+  with G show ?thesis by (simp del: l_inv Units_l_inv)
 qed
 
 lemma (in group) inv_comm:
@@ -401,7 +425,10 @@
 proof -
   interpret group [G] by fact
   show ?thesis
-    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
+    apply (rule monoid.group_l_invI)
+    apply (unfold_locales) [1]
+    apply (auto intro: m_assoc l_inv mem_carrier)
+    done
 qed
 
 text {*
@@ -499,27 +526,11 @@
 proof -
   interpret G: group [G] by fact
   interpret H: group [H] by fact
-  show ?thesis apply (rule group.inv_equality [OF DirProd_group])
-  apply (simp_all add: prems group.l_inv)
-  done
-qed
-
-text{*This alternative proof of the previous result demonstrates interpret.
-   It uses @{text Prod.inv_equality} (available after @{text interpret})
-   instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
-lemma
-  assumes "group G" and "group H"
-  assumes g: "g \<in> carrier G"
-      and h: "h \<in> carrier H"
-  shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
-proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
   interpret Prod: group ["G \<times>\<times> H"]
     by (auto intro: DirProd_group group.intro group.axioms prems)
   show ?thesis by (simp add: Prod.inv_equality g h)
 qed
-  
+
 
 subsection {* Homomorphisms and Isomorphisms *}
 
@@ -604,7 +615,7 @@
   also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
     by (simp add: hom_mult [symmetric] del: hom_mult)
   finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
-  with x show ?thesis by (simp del: H.r_inv)
+  with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)
 qed
 
 

--- a/src/HOL/Algebra/Ideal.thy	Tue Jul 29 16:16:10 2008 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Tue Jul 29 16:17:13 2008 +0200
@@ -950,7 +950,7 @@
         have aUnit: "a \<in> Units R" by (simp add: field_Units)
     hence a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
     from aI and aUnit
-        have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed)
+        have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv)
     hence oneI: "\<one> \<in> I" by (simp add: a[symmetric])
 
     have "carrier R \<subseteq> I"