src/HOL/Algebra/More_Group.thy
 author paulson Wed Jun 06 14:25:53 2018 +0100 (12 months ago) changeset 68399 0b71d08528f0 parent 67341 df79ef3b3a41 permissions -rw-r--r--
resolution of name clashes in Algebra
 haftmann@65416 ` 1` ```(* Title: HOL/Algebra/More_Group.thy ``` haftmann@65416 ` 2` ``` Author: Jeremy Avigad ``` haftmann@65416 ` 3` ```*) ``` haftmann@65416 ` 4` haftmann@65416 ` 5` ```section \More on groups\ ``` haftmann@65416 ` 6` haftmann@65416 ` 7` ```theory More_Group ``` wenzelm@66760 ` 8` ``` imports Ring ``` haftmann@65416 ` 9` ```begin ``` haftmann@65416 ` 10` haftmann@65416 ` 11` ```text \ ``` haftmann@65416 ` 12` ``` Show that the units in any monoid give rise to a group. ``` haftmann@65416 ` 13` haftmann@65416 ` 14` ``` The file Residues.thy provides some infrastructure to use ``` haftmann@65416 ` 15` ``` facts about the unit group within the ring locale. ``` haftmann@65416 ` 16` ```\ ``` haftmann@65416 ` 17` wenzelm@66760 ` 18` ```definition units_of :: "('a, 'b) monoid_scheme \ 'a monoid" ``` wenzelm@66760 ` 19` ``` where "units_of G = ``` wenzelm@66760 ` 20` ``` \carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one = one G\" ``` haftmann@65416 ` 21` wenzelm@66760 ` 22` ```lemma (in monoid) units_group: "group (units_of G)" ``` haftmann@65416 ` 23` ``` apply (unfold units_of_def) ``` haftmann@65416 ` 24` ``` apply (rule groupI) ``` wenzelm@66760 ` 25` ``` apply auto ``` wenzelm@66760 ` 26` ``` apply (subst m_assoc) ``` wenzelm@66760 ` 27` ``` apply auto ``` haftmann@65416 ` 28` ``` apply (rule_tac x = "inv x" in bexI) ``` wenzelm@66760 ` 29` ``` apply auto ``` haftmann@65416 ` 30` ``` done ``` haftmann@65416 ` 31` wenzelm@66760 ` 32` ```lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)" ``` haftmann@65416 ` 33` ``` apply (rule group.group_comm_groupI) ``` wenzelm@66760 ` 34` ``` apply (rule units_group) ``` haftmann@65416 ` 35` ``` apply (insert comm_monoid_axioms) ``` haftmann@65416 ` 36` ``` apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) ``` haftmann@65416 ` 37` ``` apply auto ``` haftmann@65416 ` 38` ``` done ``` haftmann@65416 ` 39` haftmann@65416 ` 40` ```lemma units_of_carrier: "carrier (units_of G) = Units G" ``` wenzelm@66760 ` 41` ``` by (auto simp: units_of_def) ``` haftmann@65416 ` 42` wenzelm@66760 ` 43` ```lemma units_of_mult: "mult (units_of G) = mult G" ``` wenzelm@66760 ` 44` ``` by (auto simp: units_of_def) ``` haftmann@65416 ` 45` wenzelm@66760 ` 46` ```lemma units_of_one: "one (units_of G) = one G" ``` wenzelm@66760 ` 47` ``` by (auto simp: units_of_def) ``` haftmann@65416 ` 48` wenzelm@66760 ` 49` ```lemma (in monoid) units_of_inv: "x \ Units G \ m_inv (units_of G) x = m_inv G x" ``` haftmann@65416 ` 50` ``` apply (rule sym) ``` haftmann@65416 ` 51` ``` apply (subst m_inv_def) ``` haftmann@65416 ` 52` ``` apply (rule the1_equality) ``` wenzelm@66760 ` 53` ``` apply (rule ex_ex1I) ``` wenzelm@66760 ` 54` ``` apply (subst (asm) Units_def) ``` wenzelm@66760 ` 55` ``` apply auto ``` wenzelm@66760 ` 56` ``` apply (erule inv_unique) ``` wenzelm@66760 ` 57` ``` apply auto ``` wenzelm@66760 ` 58` ``` apply (rule Units_closed) ``` wenzelm@66760 ` 59` ``` apply (simp_all only: units_of_carrier [symmetric]) ``` wenzelm@66760 ` 60` ``` apply (insert units_group) ``` wenzelm@66760 ` 61` ``` apply auto ``` wenzelm@66760 ` 62` ``` apply (subst units_of_mult [symmetric]) ``` wenzelm@66760 ` 63` ``` apply (subst units_of_one [symmetric]) ``` wenzelm@66760 ` 64` ``` apply (erule group.r_inv, assumption) ``` haftmann@65416 ` 65` ``` apply (subst units_of_mult [symmetric]) ``` haftmann@65416 ` 66` ``` apply (subst units_of_one [symmetric]) ``` haftmann@65416 ` 67` ``` apply (erule group.l_inv, assumption) ``` haftmann@65416 ` 68` ``` done ``` haftmann@65416 ` 69` wenzelm@66760 ` 70` ```lemma (in group) inj_on_const_mult: "a \ carrier G \ inj_on (\x. a \ x) (carrier G)" ``` haftmann@65416 ` 71` ``` unfolding inj_on_def by auto ``` haftmann@65416 ` 72` wenzelm@66760 ` 73` ```lemma (in group) surj_const_mult: "a \ carrier G \ (\x. a \ x) ` carrier G = carrier G" ``` haftmann@65416 ` 74` ``` apply (auto simp add: image_def) ``` haftmann@65416 ` 75` ``` apply (rule_tac x = "(m_inv G a) \ x" in bexI) ``` haftmann@65416 ` 76` ``` apply auto ``` haftmann@65416 ` 77` ```(* auto should get this. I suppose we need "comm_monoid_simprules" ``` haftmann@65416 ` 78` ``` for ac_simps rewriting. *) ``` haftmann@65416 ` 79` ``` apply (subst m_assoc [symmetric]) ``` haftmann@65416 ` 80` ``` apply auto ``` haftmann@65416 ` 81` ``` done ``` haftmann@65416 ` 82` wenzelm@66760 ` 83` ```lemma (in group) l_cancel_one [simp]: "x \ carrier G \ a \ carrier G \ x \ a = x \ a = one G" ``` lp15@68399 ` 84` ``` by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed) ``` haftmann@65416 ` 85` wenzelm@66760 ` 86` ```lemma (in group) r_cancel_one [simp]: "x \ carrier G \ a \ carrier G \ a \ x = x \ a = one G" ``` lp15@68399 ` 87` ``` by (metis monoid.l_one monoid_axioms one_closed right_cancel) ``` haftmann@65416 ` 88` wenzelm@66760 ` 89` ```lemma (in group) l_cancel_one' [simp]: "x \ carrier G \ a \ carrier G \ x = x \ a \ a = one G" ``` lp15@68399 ` 90` ``` using l_cancel_one by fastforce ``` haftmann@65416 ` 91` wenzelm@66760 ` 92` ```lemma (in group) r_cancel_one' [simp]: "x \ carrier G \ a \ carrier G \ x = a \ x \ a = one G" ``` lp15@68399 ` 93` ``` using r_cancel_one by fastforce ``` haftmann@65416 ` 94` haftmann@65416 ` 95` ```(* This should be generalized to arbitrary groups, not just commutative ``` haftmann@65416 ` 96` ``` ones, using Lagrange's theorem. *) ``` haftmann@65416 ` 97` haftmann@65416 ` 98` ```lemma (in comm_group) power_order_eq_one: ``` haftmann@65416 ` 99` ``` assumes fin [simp]: "finite (carrier G)" ``` wenzelm@66760 ` 100` ``` and a [simp]: "a \ carrier G" ``` nipkow@67341 ` 101` ``` shows "a [^] card(carrier G) = one G" ``` haftmann@65416 ` 102` ```proof - ``` haftmann@65416 ` 103` ``` have "(\x\carrier G. x) = (\x\carrier G. a \ x)" ``` haftmann@65416 ` 104` ``` by (subst (2) finprod_reindex [symmetric], ``` haftmann@65416 ` 105` ``` auto simp add: Pi_def inj_on_const_mult surj_const_mult) ``` haftmann@65416 ` 106` ``` also have "\ = (\x\carrier G. a) \ (\x\carrier G. x)" ``` haftmann@65416 ` 107` ``` by (auto simp add: finprod_multf Pi_def) ``` nipkow@67341 ` 108` ``` also have "(\x\carrier G. a) = a [^] card(carrier G)" ``` haftmann@65416 ` 109` ``` by (auto simp add: finprod_const) ``` haftmann@65416 ` 110` ``` finally show ?thesis ``` haftmann@65416 ` 111` ```(* uses the preceeding lemma *) ``` haftmann@65416 ` 112` ``` by auto ``` haftmann@65416 ` 113` ```qed ``` haftmann@65416 ` 114` haftmann@65416 ` 115` ```end ```