author | immler |
Wed, 02 May 2018 13:49:38 +0200 | |
changeset 68072 | 493b818e8e10 |
parent 67341 | df79ef3b3a41 |
child 68399 | 0b71d08528f0 |
permissions | -rw-r--r-- |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Algebra/More_Group.thy |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
2 |
Author: Jeremy Avigad |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
3 |
*) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
4 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
5 |
section \<open>More on groups\<close> |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
6 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
7 |
theory More_Group |
66760 | 8 |
imports Ring |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
9 |
begin |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
10 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
11 |
text \<open> |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
12 |
Show that the units in any monoid give rise to a group. |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
13 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
14 |
The file Residues.thy provides some infrastructure to use |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
15 |
facts about the unit group within the ring locale. |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
16 |
\<close> |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
17 |
|
66760 | 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>" |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
21 |
|
66760 | 22 |
lemma (in monoid) units_group: "group (units_of G)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
23 |
apply (unfold units_of_def) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
24 |
apply (rule groupI) |
66760 | 25 |
apply auto |
26 |
apply (subst m_assoc) |
|
27 |
apply auto |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
28 |
apply (rule_tac x = "inv x" in bexI) |
66760 | 29 |
apply auto |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
30 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
31 |
|
66760 | 32 |
lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
33 |
apply (rule group.group_comm_groupI) |
66760 | 34 |
apply (rule units_group) |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
35 |
apply (insert comm_monoid_axioms) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
36 |
apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
37 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
38 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
39 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
40 |
lemma units_of_carrier: "carrier (units_of G) = Units G" |
66760 | 41 |
by (auto simp: units_of_def) |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
42 |
|
66760 | 43 |
lemma units_of_mult: "mult (units_of G) = mult G" |
44 |
by (auto simp: units_of_def) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
45 |
|
66760 | 46 |
lemma units_of_one: "one (units_of G) = one G" |
47 |
by (auto simp: units_of_def) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
48 |
|
66760 | 49 |
lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
50 |
apply (rule sym) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
51 |
apply (subst m_inv_def) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
52 |
apply (rule the1_equality) |
66760 | 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) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
65 |
apply (subst units_of_mult [symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
66 |
apply (subst units_of_one [symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
67 |
apply (erule group.l_inv, assumption) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
68 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
69 |
|
66760 | 70 |
lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
71 |
unfolding inj_on_def by auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
72 |
|
66760 | 73 |
lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
74 |
apply (auto simp add: image_def) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
75 |
apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
76 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
77 |
(* auto should get this. I suppose we need "comm_monoid_simprules" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
78 |
for ac_simps rewriting. *) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
79 |
apply (subst m_assoc [symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
80 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
81 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
82 |
|
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" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
84 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
85 |
apply (subst l_cancel [symmetric]) |
66760 | 86 |
prefer 4 |
87 |
apply (erule ssubst) |
|
88 |
apply auto |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
89 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
90 |
|
66760 | 91 |
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" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
92 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
93 |
apply (subst r_cancel [symmetric]) |
66760 | 94 |
prefer 4 |
95 |
apply (erule ssubst) |
|
96 |
apply auto |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
97 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
98 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
99 |
(* Is there a better way to do this? *) |
66760 | 100 |
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" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
101 |
apply (subst eq_commute) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
102 |
apply simp |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
103 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
104 |
|
66760 | 105 |
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" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
106 |
apply (subst eq_commute) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
107 |
apply simp |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
108 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
109 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
110 |
(* This should be generalized to arbitrary groups, not just commutative |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
111 |
ones, using Lagrange's theorem. *) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
112 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
113 |
lemma (in comm_group) power_order_eq_one: |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
114 |
assumes fin [simp]: "finite (carrier G)" |
66760 | 115 |
and a [simp]: "a \<in> carrier G" |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
66760
diff
changeset
|
116 |
shows "a [^] card(carrier G) = one G" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
117 |
proof - |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
118 |
have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
119 |
by (subst (2) finprod_reindex [symmetric], |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
120 |
auto simp add: Pi_def inj_on_const_mult surj_const_mult) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
121 |
also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
122 |
by (auto simp add: finprod_multf Pi_def) |
67341
df79ef3b3a41
Renamed (^) to [^] in preparation of the move from "op X" to (X)
nipkow
parents:
66760
diff
changeset
|
123 |
also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
124 |
by (auto simp add: finprod_const) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
125 |
finally show ?thesis |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
126 |
(* uses the preceeding lemma *) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
127 |
by auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
128 |
qed |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
129 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
130 |
end |