author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 33057  764547b68538 
child 35416  d8d7d1b785af 
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 

33057  34 
lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S" 
35 
by (simp add: Bij_def bij_betw_inv_into) 

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: 

33057  44 
"f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_into S f) S) f = (\<lambda>x\<in>S. x)" 
45 
by (simp add: Bij_def compose_inv_into_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) 

31754  53 
apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset) 
13945  54 
apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) 
33057  55 
apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij) 
13945  56 
done 
57 

58 

59 
subsection{*Automorphisms Form a Group*} 

60 

33057  61 
lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S" 
62 
by (simp add: Bij_def bij_betw_def inv_into_into) 

13945  63 

33057  64 
lemma Bij_inv_into_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> 

33057  67 
\<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into 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) 

32988  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 

33057  87 
lemma (in group) restrict_inv_into_hom: 
14963  88 
"\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk> 
33057  89 
\<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G" 
90 
by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset 

91 
group.axioms Bij_inv_into_lemma) 

13945  92 

93 
lemma inv_BijGroup: 

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

33057  97 
apply (simp_all add:BijGroup_def restrict_inv_into_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 

33057  118 
add: inv_BijGroup auto_def restrict_inv_into_Bij restrict_inv_into_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 