1 needs "Library/prime.ml";;
3 let group = new_definition
4 `group(g,(**),i,(e:A)) <=>
5 (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
6 (!x y. x IN g /\ y IN g ==> x**y IN g) /\
7 (!x y z. x IN g /\ y IN g /\ z IN g ==> x**(y**z) = (x**y)**z) /\
8 (!x. x IN g ==> x**e = x /\ e**x = x) /\
9 (!x. x IN g ==> x**i(x) = e /\ i(x)**x = e)`;;
11 let subgroup = new_definition
12 `subgroup h (g,(**),i,(e:A)) <=> h SUBSET g /\ group(h,(**),i,e)`;;
14 let bijection = new_definition
15 `bijection f s t <=> ?g. (!x:A. x IN s ==> f x IN t /\ g (f x) = x) /\
16 (!y:B. y IN t ==> g y IN s /\ f (g y) = y)`;;
18 parse_as_infix("PARTITIONS",(12,"right"));;
20 let PARTITIONS = new_definition
21 `X PARTITIONS s <=> UNIONS X = (s:A->bool) /\
22 !t u. t IN X /\ u IN X /\ ~(t = u) ==> t INTER u = {}`;;
24 parse_as_infix("**",(20,"left"));;
25 parse_as_infix("***",(20,"left"));;
29 let LAGRANGE_SKETCH = ref None;;
31 LAGRANGE_SKETCH := Some `;
32 let H G be A->bool; let (**) be A->A->A; let i be A->A; let e be A;
33 assume FINITE H /\ group (H,(**),i,e:A) /\ subgroup G (H,(**),i,e);
34 consider (***) such that !h G. h***G = {h**g | g IN G};
36 now let a be A; assume a IN H; let b be A; assume b IN H;
38 b***G = a**i(a)**b***G; .= a***(i(a)**b***G); thus .= a***G;
40 !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {}
41 proof let a be A; assume a IN H; let b be A; assume b IN H;
42 now assume ~(a***G INTER b***G = {});
43 consider g1 g2 such that g1 IN G /\ g2 IN G /\ a**g1 = b**g2;
49 !a. a IN H ==> a IN a***G
50 proof let a be A; assume a IN H;
53 {a***G | a IN H} PARTITIONS H;
54 !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G)
55 proof let a be A; assume a IN H; let b be A; assume b IN H;
56 consider f such that !g. g IN G ==> f(a**g) = b**g;
57 bijection f (a***G) (b***G);
59 set INDEX = CARD {a***G | a IN H};
60 set N = CARD H; set n = CARD G; set j = INDEX;
62 thus CARD G divides CARD H;
66 LAGRANGE_SKETCH := Some `;
67 let H G be A->bool; let (**) be A->A->A; let i be A->A; let e be A;
68 assume FINITE H /\ group (H,(**),i,e:A) /\ subgroup G (H,(**),i,e);
69 consider (***) such that !h G. h***G = {h**g | g IN G};
71 :: 2: inference time-out
73 now let a be A; assume a IN H; let b be A; assume b IN H;
75 b***G = a**i(a)**b***G; .= a***(i(a)**b***G); thus .= a***G;
78 !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {}
79 proof let a be A; assume a IN H; let b be A; assume b IN H;
80 now assume ~(a***G INTER b***G = {});
81 consider g1 g2 such that g1 IN G /\ g2 IN G /\ a**g1 = b**g2;
90 !a. a IN H ==> a IN a***G
91 proof let a be A; assume a IN H;
97 {a***G | a IN H} PARTITIONS H;
99 !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G)
100 proof let a be A; assume a IN H; let b be A; assume b IN H;
101 consider f such that !g. g IN G ==> f(a**g) = b**g;
103 bijection f (a***G) (b***G);
107 set INDEX = CARD {a***G | a IN H};
108 set N = CARD H; set n = CARD G; set j = INDEX;
111 thus CARD G divides CARD H;
118 let UNIONS_FINITE = thm `;
119 !s. FINITE (UNIONS s) <=>
120 FINITE s /\ !t:A->bool. t IN s ==> FINITE t
122 let s be (A->bool)->bool;
123 now assume FINITE (UNIONS s) [1];
124 now let t be A->bool; assume t IN s;
125 now let x be A; assume x IN t;
126 ?t. t IN s /\ x IN t;
127 thus x IN UNIONS s by ALL_TAC,UNIONS,IN_ELIM_THM;
129 thus t IN {t | t SUBSET UNIONS s} by SUBSET,IN_ELIM_THM;
131 s SUBSET {t | t SUBSET UNIONS s} by REWRITE_TAC,SUBSET;
132 FINITE {t | t SUBSET UNIONS s} by 1,FINITE_POWERSET;
133 thus FINITE s by FINITE_SUBSET;
135 qed by FINITE_UNIONS`;;
137 let CARD_UNIONS_EQUAL = thm `;
138 !X s n. FINITE s /\ X PARTITIONS s /\ (!t:A->bool. t IN X ==> CARD t = n)
139 ==> CARD s = (CARD X)*n
141 let X be (A->bool)->bool;
145 assume X PARTITIONS s [1];
146 assume !t. t IN X ==> CARD t = n [2];
147 FINITE (UNIONS X) by PARTITIONS;
148 !t. t IN X ==> FINITE t [3] by UNIONS_FINITE;
149 FINITE X [4] by UNIONS_FINITE;
150 !t. t IN X ==> CARD t = (\t. n) t [5] by 2;
151 !t u. t IN X /\ u IN X /\ ~(t = u) ==> t INTER u = {} by 1,PARTITIONS;
152 CARD s = CARD (UNIONS X) by 1,PARTITIONS;
153 .= nsum X CARD by 2,3,4,CARD_UNIONS;
154 .= nsum X (\t. n) by 5,NSUM_EQ;
155 qed by 4,NSUM_CONST`;;
157 let BIJECTION_CARD_EQ = thm `;
161 assume FINITE s /\ bijection f s t [1];
162 ?g. (!x. x IN s ==> f x IN t /\ g (f x) = x) /\
163 (!y. y IN t ==> g y IN s /\ f (g y) = y)
164 by REWRITE_TAC,-,GSYM bijection;
165 thus CARD s = CARD t by -,1,BIJECTIONS_CARD_EQ`;;
169 let LAGRANGE = thm `;
174 assume FINITE H /\ group (H,(**),i,e) /\ subgroup G (H,(**),i,e) [1];
175 (e IN H) /\ (!x. x IN H ==> i(x) IN H) /\
176 (!x y. x IN H /\ y IN H ==> x**y IN H) /\
177 (!x y z. x IN H /\ y IN H /\ z IN H ==> x**(y**z) = (x**y)**z) /\
178 (!x. x IN H ==> x**e = x /\ e**x = x) /\
179 (!x. x IN H ==> x**i(x) = e /\ i(x)**x = e) [2]
180 by REWRITE_TAC,1,GSYM group;
181 (G SUBSET H) /\ group (G,(**),i,e) [3] by 1,subgroup;
182 !x. x IN G ==> x IN H [4] by -,SUBSET;
183 FINITE G [5] by 3,1,FINITE_SUBSET;
184 (e IN G) /\ (!x. x IN G ==> i(x) IN G) /\
185 (!x y. x IN G /\ y IN G ==> x**y IN G) /\
186 (!x y z. x IN G /\ y IN G /\ z IN G ==> x**(y**z) = (x**y)**z) /\
187 (!x. x IN G ==> x**e = x /\ e**x = x) /\
188 (!x. x IN G ==> x**i(x) = e /\ i(x)**x = e) [6]
189 by REWRITE_TAC,3,GSYM group;
190 set (***) = \h G. {h**g | g IN G} [7];
191 !x h G. x IN h***G <=> ?g. g IN G /\ x = h**g [8] by ALL_TAC,-,IN_ELIM_THM;
192 !h1 h2. h1 IN H /\ h2 IN H ==> (h1**h2)***G = h1***(h2***G) [9]
195 assume h1 IN H /\ h2 IN H [10];
198 assume x IN (h1**h2)***G;
199 consider g such that g IN G /\ x = (h1**h2)**g [12] by -,8;
201 x = h1**(h2**g) [13] by -,2,10,12;
202 h2**g IN h2***G by 8,12;
203 thus x IN h1***(h2***G) by -,13,8;
207 assume x IN h1***(h2***G);
208 consider y such that y IN h2***G /\ x = h1**y [14] by -,8;
209 consider g such that g IN G /\ y = h2**g [15] by -,8;
211 x = h1**(h2**g) by 14,15;
212 .= (h1**h2)**g by -,2,10,14,16;
213 thus x IN (h1**h2)***G by -,8,15;
215 qed by -,11,EXTENSION;
216 !g. g IN G ==> g***G = G [17]
223 consider g' such that g' IN G /\ x = g**g' by -,8;
224 thus x IN G by -,6,18;
229 x = g**i(g)**x by -,6,18;
230 .= g**(i(g)**x) [21] by -,6,18,20;
231 i(g)**x IN G by 6,18,20;
232 thus x IN g***G by -,21,8;
234 qed by -,19,EXTENSION;
237 let a be A; assume a IN H [23];
238 let b be A; assume b IN H [24];
239 i(a)**b IN H [25] by 2,23,24;
240 assume i(a)**b IN G [26];
241 b***G = e**b***G by 2,24;
242 .= a**i(a)**b***G by -,2,23;
243 .= a**(i(a)**b)***G by -,2,23,24;
244 .= a***(i(a)**b***G) by -,9,23,25;
245 thus .= a***G by -,17,26;
247 !a b. a IN H /\ b IN H /\ ~(a***G = b***G) ==> a***G INTER b***G = {} [27]
249 let a be A; assume a IN H [28];
250 let b be A; assume b IN H [29];
251 now assume ~(a***G INTER b***G = {});
252 consider x such that x IN a***G INTER b***G by -,MEMBER_NOT_EMPTY;
253 x IN a***G /\ x IN b***G [30] by -,IN_INTER;
254 consider g1 such that g1 IN G /\ x = a**g1 [31] by 8,30;
255 consider g2 such that g2 IN G /\ x = b**g2 [32] by 8,30;
256 g1 IN H /\ g2 IN H [33] by 4,31,32;
257 a**g1 = b**g2 [34] by 31,32;
258 g1**i(g2) = e**g1**i(g2) by 2,33;
259 .= (i(a)**a)**g1**i(g2) by -,2,28;
260 .= i(a)**(a**g1)**i(g2) by -,2,28,33;
261 .= i(a)**(b**g2)**i(g2) by -,34;
262 .= i(a)**(b**g2**i(g2)) by -,2,28,29,33;
263 .= i(a)**(b**(g2**i(g2))) by -,2,29,33;
264 .= i(a)**(b**e) by -,2,33;
265 .= i(a)**b by -,2,29;
266 i(a)**b IN G by -,6,31,32;
267 thus a***G = b***G by -,22,28,29;
270 !a. a IN H ==> a IN a***G [35]
272 let a be A; assume a IN H;
278 assume x IN UNIONS {a***G | a IN H};
279 consider s such that s IN {a***G | a IN H} /\ x IN s [37]
281 consider a such that a IN H /\ s = a***G [38] by -;
282 consider g such that g IN G /\ x = a**g by -,8,37;
283 thus x IN H by -,2,4,38;
288 x IN x***G /\ x***G IN {a***G | a IN H} by -,35;
289 thus x IN UNIONS {a***G | a IN H} by -,IN_UNIONS;
291 thus UNIONS {a***G | a IN H} = H by -,36,EXTENSION;
293 assume t IN {a***G | a IN H} /\ u IN {a***G | a IN H} /\ ~(t = u) [39];
294 consider a b such that a IN H /\ t = a***G /\ b IN H /\ t = b***G by -;
295 thus t INTER u = {} by -,27,39;
297 {a***G | a IN H} PARTITIONS H [40] by REWRITE_TAC,-,PARTITIONS;
298 !a b. a IN H /\ b IN H ==> CARD (a***G) = CARD (b***G) [41]
300 let a be A; assume a IN H [42];
301 let b be A; assume b IN H [43];
302 set f = \x. b**(i(a)**x);
303 set f' = \x. a**(i(b)**x);
304 !g. g IN G ==> f(a**g) = b**g /\ f'(b**g) = a**g [44]
306 let g be A; assume g IN G;
308 f(a**g) = b**(i(a)**(a**g));
309 .= b**(i(a)**a**g) by -,2,42,45;
310 .= b**(e**g) by -,2,42;
311 .= b**g [46] by -,2,45;
312 f'(b**g) = a**(i(b)**(b**g));
313 .= a**(i(b)**b**g) by -,2,43,45;
314 .= a**(e**g) by -,2,43;
319 thus !x. x IN a***G ==> f x IN b***G /\ f' (f x) = x
321 let x be A; assume x IN a***G;
322 consider g such that g IN G /\ x = a**g [47] by -,8;
325 thus !y. y IN b***G ==> f' y IN a***G /\ f (f' y) = y
327 let y be A; assume y IN b***G;
328 consider g such that g IN G /\ y = b**g [48] by -,8;
332 bijection f (a***G) (b***G) [49] by ALL_TAC,-,bijection;
333 FINITE {a**g | g IN G} by SIMP_TAC,5,SIMPLE_IMAGE,FINITE_IMAGE;
334 qed by -,7,49,BIJECTION_CARD_EQ;
335 set INDEX = CARD {a***G | a IN H};
338 assume t IN {a***G | a IN H};
339 consider a such that a IN H /\ t = a***G [50] by -;
340 CARD t = CARD (a***G) by -;
341 .= CARD (e***G) by -,2,41,50;
342 thus .= CARD G by -,6,17;
347 N = (CARD {a***G | a IN H})*(CARD G) by -,1,40,CARD_UNIONS_EQUAL;
349 thus CARD G divides CARD H by -,divides,MULT_SYM;
353 parse_as_infix("**",(20,"right"));;