src/HOL/Algebra/More_Group.thy
changeset 68446 92ddca1edc43
parent 68441 3b11d48a711a
parent 68445 c183a6a69f2d
child 68447 0beb927eed89
     1.1 --- a/src/HOL/Algebra/More_Group.thy	Thu Jun 14 10:51:12 2018 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,115 +0,0 @@
     1.4 -(*  Title:      HOL/Algebra/More_Group.thy
     1.5 -    Author:     Jeremy Avigad
     1.6 -*)
     1.7 -
     1.8 -section \<open>More on groups\<close>
     1.9 -
    1.10 -theory More_Group
    1.11 -  imports Ring
    1.12 -begin
    1.13 -
    1.14 -text \<open>
    1.15 -  Show that the units in any monoid give rise to a group.
    1.16 -
    1.17 -  The file Residues.thy provides some infrastructure to use
    1.18 -  facts about the unit group within the ring locale.
    1.19 -\<close>
    1.20 -
    1.21 -definition units_of :: "('a, 'b) monoid_scheme \<Rightarrow> 'a monoid"
    1.22 -  where "units_of G =
    1.23 -    \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
    1.24 -
    1.25 -lemma (in monoid) units_group: "group (units_of G)"
    1.26 -  apply (unfold units_of_def)
    1.27 -  apply (rule groupI)
    1.28 -      apply auto
    1.29 -   apply (subst m_assoc)
    1.30 -      apply auto
    1.31 -  apply (rule_tac x = "inv x" in bexI)
    1.32 -   apply auto
    1.33 -  done
    1.34 -
    1.35 -lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
    1.36 -  apply (rule group.group_comm_groupI)
    1.37 -   apply (rule units_group)
    1.38 -  apply (insert comm_monoid_axioms)
    1.39 -  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
    1.40 -  apply auto
    1.41 -  done
    1.42 -
    1.43 -lemma units_of_carrier: "carrier (units_of G) = Units G"
    1.44 -  by (auto simp: units_of_def)
    1.45 -
    1.46 -lemma units_of_mult: "mult (units_of G) = mult G"
    1.47 -  by (auto simp: units_of_def)
    1.48 -
    1.49 -lemma units_of_one: "one (units_of G) = one G"
    1.50 -  by (auto simp: units_of_def)
    1.51 -
    1.52 -lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
    1.53 -  apply (rule sym)
    1.54 -  apply (subst m_inv_def)
    1.55 -  apply (rule the1_equality)
    1.56 -   apply (rule ex_ex1I)
    1.57 -    apply (subst (asm) Units_def)
    1.58 -    apply auto
    1.59 -     apply (erule inv_unique)
    1.60 -        apply auto
    1.61 -    apply (rule Units_closed)
    1.62 -    apply (simp_all only: units_of_carrier [symmetric])
    1.63 -    apply (insert units_group)
    1.64 -    apply auto
    1.65 -   apply (subst units_of_mult [symmetric])
    1.66 -   apply (subst units_of_one [symmetric])
    1.67 -   apply (erule group.r_inv, assumption)
    1.68 -  apply (subst units_of_mult [symmetric])
    1.69 -  apply (subst units_of_one [symmetric])
    1.70 -  apply (erule group.l_inv, assumption)
    1.71 -  done
    1.72 -
    1.73 -lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
    1.74 -  unfolding inj_on_def by auto
    1.75 -
    1.76 -lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
    1.77 -  apply (auto simp add: image_def)
    1.78 -  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
    1.79 -  apply auto
    1.80 -(* auto should get this. I suppose we need "comm_monoid_simprules"
    1.81 -   for ac_simps rewriting. *)
    1.82 -  apply (subst m_assoc [symmetric])
    1.83 -  apply auto
    1.84 -  done
    1.85 -
    1.86 -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"
    1.87 -  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
    1.88 -
    1.89 -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"
    1.90 -  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
    1.91 -
    1.92 -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"
    1.93 -  using l_cancel_one by fastforce
    1.94 -
    1.95 -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"
    1.96 -  using r_cancel_one by fastforce
    1.97 -
    1.98 -(* This should be generalized to arbitrary groups, not just commutative
    1.99 -   ones, using Lagrange's theorem. *)
   1.100 -
   1.101 -lemma (in comm_group) power_order_eq_one:
   1.102 -  assumes fin [simp]: "finite (carrier G)"
   1.103 -    and a [simp]: "a \<in> carrier G"
   1.104 -  shows "a [^] card(carrier G) = one G"
   1.105 -proof -
   1.106 -  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
   1.107 -    by (subst (2) finprod_reindex [symmetric],
   1.108 -      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   1.109 -  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
   1.110 -    by (auto simp add: finprod_multf Pi_def)
   1.111 -  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
   1.112 -    by (auto simp add: finprod_const)
   1.113 -  finally show ?thesis
   1.114 -(* uses the preceeding lemma *)
   1.115 -    by auto
   1.116 -qed
   1.117 -
   1.118 -end