14706
|
1 |
(* Title: HOL/Algebra/Bij.thy
|
13945
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, with new proofs by L C Paulson
|
|
4 |
*)
|
|
5 |
|
14666
|
6 |
header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
|
13945
|
7 |
|
|
8 |
theory Bij = Group:
|
|
9 |
|
|
10 |
constdefs
|
14666
|
11 |
Bij :: "'a set => ('a => 'a) set"
|
13945
|
12 |
--{*Only extensional functions, since otherwise we get too many.*}
|
14853
|
13 |
"Bij S == extensional S \<inter> {f. bij_betw f S S}"
|
13945
|
14 |
|
14666
|
15 |
BijGroup :: "'a set => ('a => 'a) monoid"
|
|
16 |
"BijGroup S ==
|
|
17 |
(| carrier = Bij S,
|
|
18 |
mult = %g: Bij S. %f: Bij S. compose S g f,
|
|
19 |
one = %x: S. x |)"
|
13945
|
20 |
|
|
21 |
|
|
22 |
declare Id_compose [simp] compose_Id [simp]
|
|
23 |
|
|
24 |
lemma Bij_imp_extensional: "f \<in> Bij S ==> f \<in> extensional S"
|
14666
|
25 |
by (simp add: Bij_def)
|
13945
|
26 |
|
|
27 |
lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
|
14853
|
28 |
by (auto simp add: Bij_def bij_betw_imp_funcset)
|
13945
|
29 |
|
|
30 |
|
14666
|
31 |
subsection {*Bijections Form a Group *}
|
13945
|
32 |
|
|
33 |
lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
|
14853
|
34 |
by (simp add: Bij_def bij_betw_Inv)
|
13945
|
35 |
|
|
36 |
lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
|
14853
|
37 |
by (auto simp add: Bij_def bij_betw_def inj_on_def)
|
13945
|
38 |
|
|
39 |
lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
|
14853
|
40 |
by (auto simp add: Bij_def bij_betw_compose)
|
13945
|
41 |
|
|
42 |
lemma Bij_compose_restrict_eq:
|
|
43 |
"f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
|
14853
|
44 |
by (simp add: Bij_def compose_Inv_id)
|
13945
|
45 |
|
|
46 |
theorem group_BijGroup: "group (BijGroup S)"
|
14666
|
47 |
apply (simp add: BijGroup_def)
|
13945
|
48 |
apply (rule groupI)
|
|
49 |
apply (simp add: compose_Bij)
|
|
50 |
apply (simp add: id_Bij)
|
|
51 |
apply (simp add: compose_Bij)
|
|
52 |
apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset)
|
|
53 |
apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
|
14666
|
54 |
apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
|
13945
|
55 |
done
|
|
56 |
|
|
57 |
|
|
58 |
subsection{*Automorphisms Form a Group*}
|
|
59 |
|
14853
|
60 |
lemma Bij_Inv_mem: "[| f \<in> Bij S; x \<in> S |] ==> Inv S f x \<in> S"
|
|
61 |
by (simp add: Bij_def bij_betw_def Inv_mem)
|
13945
|
62 |
|
|
63 |
lemma Bij_Inv_lemma:
|
|
64 |
assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
|
14666
|
65 |
shows "[| h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S |]
|
13945
|
66 |
==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
|
14853
|
67 |
apply (simp add: Bij_def bij_betw_def)
|
|
68 |
apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
|
|
69 |
apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast )
|
13945
|
70 |
done
|
|
71 |
|
|
72 |
constdefs
|
14666
|
73 |
auto :: "('a, 'b) monoid_scheme => ('a => 'a) set"
|
13945
|
74 |
"auto G == hom G G \<inter> Bij (carrier G)"
|
|
75 |
|
14666
|
76 |
AutoGroup :: "('a, 'c) monoid_scheme => ('a => 'a) monoid"
|
13945
|
77 |
"AutoGroup G == BijGroup (carrier G) (|carrier := auto G |)"
|
|
78 |
|
|
79 |
lemma id_in_auto: "group G ==> (%x: carrier G. x) \<in> auto G"
|
14666
|
80 |
by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
|
13945
|
81 |
|
|
82 |
lemma mult_funcset: "group G ==> mult G \<in> carrier G -> carrier G -> carrier G"
|
|
83 |
by (simp add: Pi_I group.axioms)
|
|
84 |
|
|
85 |
lemma restrict_Inv_hom:
|
|
86 |
"[|group G; h \<in> hom G G; h \<in> Bij (carrier G)|]
|
|
87 |
==> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
|
|
88 |
by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
|
|
89 |
group.axioms Bij_Inv_lemma)
|
|
90 |
|
|
91 |
lemma inv_BijGroup:
|
|
92 |
"f \<in> Bij S ==> m_inv (BijGroup S) f = (%x: S. (Inv S f) x)"
|
|
93 |
apply (rule group.inv_equality)
|
|
94 |
apply (rule group_BijGroup)
|
14666
|
95 |
apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
|
13945
|
96 |
done
|
|
97 |
|
|
98 |
lemma subgroup_auto:
|
|
99 |
"group G ==> subgroup (auto G) (BijGroup (carrier G))"
|
14666
|
100 |
apply (rule group.subgroupI)
|
|
101 |
apply (rule group_BijGroup)
|
|
102 |
apply (force simp add: auto_def BijGroup_def)
|
14853
|
103 |
apply (blast dest: id_in_auto)
|
13945
|
104 |
apply (simp del: restrict_apply
|
14666
|
105 |
add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
|
14761
|
106 |
apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
|
|
107 |
compose_Bij)
|
13945
|
108 |
done
|
|
109 |
|
|
110 |
theorem AutoGroup: "group G ==> group (AutoGroup G)"
|
14666
|
111 |
apply (simp add: AutoGroup_def)
|
13945
|
112 |
apply (rule Group.subgroup.groupI)
|
14666
|
113 |
apply (erule subgroup_auto)
|
|
114 |
apply (insert Bij.group_BijGroup [of "carrier G"])
|
|
115 |
apply (simp_all add: group_def)
|
13945
|
116 |
done
|
|
117 |
|
|
118 |
end
|