1 (* ========================================================================= *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Authour : VU KHAC KY *)
\r
6 (* Chaper : Packing (Cells cluster) *)
\r
8 (* ------------------ The lemma about sum of beta_bump --------------------- *)
\r
9 (* ========================================================================= *)
\r
11 (* ========================================================================= *)
\r
12 (* Checkpointed files *)
\r
13 (* ========================================================================= *)
\r
16 loads "/home/vu/flyspeck/working/marchal_cells_3.hl";;
\r
17 flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;
\r
18 open Upfzbzm_support_lemmas;;
\r
19 flyspeck_needs "packing/LEPJBDJ.hl";;
\r
24 (* ========================================================================== *)
\r
25 (* Begin the proof *)
\r
26 (* ========================================================================== *)
\r
28 module Sum_beta_bump = struct
\r
31 open Vukhacky_tactics;;
\r
36 open Marchal_cells;;
\r
38 open Marchal_cells_2_new;;
\r
40 open Upfzbzm_support_lemmas;;
\r
42 let SUM_BETA_BUMP_LEMMA = prove_by_refinement (
\r
43 `!V X. saturated V /\ packing V /\ mcell_set V X ==>
\r
44 sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`,
\r
46 [(REPEAT STRIP_TAC THEN UP_ASM_TAC);
\r
47 (ASM_CASES_TAC `~(X:real^3->bool = {})`);
\r
48 (REWRITE_TAC[mcell_set; IN_ELIM_THM]);
\r
50 (NEW_GOAL `barV V 3 ul`);
\r
53 (ASM_CASES_TAC `i < 4`); (* consider case i < 4 va i >= 4 *)
\r
54 (NEW_GOAL `~(i = 4)`);
\r
56 (NEW_GOAL `i <= 4`);
\r
58 (ASM_REWRITE_TAC[beta_bump]);
\r
60 (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);
\r
61 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
63 (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\
\r
64 mcell i V ul = mcell k V ul')`);
\r
65 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
\r
66 (ASM_REWRITE_TAC[]);
\r
67 (MATCH_MP_TAC SELECT_AX);
\r
68 (EXISTS_TAC `(i:num,ul:(real^3)list)`);
\r
70 (REWRITE_TAC[BETA_THM]);
\r
71 (ASM_REWRITE_TAC[IN]);
\r
72 (UP_ASM_TAC THEN EXPAND_TAC "P");
\r
73 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
\r
74 (NEW_GOAL `barV V 3 ul'`);
\r
77 (NEW_GOAL `i = k:num`);
\r
78 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
\r
79 (MATCH_MP_TAC BARV_3_EXPLICIT);
\r
80 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
81 (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);
\r
82 (MATCH_MP_TAC BARV_3_EXPLICIT);
\r
83 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
84 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
86 (ASM_CASES_TAC `i = 0`);
\r
87 (NEW_GOAL `V INTER mcell i V ul = {} `);
\r
88 (REWRITE_TAC[ASSUME `i = 0`]);
\r
89 (MATCH_MP_TAC LEPJBDJ_0);
\r
90 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
\r
91 (ASM_CASES_TAC `k = 0`);
\r
92 (ASM_REWRITE_TAC[]);
\r
93 (NEW_GOAL `V INTER mcell k V ul'
\r
94 = set_of_list (truncate_simplex (k - 1) ul')`);
\r
95 (MATCH_MP_TAC LEPJBDJ);
\r
96 (ASM_REWRITE_TAC[]);
\r
100 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
102 (ASM_CASES_TAC `k = 1`);
\r
103 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
\r
105 (ASM_CASES_TAC `k = 2`);
\r
106 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
\r
108 (ASM_CASES_TAC `k = 3`);
\r
109 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
\r
111 (ASM_CASES_TAC `k = 4`);
\r
112 (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);
\r
116 (ASM_MESON_TAC[]); (* Finish the case i = 0 *)
\r
118 (NEW_GOAL `V INTER mcell i V ul
\r
119 = set_of_list (truncate_simplex (i - 1) ul)`);
\r
120 (MATCH_MP_TAC LEPJBDJ);
\r
121 (ASM_REWRITE_TAC[]);
\r
126 (ASM_CASES_TAC `k = 0`);
\r
127 (NEW_GOAL `V INTER mcell k V ul' = {}`);
\r
128 (ASM_REWRITE_TAC[]);
\r
129 (MATCH_MP_TAC LEPJBDJ_0);
\r
130 (ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);
\r
133 `~(set_of_list (truncate_simplex (i - 1) (ul:(real^3)list)) = {})`);
\r
134 (ASM_CASES_TAC `i = 1`);
\r
135 (ASM_REWRITE_TAC[ARITH_RULE `1 - 1 = 0`; TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
\r
137 (ASM_CASES_TAC `i = 2`);
\r
138 (ASM_REWRITE_TAC[ARITH_RULE `2 - 1 = 1`; TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
\r
140 (ASM_CASES_TAC `i = 3`);
\r
141 (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
\r
149 (NEW_GOAL `V INTER mcell k V ul'
\r
150 = set_of_list (truncate_simplex (k - 1) ul')`);
\r
151 (MATCH_MP_TAC LEPJBDJ);
\r
152 (ASM_REWRITE_TAC[]);
\r
157 (NEW_GOAL `CARD (set_of_list (truncate_simplex (i - 1) (ul:(real^3)list)))
\r
160 `LENGTH (truncate_simplex (i - 1) (ul:(real^3)list)) = (i - 1) + 1 /\
\r
161 CARD (set_of_list (truncate_simplex (i - 1) ul)) = (i - 1) + 1`);
\r
162 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
163 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
\r
164 (ASM_REWRITE_TAC[]);
\r
165 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
168 (ASM_REWRITE_TAC[]);
\r
172 (NEW_GOAL `CARD (set_of_list (truncate_simplex (k - 1) (ul':(real^3)list)))
\r
175 `LENGTH (truncate_simplex (k - 1) (ul':(real^3)list)) = (k - 1) + 1 /\
\r
176 CARD (set_of_list (truncate_simplex (k - 1) ul')) = (k - 1) + 1`);
\r
177 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
178 (EXISTS_TAC `V:real^3->bool` THEN STRIP_TAC);
\r
179 (ASM_REWRITE_TAC[]);
\r
180 (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV);
\r
183 (ASM_REWRITE_TAC[]);
\r
187 (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);
\r
188 (ASM_REWRITE_TAC[]);
\r
191 {e',e'',p,vl | k = 4 /\ critical_edgeX V (mcell k V ul') = {e', e''} /\
\r
192 e = e' /\ p permutes 0..3 /\ vl = left_action_list p ul' /\
\r
193 e' = {EL 0 vl, EL 1 vl} /\ e'' = {EL 2 vl, EL 3 vl}}
\r
195 (bump (hl [EL 0 vl; EL 1 vl]) - bump (hl [EL 2 vl; EL 3 vl])) / &4)
\r
198 (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\
\r
199 critical_edgeX V (mcell k V ul') = {e', e''} /\
\r
200 e = e' /\ p permutes 0..3 /\
\r
201 vl = left_action_list p ul' /\
\r
202 e' = {EL 0 vl, EL 1 vl} /\
\r
203 e'' = {EL 2 vl, EL 3 vl}}`);
\r
205 `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`);
\r
206 (EXPAND_TAC "SET1");
\r
207 (NEW_GOAL `~(k = 4)`);
\r
211 (ASM_REWRITE_TAC[]);
\r
212 (ASM_REWRITE_TAC[SUM_CLAUSES]);
\r
214 (ASM_REWRITE_TAC[]);
\r
215 (REWRITE_TAC[SUM_0]);
\r
217 (* Finish the case where i < 4 *)
\r
218 (* ========================================================================= *)
\r
219 (* begin with the case i >= 4 *)
\r
221 (ASM_REWRITE_TAC[beta_bump]);
\r
223 (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);
\r
224 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
226 (ABBREV_TAC `P = (\(k,ul'). k <= 4 /\ ul' IN barV V 3 /\
\r
227 mcell i V ul = mcell k V ul')`);
\r
228 (NEW_GOAL `(P:(num#(real^3)list->bool)) (k,ul')`);
\r
229 (ASM_REWRITE_TAC[]);
\r
230 (MATCH_MP_TAC SELECT_AX);
\r
231 (EXISTS_TAC `(4,ul:(real^3)list)`);
\r
233 (REWRITE_TAC[BETA_THM]);
\r
234 (ASM_REWRITE_TAC[IN; ARITH_RULE `4 <= 4`]);
\r
235 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`;
\r
236 ARITH_RULE `4 >= 4`; mcell4]);
\r
237 (UP_ASM_TAC THEN EXPAND_TAC "P");
\r
238 (REWRITE_TAC[BETA_THM] THEN STRIP_TAC);
\r
239 (NEW_GOAL `barV V 3 ul'`);
\r
241 (REWRITE_TAC[REAL_ARITH `&0 = a <=> a = &0`]);
\r
243 (NEW_GOAL `?u0 u1 u2 u3. ul = [u0;u1;u2;u3:real^3]`);
\r
244 (MATCH_MP_TAC BARV_3_EXPLICIT);
\r
245 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
246 (NEW_GOAL `?v0 v1 v2 v3. ul' = [v0;v1;v2;v3:real^3]`);
\r
247 (MATCH_MP_TAC BARV_3_EXPLICIT);
\r
248 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
249 (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
\r
250 (NEW_GOAL `mcell i V ul = mcell 4 V ul`);
\r
251 (UNDISCH_TAC `mcell i V ul = mcell k V ul'` THEN DISCH_TAC THEN DEL_TAC);
\r
252 (ASM_SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `~(i < 4) ==> i >= 4`;
\r
253 ARITH_RULE `4 >= 4`; mcell4]);
\r
255 (NEW_GOAL `k = 4:num`);
\r
257 (NEW_GOAL `V INTER mcell 4 V ul =
\r
258 set_of_list (truncate_simplex 3 ul)`);
\r
259 (REWRITE_TAC[ARITH_RULE `3 = 4 - 1`]);
\r
260 (MATCH_MP_TAC LEPJBDJ);
\r
261 (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);
\r
264 (ASM_CASES_TAC `k = 0`);
\r
265 (NEW_GOAL `V INTER mcell k V ul' = {}`);
\r
266 (REWRITE_TAC[ASSUME `k = 0`]);
\r
267 (MATCH_MP_TAC LEPJBDJ_0);
\r
268 (ASM_REWRITE_TAC[]);
\r
270 (UNDISCH_TAC `V INTER mcell 4 V ul = set_of_list (truncate_simplex 3 ul)`);
\r
271 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);
\r
275 (* ============================= *)
\r
277 (NEW_GOAL `V INTER mcell k V ul' =
\r
278 set_of_list (truncate_simplex (k - 1) ul')`);
\r
279 (MATCH_MP_TAC LEPJBDJ);
\r
280 (ASM_REWRITE_TAC[]);
\r
285 (NEW_GOAL `set_of_list (truncate_simplex 3 (ul:(real^3)list)) =
\r
286 set_of_list (truncate_simplex (k - 1) ul')`);
\r
288 (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} = 4`);
\r
289 (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list ul`);
\r
290 (ASM_REWRITE_TAC[set_of_list]);
\r
291 (REWRITE_WITH `LENGTH (ul:(real^3)list) = 3 + 1 /\ CARD (set_of_list ul) = 3 + 1`);
\r
292 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
293 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
296 (ASM_CASES_TAC `k = 1`);
\r
298 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) =
\r
299 set_of_list (truncate_simplex (k - 1) ul')`);
\r
300 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `1 - 1 = 0`;
\r
301 TRUNCATE_SIMPLEX_EXPLICIT_0; set_of_list]);
\r
303 (NEW_GOAL `CARD {v0:real^3} = 4`);
\r
305 (UP_ASM_TAC THEN REWRITE_TAC[Geomdetail.CARD_SING]);
\r
309 (ASM_CASES_TAC `k = 2`);
\r
311 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) =
\r
312 set_of_list (truncate_simplex (k - 1) ul')`);
\r
313 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `2 - 1 = 1`;
\r
314 TRUNCATE_SIMPLEX_EXPLICIT_1; set_of_list]);
\r
316 (NEW_GOAL `CARD {v0, v1:real^3} = 4`);
\r
318 (NEW_GOAL `CARD {v0, v1:real^3} <= 2`);
\r
319 (MESON_TAC[Geomdetail.CARD2]);
\r
323 (ASM_CASES_TAC `k = 3`);
\r
325 (UNDISCH_TAC `set_of_list (truncate_simplex 3 (ul:(real^3)list)) =
\r
326 set_of_list (truncate_simplex (k - 1) ul')`);
\r
327 (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_3; ARITH_RULE `3 - 1 = 2`;
\r
328 TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);
\r
330 (NEW_GOAL `CARD {v0, v1, v2:real^3} = 4`);
\r
332 (NEW_GOAL `CARD {v0, v1, v2:real^3} <= 3`);
\r
333 (MESON_TAC[Geomdetail.CARD3]);
\r
337 (ASM_ARITH_TAC); (* concluded that k = 4 now *)
\r
339 (* ======================================================================== *)
\r
342 (REWRITE_TAC[ASSUME `mcell i V ul = mcell k V ul'`; ASSUME `k = 4`]);
\r
343 (ASM_CASES_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`);
\r
344 (MATCH_MP_TAC SUM_EQ_0);
\r
345 (REPEAT STRIP_TAC);
\r
346 (ABBREV_TAC `y = {v0,v1,v2,v3:real^3} DIFF x`);
\r
347 (ASM_CASES_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);
\r
349 `{e',e'',p,vl | critical_edgeX V (mcell 4 V ul') = {e', e''} /\
\r
352 vl = left_action_list p ul' /\
\r
353 e' = {EL 0 vl, EL 1 vl} /\
\r
354 e'' = {EL 2 vl, EL 3 vl}} = {}`);
\r
355 (REWRITE_TAC[SET_RULE `a = {} <=> (!t. t IN a ==> F)`]);
\r
356 (REWRITE_TAC[IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
357 (NEW_GOAL `y = e'':real^3->bool`);
\r
358 (ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "y");
\r
359 (REWRITE_TAC[ASSUME `x = e':real^3->bool`;
\r
360 ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
\r
361 (REWRITE_WITH `{v0, v1, v2, v3:real^3} = set_of_list (ul')`);
\r
362 (ASM_REWRITE_TAC[set_of_list]);
\r
363 (REWRITE_WITH `set_of_list (ul':(real^3)list) = set_of_list vl`);
\r
364 (ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REWRITE_TAC[ASSUME
\r
365 `vl:(real^3)list = left_action_list p ul'`]);
\r
366 (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);
\r
367 (ASM_REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
\r
369 (NEW_GOAL `vl:(real^3)list = [EL 0 vl; EL 1 vl; EL 2 vl; EL 3 vl]`);
\r
370 (ASM_REWRITE_TAC[TABLE_4; left_action_list; LENGTH; EL; HD; TL;
\r
371 ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4 /\ 1 = SUC 0 /\ 2 = SUC 1/\ 3 = SUC 2`]);
\r
372 (ABBREV_TAC `w0:real^3 = EL 0 vl`);
\r
373 (ABBREV_TAC `w1:real^3 = EL 1 vl`);
\r
374 (ABBREV_TAC `w2:real^3 = EL 2 vl`);
\r
375 (ABBREV_TAC `w3:real^3 = EL 3 vl`);
\r
376 (REWRITE_TAC[ASSUME `vl = [w0;w1;w2;w3:real^3]`; set_of_list]);
\r
377 (REWRITE_WITH `{w0,w1,w2,w3} = {w0,w1} UNION {w2,w3:real^3}`);
\r
379 (MATCH_MP_TAC (SET_RULE `DISJOINT a b ==> ((a UNION b) DIFF a = b)`));
\r
381 (REWRITE_TAC[DISJOINT; INTER]);
\r
382 (NEW_GOAL `CARD {w0, w1, w2 , w3:real^3} = 4`);
\r
383 (REWRITE_WITH `{w0, w1, w2 , w3:real^3} = set_of_list vl`);
\r
384 (REWRITE_TAC[ASSUME `vl = [w0; w1; w2; w3:real^3]`; set_of_list]);
\r
385 (ONCE_ASM_REWRITE_TAC[]);
\r
386 (REWRITE_WITH `set_of_list (left_action_list p ul')
\r
387 = set_of_list (ul':(real^3)list)`);
\r
388 (MATCH_MP_TAC Packing3.SET_OF_LIST_LEFT_ACTION_LIST);
\r
389 (ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]);
\r
390 (REWRITE_WITH `LENGTH (ul':(real^3)list) = 3 + 1 /\
\r
391 CARD (set_of_list ul') = 3 + 1`);
\r
392 (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD);
\r
393 (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);
\r
395 (REWRITE_TAC[SET_RULE `x IN {a,b} <=> x = a \/ x = b`]);
\r
396 (REWRITE_TAC[SET_RULE `x = {} <=> (!z. z IN x ==> F)`]);
\r
397 (REWRITE_TAC[IN;IN_ELIM_THM] THEN STRIP_TAC);
\r
398 (REPEAT STRIP_TAC);
\r
400 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
\r
401 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);
\r
402 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
403 (REWRITE_TAC[Geomdetail.CARD3]);
\r
405 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
\r
406 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w1, w2, w3}`);
\r
407 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
408 (REWRITE_TAC[Geomdetail.CARD3]);
\r
410 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
\r
411 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);
\r
412 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
413 (REWRITE_TAC[Geomdetail.CARD3]);
\r
415 (NEW_GOAL `CARD {w0, w1, w2, w3:real^3} <= 3`);
\r
416 (REWRITE_WITH `{w0, w1, w2, w3:real^3} = {w0, w2, w3}`);
\r
417 (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);
\r
418 (REWRITE_TAC[Geomdetail.CARD3]);
\r
421 (UNDISCH_TAC `~(critical_edgeX V (mcell 4 V ul') = {x, y})`);
\r
422 (REWRITE_TAC[ASSUME `x = e':real^3->bool`; ASSUME `y = e'':real^3->bool`]);
\r
423 (ASM_REWRITE_TAC[]);
\r
424 (REWRITE_TAC[SUM_CLAUSES]);
\r
425 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);
\r
427 (UNDISCH_TAC `~(CARD (critical_edgeX V (mcell 4 V ul')) = 2)`);
\r
428 (REWRITE_TAC[ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);
\r
429 (REWRITE_TAC[Geomdetail.CARD_SET2]);
\r
432 (NEW_GOAL `{v0, v1,v2,v3:real^3} = {}`);
\r
433 (MATCH_MP_TAC (SET_RULE `!s:real^3->bool. x = s DIFF x ==> s = {}`));
\r
435 (UP_ASM_TAC THEN SET_TAC[]);
\r
438 (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ a <=> a`] THEN STRIP_TAC);
\r
439 (NEW_GOAL `?x y. critical_edgeX V (mcell 4 V ul') = {x, y} /\ ~(x = y)`);
\r
440 (MATCH_MP_TAC Rogers.CARD_2_IMP_DOUBLE);
\r
441 (ASM_REWRITE_TAC[FINITE_critical_edgeX]);
\r
442 (UP_ASM_TAC THEN STRIP_TAC);
\r
443 (REWRITE_TAC[SET_RULE `{x | x IN s} = s`;
\r
444 ASSUME `critical_edgeX V (mcell 4 V ul') = {x, y}`]);
\r
445 (ASM_SIMP_TAC[Collect_geom.SUM_DIS2]);
\r
449 `{e',e'',p,vl | {x, y} = {e', e''} /\
\r
452 vl = left_action_list p [v0; v1; v2; v3:real^3] /\
\r
453 e' = {EL 0 vl, EL 1 vl} /\
\r
454 e'' = {EL 2 vl, EL 3 vl}} =
\r
455 {e',e'',p,vl | e' = x /\ e'' = y /\
\r
457 vl = left_action_list p [v0; v1; v2; v3] /\
\r
458 x = {EL 0 vl, EL 1 vl} /\
\r
459 y = {EL 2 vl, EL 3 vl}}`);
\r
460 (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
\r
463 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
\r
464 (REPEAT STRIP_TAC);
\r
465 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
\r
466 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
\r
467 (REPEAT STRIP_TAC);
\r
468 (ASM_REWRITE_TAC[]);
\r
469 (ASM_REWRITE_TAC[]);
\r
470 (ASM_REWRITE_TAC[]);
\r
471 (ASM_REWRITE_TAC[]);
\r
472 (REWRITE_TAC[ASSUME `e':real^3->bool = x`;
\r
473 ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`]);
\r
474 (REWRITE_TAC[ASSUME `e'':real^3->bool = y`;
\r
475 ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`]);
\r
476 (ASM_REWRITE_TAC[]);
\r
478 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
\r
479 (REPEAT STRIP_TAC);
\r
480 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
\r
481 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
\r
482 (NEW_GOAL `y = e'':(real^3->bool)`);
\r
484 (REPEAT STRIP_TAC);
\r
485 (ASM_REWRITE_TAC[]);
\r
486 (ASM_REWRITE_TAC[]);
\r
487 (ASM_REWRITE_TAC[]);
\r
488 (ASM_REWRITE_TAC[]);
\r
489 (REWRITE_TAC[ASSUME `x:real^3->bool = e'`;
\r
490 ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
\r
491 (REWRITE_TAC[ASSUME `y:real^3->bool = e''`;
\r
492 ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);
\r
493 (ASM_REWRITE_TAC[]);
\r
497 `{e',e'',p,vl | {x, y} = {e', e''} /\
\r
500 vl = left_action_list p [v0; v1; v2; v3:real^3] /\
\r
501 e' = {EL 0 vl, EL 1 vl} /\
\r
502 e'' = {EL 2 vl, EL 3 vl}} =
\r
503 {e',e'',p,vl | e' = y /\ e'' = x /\
\r
505 vl = left_action_list p [v0; v1; v2; v3] /\
\r
506 y = {EL 0 vl, EL 1 vl} /\
\r
507 x = {EL 2 vl, EL 3 vl}}`);
\r
508 (ONCE_REWRITE_TAC[SET_RULE `a = b <=> b SUBSET a /\ a SUBSET b`]);
\r
511 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
\r
512 (REPEAT STRIP_TAC);
\r
513 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
\r
514 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
\r
515 (REPEAT STRIP_TAC);
\r
517 (REWRITE_TAC[ASSUME `e' = y:real^3->bool`; ASSUME `e'' = x:real^3->bool`]);
\r
519 (ASM_REWRITE_TAC[]);
\r
520 (ASM_REWRITE_TAC[]);
\r
521 (ASM_REWRITE_TAC[]);
\r
522 (REWRITE_TAC[ASSUME `e':real^3->bool = y`;
\r
523 ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`]);
\r
524 (REWRITE_TAC[ASSUME `e'':real^3->bool = x`;
\r
525 ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`]);
\r
526 (ASM_REWRITE_TAC[]);
\r
528 (REWRITE_TAC[SUBSET] THEN ONCE_REWRITE_TAC[IN] THEN REWRITE_TAC[IN_ELIM_THM]);
\r
529 (REPEAT STRIP_TAC);
\r
530 (EXISTS_TAC `e':real^3->bool` THEN EXISTS_TAC `e'':real^3->bool`);
\r
531 (EXISTS_TAC `p:num->num` THEN EXISTS_TAC `vl:(real^3)list`);
\r
532 (NEW_GOAL `x = e'':(real^3->bool)`);
\r
534 (REPEAT STRIP_TAC);
\r
535 (ASM_REWRITE_TAC[]);
\r
536 (ASM_REWRITE_TAC[]);
\r
537 (ASM_REWRITE_TAC[]);
\r
538 (ASM_REWRITE_TAC[]);
\r
539 (REWRITE_TAC[ASSUME `y:real^3->bool = e'`;
\r
540 ASSUME `e':real^3->bool = {EL 0 vl, EL 1 vl}`]);
\r
541 (REWRITE_TAC[ASSUME `x:real^3->bool = e''`;
\r
542 ASSUME `e'':real^3->bool = {EL 2 vl, EL 3 vl}`]);
\r
543 (ASM_REWRITE_TAC[]);
\r
545 (ABBREV_TAC `S1 = {e',e'',p,vl | e' = x /\
\r
548 vl = left_action_list p [v0; v1; v2; v3:real^3] /\
\r
549 x = {EL 0 vl, EL 1 vl} /\
\r
550 y = {EL 2 vl, EL 3 vl}}`);
\r
551 (ABBREV_TAC `S2 = {e',e'',p,vl | e' = y /\
\r
554 vl = left_action_list p [v0; v1; v2; v3:real^3] /\
\r
555 y = {EL 0 vl, EL 1 vl} /\
\r
556 x = {EL 2 vl, EL 3 vl}}`);
\r
558 `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool)
\r
559 (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
\r
560 bump (hl [EL 2 vl; EL 3 vl])) / &4) =
\r
561 sum S2 (\(e',e'',p,vl). -- ((bump (hl [EL 2 vl; EL 3 vl]) -
\r
562 bump (hl [EL 0 vl; EL 1 vl])) / &4))`);
\r
563 (ONCE_REWRITE_TAC[REAL_ARITH `(bump (hl [EL 0 vl; EL 1 vl]) -
\r
564 bump (hl [EL 2 vl; EL 3 vl])) /
\r
565 &4 = -- ((bump (hl [EL 2 vl; EL 3 vl]) -
\r
566 bump (hl [EL 0 vl; EL 1 vl])) /
\r
568 (ASM_REWRITE_TAC[]);
\r
569 (ONCE_REWRITE_TAC[SUM_NEG]);
\r
570 (ABBREV_TAC `f = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).
\r
571 ((bump (hl [EL 2 vl; EL 3 vl]) - bump (hl [EL 0 vl; EL 1 vl])) / &4))`);
\r
574 --((bump (hl [EL 2 vl; EL 3 vl]) -bump (hl [EL 0 vl; EL 1 vl])) / &4))
\r
575 = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).
\r
576 -- f (e',e'',p,vl))`);
\r
578 (REWRITE_TAC[BETA_THM]);
\r
581 `sum (S2:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool) (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).
\r
582 -- f (e',e'',p,vl)) =
\r
583 sum S2 (\x. -- f x)`);
\r
585 (REWRITE_TAC[FUN_EQ_THM]);
\r
587 (REWRITE_TAC[BETA_THM]);
\r
588 (REPEAT STRIP_TAC);
\r
590 (ABBREV_TAC `e' = FST (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);
\r
591 (ABBREV_TAC `e'' = FST (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);
\r
592 (ABBREV_TAC `p = FST (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
\r
593 (ABBREV_TAC `vl = SND (SND (SND (x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
\r
595 (REWRITE_WITH `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list =
\r
597 (EXPAND_TAC "e'" THEN EXPAND_TAC "e''" THEN EXPAND_TAC "p" THEN EXPAND_TAC "vl");
\r
598 (REWRITE_TAC[PAIR]);
\r
599 (REWRITE_TAC[SUM_NEG]);
\r
600 (REWRITE_TAC[REAL_ARITH `a + -- b = &0 <=> a = b`]);
\r
602 (* --------------------------------------------------------------------------- *)
\r
603 (* Begin new part *)
\r
607 `g = (\x. let (e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list) = x
\r
610 if p i = 0 then 2 else
\r
611 if p i = 1 then 3 else
\r
612 if p i = 2 then 0 else
\r
613 if p i = 3 then 1 else i),
\r
614 [EL 2 vl;EL 3 vl;EL 0 vl;EL 1 vl]))`);
\r
617 (g:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->(real^3->bool)#
\r
618 (real^3->bool)#(num->num)#(real^3)list) S2 /\
\r
619 (\(e',e'',p,vl). (bump (hl [EL 2 vl; EL 3 vl]) -
\r
620 bump (hl [EL 0 vl; EL 1 vl])) / &4) =
\r
621 (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
\r
622 bump (hl [EL 2 vl; EL 3 vl])) / &4) o g `);
\r
624 (* ======================================================================= *)
\r
626 (REPEAT STRIP_TAC);
\r
627 (* New goal 1: to prove S1 = IMAGE g S2 *)
\r
629 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");
\r
630 (REWRITE_TAC[IMAGE]);
\r
631 (ONCE_REWRITE_TAC[SET_EQ_LEMMA] THEN ONCE_REWRITE_TAC[IN] THEN
\r
632 REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC);
\r
634 `(e'':real^3->bool,
\r
640 else if p i = 2 then 0 else if p i = 3 then 1 else i),
\r
641 [EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl])`);
\r
642 (REPEAT STRIP_TAC);
\r
643 (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);
\r
644 (ABBREV_TAC `p' = (\i. if p i = 0
\r
648 else if p i = 2 then 0 else if p i = 3 then 1 else i)`);
\r
649 (EXISTS_TAC `p':num->num`);
\r
650 (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);
\r
652 `EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 2 (vl:(real^3)list) /\
\r
653 EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 3 vl /\
\r
654 EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 0 vl /\
\r
655 EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl] = EL 1 vl`);
\r
656 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
657 (REWRITE_TAC[ASSUME `e'' = y:real^3->bool`; ASSUME `e' = x:real^3->bool`;
\r
658 ASSUME `y:real^3->bool = {EL 2 vl, EL 3 vl}`;
\r
659 ASSUME `x:real^3->bool = {EL 0 vl, EL 1 vl}`;left_action_list;
\r
660 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
662 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
\r
663 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
670 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
\r
671 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
682 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
\r
683 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
698 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
\r
699 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
718 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
\r
719 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
738 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
\r
739 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
740 (REPEAT STRIP_TAC);
\r
741 (ABBREV_TAC `s = (p:num->num) u`);
\r
742 (NEW_GOAL `(p:num->num) s = s`);
\r
743 (FIRST_ASSUM MATCH_MP_TAC);
\r
744 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
745 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
\r
746 (ASM_REWRITE_TAC[]);
\r
747 (UP_ASM_TAC THEN STRIP_TAC);
\r
748 (NEW_GOAL `s = x'':num`);
\r
749 (FIRST_ASSUM MATCH_MP_TAC);
\r
750 (ASM_REWRITE_TAC[]);
\r
751 (NEW_GOAL `u = x'':num`);
\r
752 (FIRST_ASSUM MATCH_MP_TAC);
\r
753 (ASM_REWRITE_TAC[]);
\r
754 (ASM_REWRITE_TAC[]);
\r
758 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
\r
759 (REPEAT STRIP_TAC);
\r
760 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
761 (NEW_GOAL `(p':num->num) u = 2`);
\r
762 (FIRST_ASSUM MATCH_MP_TAC);
\r
763 (ASM_REWRITE_TAC[]);
\r
767 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
768 (NEW_GOAL `(p':num->num) u = 3`);
\r
769 (FIRST_ASSUM MATCH_MP_TAC);
\r
770 (ASM_REWRITE_TAC[]);
\r
774 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
775 (NEW_GOAL `(p':num->num) u = 1`);
\r
776 (FIRST_ASSUM MATCH_MP_TAC);
\r
777 (ASM_REWRITE_TAC[]);
\r
781 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
782 (NEW_GOAL `(p':num->num) u = u`);
\r
783 (FIRST_ASSUM MATCH_MP_TAC);
\r
784 (ASM_REWRITE_TAC[]);
\r
785 (NEW_GOAL `(p:num->num) u = u`);
\r
786 (FIRST_ASSUM MATCH_MP_TAC);
\r
787 (ASM_REWRITE_TAC[]);
\r
793 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
\r
794 (REPEAT STRIP_TAC);
\r
795 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
796 (NEW_GOAL `(p':num->num) u = 2`);
\r
797 (FIRST_ASSUM MATCH_MP_TAC);
\r
798 (ASM_REWRITE_TAC[]);
\r
802 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
803 (NEW_GOAL `(p':num->num) u = 3`);
\r
804 (FIRST_ASSUM MATCH_MP_TAC);
\r
805 (ASM_REWRITE_TAC[]);
\r
809 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
810 (NEW_GOAL `(p':num->num) u = 0`);
\r
811 (FIRST_ASSUM MATCH_MP_TAC);
\r
812 (ASM_REWRITE_TAC[]);
\r
816 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
817 (NEW_GOAL `(p':num->num) u = u`);
\r
818 (FIRST_ASSUM MATCH_MP_TAC);
\r
819 (ASM_REWRITE_TAC[]);
\r
820 (NEW_GOAL `(p:num->num) u = u`);
\r
821 (FIRST_ASSUM MATCH_MP_TAC);
\r
822 (ASM_REWRITE_TAC[]);
\r
828 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
\r
829 (REPEAT STRIP_TAC);
\r
830 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
831 (NEW_GOAL `(p':num->num) u = 3`);
\r
832 (FIRST_ASSUM MATCH_MP_TAC);
\r
833 (ASM_REWRITE_TAC[]);
\r
837 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
838 (NEW_GOAL `(p':num->num) u = 0`);
\r
839 (FIRST_ASSUM MATCH_MP_TAC);
\r
840 (ASM_REWRITE_TAC[]);
\r
844 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
845 (NEW_GOAL `(p':num->num) u = 1`);
\r
846 (FIRST_ASSUM MATCH_MP_TAC);
\r
847 (ASM_REWRITE_TAC[]);
\r
851 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
852 (NEW_GOAL `(p':num->num) u = u`);
\r
853 (FIRST_ASSUM MATCH_MP_TAC);
\r
854 (ASM_REWRITE_TAC[]);
\r
855 (NEW_GOAL `(p:num->num) u = u`);
\r
856 (FIRST_ASSUM MATCH_MP_TAC);
\r
857 (ASM_REWRITE_TAC[]);
\r
863 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
\r
864 (REPEAT STRIP_TAC);
\r
865 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
866 (NEW_GOAL `(p':num->num) u = 2`);
\r
867 (FIRST_ASSUM MATCH_MP_TAC);
\r
868 (ASM_REWRITE_TAC[]);
\r
872 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
873 (NEW_GOAL `(p':num->num) u = 0`);
\r
874 (FIRST_ASSUM MATCH_MP_TAC);
\r
875 (ASM_REWRITE_TAC[]);
\r
879 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
880 (NEW_GOAL `(p':num->num) u = 1`);
\r
881 (FIRST_ASSUM MATCH_MP_TAC);
\r
882 (ASM_REWRITE_TAC[]);
\r
886 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
887 (NEW_GOAL `(p':num->num) u = u`);
\r
888 (FIRST_ASSUM MATCH_MP_TAC);
\r
889 (ASM_REWRITE_TAC[]);
\r
890 (NEW_GOAL `(p:num->num) u = u`);
\r
891 (FIRST_ASSUM MATCH_MP_TAC);
\r
892 (ASM_REWRITE_TAC[]);
\r
898 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
\r
899 (REPEAT STRIP_TAC);
\r
900 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
901 (NEW_GOAL `(p':num->num) u = 2`);
\r
902 (FIRST_ASSUM MATCH_MP_TAC);
\r
903 (ASM_REWRITE_TAC[]);
\r
907 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
908 (NEW_GOAL `(p':num->num) u = 3`);
\r
909 (FIRST_ASSUM MATCH_MP_TAC);
\r
910 (ASM_REWRITE_TAC[]);
\r
914 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
915 (NEW_GOAL `(p':num->num) u = 0`);
\r
916 (FIRST_ASSUM MATCH_MP_TAC);
\r
917 (ASM_REWRITE_TAC[]);
\r
921 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
922 (NEW_GOAL `(p':num->num) u = 1`);
\r
923 (FIRST_ASSUM MATCH_MP_TAC);
\r
924 (ASM_REWRITE_TAC[]);
\r
930 (* ------------------------------------------------------------------------- *)
\r
931 (* begin to prove that p' permutes 0..3 *)
\r
934 (NEW_GOAL `p' permutes 0..3`);
\r
935 (REWRITE_TAC[permutes]);
\r
936 (REPEAT STRIP_TAC);
\r
937 (NEW_GOAL `x'' > 3`);
\r
938 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
940 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);
\r
941 (NEW_GOAL `(p:num->num) x'' = x''`);
\r
953 (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);
\r
955 (ASM_CASES_TAC `y' = 0`);
\r
956 (NEW_GOAL `?z. (p:num->num) z = 2`);
\r
957 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
958 (UP_ASM_TAC THEN STRIP_TAC);
\r
959 (EXISTS_TAC `z:num`);
\r
960 (ASM_REWRITE_TAC[]);
\r
961 (REPEAT STRIP_TAC);
\r
962 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
963 (NEW_GOAL `(p:num->num) y'' = 2`);
\r
964 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
965 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
966 (REPEAT STRIP_TAC);
\r
967 (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);
\r
968 (ASM_REWRITE_TAC[]);
\r
969 (UP_ASM_TAC THEN STRIP_TAC);
\r
970 (REWRITE_WITH `y'' = s:num`);
\r
971 (FIRST_ASSUM MATCH_MP_TAC);
\r
972 (ASM_REWRITE_TAC[]);
\r
973 (REWRITE_WITH `z = s:num`);
\r
974 (FIRST_ASSUM MATCH_MP_TAC);
\r
975 (ASM_REWRITE_TAC[]);
\r
977 (ASM_CASES_TAC `y' = 1`);
\r
978 (NEW_GOAL `?z. (p:num->num) z = 3`);
\r
979 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
980 (UP_ASM_TAC THEN STRIP_TAC);
\r
981 (EXISTS_TAC `z:num`);
\r
982 (ASM_REWRITE_TAC[]);
\r
983 (REPEAT STRIP_TAC);
\r
984 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
985 (NEW_GOAL `(p:num->num) y'' = 3`);
\r
986 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
987 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
988 (REPEAT STRIP_TAC);
\r
989 (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);
\r
990 (ASM_REWRITE_TAC[]);
\r
991 (UP_ASM_TAC THEN STRIP_TAC);
\r
992 (REWRITE_WITH `y'' = s:num`);
\r
993 (FIRST_ASSUM MATCH_MP_TAC);
\r
994 (ASM_REWRITE_TAC[]);
\r
995 (REWRITE_WITH `z = s:num`);
\r
996 (FIRST_ASSUM MATCH_MP_TAC);
\r
997 (ASM_REWRITE_TAC[]);
\r
999 (ASM_CASES_TAC `y' = 2`);
\r
1000 (NEW_GOAL `?z. (p:num->num) z = 0`);
\r
1001 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1002 (UP_ASM_TAC THEN STRIP_TAC);
\r
1003 (EXISTS_TAC `z:num`);
\r
1004 (ASM_REWRITE_TAC[]);
\r
1005 (REPEAT STRIP_TAC);
\r
1006 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1007 (NEW_GOAL `(p:num->num) y'' = 0`);
\r
1008 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1009 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1010 (REPEAT STRIP_TAC);
\r
1011 (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);
\r
1012 (ASM_REWRITE_TAC[]);
\r
1013 (UP_ASM_TAC THEN STRIP_TAC);
\r
1014 (REWRITE_WITH `y'' = s:num`);
\r
1015 (FIRST_ASSUM MATCH_MP_TAC);
\r
1016 (ASM_REWRITE_TAC[]);
\r
1017 (REWRITE_WITH `z = s:num`);
\r
1018 (FIRST_ASSUM MATCH_MP_TAC);
\r
1019 (ASM_REWRITE_TAC[]);
\r
1021 (ASM_CASES_TAC `y' = 3`);
\r
1022 (NEW_GOAL `?z. (p:num->num) z = 1`);
\r
1023 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1024 (UP_ASM_TAC THEN STRIP_TAC);
\r
1025 (EXISTS_TAC `z:num`);
\r
1026 (ASM_REWRITE_TAC[]);
\r
1027 (REPEAT STRIP_TAC);
\r
1028 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1029 (NEW_GOAL `(p:num->num) y'' = 1`);
\r
1030 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1031 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1032 (REPEAT STRIP_TAC);
\r
1033 (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);
\r
1034 (ASM_REWRITE_TAC[]);
\r
1035 (UP_ASM_TAC THEN STRIP_TAC);
\r
1036 (REWRITE_WITH `y'' = s:num`);
\r
1037 (FIRST_ASSUM MATCH_MP_TAC);
\r
1038 (ASM_REWRITE_TAC[]);
\r
1039 (REWRITE_WITH `z = s:num`);
\r
1040 (FIRST_ASSUM MATCH_MP_TAC);
\r
1041 (ASM_REWRITE_TAC[]);
\r
1045 (NEW_GOAL `y' > 3`);
\r
1047 (NEW_GOAL `?z. (p:num->num) z = y'`);
\r
1048 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1049 (UP_ASM_TAC THEN STRIP_TAC);
\r
1050 (EXISTS_TAC `z:num`);
\r
1051 (ASM_REWRITE_TAC[]);
\r
1052 (REPEAT STRIP_TAC);
\r
1053 (NEW_GOAL `(p:num->num) z = z`);
\r
1054 (FIRST_ASSUM MATCH_MP_TAC);
\r
1056 (NEW_GOAL `(p':num->num) z = z`);
\r
1057 (FIRST_ASSUM MATCH_MP_TAC);
\r
1061 (NEW_GOAL `(p:num->num) z = z`);
\r
1062 (FIRST_ASSUM MATCH_MP_TAC);
\r
1064 (NEW_GOAL `(p':num->num) z = z`);
\r
1065 (FIRST_ASSUM MATCH_MP_TAC);
\r
1067 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1068 (REPEAT STRIP_TAC);
\r
1069 (NEW_GOAL `(p:num->num) y'' > 3`);
\r
1070 (FIRST_ASSUM MATCH_MP_TAC);
\r
1071 (ASM_REWRITE_TAC[]);
\r
1073 (NEW_GOAL `(p:num->num) y'' = y''`);
\r
1074 (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));
\r
1075 (ASM_REWRITE_TAC[]);
\r
1076 (NEW_GOAL `(p':num->num) y'' = y''`);
\r
1077 (FIRST_ASSUM MATCH_MP_TAC);
\r
1078 (ASM_REWRITE_TAC[]);
\r
1080 (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);
\r
1081 (ASM_REWRITE_TAC[]);
\r
1082 (UP_ASM_TAC THEN STRIP_TAC);
\r
1083 (REWRITE_WITH `y'' = s:num`);
\r
1084 (FIRST_ASSUM MATCH_MP_TAC);
\r
1085 (ASM_MESON_TAC[]);
\r
1086 (REWRITE_WITH `z = s:num`);
\r
1087 (FIRST_ASSUM MATCH_MP_TAC);
\r
1088 (ASM_MESON_TAC[]);
\r
1091 (* finish proving that p' permutes 0..3 *)
\r
1093 (REWRITE_TAC[ASSUME `p' permutes 0..3`]);
\r
1095 (* --------------------------------------------------------------------- *)
\r
1097 (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);
\r
1098 (ASM_REWRITE_TAC[left_action_list;
\r
1099 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1100 (REWRITE_WITH `EL 2
\r
1101 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
1102 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
1103 = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);
\r
1104 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1105 (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);
\r
1106 (ABBREV_TAC `j = inverse (p:num->num) 2`);
\r
1107 (NEW_GOAL `(p:num->num) j = 2`);
\r
1108 (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);
\r
1109 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1110 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1111 (ASM_REWRITE_TAC[]);
\r
1112 (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);
\r
1113 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1114 (EXPAND_TAC "p'");
\r
1118 (ASM_MESON_TAC[]);
\r
1122 (ASM_MESON_TAC[]);
\r
1126 (ASM_MESON_TAC[]);
\r
1127 (ASM_MESON_TAC[]);
\r
1131 (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);
\r
1132 (ASM_REWRITE_TAC[left_action_list;
\r
1133 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1134 (REWRITE_WITH `EL 3
\r
1135 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
1136 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
1137 = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);
\r
1138 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1139 (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);
\r
1140 (ABBREV_TAC `j = inverse (p:num->num) 3`);
\r
1141 (NEW_GOAL `(p:num->num) j = 3`);
\r
1142 (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);
\r
1143 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1144 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1145 (ASM_REWRITE_TAC[]);
\r
1146 (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);
\r
1147 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1148 (EXPAND_TAC "p'");
\r
1154 (ASM_MESON_TAC[]);
\r
1158 (ASM_MESON_TAC[]);
\r
1162 (ASM_MESON_TAC[]);
\r
1166 (ASM_MESON_TAC[]);
\r
1167 (ASM_MESON_TAC[]);
\r
1169 (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);
\r
1170 (ASM_REWRITE_TAC[left_action_list;
\r
1171 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1172 (REWRITE_WITH `EL 0
\r
1173 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
1174 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
1175 = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);
\r
1176 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1177 (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);
\r
1178 (ABBREV_TAC `j = inverse (p:num->num) 0`);
\r
1179 (NEW_GOAL `(p:num->num) j = 0`);
\r
1180 (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);
\r
1181 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1182 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1183 (ASM_REWRITE_TAC[]);
\r
1184 (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);
\r
1185 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1186 (EXPAND_TAC "p'");
\r
1191 (ASM_MESON_TAC[]);
\r
1193 (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);
\r
1194 (ASM_REWRITE_TAC[left_action_list;
\r
1195 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1196 (REWRITE_WITH `EL 1
\r
1197 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
1198 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
1199 = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);
\r
1200 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1201 (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);
\r
1202 (ABBREV_TAC `j = inverse (p:num->num) 1`);
\r
1203 (NEW_GOAL `(p:num->num) j = 1`);
\r
1204 (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);
\r
1205 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1206 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1207 (ASM_REWRITE_TAC[]);
\r
1208 (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);
\r
1209 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1210 (EXPAND_TAC "p'");
\r
1214 (ASM_MESON_TAC[]);
\r
1219 (ASM_MESON_TAC[]);
\r
1222 (* ======================================================================= *)
\r
1226 (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ;
\r
1227 ASSUME `x': (real^3->bool)#(real^3->bool)#(num->num)#(real^3)list =
\r
1229 (REPEAT STRIP_TAC);
\r
1230 (REWRITE_TAC[ASSUME `e':real^3->bool = e''''`]);
\r
1231 (REWRITE_TAC[ASSUME `e'':real^3->bool = e'''`]);
\r
1232 (REWRITE_TAC[FUN_EQ_THM]);
\r
1234 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
\r
1235 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1240 (ASM_MESON_TAC[]);
\r
1242 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
\r
1243 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1247 (ASM_MESON_TAC[]);
\r
1252 (ASM_MESON_TAC[]);
\r
1254 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
\r
1255 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1259 (ASM_MESON_TAC[]);
\r
1263 (ASM_MESON_TAC[]);
\r
1268 (ASM_MESON_TAC[]);
\r
1270 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
\r
1271 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1275 (ASM_MESON_TAC[]);
\r
1279 (ASM_MESON_TAC[]);
\r
1283 (ASM_MESON_TAC[]);
\r
1288 (ASM_MESON_TAC[]);
\r
1290 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
\r
1291 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1295 (ASM_MESON_TAC[]);
\r
1299 (ASM_MESON_TAC[]);
\r
1303 (ASM_MESON_TAC[]);
\r
1307 (ASM_MESON_TAC[]);
\r
1310 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
\r
1311 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1312 (REPEAT STRIP_TAC);
\r
1313 (ABBREV_TAC `s = (p:num->num) u`);
\r
1314 (NEW_GOAL `(p:num->num) s = s`);
\r
1315 (FIRST_ASSUM MATCH_MP_TAC);
\r
1316 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
1317 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
\r
1318 (ASM_REWRITE_TAC[]);
\r
1319 (UP_ASM_TAC THEN STRIP_TAC);
\r
1320 (NEW_GOAL `s = x'':num`);
\r
1321 (FIRST_ASSUM MATCH_MP_TAC);
\r
1322 (ASM_REWRITE_TAC[]);
\r
1323 (NEW_GOAL `u = x'':num`);
\r
1324 (FIRST_ASSUM MATCH_MP_TAC);
\r
1325 (ASM_REWRITE_TAC[]);
\r
1326 (ASM_REWRITE_TAC[]);
\r
1328 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
\r
1329 (REPEAT STRIP_TAC);
\r
1330 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1331 (NEW_GOAL `(p':num->num) u = 2`);
\r
1332 (FIRST_ASSUM MATCH_MP_TAC);
\r
1333 (ASM_REWRITE_TAC[]);
\r
1336 (ASM_MESON_TAC[]);
\r
1337 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1338 (NEW_GOAL `(p':num->num) u = 3`);
\r
1339 (FIRST_ASSUM MATCH_MP_TAC);
\r
1340 (ASM_REWRITE_TAC[]);
\r
1343 (ASM_MESON_TAC[]);
\r
1344 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1345 (NEW_GOAL `(p':num->num) u = 1`);
\r
1346 (FIRST_ASSUM MATCH_MP_TAC);
\r
1347 (ASM_REWRITE_TAC[]);
\r
1350 (ASM_MESON_TAC[]);
\r
1351 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1352 (NEW_GOAL `(p':num->num) u = u`);
\r
1353 (FIRST_ASSUM MATCH_MP_TAC);
\r
1354 (ASM_REWRITE_TAC[]);
\r
1355 (NEW_GOAL `(p:num->num) u = u`);
\r
1356 (FIRST_ASSUM MATCH_MP_TAC);
\r
1357 (ASM_REWRITE_TAC[]);
\r
1360 (ASM_MESON_TAC[]);
\r
1363 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
\r
1364 (REPEAT STRIP_TAC);
\r
1365 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1366 (NEW_GOAL `(p':num->num) u = 2`);
\r
1367 (FIRST_ASSUM MATCH_MP_TAC);
\r
1368 (ASM_REWRITE_TAC[]);
\r
1371 (ASM_MESON_TAC[]);
\r
1372 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1373 (NEW_GOAL `(p':num->num) u = 3`);
\r
1374 (FIRST_ASSUM MATCH_MP_TAC);
\r
1375 (ASM_REWRITE_TAC[]);
\r
1378 (ASM_MESON_TAC[]);
\r
1379 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1380 (NEW_GOAL `(p':num->num) u = 0`);
\r
1381 (FIRST_ASSUM MATCH_MP_TAC);
\r
1382 (ASM_REWRITE_TAC[]);
\r
1385 (ASM_MESON_TAC[]);
\r
1386 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1387 (NEW_GOAL `(p':num->num) u = u`);
\r
1388 (FIRST_ASSUM MATCH_MP_TAC);
\r
1389 (ASM_REWRITE_TAC[]);
\r
1390 (NEW_GOAL `(p:num->num) u = u`);
\r
1391 (FIRST_ASSUM MATCH_MP_TAC);
\r
1392 (ASM_REWRITE_TAC[]);
\r
1395 (ASM_MESON_TAC[]);
\r
1398 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
\r
1399 (REPEAT STRIP_TAC);
\r
1400 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1401 (NEW_GOAL `(p':num->num) u = 3`);
\r
1402 (FIRST_ASSUM MATCH_MP_TAC);
\r
1403 (ASM_REWRITE_TAC[]);
\r
1406 (ASM_MESON_TAC[]);
\r
1407 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1408 (NEW_GOAL `(p':num->num) u = 0`);
\r
1409 (FIRST_ASSUM MATCH_MP_TAC);
\r
1410 (ASM_REWRITE_TAC[]);
\r
1413 (ASM_MESON_TAC[]);
\r
1414 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1415 (NEW_GOAL `(p':num->num) u = 1`);
\r
1416 (FIRST_ASSUM MATCH_MP_TAC);
\r
1417 (ASM_REWRITE_TAC[]);
\r
1420 (ASM_MESON_TAC[]);
\r
1421 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1422 (NEW_GOAL `(p':num->num) u = u`);
\r
1423 (FIRST_ASSUM MATCH_MP_TAC);
\r
1424 (ASM_REWRITE_TAC[]);
\r
1425 (NEW_GOAL `(p:num->num) u = u`);
\r
1426 (FIRST_ASSUM MATCH_MP_TAC);
\r
1427 (ASM_REWRITE_TAC[]);
\r
1430 (ASM_MESON_TAC[]);
\r
1433 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
\r
1434 (REPEAT STRIP_TAC);
\r
1435 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1436 (NEW_GOAL `(p':num->num) u = 2`);
\r
1437 (FIRST_ASSUM MATCH_MP_TAC);
\r
1438 (ASM_REWRITE_TAC[]);
\r
1441 (ASM_MESON_TAC[]);
\r
1442 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1443 (NEW_GOAL `(p':num->num) u = 0`);
\r
1444 (FIRST_ASSUM MATCH_MP_TAC);
\r
1445 (ASM_REWRITE_TAC[]);
\r
1448 (ASM_MESON_TAC[]);
\r
1449 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1450 (NEW_GOAL `(p':num->num) u = 1`);
\r
1451 (FIRST_ASSUM MATCH_MP_TAC);
\r
1452 (ASM_REWRITE_TAC[]);
\r
1455 (ASM_MESON_TAC[]);
\r
1456 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1457 (NEW_GOAL `(p':num->num) u = u`);
\r
1458 (FIRST_ASSUM MATCH_MP_TAC);
\r
1459 (ASM_REWRITE_TAC[]);
\r
1460 (NEW_GOAL `(p:num->num) u = u`);
\r
1461 (FIRST_ASSUM MATCH_MP_TAC);
\r
1462 (ASM_REWRITE_TAC[]);
\r
1465 (ASM_MESON_TAC[]);
\r
1468 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
\r
1469 (REPEAT STRIP_TAC);
\r
1470 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1471 (NEW_GOAL `(p':num->num) u = 2`);
\r
1472 (FIRST_ASSUM MATCH_MP_TAC);
\r
1473 (ASM_REWRITE_TAC[]);
\r
1476 (ASM_MESON_TAC[]);
\r
1477 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1478 (NEW_GOAL `(p':num->num) u = 3`);
\r
1479 (FIRST_ASSUM MATCH_MP_TAC);
\r
1480 (ASM_REWRITE_TAC[]);
\r
1483 (ASM_MESON_TAC[]);
\r
1484 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1485 (NEW_GOAL `(p':num->num) u = 0`);
\r
1486 (FIRST_ASSUM MATCH_MP_TAC);
\r
1487 (ASM_REWRITE_TAC[]);
\r
1490 (ASM_MESON_TAC[]);
\r
1491 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1492 (NEW_GOAL `(p':num->num) u = 1`);
\r
1493 (FIRST_ASSUM MATCH_MP_TAC);
\r
1494 (ASM_REWRITE_TAC[]);
\r
1497 (ASM_MESON_TAC[]);
\r
1502 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1504 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1506 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1508 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1509 (NEW_GOAL `(p:num->num) x'' > 3`);
\r
1510 (FIRST_ASSUM MATCH_MP_TAC);
\r
1512 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1514 (* ------------------------------------------------------------------------- *)
\r
1516 (EXPAND_TAC "vl'");
\r
1517 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1518 (REWRITE_TAC[ASSUME `vl = left_action_list p [v0; v1; v2; v3:real^3]`; left_action_list; TABLE_4; LENGTH;EL; HD;TL;
\r
1519 ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
\r
1520 (* ======================================================================= *)
\r
1522 (EXISTS_TAC `e'':real^3->bool` THEN EXISTS_TAC `e':real^3->bool`);
\r
1523 (ABBREV_TAC `p' = (\i. if p i = 0
\r
1527 else if p i = 2 then 0 else if p i = 3 then 1 else i)`);
\r
1528 (EXISTS_TAC `p':num->num`);
\r
1529 (EXISTS_TAC `[EL 2 (vl:(real^3)list); EL 3 vl; EL 0 vl; EL 1 vl]`);
\r
1531 `{EL 2 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl],
\r
1532 EL 3 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]}
\r
1533 = {EL 0 vl, EL 1 (vl:(real^3)list)}`);
\r
1534 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1536 `{EL 0 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl],
\r
1537 EL 1 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl]}
\r
1538 = {EL 2 vl, EL 3 (vl:(real^3)list)}`);
\r
1539 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1540 (REWRITE_TAC[ASSUME `e'' = x:real^3->bool`; ASSUME `e' = y:real^3->bool`;
\r
1541 ASSUME `y:real^3->bool = {EL 0 vl, EL 1 vl}`;
\r
1542 ASSUME `x:real^3->bool = {EL 2 vl, EL 3 vl}`;left_action_list;
\r
1543 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1545 (NEW_GOAL `!u:num. p u = 0 ==> p' u = 2`);
\r
1546 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1551 (ASM_MESON_TAC[]);
\r
1553 (NEW_GOAL `!u:num. p u = 1 ==> p' u = 3`);
\r
1554 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1558 (ASM_MESON_TAC[]);
\r
1563 (ASM_MESON_TAC[]);
\r
1565 (NEW_GOAL `!u:num. p u = 2 ==> p' u = 0`);
\r
1566 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1570 (ASM_MESON_TAC[]);
\r
1574 (ASM_MESON_TAC[]);
\r
1579 (ASM_MESON_TAC[]);
\r
1581 (NEW_GOAL `!u:num. p u = 3 ==> p' u = 1`);
\r
1582 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1586 (ASM_MESON_TAC[]);
\r
1590 (ASM_MESON_TAC[]);
\r
1594 (ASM_MESON_TAC[]);
\r
1599 (ASM_MESON_TAC[]);
\r
1601 (NEW_GOAL `!u:num. p u > 3 ==> p' u = u`);
\r
1602 (REPEAT STRIP_TAC THEN EXPAND_TAC "p'");
\r
1606 (ASM_MESON_TAC[]);
\r
1610 (ASM_MESON_TAC[]);
\r
1614 (ASM_MESON_TAC[]);
\r
1618 (ASM_MESON_TAC[]);
\r
1621 (NEW_GOAL `!u:num. p u > 3 ==> p u = u`);
\r
1622 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1623 (REPEAT STRIP_TAC);
\r
1624 (ABBREV_TAC `s = (p:num->num) u`);
\r
1625 (NEW_GOAL `(p:num->num) s = s`);
\r
1626 (FIRST_ASSUM MATCH_MP_TAC);
\r
1627 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
1628 (NEW_GOAL `?x. (p:num->num) x = s /\ (!y'. p y' = s ==> y' = x)`);
\r
1629 (ASM_REWRITE_TAC[]);
\r
1630 (UP_ASM_TAC THEN STRIP_TAC);
\r
1631 (NEW_GOAL `s = x''':num`);
\r
1632 (FIRST_ASSUM MATCH_MP_TAC);
\r
1633 (ASM_REWRITE_TAC[]);
\r
1634 (NEW_GOAL `u = x''':num`);
\r
1635 (FIRST_ASSUM MATCH_MP_TAC);
\r
1636 (ASM_REWRITE_TAC[]);
\r
1637 (ASM_REWRITE_TAC[]);
\r
1639 (NEW_GOAL `!u:num. p' u = 0 ==> p u = 2`);
\r
1640 (REPEAT STRIP_TAC);
\r
1641 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1642 (NEW_GOAL `(p':num->num) u = 2`);
\r
1643 (FIRST_ASSUM MATCH_MP_TAC);
\r
1644 (ASM_REWRITE_TAC[]);
\r
1647 (ASM_MESON_TAC[]);
\r
1648 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1649 (NEW_GOAL `(p':num->num) u = 3`);
\r
1650 (FIRST_ASSUM MATCH_MP_TAC);
\r
1651 (ASM_REWRITE_TAC[]);
\r
1654 (ASM_MESON_TAC[]);
\r
1655 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1656 (NEW_GOAL `(p':num->num) u = 1`);
\r
1657 (FIRST_ASSUM MATCH_MP_TAC);
\r
1658 (ASM_REWRITE_TAC[]);
\r
1661 (ASM_MESON_TAC[]);
\r
1662 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1663 (NEW_GOAL `(p':num->num) u = u`);
\r
1664 (FIRST_ASSUM MATCH_MP_TAC);
\r
1665 (ASM_REWRITE_TAC[]);
\r
1666 (NEW_GOAL `(p:num->num) u = u`);
\r
1667 (FIRST_ASSUM MATCH_MP_TAC);
\r
1668 (ASM_REWRITE_TAC[]);
\r
1671 (ASM_MESON_TAC[]);
\r
1674 (NEW_GOAL `!u:num. p' u = 1 ==> p u = 3`);
\r
1675 (REPEAT STRIP_TAC);
\r
1676 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1677 (NEW_GOAL `(p':num->num) u = 2`);
\r
1678 (FIRST_ASSUM MATCH_MP_TAC);
\r
1679 (ASM_REWRITE_TAC[]);
\r
1682 (ASM_MESON_TAC[]);
\r
1683 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1684 (NEW_GOAL `(p':num->num) u = 3`);
\r
1685 (FIRST_ASSUM MATCH_MP_TAC);
\r
1686 (ASM_REWRITE_TAC[]);
\r
1689 (ASM_MESON_TAC[]);
\r
1690 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1691 (NEW_GOAL `(p':num->num) u = 0`);
\r
1692 (FIRST_ASSUM MATCH_MP_TAC);
\r
1693 (ASM_REWRITE_TAC[]);
\r
1696 (ASM_MESON_TAC[]);
\r
1697 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1698 (NEW_GOAL `(p':num->num) u = u`);
\r
1699 (FIRST_ASSUM MATCH_MP_TAC);
\r
1700 (ASM_REWRITE_TAC[]);
\r
1701 (NEW_GOAL `(p:num->num) u = u`);
\r
1702 (FIRST_ASSUM MATCH_MP_TAC);
\r
1703 (ASM_REWRITE_TAC[]);
\r
1706 (ASM_MESON_TAC[]);
\r
1709 (NEW_GOAL `!u:num. p' u = 2 ==> p u = 0`);
\r
1710 (REPEAT STRIP_TAC);
\r
1711 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1712 (NEW_GOAL `(p':num->num) u = 3`);
\r
1713 (FIRST_ASSUM MATCH_MP_TAC);
\r
1714 (ASM_REWRITE_TAC[]);
\r
1717 (ASM_MESON_TAC[]);
\r
1718 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1719 (NEW_GOAL `(p':num->num) u = 0`);
\r
1720 (FIRST_ASSUM MATCH_MP_TAC);
\r
1721 (ASM_REWRITE_TAC[]);
\r
1724 (ASM_MESON_TAC[]);
\r
1725 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1726 (NEW_GOAL `(p':num->num) u = 1`);
\r
1727 (FIRST_ASSUM MATCH_MP_TAC);
\r
1728 (ASM_REWRITE_TAC[]);
\r
1731 (ASM_MESON_TAC[]);
\r
1732 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1733 (NEW_GOAL `(p':num->num) u = u`);
\r
1734 (FIRST_ASSUM MATCH_MP_TAC);
\r
1735 (ASM_REWRITE_TAC[]);
\r
1736 (NEW_GOAL `(p:num->num) u = u`);
\r
1737 (FIRST_ASSUM MATCH_MP_TAC);
\r
1738 (ASM_REWRITE_TAC[]);
\r
1741 (ASM_MESON_TAC[]);
\r
1744 (NEW_GOAL `!u:num. p' u = 3 ==> p u = 1`);
\r
1745 (REPEAT STRIP_TAC);
\r
1746 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1747 (NEW_GOAL `(p':num->num) u = 2`);
\r
1748 (FIRST_ASSUM MATCH_MP_TAC);
\r
1749 (ASM_REWRITE_TAC[]);
\r
1752 (ASM_MESON_TAC[]);
\r
1753 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1754 (NEW_GOAL `(p':num->num) u = 0`);
\r
1755 (FIRST_ASSUM MATCH_MP_TAC);
\r
1756 (ASM_REWRITE_TAC[]);
\r
1759 (ASM_MESON_TAC[]);
\r
1760 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1761 (NEW_GOAL `(p':num->num) u = 1`);
\r
1762 (FIRST_ASSUM MATCH_MP_TAC);
\r
1763 (ASM_REWRITE_TAC[]);
\r
1766 (ASM_MESON_TAC[]);
\r
1767 (ASM_CASES_TAC `(p:num->num) u > 3`);
\r
1768 (NEW_GOAL `(p':num->num) u = u`);
\r
1769 (FIRST_ASSUM MATCH_MP_TAC);
\r
1770 (ASM_REWRITE_TAC[]);
\r
1771 (NEW_GOAL `(p:num->num) u = u`);
\r
1772 (FIRST_ASSUM MATCH_MP_TAC);
\r
1773 (ASM_REWRITE_TAC[]);
\r
1776 (ASM_MESON_TAC[]);
\r
1779 (NEW_GOAL `!u:num. p' u > 3 ==> p u > 3`);
\r
1780 (REPEAT STRIP_TAC);
\r
1781 (ASM_CASES_TAC `(p:num->num) u = 0`);
\r
1782 (NEW_GOAL `(p':num->num) u = 2`);
\r
1783 (FIRST_ASSUM MATCH_MP_TAC);
\r
1784 (ASM_REWRITE_TAC[]);
\r
1787 (ASM_MESON_TAC[]);
\r
1788 (ASM_CASES_TAC `(p:num->num) u = 1`);
\r
1789 (NEW_GOAL `(p':num->num) u = 3`);
\r
1790 (FIRST_ASSUM MATCH_MP_TAC);
\r
1791 (ASM_REWRITE_TAC[]);
\r
1794 (ASM_MESON_TAC[]);
\r
1795 (ASM_CASES_TAC `(p:num->num) u = 2`);
\r
1796 (NEW_GOAL `(p':num->num) u = 0`);
\r
1797 (FIRST_ASSUM MATCH_MP_TAC);
\r
1798 (ASM_REWRITE_TAC[]);
\r
1801 (ASM_MESON_TAC[]);
\r
1802 (ASM_CASES_TAC `(p:num->num) u = 3`);
\r
1803 (NEW_GOAL `(p':num->num) u = 1`);
\r
1804 (FIRST_ASSUM MATCH_MP_TAC);
\r
1805 (ASM_REWRITE_TAC[]);
\r
1808 (ASM_MESON_TAC[]);
\r
1811 (* ------------------------------------------------------------------------- *)
\r
1812 (* begin to prove that p' permutes 0..3 *)
\r
1814 (NEW_GOAL `p' permutes 0..3`);
\r
1815 (REWRITE_TAC[permutes]);
\r
1816 (REPEAT STRIP_TAC);
\r
1817 (NEW_GOAL `x''' > 3`);
\r
1818 (UP_ASM_TAC THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
1819 (EXPAND_TAC "p'");
\r
1820 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC);
\r
1822 (NEW_GOAL `(p:num->num) x''' = x'''`);
\r
1827 (ASM_MESON_TAC[]);
\r
1831 (ASM_MESON_TAC[]);
\r
1835 (ASM_MESON_TAC[]);
\r
1839 (ASM_MESON_TAC[]);
\r
1842 (REWRITE_TAC[EXISTS_UNIQUE] THEN REPEAT STRIP_TAC);
\r
1844 (ASM_CASES_TAC `y' = 0`);
\r
1845 (NEW_GOAL `?z. (p:num->num) z = 2`);
\r
1846 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1847 (UP_ASM_TAC THEN STRIP_TAC);
\r
1848 (EXISTS_TAC `z:num`);
\r
1849 (ASM_REWRITE_TAC[]);
\r
1850 (REPEAT STRIP_TAC);
\r
1851 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1852 (NEW_GOAL `(p:num->num) y'' = 2`);
\r
1853 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1854 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1855 (REPEAT STRIP_TAC);
\r
1856 (NEW_GOAL `?s:num. p s = 2 /\ (!y'. p y' = 2 ==> y' = s)`);
\r
1857 (ASM_REWRITE_TAC[]);
\r
1858 (UP_ASM_TAC THEN STRIP_TAC);
\r
1859 (REWRITE_WITH `y'' = s:num`);
\r
1860 (FIRST_ASSUM MATCH_MP_TAC);
\r
1861 (ASM_REWRITE_TAC[]);
\r
1862 (REWRITE_WITH `z = s:num`);
\r
1863 (FIRST_ASSUM MATCH_MP_TAC);
\r
1864 (ASM_REWRITE_TAC[]);
\r
1866 (ASM_CASES_TAC `y' = 1`);
\r
1867 (NEW_GOAL `?z. (p:num->num) z = 3`);
\r
1868 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1869 (UP_ASM_TAC THEN STRIP_TAC);
\r
1870 (EXISTS_TAC `z:num`);
\r
1871 (ASM_REWRITE_TAC[]);
\r
1872 (REPEAT STRIP_TAC);
\r
1873 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1874 (NEW_GOAL `(p:num->num) y'' = 3`);
\r
1875 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1876 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1877 (REPEAT STRIP_TAC);
\r
1878 (NEW_GOAL `?s:num. p s = 3 /\ (!y'. p y' = 3 ==> y' = s)`);
\r
1879 (ASM_REWRITE_TAC[]);
\r
1880 (UP_ASM_TAC THEN STRIP_TAC);
\r
1881 (REWRITE_WITH `y'' = s:num`);
\r
1882 (FIRST_ASSUM MATCH_MP_TAC);
\r
1883 (ASM_REWRITE_TAC[]);
\r
1884 (REWRITE_WITH `z = s:num`);
\r
1885 (FIRST_ASSUM MATCH_MP_TAC);
\r
1886 (ASM_REWRITE_TAC[]);
\r
1888 (ASM_CASES_TAC `y' = 2`);
\r
1889 (NEW_GOAL `?z. (p:num->num) z = 0`);
\r
1890 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1891 (UP_ASM_TAC THEN STRIP_TAC);
\r
1892 (EXISTS_TAC `z:num`);
\r
1893 (ASM_REWRITE_TAC[]);
\r
1894 (REPEAT STRIP_TAC);
\r
1895 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1896 (NEW_GOAL `(p:num->num) y'' = 0`);
\r
1897 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1898 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1899 (REPEAT STRIP_TAC);
\r
1900 (NEW_GOAL `?s:num. p s = 0 /\ (!y'. p y' = 0 ==> y' = s)`);
\r
1901 (ASM_REWRITE_TAC[]);
\r
1902 (UP_ASM_TAC THEN STRIP_TAC);
\r
1903 (REWRITE_WITH `y'' = s:num`);
\r
1904 (FIRST_ASSUM MATCH_MP_TAC);
\r
1905 (ASM_REWRITE_TAC[]);
\r
1906 (REWRITE_WITH `z = s:num`);
\r
1907 (FIRST_ASSUM MATCH_MP_TAC);
\r
1908 (ASM_REWRITE_TAC[]);
\r
1910 (ASM_CASES_TAC `y' = 3`);
\r
1911 (NEW_GOAL `?z. (p:num->num) z = 1`);
\r
1912 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1913 (UP_ASM_TAC THEN STRIP_TAC);
\r
1914 (EXISTS_TAC `z:num`);
\r
1915 (ASM_REWRITE_TAC[]);
\r
1916 (REPEAT STRIP_TAC);
\r
1917 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1918 (NEW_GOAL `(p:num->num) y'' = 1`);
\r
1919 (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);
\r
1920 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1921 (REPEAT STRIP_TAC);
\r
1922 (NEW_GOAL `?s:num. p s = 1 /\ (!y'. p y' = 1 ==> y' = s)`);
\r
1923 (ASM_REWRITE_TAC[]);
\r
1924 (UP_ASM_TAC THEN STRIP_TAC);
\r
1925 (REWRITE_WITH `y'' = s:num`);
\r
1926 (FIRST_ASSUM MATCH_MP_TAC);
\r
1927 (ASM_REWRITE_TAC[]);
\r
1928 (REWRITE_WITH `z = s:num`);
\r
1929 (FIRST_ASSUM MATCH_MP_TAC);
\r
1930 (ASM_REWRITE_TAC[]);
\r
1932 (NEW_GOAL `y' > 3`);
\r
1934 (NEW_GOAL `?z. (p:num->num) z = y'`);
\r
1935 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);
\r
1936 (UP_ASM_TAC THEN STRIP_TAC);
\r
1937 (EXISTS_TAC `z:num`);
\r
1938 (ASM_REWRITE_TAC[]);
\r
1939 (REPEAT STRIP_TAC);
\r
1940 (NEW_GOAL `(p:num->num) z = z`);
\r
1941 (FIRST_ASSUM MATCH_MP_TAC);
\r
1943 (NEW_GOAL `(p':num->num) z = z`);
\r
1944 (FIRST_ASSUM MATCH_MP_TAC);
\r
1948 (NEW_GOAL `(p:num->num) z = z`);
\r
1949 (FIRST_ASSUM MATCH_MP_TAC);
\r
1951 (NEW_GOAL `(p':num->num) z = z`);
\r
1952 (FIRST_ASSUM MATCH_MP_TAC);
\r
1954 (UNDISCH_TAC `p permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
1955 (REPEAT STRIP_TAC);
\r
1956 (NEW_GOAL `(p:num->num) y'' > 3`);
\r
1957 (FIRST_ASSUM MATCH_MP_TAC);
\r
1958 (ASM_REWRITE_TAC[]);
\r
1960 (NEW_GOAL `(p:num->num) y'' = y''`);
\r
1961 (MATCH_MP_TAC (ASSUME `!u:num. p u > 3 ==> p u = u`));
\r
1962 (ASM_REWRITE_TAC[]);
\r
1963 (NEW_GOAL `(p':num->num) y'' = y''`);
\r
1964 (FIRST_ASSUM MATCH_MP_TAC);
\r
1965 (ASM_REWRITE_TAC[]);
\r
1967 (NEW_GOAL `?s:num. p s = (y':num) /\ (!z'. p z' = y' ==> z' = s)`);
\r
1968 (ASM_REWRITE_TAC[]);
\r
1969 (UP_ASM_TAC THEN STRIP_TAC);
\r
1970 (REWRITE_WITH `y'' = s:num`);
\r
1971 (FIRST_ASSUM MATCH_MP_TAC);
\r
1972 (ASM_MESON_TAC[]);
\r
1973 (REWRITE_WITH `z = s:num`);
\r
1974 (FIRST_ASSUM MATCH_MP_TAC);
\r
1975 (ASM_MESON_TAC[]);
\r
1978 (* finish proving that p' permutes 0..3 *)
\r
1980 (REWRITE_TAC[ASSUME `p' permutes 0..3`]);
\r
1982 (* --------------------------------------------------------------------- *)
\r
1984 (REWRITE_WITH `EL (inverse p' 0) [v0; v1; v2; v3:real^3] = EL 2 vl`);
\r
1985 (ASM_REWRITE_TAC[left_action_list;
\r
1986 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
1987 (REWRITE_WITH `EL 2
\r
1988 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
1989 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
1990 = EL (inverse p 2) [v0; v1; v2; v3:real^3]`);
\r
1991 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
1992 (REWRITE_WITH `inverse p' 0 = inverse (p:num->num) 2`);
\r
1993 (ABBREV_TAC `j = inverse (p:num->num) 2`);
\r
1994 (NEW_GOAL `(p:num->num) j = 2`);
\r
1995 (REWRITE_WITH `(p j = 2) <=> inverse (p:num->num) 2 = j`);
\r
1996 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
1997 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
1998 (ASM_REWRITE_TAC[]);
\r
1999 (REWRITE_WITH `inverse (p':num->num) 0 = j <=> p' j = 0`);
\r
2000 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2001 (EXPAND_TAC "p'");
\r
2005 (ASM_MESON_TAC[]);
\r
2009 (ASM_MESON_TAC[]);
\r
2013 (ASM_MESON_TAC[]);
\r
2014 (ASM_MESON_TAC[]);
\r
2017 (REWRITE_WITH `EL (inverse p' 1) [v0; v1; v2; v3:real^3] = EL 3 vl`);
\r
2018 (ASM_REWRITE_TAC[left_action_list;
\r
2019 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
2020 (REWRITE_WITH `EL 3
\r
2021 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
2022 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
2023 = EL (inverse p 3) [v0; v1; v2; v3:real^3]`);
\r
2024 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2025 (REWRITE_WITH `inverse p' 1 = inverse (p:num->num) 3`);
\r
2026 (ABBREV_TAC `j = inverse (p:num->num) 3`);
\r
2027 (NEW_GOAL `(p:num->num) j = 3`);
\r
2028 (REWRITE_WITH `(p j = 3) <=> inverse (p:num->num) 3 = j`);
\r
2029 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2030 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2031 (ASM_REWRITE_TAC[]);
\r
2032 (REWRITE_WITH `inverse (p':num->num) 1 = j <=> p' j = 1`);
\r
2033 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2034 (EXPAND_TAC "p'");
\r
2038 (ASM_MESON_TAC[]);
\r
2042 (ASM_MESON_TAC[]);
\r
2046 (ASM_MESON_TAC[]);
\r
2050 (ASM_MESON_TAC[]);
\r
2051 (ASM_MESON_TAC[]);
\r
2053 (REWRITE_WITH `EL (inverse p' 2) [v0; v1; v2; v3:real^3] = EL 0 vl`);
\r
2054 (ASM_REWRITE_TAC[left_action_list;
\r
2055 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
2056 (REWRITE_WITH `EL 0
\r
2057 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
2058 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
2059 = EL (inverse p 0) [v0; v1; v2; v3:real^3]`);
\r
2060 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2061 (REWRITE_WITH `inverse p' 2 = inverse (p:num->num) 0`);
\r
2062 (ABBREV_TAC `j = inverse (p:num->num) 0`);
\r
2063 (NEW_GOAL `(p:num->num) j = 0`);
\r
2064 (REWRITE_WITH `(p j = 0) <=> inverse (p:num->num) 0 = j`);
\r
2065 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2066 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2067 (ASM_REWRITE_TAC[]);
\r
2068 (REWRITE_WITH `inverse (p':num->num) 2 = j <=> p' j = 2`);
\r
2069 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2070 (EXPAND_TAC "p'");
\r
2075 (ASM_MESON_TAC[]);
\r
2078 (REWRITE_WITH `EL (inverse p' 3) [v0; v1; v2; v3:real^3] = EL 1 vl`);
\r
2079 (ASM_REWRITE_TAC[left_action_list;
\r
2080 LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`; TABLE_4]);
\r
2081 (REWRITE_WITH `EL 1
\r
2082 [EL (inverse p 0) [v0; v1; v2; v3]; EL (inverse p 1) [v0; v1; v2; v3];
\r
2083 EL (inverse p 2) [v0; v1; v2; v3]; EL (inverse p 3) [v0; v1; v2; v3]]
\r
2084 = EL (inverse p 1) [v0; v1; v2; v3:real^3]`);
\r
2085 (REWRITE_TAC[EL; HD;TL;ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2086 (REWRITE_WITH `inverse p' 3 = inverse (p:num->num) 1`);
\r
2087 (ABBREV_TAC `j = inverse (p:num->num) 1`);
\r
2088 (NEW_GOAL `(p:num->num) j = 1`);
\r
2089 (REWRITE_WITH `(p j = 1) <=> inverse (p:num->num) 1 = j`);
\r
2090 (ONCE_REWRITE_TAC[EQ_SYM_EQ]);
\r
2091 (UNDISCH_TAC `p permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2092 (ASM_REWRITE_TAC[]);
\r
2093 (REWRITE_WITH `inverse (p':num->num) 3 = j <=> p' j = 3`);
\r
2094 (UNDISCH_TAC `p' permutes 0..3` THEN MESON_TAC[PERMUTES_INVERSE_EQ]);
\r
2095 (EXPAND_TAC "p'");
\r
2099 (ASM_MESON_TAC[]);
\r
2104 (ASM_MESON_TAC[]);
\r
2107 (* ======================================================================= *)
\r
2109 (ONCE_REWRITE_TAC[ASSUME
\r
2110 `x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list
\r
2111 = g (x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`]);
\r
2112 (REWRITE_TAC[ASSUME
\r
2113 `x'':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list = e',e'',p,vl`]
\r
2114 THEN EXPAND_TAC "g");
\r
2116 (REWRITE_TAC[PAIR_EQ]);
\r
2117 (EXPAND_TAC "p'" THEN REWRITE_TAC[]);
\r
2118 (ASM_REWRITE_TAC[]);
\r
2120 (* --------------------------------------------------- *)
\r
2121 (* It is left to prove only 3 subgoals *)
\r
2124 (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
\r
2125 (REWRITE_TAC[FUN_EQ_THM]);
\r
2127 (NEW_GOAL `?e1 e2 p1 vl1.
\r
2128 x' = (e1:real^3->bool,e2:real^3->bool,p1:num->num, vl1:(real^3)list)`);
\r
2130 (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)`);
\r
2131 (EXISTS_TAC `FST (SND
\r
2132 (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list))`);
\r
2133 (EXISTS_TAC `FST (SND (SND
\r
2134 (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
\r
2135 (EXISTS_TAC `SND (SND (SND
\r
2136 (x':(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list)))`);
\r
2137 (REWRITE_TAC[PAIR]);
\r
2138 (UP_ASM_TAC THEN STRIP_TAC);
\r
2139 (ASM_REWRITE_TAC[]);
\r
2141 `(\x. let e',e'',p,vl = x in
\r
2142 e'', e', (\i. if p i = 0 then 2
\r
2143 else if p i = 1 then 3
\r
2144 else if p i = 2 then 0
\r
2145 else if p i = 3 then 1 else i),
\r
2146 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])
\r
2147 = (\(e':real^3->bool,e'':real^3->bool,p:num->num,vl:(real^3)list).
\r
2148 e'', e', (\i. if p i = 0 then 2
\r
2149 else if p i = 1 then 3
\r
2150 else if p i = 2 then 0
\r
2151 else if p i = 3 then 1 else i),
\r
2152 [EL 2 vl; EL 3 vl; EL 0 vl; EL 1 vl])`);
\r
2153 (REWRITE_TAC[FUN_EQ_THM]);
\r
2156 (REWRITE_TAC[BETA_THM]);
\r
2157 (REWRITE_TAC[o_THM]);
\r
2159 `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 2 (vl1:(real^3)list) /\
\r
2160 EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 3 (vl1:(real^3)list) /\
\r
2161 EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 0 (vl1:(real^3)list) /\
\r
2162 EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1] = EL 1 (vl1:(real^3)list)`);
\r
2163 (REWRITE_TAC[EL;HD;TL; LENGTH; ARITH_RULE `1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2165 (MATCH_MP_TAC SUM_IMAGE);
\r
2166 (EXPAND_TAC "S1" THEN EXPAND_TAC "S2");
\r
2167 (ONCE_REWRITE_TAC[IN]);
\r
2168 (REWRITE_TAC[IN_ELIM_THM]);
\r
2170 (REPEAT STRIP_TAC);
\r
2172 (NEW_GOAL `(let e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1 = x' in
\r
2179 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i),
\r
2180 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 vl1]) =
\r
2181 (let f1,f2,p2,vl2 = y' in
\r
2188 else if p2 i = 2 then 0 else if p2 i = 3 then 1 else i),
\r
2189 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)])`);
\r
2190 (ASM_REWRITE_TAC[ETA_AX]);
\r
2191 (UP_ASM_TAC THEN DEL_TAC THEN REPEAT LET_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
\r
2192 REPEAT STRIP_TAC);
\r
2193 (ASM_REWRITE_TAC[]);
\r
2194 (ASM_REWRITE_TAC[]);
\r
2195 (REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC);
\r
2197 `q = (\i. if p1 i = 0
\r
2201 else if p1 i = 2 then 0 else if p1 i = 3 then 1 else i)`);
\r
2203 (NEW_GOAL `!u:num. p1 u = 0 ==> q u = 2`);
\r
2204 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
\r
2209 (ASM_MESON_TAC[]);
\r
2211 (NEW_GOAL `!u:num. p1 u = 1 ==> q u = 3`);
\r
2212 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
\r
2216 (ASM_MESON_TAC[]);
\r
2221 (ASM_MESON_TAC[]);
\r
2223 (NEW_GOAL `!u:num. p1 u = 2 ==> q u = 0`);
\r
2224 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
\r
2228 (ASM_MESON_TAC[]);
\r
2232 (ASM_MESON_TAC[]);
\r
2237 (ASM_MESON_TAC[]);
\r
2239 (NEW_GOAL `!u:num. p1 u = 3 ==> q u = 1`);
\r
2240 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
\r
2244 (ASM_MESON_TAC[]);
\r
2248 (ASM_MESON_TAC[]);
\r
2252 (ASM_MESON_TAC[]);
\r
2257 (ASM_MESON_TAC[]);
\r
2259 (NEW_GOAL `!u:num. p1 u > 3 ==> q u = u`);
\r
2260 (REPEAT STRIP_TAC THEN EXPAND_TAC "q");
\r
2264 (ASM_MESON_TAC[]);
\r
2268 (ASM_MESON_TAC[]);
\r
2272 (ASM_MESON_TAC[]);
\r
2276 (ASM_MESON_TAC[]);
\r
2279 (NEW_GOAL `!u:num. p1 u > 3 ==> p1 u = u`);
\r
2280 (NEW_GOAL `p1 permutes 0..3`);
\r
2281 (REWRITE_WITH `p1:num->num = p`);
\r
2282 (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list = e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);
\r
2284 (ASM_REWRITE_TAC[]);
\r
2285 (UNDISCH_TAC `p1 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
2286 (REPEAT STRIP_TAC);
\r
2287 (ABBREV_TAC `s = (p1:num->num) u`);
\r
2288 (NEW_GOAL `(p1:num->num) s = s`);
\r
2289 (FIRST_ASSUM MATCH_MP_TAC);
\r
2290 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
2291 (NEW_GOAL `?z. (p1:num->num) z = s /\ (!y'. p1 y' = s ==> y' = z)`);
\r
2292 (ASM_REWRITE_TAC[]);
\r
2293 (UP_ASM_TAC THEN STRIP_TAC);
\r
2294 (NEW_GOAL `s = z:num`);
\r
2295 (FIRST_ASSUM MATCH_MP_TAC);
\r
2296 (ASM_REWRITE_TAC[]);
\r
2297 (NEW_GOAL `u = z:num`);
\r
2298 (FIRST_ASSUM MATCH_MP_TAC);
\r
2299 (ASM_REWRITE_TAC[]);
\r
2300 (ASM_REWRITE_TAC[]);
\r
2302 (NEW_GOAL `!u:num. q u = 0 ==> p1 u = 2`);
\r
2303 (REPEAT STRIP_TAC);
\r
2304 (ASM_CASES_TAC `(p1:num->num) u = 0`);
\r
2305 (NEW_GOAL `(q:num->num) u = 2`);
\r
2306 (FIRST_ASSUM MATCH_MP_TAC);
\r
2307 (ASM_REWRITE_TAC[]);
\r
2310 (ASM_MESON_TAC[]);
\r
2311 (ASM_CASES_TAC `(p1:num->num) u = 1`);
\r
2312 (NEW_GOAL `(q:num->num) u = 3`);
\r
2313 (FIRST_ASSUM MATCH_MP_TAC);
\r
2314 (ASM_REWRITE_TAC[]);
\r
2317 (ASM_MESON_TAC[]);
\r
2318 (ASM_CASES_TAC `(p1:num->num) u = 3`);
\r
2319 (NEW_GOAL `(q:num->num) u = 1`);
\r
2320 (FIRST_ASSUM MATCH_MP_TAC);
\r
2321 (ASM_REWRITE_TAC[]);
\r
2324 (ASM_MESON_TAC[]);
\r
2325 (ASM_CASES_TAC `(p1:num->num) u > 3`);
\r
2326 (NEW_GOAL `(q:num->num) u = u`);
\r
2327 (FIRST_ASSUM MATCH_MP_TAC);
\r
2328 (ASM_REWRITE_TAC[]);
\r
2329 (NEW_GOAL `(p1:num->num) u = u`);
\r
2330 (FIRST_ASSUM MATCH_MP_TAC);
\r
2331 (ASM_REWRITE_TAC[]);
\r
2334 (ASM_MESON_TAC[]);
\r
2337 (NEW_GOAL `!u:num. q u = 1 ==> p1 u = 3`);
\r
2338 (REPEAT STRIP_TAC);
\r
2339 (ASM_CASES_TAC `(p1:num->num) u = 0`);
\r
2340 (NEW_GOAL `(q:num->num) u = 2`);
\r
2341 (FIRST_ASSUM MATCH_MP_TAC);
\r
2342 (ASM_REWRITE_TAC[]);
\r
2345 (ASM_MESON_TAC[]);
\r
2346 (ASM_CASES_TAC `(p1:num->num) u = 1`);
\r
2347 (NEW_GOAL `(q:num->num) u = 3`);
\r
2348 (FIRST_ASSUM MATCH_MP_TAC);
\r
2349 (ASM_REWRITE_TAC[]);
\r
2352 (ASM_MESON_TAC[]);
\r
2353 (ASM_CASES_TAC `(p1:num->num) u = 2`);
\r
2354 (NEW_GOAL `(q:num->num) u = 0`);
\r
2355 (FIRST_ASSUM MATCH_MP_TAC);
\r
2356 (ASM_REWRITE_TAC[]);
\r
2359 (ASM_MESON_TAC[]);
\r
2360 (ASM_CASES_TAC `(p1:num->num) u > 3`);
\r
2361 (NEW_GOAL `(q:num->num) u = u`);
\r
2362 (FIRST_ASSUM MATCH_MP_TAC);
\r
2363 (ASM_REWRITE_TAC[]);
\r
2364 (NEW_GOAL `(p1:num->num) u = u`);
\r
2365 (FIRST_ASSUM MATCH_MP_TAC);
\r
2366 (ASM_REWRITE_TAC[]);
\r
2369 (ASM_MESON_TAC[]);
\r
2372 (NEW_GOAL `!u:num. q u = 2 ==> p1 u = 0`);
\r
2373 (REPEAT STRIP_TAC);
\r
2374 (ASM_CASES_TAC `(p1:num->num) u = 1`);
\r
2375 (NEW_GOAL `(q:num->num) u = 3`);
\r
2376 (FIRST_ASSUM MATCH_MP_TAC);
\r
2377 (ASM_REWRITE_TAC[]);
\r
2380 (ASM_MESON_TAC[]);
\r
2381 (ASM_CASES_TAC `(p1:num->num) u = 2`);
\r
2382 (NEW_GOAL `(q:num->num) u = 0`);
\r
2383 (FIRST_ASSUM MATCH_MP_TAC);
\r
2384 (ASM_REWRITE_TAC[]);
\r
2387 (ASM_MESON_TAC[]);
\r
2388 (ASM_CASES_TAC `(p1:num->num) u = 3`);
\r
2389 (NEW_GOAL `(q:num->num) u = 1`);
\r
2390 (FIRST_ASSUM MATCH_MP_TAC);
\r
2391 (ASM_REWRITE_TAC[]);
\r
2394 (ASM_MESON_TAC[]);
\r
2395 (ASM_CASES_TAC `(p1:num->num) u > 3`);
\r
2396 (NEW_GOAL `(q:num->num) u = u`);
\r
2397 (FIRST_ASSUM MATCH_MP_TAC);
\r
2398 (ASM_REWRITE_TAC[]);
\r
2399 (NEW_GOAL `(p1:num->num) u = u`);
\r
2400 (FIRST_ASSUM MATCH_MP_TAC);
\r
2401 (ASM_REWRITE_TAC[]);
\r
2404 (ASM_MESON_TAC[]);
\r
2407 (NEW_GOAL `!u:num. q u = 3 ==> p1 u = 1`);
\r
2408 (REPEAT STRIP_TAC);
\r
2409 (ASM_CASES_TAC `(p1:num->num) u = 0`);
\r
2410 (NEW_GOAL `(q:num->num) u = 2`);
\r
2411 (FIRST_ASSUM MATCH_MP_TAC);
\r
2412 (ASM_REWRITE_TAC[]);
\r
2415 (ASM_MESON_TAC[]);
\r
2416 (ASM_CASES_TAC `(p1:num->num) u = 2`);
\r
2417 (NEW_GOAL `(q:num->num) u = 0`);
\r
2418 (FIRST_ASSUM MATCH_MP_TAC);
\r
2419 (ASM_REWRITE_TAC[]);
\r
2422 (ASM_MESON_TAC[]);
\r
2423 (ASM_CASES_TAC `(p1:num->num) u = 3`);
\r
2424 (NEW_GOAL `(q:num->num) u = 1`);
\r
2425 (FIRST_ASSUM MATCH_MP_TAC);
\r
2426 (ASM_REWRITE_TAC[]);
\r
2429 (ASM_MESON_TAC[]);
\r
2430 (ASM_CASES_TAC `(p1:num->num) u > 3`);
\r
2431 (NEW_GOAL `(q:num->num) u = u`);
\r
2432 (FIRST_ASSUM MATCH_MP_TAC);
\r
2433 (ASM_REWRITE_TAC[]);
\r
2434 (NEW_GOAL `(p1:num->num) u = u`);
\r
2435 (FIRST_ASSUM MATCH_MP_TAC);
\r
2436 (ASM_REWRITE_TAC[]);
\r
2439 (ASM_MESON_TAC[]);
\r
2442 (NEW_GOAL `!u:num. q u > 3 ==> p1 u > 3`);
\r
2443 (REPEAT STRIP_TAC);
\r
2444 (ASM_CASES_TAC `(p1:num->num) u = 0`);
\r
2445 (NEW_GOAL `(q:num->num) u = 2`);
\r
2446 (FIRST_ASSUM MATCH_MP_TAC);
\r
2447 (ASM_REWRITE_TAC[]);
\r
2450 (ASM_MESON_TAC[]);
\r
2451 (ASM_CASES_TAC `(p1:num->num) u = 1`);
\r
2452 (NEW_GOAL `(q:num->num) u = 3`);
\r
2453 (FIRST_ASSUM MATCH_MP_TAC);
\r
2454 (ASM_REWRITE_TAC[]);
\r
2457 (ASM_MESON_TAC[]);
\r
2458 (ASM_CASES_TAC `(p1:num->num) u = 2`);
\r
2459 (NEW_GOAL `(q:num->num) u = 0`);
\r
2460 (FIRST_ASSUM MATCH_MP_TAC);
\r
2461 (ASM_REWRITE_TAC[]);
\r
2464 (ASM_MESON_TAC[]);
\r
2465 (ASM_CASES_TAC `(p1:num->num) u = 3`);
\r
2466 (NEW_GOAL `(q:num->num) u = 1`);
\r
2467 (FIRST_ASSUM MATCH_MP_TAC);
\r
2468 (ASM_REWRITE_TAC[]);
\r
2471 (ASM_MESON_TAC[]);
\r
2475 (NEW_GOAL `!u:num. p2 u = 0 ==> q u = 2`);
\r
2476 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
2477 (NEW_GOAL `!u:num. p2 u = 1 ==> q u = 3`);
\r
2478 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
2482 (ASM_MESON_TAC[]);
\r
2485 (NEW_GOAL `!u:num. p2 u = 2 ==> q u = 0`);
\r
2486 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
2491 (ASM_MESON_TAC[]);
\r
2494 (NEW_GOAL `!u:num. p2 u = 3 ==> q u = 1`);
\r
2495 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
2499 (ASM_MESON_TAC[]);
\r
2504 (ASM_MESON_TAC[]);
\r
2507 (NEW_GOAL `!u:num. p2 u > 3 ==> q u = u`);
\r
2508 (REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
\r
2512 (ASM_MESON_TAC[]);
\r
2516 (ASM_MESON_TAC[]);
\r
2520 (ASM_MESON_TAC[]);
\r
2524 (ASM_MESON_TAC[]);
\r
2527 (NEW_GOAL `!u:num. p2 u > 3 ==> p2 u = u`);
\r
2528 (NEW_GOAL `p2 permutes 0..3`);
\r
2529 (REWRITE_WITH `p2:num->num = p'`);
\r
2530 (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list = e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);
\r
2532 (ASM_REWRITE_TAC[]);
\r
2533 (UNDISCH_TAC `p2 permutes 0..3` THEN REWRITE_TAC[permutes; EXISTS_UNIQUE]);
\r
2534 (REPEAT STRIP_TAC);
\r
2535 (ABBREV_TAC `s = (p2:num->num) u`);
\r
2536 (NEW_GOAL `(p2:num->num) s = s`);
\r
2537 (FIRST_ASSUM MATCH_MP_TAC);
\r
2538 (UNDISCH_TAC `s > 3` THEN REWRITE_TAC[IN_NUMSEG_0] THEN ARITH_TAC);
\r
2539 (NEW_GOAL `?z. (p2:num->num) z = s /\ (!y'. p2 y' = s ==> y' = z)`);
\r
2540 (ASM_REWRITE_TAC[]);
\r
2541 (UP_ASM_TAC THEN STRIP_TAC);
\r
2542 (NEW_GOAL `s = z:num`);
\r
2543 (FIRST_ASSUM MATCH_MP_TAC);
\r
2544 (ASM_REWRITE_TAC[]);
\r
2545 (NEW_GOAL `u = z:num`);
\r
2546 (FIRST_ASSUM MATCH_MP_TAC);
\r
2547 (ASM_REWRITE_TAC[]);
\r
2548 (ASM_REWRITE_TAC[]);
\r
2550 (NEW_GOAL `!u:num. q u = 0 ==> p2 u = 2`);
\r
2551 (REPEAT STRIP_TAC);
\r
2552 (ASM_CASES_TAC `(p2:num->num) u = 0`);
\r
2553 (NEW_GOAL `(q:num->num) u = 2`);
\r
2554 (FIRST_ASSUM MATCH_MP_TAC);
\r
2555 (ASM_REWRITE_TAC[]);
\r
2558 (ASM_MESON_TAC[]);
\r
2559 (ASM_CASES_TAC `(p2:num->num) u = 1`);
\r
2560 (NEW_GOAL `(q:num->num) u = 3`);
\r
2561 (FIRST_ASSUM MATCH_MP_TAC);
\r
2562 (ASM_REWRITE_TAC[]);
\r
2565 (ASM_MESON_TAC[]);
\r
2566 (ASM_CASES_TAC `(p2:num->num) u = 3`);
\r
2567 (NEW_GOAL `(q:num->num) u = 1`);
\r
2568 (FIRST_ASSUM MATCH_MP_TAC);
\r
2569 (ASM_REWRITE_TAC[]);
\r
2572 (ASM_MESON_TAC[]);
\r
2573 (ASM_CASES_TAC `(p2:num->num) u > 3`);
\r
2574 (NEW_GOAL `(q:num->num) u = u`);
\r
2575 (FIRST_ASSUM MATCH_MP_TAC);
\r
2576 (ASM_REWRITE_TAC[]);
\r
2577 (NEW_GOAL `(p2:num->num) u = u`);
\r
2578 (FIRST_ASSUM MATCH_MP_TAC);
\r
2579 (ASM_REWRITE_TAC[]);
\r
2582 (ASM_MESON_TAC[]);
\r
2585 (NEW_GOAL `!u:num. q u = 1 ==> p2 u = 3`);
\r
2586 (REPEAT STRIP_TAC);
\r
2587 (ASM_CASES_TAC `(p2:num->num) u = 0`);
\r
2588 (NEW_GOAL `(q:num->num) u = 2`);
\r
2589 (FIRST_ASSUM MATCH_MP_TAC);
\r
2590 (ASM_REWRITE_TAC[]);
\r
2593 (ASM_MESON_TAC[]);
\r
2594 (ASM_CASES_TAC `(p2:num->num) u = 1`);
\r
2595 (NEW_GOAL `(q:num->num) u = 3`);
\r
2596 (FIRST_ASSUM MATCH_MP_TAC);
\r
2597 (ASM_REWRITE_TAC[]);
\r
2600 (ASM_MESON_TAC[]);
\r
2601 (ASM_CASES_TAC `(p2:num->num) u = 2`);
\r
2602 (NEW_GOAL `(q:num->num) u = 0`);
\r
2603 (FIRST_ASSUM MATCH_MP_TAC);
\r
2604 (ASM_REWRITE_TAC[]);
\r
2607 (ASM_MESON_TAC[]);
\r
2608 (ASM_CASES_TAC `(p2:num->num) u > 3`);
\r
2609 (NEW_GOAL `(q:num->num) u = u`);
\r
2610 (FIRST_ASSUM MATCH_MP_TAC);
\r
2611 (ASM_REWRITE_TAC[]);
\r
2612 (NEW_GOAL `(p2:num->num) u = u`);
\r
2613 (FIRST_ASSUM MATCH_MP_TAC);
\r
2614 (ASM_REWRITE_TAC[]);
\r
2617 (ASM_MESON_TAC[]);
\r
2620 (NEW_GOAL `!u:num. q u = 2 ==> p2 u = 0`);
\r
2621 (REPEAT STRIP_TAC);
\r
2622 (ASM_CASES_TAC `(p2:num->num) u = 1`);
\r
2623 (NEW_GOAL `(q:num->num) u = 3`);
\r
2624 (FIRST_ASSUM MATCH_MP_TAC);
\r
2625 (ASM_REWRITE_TAC[]);
\r
2628 (ASM_MESON_TAC[]);
\r
2629 (ASM_CASES_TAC `(p2:num->num) u = 2`);
\r
2630 (NEW_GOAL `(q:num->num) u = 0`);
\r
2631 (FIRST_ASSUM MATCH_MP_TAC);
\r
2632 (ASM_REWRITE_TAC[]);
\r
2635 (ASM_MESON_TAC[]);
\r
2636 (ASM_CASES_TAC `(p2:num->num) u = 3`);
\r
2637 (NEW_GOAL `(q:num->num) u = 1`);
\r
2638 (FIRST_ASSUM MATCH_MP_TAC);
\r
2639 (ASM_REWRITE_TAC[]);
\r
2642 (ASM_MESON_TAC[]);
\r
2643 (ASM_CASES_TAC `(p2:num->num) u > 3`);
\r
2644 (NEW_GOAL `(q:num->num) u = u`);
\r
2645 (FIRST_ASSUM MATCH_MP_TAC);
\r
2646 (ASM_REWRITE_TAC[]);
\r
2647 (NEW_GOAL `(p2:num->num) u = u`);
\r
2648 (FIRST_ASSUM MATCH_MP_TAC);
\r
2649 (ASM_REWRITE_TAC[]);
\r
2652 (ASM_MESON_TAC[]);
\r
2655 (NEW_GOAL `!u:num. q u = 3 ==> p2 u = 1`);
\r
2656 (REPEAT STRIP_TAC);
\r
2657 (ASM_CASES_TAC `(p2:num->num) u = 0`);
\r
2658 (NEW_GOAL `(q:num->num) u = 2`);
\r
2659 (FIRST_ASSUM MATCH_MP_TAC);
\r
2660 (ASM_REWRITE_TAC[]);
\r
2663 (ASM_MESON_TAC[]);
\r
2664 (ASM_CASES_TAC `(p2:num->num) u = 2`);
\r
2665 (NEW_GOAL `(q:num->num) u = 0`);
\r
2666 (FIRST_ASSUM MATCH_MP_TAC);
\r
2667 (ASM_REWRITE_TAC[]);
\r
2670 (ASM_MESON_TAC[]);
\r
2671 (ASM_CASES_TAC `(p2:num->num) u = 3`);
\r
2672 (NEW_GOAL `(q:num->num) u = 1`);
\r
2673 (FIRST_ASSUM MATCH_MP_TAC);
\r
2674 (ASM_REWRITE_TAC[]);
\r
2677 (ASM_MESON_TAC[]);
\r
2678 (ASM_CASES_TAC `(p2:num->num) u > 3`);
\r
2679 (NEW_GOAL `(q:num->num) u = u`);
\r
2680 (FIRST_ASSUM MATCH_MP_TAC);
\r
2681 (ASM_REWRITE_TAC[]);
\r
2682 (NEW_GOAL `(p2:num->num) u = u`);
\r
2683 (FIRST_ASSUM MATCH_MP_TAC);
\r
2684 (ASM_REWRITE_TAC[]);
\r
2687 (ASM_MESON_TAC[]);
\r
2690 (NEW_GOAL `!u:num. q u > 3 ==> p2 u > 3`);
\r
2691 (REPEAT STRIP_TAC);
\r
2692 (ASM_CASES_TAC `(p2:num->num) u = 0`);
\r
2693 (NEW_GOAL `(q:num->num) u = 2`);
\r
2694 (FIRST_ASSUM MATCH_MP_TAC);
\r
2695 (ASM_REWRITE_TAC[]);
\r
2698 (ASM_MESON_TAC[]);
\r
2699 (ASM_CASES_TAC `(p2:num->num) u = 1`);
\r
2700 (NEW_GOAL `(q:num->num) u = 3`);
\r
2701 (FIRST_ASSUM MATCH_MP_TAC);
\r
2702 (ASM_REWRITE_TAC[]);
\r
2705 (ASM_MESON_TAC[]);
\r
2706 (ASM_CASES_TAC `(p2:num->num) u = 2`);
\r
2707 (NEW_GOAL `(q:num->num) u = 0`);
\r
2708 (FIRST_ASSUM MATCH_MP_TAC);
\r
2709 (ASM_REWRITE_TAC[]);
\r
2712 (ASM_MESON_TAC[]);
\r
2713 (ASM_CASES_TAC `(p2:num->num) u = 3`);
\r
2714 (NEW_GOAL `(q:num->num) u = 1`);
\r
2715 (FIRST_ASSUM MATCH_MP_TAC);
\r
2716 (ASM_REWRITE_TAC[]);
\r
2719 (ASM_MESON_TAC[]);
\r
2722 (ASM_CASES_TAC `(q:num->num) x'' = 0`);
\r
2723 (NEW_GOAL `(p1:num->num) x'' = 2`);
\r
2725 (NEW_GOAL `(p2:num->num) x'' = 2`);
\r
2727 (ASM_REWRITE_TAC[]);
\r
2729 (ASM_CASES_TAC `(q:num->num) x'' = 1`);
\r
2730 (NEW_GOAL `(p1:num->num) x'' = 3`);
\r
2732 (NEW_GOAL `(p2:num->num) x'' = 3`);
\r
2734 (ASM_REWRITE_TAC[]);
\r
2736 (ASM_CASES_TAC `(q:num->num) x'' = 2`);
\r
2737 (NEW_GOAL `(p1:num->num) x'' = 0`);
\r
2739 (NEW_GOAL `(p2:num->num) x'' = 0`);
\r
2741 (ASM_REWRITE_TAC[]);
\r
2743 (ASM_CASES_TAC `(q:num->num) x'' = 3`);
\r
2744 (NEW_GOAL `(p1:num->num) x'' = 1`);
\r
2746 (NEW_GOAL `(p2:num->num) x'' = 1`);
\r
2748 (ASM_REWRITE_TAC[]);
\r
2750 (NEW_GOAL `(q:num->num) x'' > 3`);
\r
2752 (NEW_GOAL `(p1:num->num) x'' > 3`);
\r
2756 (REWRITE_TAC[Packing3.LIST_EL_EQ]);
\r
2758 (* ------------------------------------------------------------------------- *)
\r
2760 (REWRITE_WITH `LENGTH (vl1:(real^3)list) = 4`);
\r
2761 (REWRITE_WITH `(vl1:(real^3)list) = vl`);
\r
2762 (UNDISCH_TAC `e1:real^3->bool,e2:real^3->bool,p1:num->num,vl1:(real^3)list
\r
2763 = e',e'',p,vl` THEN REWRITE_TAC[PAIR_EQ]);
\r
2765 (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
\r
2766 (REWRITE_WITH `LENGTH (vl2:(real^3)list) = 4`);
\r
2767 (REWRITE_WITH `(vl2:(real^3)list) = vl'`);
\r
2768 (UNDISCH_TAC `f1:real^3->bool,f2:real^3->bool,p2:num->num,vl2:(real^3)list
\r
2769 = e''',e'''',p',vl'` THEN REWRITE_TAC[PAIR_EQ]);
\r
2771 (ASM_REWRITE_TAC[left_action_list; TABLE_4; LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4`]);
\r
2772 (REPEAT STRIP_TAC);
\r
2774 (ASM_CASES_TAC `j = 0`);
\r
2775 (NEW_GOAL `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
\r
2776 EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
\r
2778 (ASM_REWRITE_TAC[]);
\r
2779 (UP_ASM_TAC THEN REWRITE_WITH
\r
2780 `EL 2 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 0 vl1 /\
\r
2781 EL 2 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 0 vl2`);
\r
2782 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2783 (ASM_REWRITE_TAC[]);
\r
2785 (ASM_CASES_TAC `j = 1`);
\r
2786 (NEW_GOAL `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
\r
2787 EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
\r
2789 (ASM_REWRITE_TAC[]);
\r
2790 (UP_ASM_TAC THEN REWRITE_WITH
\r
2791 `EL 3 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 1 vl1 /\
\r
2792 EL 3 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 1 vl2`);
\r
2793 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2794 (ASM_REWRITE_TAC[]);
\r
2796 (ASM_CASES_TAC `j = 2`);
\r
2797 (NEW_GOAL `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
\r
2798 EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
\r
2800 (ASM_REWRITE_TAC[]);
\r
2801 (UP_ASM_TAC THEN REWRITE_WITH
\r
2802 `EL 0 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 2 vl1 /\
\r
2803 EL 0 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 2 vl2`);
\r
2804 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2805 (ASM_REWRITE_TAC[]);
\r
2807 (ASM_CASES_TAC `j = 3`);
\r
2808 (NEW_GOAL `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] =
\r
2809 EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 vl2]`);
\r
2811 (ASM_REWRITE_TAC[]);
\r
2812 (UP_ASM_TAC THEN REWRITE_WITH
\r
2813 `EL 1 [EL 2 vl1; EL 3 vl1; EL 0 vl1; EL 1 (vl1:(real^3)list)] = EL 3 vl1 /\
\r
2814 EL 1 [EL 2 vl2; EL 3 vl2; EL 0 vl2; EL 1 (vl2:(real^3)list)] = EL 3 vl2`);
\r
2815 (REWRITE_TAC[EL;HD;TL;ARITH_RULE`1=SUC 0/\2=SUC 1/\3=SUC 2`]);
\r
2816 (ASM_REWRITE_TAC[]);
\r
2820 (ASM_MESON_TAC[]);
\r
2822 (NEW_GOAL `X:real^3->bool = {}`);
\r
2823 (ASM_MESON_TAC[]);
\r
2824 (REPEAT STRIP_TAC);
\r
2825 (REWRITE_WITH `{e | e IN critical_edgeX V X} = {}`);
\r
2826 (REWRITE_TAC[SET_RULE `{x| x IN s} = s`]);
\r
2827 (ASM_REWRITE_TAC[critical_edgeX; edgeX]);
\r
2828 (REWRITE_WITH `VX V {} = {}`);
\r
2829 (REWRITE_TAC [VX]);
\r
2833 (UP_ASM_TAC THEN REWRITE_TAC[NEGLIGIBLE_EMPTY]);
\r
2834 (ASM_MESON_TAC[]);
\r
2835 (REWRITE_WITH `{{u:real^3, v:real^3} | {} u /\ {} v /\ ~(u = v)} =
\r
2836 {{u, v} | u IN {} /\ v IN {} /\ ~(u = v)}`);
\r
2837 (REWRITE_TAC[IN]);
\r
2838 (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);
\r
2839 (REWRITE_WITH `{{u:real^3, v:real^3} | F} = {}`);
\r
2840 (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);
\r
2842 (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);
\r
2843 (REWRITE_TAC[IN]);
\r
2845 (REWRITE_TAC[MESON[NOT_IN_EMPTY] `x IN {} <=> F`]);
\r
2846 (REWRITE_TAC[SET_EQ_LEMMA; IN; IN_ELIM_THM]);
\r
2848 (REWRITE_WITH `{} (x:real^3->bool) <=> x IN {}`);
\r
2849 (REWRITE_TAC[IN]);
\r
2851 (REWRITE_TAC[SUM_CLAUSES])]);;
\r