src/HOL/Algebra/More_Group.thy
author paulson <lp15@cam.ac.uk>
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 \<open>More on groups\<close>
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 \<open>
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
\<close>
haftmann@65416
    17
wenzelm@66760
    18
definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
wenzelm@66760
    19
  where "units_of G =
wenzelm@66760
    20
    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
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 \<in> Units G \<Longrightarrow> 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 \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> 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 \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> 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) \<otimes> 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 \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> 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 \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> 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 \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> 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 \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> 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 \<in> carrier G"
nipkow@67341
   101
  shows "a [^] card(carrier G) = one G"
haftmann@65416
   102
proof -
haftmann@65416
   103
  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> 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 "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
haftmann@65416
   107
    by (auto simp add: finprod_multf Pi_def)
nipkow@67341
   108
  also have "(\<Otimes>x\<in>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