author | wenzelm |
Mon, 02 Oct 2017 22:48:01 +0200 | |
changeset 66760 | d44ea023ac09 |
parent 65416 | f707dbcf11e3 |
child 67341 | df79ef3b3a41 |
permissions | -rw-r--r-- |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Algebra/More_Finite_Product.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 finite products\<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_Finite_Product |
66760 | 8 |
imports More_Group |
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 |
lemma (in comm_monoid) finprod_UN_disjoint: |
66760 | 12 |
"finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow> |
13 |
(\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow> |
|
14 |
finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I" |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
15 |
apply (induct set: finite) |
66760 | 16 |
apply force |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
17 |
apply clarsimp |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
18 |
apply (subst finprod_Un_disjoint) |
66760 | 19 |
apply blast |
20 |
apply (erule finite_UN_I) |
|
21 |
apply blast |
|
22 |
apply (fastforce) |
|
23 |
apply (auto intro!: funcsetI finprod_closed) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
24 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
25 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
26 |
lemma (in comm_monoid) finprod_Union_disjoint: |
66760 | 27 |
"finite C \<Longrightarrow> |
28 |
\<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow> |
|
29 |
\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow> |
|
30 |
finprod G f (\<Union>C) = finprod G (finprod G f) C" |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
31 |
apply (frule finprod_UN_disjoint [of C id f]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
32 |
apply auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
33 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
34 |
|
66760 | 35 |
lemma (in comm_monoid) finprod_one: "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
36 |
by (induct set: finite) auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
37 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
38 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
39 |
(* need better simplification rules for rings *) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
40 |
(* the next one holds more generally for abelian groups *) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
41 |
|
66760 | 42 |
lemma (in cring) sum_zero_eq_neg: "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
43 |
by (metis minus_equality) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
44 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
45 |
lemma (in domain) square_eq_one: |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
46 |
fixes x |
66760 | 47 |
assumes [simp]: "x \<in> carrier R" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
48 |
and "x \<otimes> x = \<one>" |
66760 | 49 |
shows "x = \<one> \<or> x = \<ominus>\<one>" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
50 |
proof - |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
51 |
have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
52 |
by (simp add: ring_simprules) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
53 |
also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
54 |
by (simp add: ring_simprules) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
55 |
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" . |
66760 | 56 |
then have "(x \<oplus> \<one>) = \<zero> \<or> (x \<oplus> \<ominus> \<one>) = \<zero>" |
57 |
by (intro integral) auto |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
58 |
then show ?thesis |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
59 |
apply auto |
66760 | 60 |
apply (erule notE) |
61 |
apply (rule sum_zero_eq_neg) |
|
62 |
apply auto |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
63 |
apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)") |
66760 | 64 |
apply (simp add: ring_simprules) |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
65 |
apply (rule sum_zero_eq_neg) |
66760 | 66 |
apply auto |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
67 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
68 |
qed |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
69 |
|
66760 | 70 |
lemma (in domain) inv_eq_self: "x \<in> Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
71 |
by (metis Units_closed Units_l_inv square_eq_one) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
72 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
73 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
74 |
text \<open> |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
75 |
The following translates theorems about groups to the facts about |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
76 |
the units of a ring. (The list should be expanded as more things are |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
77 |
needed.) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
78 |
\<close> |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
79 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
80 |
lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
81 |
by (rule finite_subset) auto |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
82 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
83 |
lemma (in monoid) units_of_pow: |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
84 |
fixes n :: nat |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
85 |
shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
86 |
apply (induct n) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
87 |
apply (auto simp add: units_group group.is_monoid |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
88 |
monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) |
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 cring) units_power_order_eq_one: |
92 |
"finite (Units R) \<Longrightarrow> a \<in> Units R \<Longrightarrow> a (^) card(Units R) = \<one>" |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
93 |
apply (subst units_of_carrier [symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
94 |
apply (subst units_of_one [symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
95 |
apply (subst units_of_pow [symmetric]) |
66760 | 96 |
apply assumption |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
97 |
apply (rule comm_group.power_order_eq_one) |
66760 | 98 |
apply (rule units_comm_group) |
99 |
apply (unfold units_of_def, auto) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
100 |
done |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
diff
changeset
|
101 |
|
66760 | 102 |
end |