11448
|
1 |
(* Title: HOL/GroupTheory/Bij
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, with new proofs by L C Paulson
|
|
4 |
Copyright 1998-2001 University of Cambridge
|
|
5 |
|
|
6 |
Bijections of a set and the group of bijections
|
|
7 |
Sigma version with locales
|
|
8 |
*)
|
|
9 |
|
|
10 |
Addsimps [Id_compose, compose_Id];
|
|
11 |
|
|
12 |
(*Inv_f_f should suffice, only here A=B=S so the equality remains.*)
|
|
13 |
Goalw [Inv_def]
|
|
14 |
"[| f`A = B; x : B |] ==> Inv A f x : A";
|
|
15 |
by (Clarify_tac 1);
|
|
16 |
by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
|
|
17 |
qed "Inv_mem";
|
|
18 |
|
|
19 |
Open_locale "bij";
|
|
20 |
|
|
21 |
val B_def = thm "B_def";
|
|
22 |
val o'_def = thm "o'_def";
|
|
23 |
val inv'_def = thm "inv'_def";
|
|
24 |
val e'_def = thm "e'_def";
|
|
25 |
|
|
26 |
Addsimps [B_def, o'_def, inv'_def];
|
|
27 |
|
|
28 |
Goal "f \\<in> B ==> f \\<in> S \\<rightarrow> S";
|
|
29 |
by (afs [Bij_def] 1);
|
|
30 |
qed "BijE1";
|
|
31 |
|
|
32 |
Goal "f \\<in> B ==> f ` S = S";
|
|
33 |
by (afs [Bij_def] 1);
|
|
34 |
qed "BijE2";
|
|
35 |
|
|
36 |
Goal "f \\<in> B ==> inj_on f S";
|
|
37 |
by (afs [Bij_def] 1);
|
|
38 |
qed "BijE3";
|
|
39 |
|
|
40 |
Goal "[| f \\<in> S \\<rightarrow> S; f ` S = S; inj_on f S |] ==> f \\<in> B";
|
|
41 |
by (afs [Bij_def] 1);
|
|
42 |
qed "BijI";
|
|
43 |
|
|
44 |
Delsimps [B_def];
|
|
45 |
Addsimps [BijE1,BijE2,BijE3];
|
|
46 |
|
|
47 |
|
|
48 |
(* restrict (Inv S f) S *)
|
|
49 |
Goal "f \\<in> B ==> (lam x: S. (inv' f) x) \\<in> B";
|
|
50 |
by (rtac BijI 1);
|
|
51 |
(* 1. (lam x: S. (inv' f) x): S \\<rightarrow> S *)
|
|
52 |
by (afs [Inv_funcset] 1);
|
|
53 |
(* 2. (lam x: S. (inv' f) x) ` S = S *)
|
|
54 |
by (asm_full_simp_tac (simpset() addsimps [inv_def]) 1);
|
|
55 |
by (rtac equalityI 1);
|
|
56 |
(* 2. <= *)
|
|
57 |
by (Clarify_tac 1);
|
|
58 |
by (afs [Inv_mem, BijE2] 1);
|
|
59 |
(* 2. => *)
|
|
60 |
by (rtac subsetI 1);
|
|
61 |
by (res_inst_tac [("x","f x")] image_eqI 1);
|
|
62 |
by (asm_simp_tac (simpset() addsimps [Inv_f_f, BijE1 RS funcset_mem]) 1);
|
|
63 |
by (asm_simp_tac (simpset() addsimps [BijE1 RS funcset_mem]) 1);
|
|
64 |
(* 3. *)
|
|
65 |
by (rtac inj_onI 1);
|
|
66 |
by (auto_tac (claset() addEs [Inv_injective], simpset()));
|
|
67 |
qed "restrict_Inv_Bij";
|
|
68 |
|
|
69 |
Addsimps [e'_def];
|
|
70 |
|
|
71 |
Goal "e'\\<in>B ";
|
|
72 |
by (rtac BijI 1);
|
|
73 |
by (auto_tac (claset(), simpset() addsimps [funcsetI, inj_on_def]));
|
|
74 |
qed "restrict_id_Bij";
|
|
75 |
|
|
76 |
Goal "f \\<in> B ==> (lam g: B. lam x: S. (inv' g) x) f = (lam x: S. (inv' f) x)";
|
|
77 |
by (Asm_full_simp_tac 1);
|
|
78 |
qed "eval_restrict_Inv";
|
|
79 |
|
|
80 |
Goal "[| x \\<in> B; y \\<in> B|] ==> x o' y \\<in> B";
|
|
81 |
by (simp_tac (simpset() addsimps [o'_def]) 1);
|
|
82 |
by (rtac BijI 1);
|
|
83 |
by (blast_tac (claset() addIs [funcset_compose] addDs [BijE1,BijE2,BijE3]) 1);
|
|
84 |
by (blast_tac (claset() delrules [equalityI]
|
|
85 |
addIs [surj_compose] addDs [BijE1,BijE2,BijE3]) 1);
|
|
86 |
by (blast_tac (claset() addIs [inj_on_compose] addDs [BijE1,BijE2,BijE3]) 1);
|
|
87 |
qed "compose_Bij";
|
|
88 |
|
|
89 |
|
|
90 |
|
|
91 |
(**** Bijections form a group ****)
|
|
92 |
|
|
93 |
|
|
94 |
Open_locale "bijgroup";
|
|
95 |
|
|
96 |
val BG_def = thm "BG_def";
|
|
97 |
|
|
98 |
Goal "[| x\\<in>B; y\\<in>B |] ==> (lam g: B. lam f: B. g o' f) x y = x o' y";
|
|
99 |
by (Asm_full_simp_tac 1);
|
|
100 |
qed "eval_restrict_comp2";
|
|
101 |
|
|
102 |
|
|
103 |
Addsimps [BG_def, B_def, o'_def, inv'_def,e'_def];
|
|
104 |
|
|
105 |
Goal "carrier BG == B";
|
|
106 |
by (afs [BijGroup_def] 1);
|
|
107 |
qed "BG_carrier";
|
|
108 |
|
|
109 |
Goal "bin_op BG == lam g: B. lam f: B. g o' f";
|
|
110 |
by (afs [BijGroup_def] 1);
|
|
111 |
qed "BG_bin_op";
|
|
112 |
|
|
113 |
Goal "inverse BG == lam f: B. lam x: S. (inv' f) x";
|
|
114 |
by (afs [BijGroup_def] 1);
|
|
115 |
qed "BG_inverse";
|
|
116 |
|
|
117 |
Goal "unit BG == e'";
|
|
118 |
by (afs [BijGroup_def] 1);
|
|
119 |
qed "BG_unit";
|
|
120 |
|
|
121 |
Goal "BG = (| carrier = BG.<cr>, bin_op = BG.<f>,\
|
|
122 |
\ inverse = BG.<inv>, unit = BG.<e> |)";
|
|
123 |
by (afs [BijGroup_def,BG_carrier, BG_bin_op, BG_inverse, BG_unit] 1);
|
|
124 |
qed "BG_defI";
|
|
125 |
|
|
126 |
Delsimps [B_def, BG_def, o'_def, inv'_def, e'_def];
|
|
127 |
|
|
128 |
|
|
129 |
Goal "(lam g: B. lam f: B. g o' f) \\<in> B \\<rightarrow> B \\<rightarrow> B";
|
|
130 |
by (simp_tac (simpset() addsimps [funcsetI, compose_Bij]) 1);
|
|
131 |
qed "restrict_compose_Bij";
|
|
132 |
|
|
133 |
|
|
134 |
Goal "BG \\<in> Group";
|
|
135 |
by (stac BG_defI 1);
|
|
136 |
by (rtac GroupI 1);
|
|
137 |
(* 1. (BG .<f>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) \\<rightarrow> (BG .<cr>) *)
|
|
138 |
by (afs [BG_bin_op, BG_carrier, restrict_compose_Bij] 1);
|
|
139 |
(* 2: (BG .<inv>)\\<in>(BG .<cr>) \\<rightarrow> (BG .<cr>) *)
|
|
140 |
by (simp_tac (simpset() addsimps [BG_inverse, BG_carrier, restrict_Inv_Bij,
|
|
141 |
funcsetI]) 1);
|
|
142 |
by (afs [BG_inverse, BG_carrier,eval_restrict_Inv, restrict_Inv_Bij] 1);
|
|
143 |
(* 3. *)
|
|
144 |
by (afs [BG_carrier, BG_unit, restrict_id_Bij] 1);
|
|
145 |
(* Now the equalities *)
|
|
146 |
(* 4. ! x:BG .<cr>. (BG .<f>) ((BG .<inv>) x) x = (BG .<e>) *)
|
|
147 |
by (simp_tac
|
|
148 |
(simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
|
|
149 |
e'_def, compose_Inv_id, inv'_def, o'_def]) 1);
|
|
150 |
by (simp_tac
|
|
151 |
(simpset() addsimps [symmetric (inv'_def), restrict_Inv_Bij]) 1);
|
|
152 |
(* 5: ! x:BG .<cr>. (BG .<f>) (BG .<e>) x = x *)
|
|
153 |
by (simp_tac
|
|
154 |
(simpset() addsimps [BG_carrier, BG_unit, BG_bin_op,
|
|
155 |
e'_def, o'_def]) 1);
|
|
156 |
by (simp_tac
|
|
157 |
(simpset() addsimps [symmetric (e'_def), restrict_id_Bij]) 1);
|
|
158 |
(* 6. ! x:BG .<cr>.
|
|
159 |
! y:BG .<cr>.
|
|
160 |
! z:BG .<cr>.
|
|
161 |
(BG .<f>) ((BG .<f>) x y) z = (BG .<f>) x ((BG .<f>) y z) *)
|
|
162 |
by (simp_tac
|
|
163 |
(simpset() addsimps [BG_carrier, BG_unit, BG_inverse, BG_bin_op,
|
|
164 |
compose_Bij]) 1);
|
|
165 |
by (simp_tac (simpset() addsimps [o'_def]) 1);
|
|
166 |
by (blast_tac (claset() addIs [compose_assoc RS sym, BijE1]) 1);
|
|
167 |
qed "Bij_are_Group";
|
|
168 |
|
|
169 |
Close_locale "bijgroup";
|
|
170 |
Close_locale "bij";
|
|
171 |
|