author  ballarin 
Tue, 16 Dec 2008 21:10:53 +0100  
changeset 29237  e90d9d51106b 
parent 27717  21bbd410ba04 
child 31754  b5260f5272a4 
permissions  rwrr 
14706  1 
(* Title: HOL/Algebra/Bij.thy 
13945  2 
ID: $Id$ 
3 
Author: Florian Kammueller, with new proofs by L C Paulson 

4 
*) 

5 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16417
diff
changeset

6 
theory Bij imports Group begin 
13945  7 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
16417
diff
changeset

8 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
20318
diff
changeset

9 
section {* Bijections of a Set, Permutation and Automorphism Groups *} 
13945  10 

11 
constdefs 

14963  12 
Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" 
13945  13 
{*Only extensional functions, since otherwise we get too many.*} 
14963  14 
"Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}" 
13945  15 

14963  16 
BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" 
17 
"BijGroup S \<equiv> 

18 
\<lparr>carrier = Bij S, 

19 
mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f, 

20 
one = \<lambda>x \<in> S. x\<rparr>" 

13945  21 

22 

23 
declare Id_compose [simp] compose_Id [simp] 

24 

14963  25 
lemma Bij_imp_extensional: "f \<in> Bij S \<Longrightarrow> f \<in> extensional S" 
14666  26 
by (simp add: Bij_def) 
13945  27 

14963  28 
lemma Bij_imp_funcset: "f \<in> Bij S \<Longrightarrow> f \<in> S \<rightarrow> S" 
14853  29 
by (auto simp add: Bij_def bij_betw_imp_funcset) 
13945  30 

31 

14666  32 
subsection {*Bijections Form a Group *} 
13945  33 

14963  34 
lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S" 
14853  35 
by (simp add: Bij_def bij_betw_Inv) 
13945  36 

37 
lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S " 

14853  38 
by (auto simp add: Bij_def bij_betw_def inj_on_def) 
13945  39 

14963  40 
lemma compose_Bij: "\<lbrakk>x \<in> Bij S; y \<in> Bij S\<rbrakk> \<Longrightarrow> compose S x y \<in> Bij S" 
14853  41 
by (auto simp add: Bij_def bij_betw_compose) 
13945  42 

43 
lemma Bij_compose_restrict_eq: 

14963  44 
"f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)" 
14853  45 
by (simp add: Bij_def compose_Inv_id) 
13945  46 

47 
theorem group_BijGroup: "group (BijGroup S)" 

14666  48 
apply (simp add: BijGroup_def) 
13945  49 
apply (rule groupI) 
50 
apply (simp add: compose_Bij) 

51 
apply (simp add: id_Bij) 

52 
apply (simp add: compose_Bij) 

53 
apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset) 

54 
apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) 

14666  55 
apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij) 
13945  56 
done 
57 

58 

59 
subsection{*Automorphisms Form a Group*} 

60 

14963  61 
lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S" 
14853  62 
by (simp add: Bij_def bij_betw_def Inv_mem) 
13945  63 

64 
lemma Bij_Inv_lemma: 

14963  65 
assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)" 
66 
shows "\<lbrakk>h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S\<rbrakk> 

67 
\<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)" 

14853  68 
apply (simp add: Bij_def bij_betw_def) 
69 
apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify) 

14963  70 
apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast) 
13945  71 
done 
72 

14963  73 

13945  74 
constdefs 
14963  75 
auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" 
76 
"auto G \<equiv> hom G G \<inter> Bij (carrier G)" 

13945  77 

14963  78 
AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" 
79 
"AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>" 

13945  80 

14963  81 
lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G" 
14666  82 
by (simp add: auto_def hom_def restrictI group.axioms id_Bij) 
13945  83 

14963  84 
lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G" 
13945  85 
by (simp add: Pi_I group.axioms) 
86 

14963  87 
lemma (in group) restrict_Inv_hom: 
88 
"\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk> 

89 
\<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G" 

13945  90 
by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset 
91 
group.axioms Bij_Inv_lemma) 

92 

93 
lemma inv_BijGroup: 

14963  94 
"f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)" 
13945  95 
apply (rule group.inv_equality) 
96 
apply (rule group_BijGroup) 

14666  97 
apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq) 
13945  98 
done 
99 

14963  100 
lemma (in group) subgroup_auto: 
101 
"subgroup (auto G) (BijGroup (carrier G))" 

102 
proof (rule subgroup.intro) 

103 
show "auto G \<subseteq> carrier (BijGroup (carrier G))" 

104 
by (force simp add: auto_def BijGroup_def) 

105 
next 

106 
fix x y 

107 
assume "x \<in> auto G" "y \<in> auto G" 

108 
thus "x \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> y \<in> auto G" 

109 
by (force simp add: BijGroup_def is_group auto_def Bij_imp_funcset 

110 
group.hom_compose compose_Bij) 

111 
next 

112 
show "\<one>\<^bsub>BijGroup (carrier G)\<^esub> \<in> auto G" by (simp add: BijGroup_def id_in_auto) 

113 
next 

114 
fix x 

115 
assume "x \<in> auto G" 

116 
thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G" 

117 
by (simp del: restrict_apply 

14666  118 
add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom) 
14963  119 
qed 
13945  120 

14963  121 
theorem (in group) AutoGroup: "group (AutoGroup G)" 
122 
by (simp add: AutoGroup_def subgroup.subgroup_is_group subgroup_auto 

123 
group_BijGroup) 

13945  124 

125 
end 