1 (* Title: HOL/Algebra/Bij |
1 (* Title: HOL/Algebra/Bij |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
4 *) |
4 *) |
5 |
5 |
6 |
6 header {* Bijections of a Set, Permutation Groups, Automorphism Groups *} |
7 header{*Bijections of a Set, Permutation Groups, Automorphism Groups*} |
|
8 |
7 |
9 theory Bij = Group: |
8 theory Bij = Group: |
10 |
9 |
11 constdefs |
10 constdefs |
12 Bij :: "'a set => (('a => 'a)set)" |
11 Bij :: "'a set => ('a => 'a) set" |
13 --{*Only extensional functions, since otherwise we get too many.*} |
12 --{*Only extensional functions, since otherwise we get too many.*} |
14 "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}" |
13 "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}" |
15 |
14 |
16 BijGroup :: "'a set => (('a => 'a) monoid)" |
15 BijGroup :: "'a set => ('a => 'a) monoid" |
17 "BijGroup S == (| carrier = Bij S, |
16 "BijGroup S == |
18 mult = %g: Bij S. %f: Bij S. compose S g f, |
17 (| carrier = Bij S, |
19 one = %x: S. x |)" |
18 mult = %g: Bij S. %f: Bij S. compose S g f, |
|
19 one = %x: S. x |)" |
20 |
20 |
21 |
21 |
22 declare Id_compose [simp] compose_Id [simp] |
22 declare Id_compose [simp] compose_Id [simp] |
23 |
23 |
24 lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S" |
24 lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S" |
25 by (simp add: Bij_def) |
25 by (simp add: Bij_def) |
26 |
26 |
27 lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S" |
27 lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S" |
28 by (auto simp add: Bij_def Pi_def) |
28 by (auto simp add: Bij_def Pi_def) |
29 |
29 |
30 lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S" |
30 lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S" |
31 by (simp add: Bij_def) |
31 by (simp add: Bij_def) |
32 |
32 |
33 lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S" |
33 lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S" |
34 by (simp add: Bij_def) |
34 by (simp add: Bij_def) |
35 |
35 |
36 lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S" |
36 lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S" |
37 by (simp add: Bij_def) |
37 by (simp add: Bij_def) |
38 |
38 |
39 |
39 |
40 subsection{*Bijections Form a Group*} |
40 subsection {*Bijections Form a Group *} |
41 |
41 |
42 lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S" |
42 lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S" |
43 apply (simp add: Bij_def) |
43 apply (simp add: Bij_def) |
44 apply (intro conjI) |
44 apply (intro conjI) |
45 txt{*Proving @{term "restrict (Inv S f) S ` S = S"}*} |
45 txt{*Proving @{term "restrict (Inv S f) S ` S = S"}*} |
58 apply (auto simp add: inj_on_def) |
58 apply (auto simp add: inj_on_def) |
59 done |
59 done |
60 |
60 |
61 lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S" |
61 lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S" |
62 apply (rule BijI) |
62 apply (rule BijI) |
63 apply (simp add: compose_extensional) |
63 apply (simp add: compose_extensional) |
64 apply (blast del: equalityI |
64 apply (blast del: equalityI |
65 intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on) |
65 intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on) |
66 apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on) |
66 apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on) |
67 done |
67 done |
68 |
68 |
69 lemma Bij_compose_restrict_eq: |
69 lemma Bij_compose_restrict_eq: |
70 "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)" |
70 "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)" |
71 apply (rule compose_Inv_id) |
71 apply (rule compose_Inv_id) |
72 apply (simp add: Bij_imp_inj_on) |
72 apply (simp add: Bij_imp_inj_on) |
73 apply (simp add: Bij_imp_apply) |
73 apply (simp add: Bij_imp_apply) |
74 done |
74 done |
75 |
75 |
76 theorem group_BijGroup: "group (BijGroup S)" |
76 theorem group_BijGroup: "group (BijGroup S)" |
77 apply (simp add: BijGroup_def) |
77 apply (simp add: BijGroup_def) |
78 apply (rule groupI) |
78 apply (rule groupI) |
79 apply (simp add: compose_Bij) |
79 apply (simp add: compose_Bij) |
80 apply (simp add: id_Bij) |
80 apply (simp add: id_Bij) |
81 apply (simp add: compose_Bij) |
81 apply (simp add: compose_Bij) |
82 apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset) |
82 apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset) |
83 apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) |
83 apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) |
84 apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij) |
84 apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij) |
85 done |
85 done |
86 |
86 |
87 |
87 |
88 subsection{*Automorphisms Form a Group*} |
88 subsection{*Automorphisms Form a Group*} |
89 |
89 |
90 lemma Bij_Inv_mem: "[| f \<in> Bij S; x : S |] ==> Inv S f x : S" |
90 lemma Bij_Inv_mem: "[| f \<in> Bij S; x : S |] ==> Inv S f x : S" |
91 by (simp add: Bij_def Inv_mem) |
91 by (simp add: Bij_def Inv_mem) |
92 |
92 |
93 lemma Bij_Inv_lemma: |
93 lemma Bij_Inv_lemma: |
94 assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)" |
94 assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)" |
95 shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |] |
95 shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |] |
96 ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)" |
96 ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)" |
97 apply (simp add: Bij_def) |
97 apply (simp add: Bij_def) |
98 apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify) |
98 apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify) |
99 apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast) |
99 apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast) |
100 done |
100 done |
101 |
101 |
102 constdefs |
102 constdefs |
103 auto :: "('a,'b) monoid_scheme => ('a => 'a)set" |
103 auto :: "('a, 'b) monoid_scheme => ('a => 'a) set" |
104 "auto G == hom G G \<inter> Bij (carrier G)" |
104 "auto G == hom G G \<inter> Bij (carrier G)" |
105 |
105 |
106 AutoGroup :: "[('a,'c) monoid_scheme] => ('a=>'a) monoid" |
106 AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid" |
107 "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)" |
107 "AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)" |
108 |
108 |
109 lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G" |
109 lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G" |
110 by (simp add: auto_def hom_def restrictI group.axioms id_Bij) |
110 by (simp add: auto_def hom_def restrictI group.axioms id_Bij) |
111 |
111 |
112 lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G" |
112 lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G" |
113 by (simp add: Pi_I group.axioms) |
113 by (simp add: Pi_I group.axioms) |
114 |
114 |
115 lemma restrict_Inv_hom: |
115 lemma restrict_Inv_hom: |
120 |
120 |
121 lemma inv_BijGroup: |
121 lemma inv_BijGroup: |
122 "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)" |
122 "f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)" |
123 apply (rule group.inv_equality) |
123 apply (rule group.inv_equality) |
124 apply (rule group_BijGroup) |
124 apply (rule group_BijGroup) |
125 apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq) |
125 apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq) |
126 done |
126 done |
127 |
127 |
128 lemma subgroup_auto: |
128 lemma subgroup_auto: |
129 "group G ==> subgroup (auto G) (BijGroup (carrier G))" |
129 "group G ==> subgroup (auto G) (BijGroup (carrier G))" |
130 apply (rule group.subgroupI) |
130 apply (rule group.subgroupI) |
131 apply (rule group_BijGroup) |
131 apply (rule group_BijGroup) |
132 apply (force simp add: auto_def BijGroup_def) |
132 apply (force simp add: auto_def BijGroup_def) |
133 apply (blast intro: dest: id_in_auto) |
133 apply (blast intro: dest: id_in_auto) |
134 apply (simp del: restrict_apply |
134 apply (simp del: restrict_apply |
135 add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom) |
135 add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom) |
136 apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij) |
136 apply (simp add: BijGroup_def auto_def Bij_imp_funcset compose_hom compose_Bij) |
137 done |
137 done |
138 |
138 |
139 theorem AutoGroup: "group G ==> group (AutoGroup G)" |
139 theorem AutoGroup: "group G ==> group (AutoGroup G)" |
140 apply (simp add: AutoGroup_def) |
140 apply (simp add: AutoGroup_def) |
141 apply (rule Group.subgroup.groupI) |
141 apply (rule Group.subgroup.groupI) |
142 apply (erule subgroup_auto) |
142 apply (erule subgroup_auto) |
143 apply (insert Bij.group_BijGroup [of "carrier G"]) |
143 apply (insert Bij.group_BijGroup [of "carrier G"]) |
144 apply (simp_all add: group_def) |
144 apply (simp_all add: group_def) |
145 done |
145 done |
146 |
146 |
147 end |
147 end |
148 |
|