# HG changeset patch # User ballarin # Date 1217341033 -7200 # Node ID 197f0517f0bd779da9620beb1dc7d3f02907446c # Parent bcf941cc33243fb52e568b7faa0e97e7a078a00c Unit_inv_l, Unit_inv_r made [simp]. diff -r bcf941cc3324 -r 197f0517f0bd src/HOL/Algebra/Coset.thy --- 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 \ carrier G" "y \ carrier G" "z \ carrier G" and "inv x \ y \ H" and "inv y \ z \ H" hence "(inv x \ y) \ (inv y \ z) \ H" by simp - hence "inv x \ (y \ inv y) \ z \ H" by (simp add: m_assoc del: r_inv) + hence "inv x \ (y \ inv y) \ z \ H" + by (simp add: m_assoc del: r_inv Units_r_inv) thus "inv x \ z \ H" by simp qed qed diff -r bcf941cc3324 -r 197f0517f0bd src/HOL/Algebra/Group.thy --- 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 \ Units G" and y: "y \ Units G" + shows "x \ y \ Units G" +proof - + from x obtain x' where x: "x \ carrier G" "x' \ carrier G" and xinv: "x \ x' = \" "x' \ x = \" + unfolding Units_def by fast + from y obtain y' where y: "y \ carrier G" "y' \ carrier G" and yinv: "y \ y' = \" "y' \ y = \" + unfolding Units_def by fast + from x y xinv yinv have "y' \ (x' \ x) \ y = \" by simp + moreover from x y xinv yinv have "x \ (y \ y') \ x' = \" 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' \ x'"]) + apply (auto simp: m_assoc) + done +qed + lemma (in monoid) Units_one_closed [intro, simp]: "\ \ Units G" by (unfold Units_def) auto @@ -96,14 +117,14 @@ "x \ Units G ==> \y \ carrier G. x \ y = \" by (unfold Units_def) auto -lemma (in monoid) Units_l_inv: +lemma (in monoid) Units_l_inv [simp]: "x \ Units G ==> inv x \ x = \" 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 \ Units G ==> x \ inv x = \" apply (unfold Units_def m_inv_def, auto) apply (rule theI2, fast) @@ -126,7 +147,7 @@ assume eq: "x \ y = x \ z" and G: "x \ Units G" "y \ carrier G" "z \ carrier G" then have "(inv x \ x) \ y = (inv x \ x) \ 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 \ Units G ==> inv (inv x) = x" proof - assume x: "x \ Units G" - then have "inv x \ inv (inv x) = inv x \ x" - by (simp add: Units_l_inv Units_r_inv) - with x show ?thesis by (simp add: Units_closed) + then have "inv x \ inv (inv x) = inv x \ 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 \ 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 \ carrier G ==> \y \ carrier G. y \ x = \" shows "group G" @@ -313,7 +337,7 @@ assume eq: "y \ x = z \ x" and G: "x \ carrier G" "y \ carrier G" "z \ carrier G" then have "y \ (x \ inv x) = z \ (x \ 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 \ = \" proof - - have "inv \ = \ \ (inv \)" by (simp del: r_inv) + have "inv \ = \ \ (inv \)" by (simp del: r_inv Units_r_inv) moreover have "... = \" by simp finally show ?thesis . qed @@ -343,7 +367,7 @@ assume G: "x \ carrier G" "y \ carrier G" then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ 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 \ carrier G" - and h: "h \ carrier H" - shows "m_inv (G \\ 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 \\ 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 \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" by (simp add: hom_mult [symmetric] del: hom_mult) finally have "h x \\<^bsub>H\<^esub> h (inv x) = h x \\<^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 diff -r bcf941cc3324 -r 197f0517f0bd src/HOL/Algebra/Ideal.thy --- 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 \ Units R" by (simp add: field_Units) hence a: "a \ inv a = \" by (rule Units_r_inv) from aI and aUnit - have "a \ inv a \ I" by (simp add: I_r_closed) + have "a \ inv a \ I" by (simp add: I_r_closed del: Units_r_inv) hence oneI: "\ \ I" by (simp add: a[symmetric]) have "carrier R \ I"