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