29 by (auto simp add: Bij_def bij_betw_imp_funcset) |
29 by (auto simp add: Bij_def bij_betw_imp_funcset) |
30 |
30 |
31 |
31 |
32 subsection {*Bijections Form a Group *} |
32 subsection {*Bijections Form a Group *} |
33 |
33 |
34 lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S" |
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_onto) |
35 by (simp add: Bij_def bij_betw_inv_into) |
36 |
36 |
37 lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S " |
37 lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S " |
38 by (auto simp add: Bij_def bij_betw_def inj_on_def) |
38 by (auto simp add: Bij_def bij_betw_def inj_on_def) |
39 |
39 |
40 lemma compose_Bij: "\<lbrakk>x \<in> Bij S; y \<in> Bij S\<rbrakk> \<Longrightarrow> compose S x y \<in> Bij S" |
40 lemma compose_Bij: "\<lbrakk>x \<in> Bij S; y \<in> Bij S\<rbrakk> \<Longrightarrow> compose S x y \<in> Bij S" |
41 by (auto simp add: Bij_def bij_betw_compose) |
41 by (auto simp add: Bij_def bij_betw_compose) |
42 |
42 |
43 lemma Bij_compose_restrict_eq: |
43 lemma Bij_compose_restrict_eq: |
44 "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)" |
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_onto_id) |
45 by (simp add: Bij_def compose_inv_into_id) |
46 |
46 |
47 theorem group_BijGroup: "group (BijGroup S)" |
47 theorem group_BijGroup: "group (BijGroup S)" |
48 apply (simp add: BijGroup_def) |
48 apply (simp add: BijGroup_def) |
49 apply (rule groupI) |
49 apply (rule groupI) |
50 apply (simp add: compose_Bij) |
50 apply (simp add: compose_Bij) |
51 apply (simp add: id_Bij) |
51 apply (simp add: id_Bij) |
52 apply (simp add: compose_Bij) |
52 apply (simp add: compose_Bij) |
53 apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset) |
53 apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset) |
54 apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) |
54 apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) |
55 apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij) |
55 apply (blast intro: Bij_compose_restrict_eq restrict_inv_into_Bij) |
56 done |
56 done |
57 |
57 |
58 |
58 |
59 subsection{*Automorphisms Form a Group*} |
59 subsection{*Automorphisms Form a Group*} |
60 |
60 |
61 lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S" |
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_onto_into) |
62 by (simp add: Bij_def bij_betw_def inv_into_into) |
63 |
63 |
64 lemma Bij_inv_onto_lemma: |
64 lemma Bij_inv_into_lemma: |
65 assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)" |
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> |
66 shows "\<lbrakk>h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S\<rbrakk> |
67 \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)" |
67 \<Longrightarrow> inv_into S h (g x y) = g (inv_into S h x) (inv_into S h y)" |
68 apply (simp add: Bij_def bij_betw_def) |
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) |
69 apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify) |
70 apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast) |
70 apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast) |
71 done |
71 done |
72 |
72 |
82 by (simp add: auto_def hom_def restrictI group.axioms id_Bij) |
82 by (simp add: auto_def hom_def restrictI group.axioms id_Bij) |
83 |
83 |
84 lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G" |
84 lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G" |
85 by (simp add: Pi_I group.axioms) |
85 by (simp add: Pi_I group.axioms) |
86 |
86 |
87 lemma (in group) restrict_inv_onto_hom: |
87 lemma (in group) restrict_inv_into_hom: |
88 "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk> |
88 "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk> |
89 \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G" |
89 \<Longrightarrow> restrict (inv_into (carrier G) h) (carrier G) \<in> hom G G" |
90 by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset |
90 by (simp add: hom_def Bij_inv_into_mem restrictI mult_funcset |
91 group.axioms Bij_inv_onto_lemma) |
91 group.axioms Bij_inv_into_lemma) |
92 |
92 |
93 lemma inv_BijGroup: |
93 lemma inv_BijGroup: |
94 "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)" |
94 "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_into S f) x)" |
95 apply (rule group.inv_equality) |
95 apply (rule group.inv_equality) |
96 apply (rule group_BijGroup) |
96 apply (rule group_BijGroup) |
97 apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq) |
97 apply (simp_all add:BijGroup_def restrict_inv_into_Bij Bij_compose_restrict_eq) |
98 done |
98 done |
99 |
99 |
100 lemma (in group) subgroup_auto: |
100 lemma (in group) subgroup_auto: |
101 "subgroup (auto G) (BijGroup (carrier G))" |
101 "subgroup (auto G) (BijGroup (carrier G))" |
102 proof (rule subgroup.intro) |
102 proof (rule subgroup.intro) |