1.1 --- a/src/HOL/Algebra/Coset.thy Tue Jul 29 16:16:10 2008 +0200
1.2 +++ b/src/HOL/Algebra/Coset.thy Tue Jul 29 16:17:13 2008 +0200
1.3 @@ -621,7 +621,8 @@
1.4 assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
1.5 and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
1.6 hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
1.7 - hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" by (simp add: m_assoc del: r_inv)
1.8 + hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
1.9 + by (simp add: m_assoc del: r_inv Units_r_inv)
1.10 thus "inv x \<otimes> z \<in> H" by simp
1.11 qed
1.12 qed
2.1 --- a/src/HOL/Algebra/Group.thy Tue Jul 29 16:16:10 2008 +0200
2.2 +++ b/src/HOL/Algebra/Group.thy Tue Jul 29 16:17:13 2008 +0200
2.3 @@ -77,6 +77,27 @@
2.4 finally show ?thesis .
2.5 qed
2.6
2.7 +lemma (in monoid) Units_m_closed [intro, simp]:
2.8 + assumes x: "x \<in> Units G" and y: "y \<in> Units G"
2.9 + shows "x \<otimes> y \<in> Units G"
2.10 +proof -
2.11 + from x obtain x' where x: "x \<in> carrier G" "x' \<in> carrier G" and xinv: "x \<otimes> x' = \<one>" "x' \<otimes> x = \<one>"
2.12 + unfolding Units_def by fast
2.13 + from y obtain y' where y: "y \<in> carrier G" "y' \<in> carrier G" and yinv: "y \<otimes> y' = \<one>" "y' \<otimes> y = \<one>"
2.14 + unfolding Units_def by fast
2.15 + from x y xinv yinv have "y' \<otimes> (x' \<otimes> x) \<otimes> y = \<one>" by simp
2.16 + moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
2.17 + moreover note x y
2.18 + ultimately show ?thesis unfolding Units_def
2.19 + -- "Must avoid premature use of @{text hyp_subst_tac}."
2.20 + apply (rule_tac CollectI)
2.21 + apply (rule)
2.22 + apply (fast)
2.23 + apply (rule bexI [where x = "y' \<otimes> x'"])
2.24 + apply (auto simp: m_assoc)
2.25 + done
2.26 +qed
2.27 +
2.28 lemma (in monoid) Units_one_closed [intro, simp]:
2.29 "\<one> \<in> Units G"
2.30 by (unfold Units_def) auto
2.31 @@ -96,14 +117,14 @@
2.32 "x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>"
2.33 by (unfold Units_def) auto
2.34
2.35 -lemma (in monoid) Units_l_inv:
2.36 +lemma (in monoid) Units_l_inv [simp]:
2.37 "x \<in> Units G ==> inv x \<otimes> x = \<one>"
2.38 apply (unfold Units_def m_inv_def, auto)
2.39 apply (rule theI2, fast)
2.40 apply (fast intro: inv_unique, fast)
2.41 done
2.42
2.43 -lemma (in monoid) Units_r_inv:
2.44 +lemma (in monoid) Units_r_inv [simp]:
2.45 "x \<in> Units G ==> x \<otimes> inv x = \<one>"
2.46 apply (unfold Units_def m_inv_def, auto)
2.47 apply (rule theI2, fast)
2.48 @@ -126,7 +147,7 @@
2.49 assume eq: "x \<otimes> y = x \<otimes> z"
2.50 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
2.51 then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
2.52 - by (simp add: m_assoc Units_closed)
2.53 + by (simp add: m_assoc Units_closed del: Units_l_inv)
2.54 with G show "y = z" by (simp add: Units_l_inv)
2.55 next
2.56 assume eq: "y = z"
2.57 @@ -138,9 +159,8 @@
2.58 "x \<in> Units G ==> inv (inv x) = x"
2.59 proof -
2.60 assume x: "x \<in> Units G"
2.61 - then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x"
2.62 - by (simp add: Units_l_inv Units_r_inv)
2.63 - with x show ?thesis by (simp add: Units_closed)
2.64 + then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" by simp
2.65 + with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv)
2.66 qed
2.67
2.68 lemma (in monoid) inv_inj_on_Units:
2.69 @@ -187,6 +207,13 @@
2.70 "x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)"
2.71 by (induct m) (simp, simp add: nat_pow_mult add_commute)
2.72
2.73 +
2.74 +(* Jacobson defines submonoid here. *)
2.75 +(* Jacobson defines the order of a monoid here. *)
2.76 +
2.77 +
2.78 +subsection {* Groups *}
2.79 +
2.80 text {*
2.81 A group is a monoid all of whose elements are invertible.
2.82 *}
2.83 @@ -194,7 +221,6 @@
2.84 locale group = monoid +
2.85 assumes Units: "carrier G <= Units G"
2.86
2.87 -
2.88 lemma (in group) is_group: "group G" by (rule group_axioms)
2.89
2.90 theorem groupI:
2.91 @@ -254,12 +280,10 @@
2.92 qed
2.93 then have carrier_subset_Units: "carrier G <= Units G"
2.94 by (unfold Units_def) fast
2.95 - show ?thesis
2.96 - by (fast intro!: group.intro monoid.intro group_axioms.intro
2.97 - carrier_subset_Units intro: prems r_one)
2.98 + show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
2.99 qed
2.100
2.101 -lemma (in monoid) monoid_groupI:
2.102 +lemma (in monoid) group_l_invI:
2.103 assumes l_inv_ex:
2.104 "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>"
2.105 shows "group G"
2.106 @@ -313,7 +337,7 @@
2.107 assume eq: "y \<otimes> x = z \<otimes> x"
2.108 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
2.109 then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
2.110 - by (simp add: m_assoc [symmetric] del: r_inv)
2.111 + by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
2.112 with G show "y = z" by simp
2.113 next
2.114 assume eq: "y = z"
2.115 @@ -324,7 +348,7 @@
2.116 lemma (in group) inv_one [simp]:
2.117 "inv \<one> = \<one>"
2.118 proof -
2.119 - have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv)
2.120 + have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv Units_r_inv)
2.121 moreover have "... = \<one>" by simp
2.122 finally show ?thesis .
2.123 qed
2.124 @@ -343,7 +367,7 @@
2.125 assume G: "x \<in> carrier G" "y \<in> carrier G"
2.126 then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
2.127 by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
2.128 - with G show ?thesis by (simp del: l_inv)
2.129 + with G show ?thesis by (simp del: l_inv Units_l_inv)
2.130 qed
2.131
2.132 lemma (in group) inv_comm:
2.133 @@ -401,7 +425,10 @@
2.134 proof -
2.135 interpret group [G] by fact
2.136 show ?thesis
2.137 - by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
2.138 + apply (rule monoid.group_l_invI)
2.139 + apply (unfold_locales) [1]
2.140 + apply (auto intro: m_assoc l_inv mem_carrier)
2.141 + done
2.142 qed
2.143
2.144 text {*
2.145 @@ -499,27 +526,11 @@
2.146 proof -
2.147 interpret G: group [G] by fact
2.148 interpret H: group [H] by fact
2.149 - show ?thesis apply (rule group.inv_equality [OF DirProd_group])
2.150 - apply (simp_all add: prems group.l_inv)
2.151 - done
2.152 -qed
2.153 -
2.154 -text{*This alternative proof of the previous result demonstrates interpret.
2.155 - It uses @{text Prod.inv_equality} (available after @{text interpret})
2.156 - instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
2.157 -lemma
2.158 - assumes "group G" and "group H"
2.159 - assumes g: "g \<in> carrier G"
2.160 - and h: "h \<in> carrier H"
2.161 - shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
2.162 -proof -
2.163 - interpret G: group [G] by fact
2.164 - interpret H: group [H] by fact
2.165 interpret Prod: group ["G \<times>\<times> H"]
2.166 by (auto intro: DirProd_group group.intro group.axioms prems)
2.167 show ?thesis by (simp add: Prod.inv_equality g h)
2.168 qed
2.169 -
2.170 +
2.171
2.172 subsection {* Homomorphisms and Isomorphisms *}
2.173
2.174 @@ -604,7 +615,7 @@
2.175 also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
2.176 by (simp add: hom_mult [symmetric] del: hom_mult)
2.177 finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" .
2.178 - with x show ?thesis by (simp del: H.r_inv)
2.179 + with x show ?thesis by (simp del: H.r_inv H.Units_r_inv)
2.180 qed
2.181
2.182
3.1 --- a/src/HOL/Algebra/Ideal.thy Tue Jul 29 16:16:10 2008 +0200
3.2 +++ b/src/HOL/Algebra/Ideal.thy Tue Jul 29 16:17:13 2008 +0200
3.3 @@ -950,7 +950,7 @@
3.4 have aUnit: "a \<in> Units R" by (simp add: field_Units)
3.5 hence a: "a \<otimes> inv a = \<one>" by (rule Units_r_inv)
3.6 from aI and aUnit
3.7 - have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed)
3.8 + have "a \<otimes> inv a \<in> I" by (simp add: I_r_closed del: Units_r_inv)
3.9 hence oneI: "\<one> \<in> I" by (simp add: a[symmetric])
3.10
3.11 have "carrier R \<subseteq> I"