1 module Hypermap_of_fan = struct
10 (* ========================================================================== *)
11 (* DEFINITION OF HYPERMAP OF FAN *)
12 (* ========================================================================== *)
16 let d1_fan =new_definition`
17 d1_fan (x,V,E) ={(x':real^3,v:real^3,w:real^3,w1:real^3)| (x'=x) /\ ({v,w} IN E)/\ (w1 = sigma_fan x V E v w)}`;;
20 let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
22 let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
25 let inverse_sigma_fan_alt=new_definition`inverse_sigma_fan_alt x V E v w = @a. sigma_fan x V E v a=w`;;
27 let e_fan=new_definition` e_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,v,(sigma_fan x V E w v)))`;;
30 let f_fan=new_definition`f_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse_sigma_fan_alt x V E w v),v) )`;;
32 (* This is the same as f_fan,
35 let f1_fan=new_definition`f1_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse1_sigma_fan x V E w v),v) )`;;
39 let n_fan=new_definition`n_fan (x:real^3) V E =(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,(sigma_fan x V E v w),(sigma_fan x V E v (sigma_fan x V E v w))))`;;
41 (* i_fan corrects the 4th coordinate to be
44 let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
46 let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
48 let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
50 let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
52 let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
54 (* if f = sigma, the power_map_points gives
55 iterates of sigma (for fixed x v) *)
58 let power_map_points= new_recursive_definition num_RECURSION `(power_map_points f x V E v w 0 = w)/\(power_map_points f x V E v w (SUC n)= f x V E v (power_map_points f x V E v w n))`;;
60 (* This is the composition operator (o),
61 specialized to functions on 4-tuples *)
64 let o_funs=new_definition`!(f:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (g:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3). o_funs f g =(\(x:real^3,y:real^3,z:real^3,t:real^3). f (pr1 (g(x,y,z,t)),pr2(g(x,y,z,t)),pr3(g(x,y,z,t)),pr4(g(x,y,z,t))))`;;
66 (* powers of permutations *)
68 let power_maps= new_recursive_definition num_RECURSION `(power_maps (f:real^3->(real^3->bool)->((real^3->bool)->bool)->real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) 0 = i_fan (x:real^3) V E) /\ (power_maps f x V E (SUC n)= o_funs (f x V E) (power_maps f x V E n))`;;
71 (* powers of node map *)
76 let power_n_fan= new_definition`power_n_fan x V E n=( \(x,v,w,w1). (x,v,(power_map_points sigma_fan x V E v w n),(power_map_points sigma_fan x V E v w (SUC n))))`;;
79 (* the node of a dart, in a special form
83 let a_node_fan=new_definition`a_node_fan x V E (x,v,w,w1)={a | ?n. a=(power_maps n_fan x V E n) (x,v,w,sigma_fan x V E v w)}`;;
88 let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
90 (* See comment by AS in fan_defs.hl. The correct definition is there. *)
91 let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;
99 let hypermap_of_fanx = new_definition
100 `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
101 (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
102 hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;
105 let hypermap1_of_fanx = new_definition
106 `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) =
107 (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in
108 hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;
118 let w_dart_fan=new_definition`w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3))=
119 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
121 (if set_of_edge v V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
122 else (if set_of_edge v V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
127 (* ========================================================================== *)
128 (* ORBITS NODE FAN *)
129 (* ========================================================================== *)
136 let image_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
137 FAN(x,V,E) /\ (u IN set_of_edge v V E)
138 ==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E`,
140 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points]
143 REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC
144 THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`] th)) THEN
145 ASM_REWRITE_TAC[] THEN DISCH_TAC
146 THEN DISJ_CASES_TAC(SET_RULE `set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i}\/ ~(set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i})`)
147 THENL[ASM_MESON_TAC[sigma_fan];
148 ASM_MESON_TAC[SIGMA_FAN]]]);;
151 let IN2_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
152 FAN(x,V,E) /\ ({v,u} IN E)
153 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
154 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
156 let IN1_ORBITS_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
157 FAN(x,V,E) /\ (u IN set_of_edge v V E)
158 ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
159 MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
162 let remark_power_map_points=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
163 FAN(x,V,E) /\ ({v,u} IN E)
165 power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E
166 /\ {v,power_map_points sigma_fan x V E v u i} IN E
168 ~(collinear {x,v,power_map_points sigma_fan x V E v u i})
169 /\ ~(x = power_map_points (sigma_fan) x V E v u i) /\
170 ~(v = power_map_points (sigma_fan) x V E v u i) /\
171 DISJOINT {x, v} {power_map_points (sigma_fan) x V E v u i} /\
172 ~((power_map_points (sigma_fan) x V E v u i) IN aff {x, v}) /\
173 DISJOINT {x} {v, (power_map_points (sigma_fan) x V E v u i)} `,
174 MESON_TAC[IN2_ORBITS_FAN;remark1_fan;image_power_map_points;properties_of_set_of_edge_fan]);;
182 (* ========================================================================== *)
183 (* PERMUTES OF E_FAN N_FAN F1_FAN (^_^) *)
184 (* ========================================================================== *)
188 (* Proof Lemma 6.1 [AAUHTVE] *)
190 let node_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) n:num. power_maps n_fan x V E n=power_n_fan x V E n`,
191 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[power_maps; n_fan; power_n_fan; power_map_points] THEN INDUCT_TAC THEN REWRITE_TAC[power_maps; power_map_points;i_fan;] THEN REWRITE_TAC[power_map_points; power_maps] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[n_fan;o_funs; pr1; pr2; pr3; pr4]);;
197 let EQ_PAIR_4=prove(`!a:real^3 b:real^3 c:real^3 d:real^3 a1:real^3 b1:real^3 c1:real^3 d:real^3.
198 (a,b,c,d)=(a1,b1,c1,d1) <=> a=a1 /\ b=b1 /\ c=c1 /\ d=d1`,
199 REPEAT GEN_TAC THEN EQ_TAC
201 DISCH_TAC THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr1(a,b,c,d)=pr1(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr1]
202 THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr2(a,b,c,d)=pr2(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr2] THEN
203 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr3(a,b,c,d)=pr3(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr3] THEN
204 MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr4(a,b,c,d)=pr4(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr4] THEN ASM_REWRITE_TAC[]
210 let MONO_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
212 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)`,
214 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;EQ_PAIR_4]
215 THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> REWRITE_TAC[])
216 THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
217 THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3` ]remark1_fan)
218 THEN ASM_REWRITE_TAC[]
219 THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w':real^3`;`v:real^3` ]remark1_fan)
220 THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MONO_SIGMA_FAN;]);;
223 let SUR_N_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
225 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,
227 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
228 THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`] SUR_SIGMA_FAN)
229 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
230 THEN EXISTS_TAC`(x:real^3,v:real^3,w':real^3,w:real^3)`
231 THEN ASM_REWRITE_TAC[n_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3`
232 THEN EXISTS_TAC`w':real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
236 let simp_inverse_sigma_fan_alt=prove(`!x V E v w.
237 inverse_sigma_fan_alt x V E v w= inverse (sigma_fan x V E v) w`,
238 REWRITE_TAC[inverse] THEN MESON_TAC[inverse_sigma_fan_alt]);;
242 let SUR_F1_FAN=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
244 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))`,
245 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC
246 THEN EXISTS_TAC`(x:real^3,sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w, v:real^3,sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w) v)`
247 THEN ASM_REWRITE_TAC[f_fan;EQ_PAIR_4;]
250 EXISTS_TAC`x:real^3` THEN EXISTS_TAC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w`
251 THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w) v`
252 THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ={w:real^3}) \/ ~(set_of_edge v V E ={w})`)
254 REWRITE_TAC[sigma_fan;SET_RULE`{a,b}={b,a}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
255 THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[])
256 THEN POP_ASSUM (fun th-> REWRITE_TAC[th]);
258 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3`]remark1_fan)
259 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
260 MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`]SIGMA_FAN)
261 THEN ASM_REWRITE_TAC[remark1_fan] THEN STRIP_TAC
262 THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`sigma_fan x V E v w:real^3`;`v:real^3`]remark1_fan)
263 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
264 THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]];
266 REWRITE_TAC[f1_fan] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`]INVERSE1_SIGMA_FAN)
267 THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th))
268 THEN ASM_REWRITE_TAC[]]);;
274 let MONO_F1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
276 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)`,
277 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;EQ_PAIR_4]
278 THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
281 let MONO_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
283 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)`,
284 REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;EQ_PAIR_4]
285 THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
288 let SUR_E_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
290 ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,
292 REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN REPEAT STRIP_TAC
293 THEN EXISTS_TAC`(x:real^3,w:real^3,v:real^3, sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v)`
294 THEN ASM_REWRITE_TAC[e_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3`
295 THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v`
296 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]);;
303 let permuters_of_enf_fan=prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
305 ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)
306 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))
307 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)
308 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))
309 /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)
310 /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))
311 `,MESON_TAC[MONO_N_FAN;SUR_N_FAN;MONO_F1_FAN;SUR_F1_FAN;MONO_E_FAN;SUR_E_FAN]);;
319 (* ========================================================================== *)
320 (* PROPERTIES OF E_FAN N_FAN F1_FAN (^_^) *)
321 (* ========================================================================== *)
324 let condition_hypermap_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
325 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> e_fan x V E((n_fan x V E) (f1_fan x V E a))=a)`,
326 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[f1_fan;n_fan; e_fan; EQ_PAIR_4]
327 THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`]INVERSE1_SIGMA_FAN)
328 THEN ASM_REWRITE_TAC[]
329 THEN STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[])
330 THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`v:real^3`th))
331 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]
332 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
336 let plain_hypermap_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
337 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==>
338 (e_fan x V E) (e_fan x V E a) =a)`,
339 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]);;
342 let e_fan_no_fix_point=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
343 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))`,
344 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]
345 THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
346 THEN ASM_MESON_TAC[]);;
348 let f_fan_no_fix_point=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
349 FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))`,
350 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC
351 THEN ASM_REWRITE_TAC[f1_fan; EQ_PAIR_4]
352 THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
353 THEN ASM_MESON_TAC[]);;
357 (* from hypermap.hl *)
359 (******************************)
360 parse_as_infix("POWER",(24,"right"));;
362 let POWER = new_recursive_definition num_RECURSION
363 `(!(f:A->A). f POWER 0 = I) /\
364 (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
366 let POWER_0 = prove(`!f:A->A. f POWER 0 = I`,
367 REWRITE_TAC[POWER]);;
369 let POWER_1 = prove(`!f:A->A. f POWER 1 = f`,
370 REWRITE_TAC[POWER; ONE; I_O_ID]);;
372 let POWER_2 = prove(`!f:A->A. f POWER 2 = f o f`,
373 REWRITE_TAC[POWER; TWO; POWER_1]);;
375 let orbit_map = new_definition `orbit_map (f:A->A) (x:A) = {(f POWER n) x | n >= 0}`;;
376 (**************************************************)
378 let POWER_RIGHT=prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
380 THENL[REWRITE_TAC[POWER;o_DEF; I_DEF];
381 REWRITE_TAC[POWER;o_ASSOC] THEN GEN_TAC THEN POP_ASSUM(fun th -> MP_TAC(SPEC`f:A->A`th)) THEN DISCH_TAC
383 POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;
387 let power_n_fan=prove(`!l:num x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 w:real^3.
388 FAN(x,V,E)/\ ({v,w} IN E)==>
389 (n_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) POWER l) (x,v,w,sigma_fan x V E v w)= (x,v, power_map_points sigma_fan x V E v w l, power_map_points sigma_fan x V E v w (SUC l) )`,
391 THENL[REWRITE_TAC[POWER; power_map_points;I_DEF];
392 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT STRIP_TAC THEN
393 REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;`(w:real^3)`]th))
394 THEN ASM_REWRITE_TAC[POWER_RIGHT; o_DEF;]
395 THEN DISCH_TAC THEN ASM_REWRITE_TAC[n_fan;power_map_points] ]);;
399 let distinct_nodes=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) .
400 FAN(x,V,E)==> (!k:num l:num a. a IN d1_fan(x,V,E) ==>
401 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)`,
402 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
403 ASM_REWRITE_TAC[o_DEF;e_fan] THEN
404 MP_TAC(ISPECL[`l:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
405 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
406 THEN MP_TAC(ISPECL[`k:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` w:real^3`;` v:real^3`]power_n_fan)
407 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC
408 THEN POP_ASSUM(fun th-> REWRITE_TAC[]) THEN POP_ASSUM(fun th-> REWRITE_TAC[])
409 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th))
410 THEN ASM_REWRITE_TAC[power_map_points] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]));;
415 let edge_lie_different_nodes=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
416 FAN(x,V,E)==> (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a)) `,
418 REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
419 ASM_REWRITE_TAC[e_fan] THEN
420 MP_TAC(ISPECL[`n:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan)
421 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4]
423 THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan)
424 THEN ASM_MESON_TAC[]);;
429 (* ========================================================================== *)
430 (* REPRESENTATION OF HYPERMAP OF FAN (^_^) *)
431 (* ========================================================================== *)
436 let finite_d1_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
437 FAN(x,V,E) ==> FINITE (d1_fan (x,V,E))`,
439 THEN DISCH_THEN(LABEL_TAC"EM")
440 THEN USE_THEN "EM" MP_TAC
441 THEN REWRITE_TAC[FAN;fan1]
443 THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
444 THEN MRESA_TAC FINITE_PRODUCT[`V:real^3->bool`;`V:real^3->bool`]
445 THEN MRESA_TAC FINITE_IMAGE[`(\(a,b:real^3). (x,a,b,sigma_fan x V E a b))`;`{x,y | x IN (V:real^3->bool) /\ y IN V}`]
446 THEN MATCH_MP_TAC FINITE_SUBSET
447 THEN EXISTS_TAC`(IMAGE (\(a,b). x,a,b,sigma_fan x V E a b) {x,y | x IN V /\ y IN (V:real^3->bool)})`
448 THEN ASM_REWRITE_TAC[IMAGE;IN_ELIM_THM;d1_fan;SUBSET]
449 THEN REPEAT STRIP_TAC
450 THEN EXISTS_TAC`(v:real^3,w:real^3)`
451 THEN ASM_REWRITE_TAC[]
452 THEN EXISTS_TAC`v:real^3`
453 THEN EXISTS_TAC`w:real^3`
454 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`]
455 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`w:real^3`]
456 THEN POP_ASSUM MP_TAC
457 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
458 THEN ASM_REWRITE_TAC[]
459 THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
463 let finite_d20_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
464 FAN(x,V,E) ==> FINITE (d20_fan (x,V,E))`,
467 THEN DISCH_THEN(LABEL_TAC"EM")
468 THEN USE_THEN "EM" MP_TAC
469 THEN REWRITE_TAC[FAN;fan1]
471 THEN MRESA_TAC FINITE_IMAGE[`(\b:real^3. (x:real^3,b,b,b))`;`V:real^3->bool`]
472 THEN MATCH_MP_TAC FINITE_SUBSET
473 THEN EXISTS_TAC`(IMAGE (\b:real^3. (x:real^3,b,b,b)) (V:real^3->bool))`
474 THEN ASM_REWRITE_TAC[d20_fan;SUBSET;IMAGE;IN_ELIM_THM]
475 THEN REPEAT STRIP_TAC
476 THEN EXISTS_TAC`v:real^3`
477 THEN ASM_REWRITE_TAC[IN]);;
481 let finite_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
483 ==> FINITE (d_fan (x,V,E))`,
485 THEN REWRITE_TAC[d_fan;FINITE_UNION]
487 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
489 let subset_d_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
490 d1_fan (x,V,E) SUBSET d_fan (x,V,E) /\ d20_fan (x,V,E) SUBSET d_fan(x,V,E)`,
491 REWRITE_TAC[d_fan] THEN SET_TAC[]);;
494 let FACE_FAN_NOT_EMPTY=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
496 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
499 THEN POP_ASSUM MP_TAC
500 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
501 THEN MRESA_TAC FACE_FINITE[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
503 THEN MRESA1_TAC CARD_EQ_0`face (hypermap1_of_fanx (x:real^3,V,E)) x'`
504 THEN MRESA_TAC FACE_NOT_EMPTY[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]
505 THEN POP_ASSUM MP_TAC
514 let into_domain_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
515 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
516 ==> (!y. y IN d_fan (x,V,E)==> ((p e_fan ) y) IN (d_fan (x,V,E)))`,
518 THEN ASM_REWRITE_TAC[res;]
519 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
524 THEN POP_ASSUM MP_TAC
525 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
527 THEN ASM_REWRITE_TAC[]
528 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
529 THEN MATCH_MP_TAC(SET_RULE`x,w,v,sigma_fan x V E w v IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E)
530 ==>x,w,v,sigma_fan x V E w v IN d_fan (x:real^3,V,E)`)
531 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
532 THEN EXISTS_TAC`x:real^3`
533 THEN EXISTS_TAC`w:real^3`
534 THEN EXISTS_TAC`v:real^3`
535 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
536 THEN ASM_REWRITE_TAC[]
537 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
538 THEN ASM_REWRITE_TAC[]]);;
543 let into_domain1_e_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
544 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (e_fan x V E y IN d1_fan (x,V,E)))`,
546 THEN POP_ASSUM MP_TAC
547 THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM]
549 THEN ASM_REWRITE_TAC[]
550 THEN EXISTS_TAC`x:real^3`
551 THEN EXISTS_TAC`w:real^3`
552 THEN EXISTS_TAC`v:real^3`
553 THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)`
554 THEN ASM_REWRITE_TAC[]
555 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
556 THEN ASM_REWRITE_TAC[]);;
562 let e_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
563 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
564 ==> (p e_fan) permutes (d_fan (x,V,E))`,
566 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
567 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (e_fan x V E) (d1_fan (x:real^3,V,E))`]
570 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
571 THEN REPEAT STRIP_TAC
572 THEN ASM_REWRITE_TAC[];
574 MRESA_TAC into_domain_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
575 THEN REPEAT STRIP_TAC
576 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
577 THENL[EXISTS_TAC`y:real^3#real^3#real^3#real^3`
578 THEN ASM_REWRITE_TAC[res];
579 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
580 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
581 THEN REWRITE_TAC[res]
582 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
583 THEN ASM_REWRITE_TAC[]
584 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
585 THEN ASM_TAC THEN SET_TAC[]]]);;
587 let into_domain_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
588 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
589 ==> (!y. y IN d_fan (x,V,E)==> ((p f1_fan ) y) IN (d_fan (x,V,E)))`,
591 THEN ASM_REWRITE_TAC[res;]
592 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
596 THEN POP_ASSUM MP_TAC
597 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
599 THEN ASM_REWRITE_TAC[]
600 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
601 THEN MATCH_MP_TAC(SET_RULE`x,w,inverse1_sigma_fan x V E w v,v IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E)
602 ==>x,w,inverse1_sigma_fan x V E w v,v IN d_fan (x:real^3,V,E)`)
603 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
604 THEN EXISTS_TAC`x:real^3`
605 THEN EXISTS_TAC`w:real^3`
606 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
607 THEN EXISTS_TAC`(v:real^3)`
608 THEN ASM_REWRITE_TAC[]
609 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
610 THEN REMOVE_ASSUM_TAC
611 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
612 THEN POP_ASSUM MP_TAC
613 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
615 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
616 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
617 THEN POP_ASSUM MP_TAC
618 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
620 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
621 THEN ASM_REWRITE_TAC[]]);;
626 let into_domain1_f1_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
627 FAN(x,V,E)==> (!y. y IN d1_fan (x,V,E)==> (f1_fan x V E y IN d1_fan (x,V,E)))`,
629 THEN ASM_REWRITE_TAC[]
630 THEN POP_ASSUM MP_TAC
631 THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM]
633 THEN EXISTS_TAC`x:real^3`
634 THEN EXISTS_TAC`w:real^3`
635 THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3`
636 THEN EXISTS_TAC`(v:real^3)`
637 THEN ASM_REWRITE_TAC[]
638 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
639 THEN REMOVE_ASSUM_TAC
640 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
641 THEN POP_ASSUM MP_TAC
642 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
644 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)])
645 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
646 THEN POP_ASSUM MP_TAC
647 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
649 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
650 THEN ASM_REWRITE_TAC[]);;
656 let f1_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
657 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
658 ==> (p f1_fan) permutes (d_fan (x,V,E))`,
661 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
662 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (f1_fan x V E) (d1_fan (x:real^3,V,E))`]
665 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
666 THEN REPEAT STRIP_TAC
667 THEN ASM_REWRITE_TAC[];
668 MRESA_TAC into_domain_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
669 THEN REPEAT STRIP_TAC
670 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
672 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
673 THEN ASM_REWRITE_TAC[res];
674 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
675 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
676 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
677 THEN REWRITE_TAC[res]
678 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
679 THEN ASM_REWRITE_TAC[]
680 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
681 THEN ASM_TAC THEN SET_TAC[]]]);;
687 let into_domain_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
688 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
689 ==> (!y. y IN d_fan (x,V,E)==> ((p n_fan ) y) IN (d_fan (x,V,E)))`,
691 THEN ASM_REWRITE_TAC[res;]
692 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
696 THEN POP_ASSUM MP_TAC
697 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
699 THEN ASM_REWRITE_TAC[]
700 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
701 THEN MATCH_MP_TAC(SET_RULE`x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E)
702 ==>x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d_fan (x:real^3,V,E)`)
703 THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM]
704 THEN EXISTS_TAC`x:real^3`
705 THEN EXISTS_TAC`v:real^3`
706 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
707 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
708 THEN ASM_REWRITE_TAC[]
709 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
710 THEN POP_ASSUM MP_TAC
711 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
712 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]]);;
716 let into_domain1_n_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
717 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (n_fan x V E y IN d1_fan (x,V,E)))`,
719 THEN POP_ASSUM MP_TAC
720 THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM]
722 THEN ASM_REWRITE_TAC[]
723 THEN EXISTS_TAC`x:real^3`
724 THEN EXISTS_TAC`v:real^3`
725 THEN EXISTS_TAC`sigma_fan x V E v w:real^3`
726 THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))`
727 THEN ASM_REWRITE_TAC[]
728 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
729 THEN POP_ASSUM MP_TAC
730 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
731 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]);;
735 let n_fan_permutes=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
736 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
737 ==> (p n_fan) permutes (d_fan (x,V,E))`,
740 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
741 THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (n_fan x V E) (d1_fan (x:real^3,V,E))`]
744 REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]
745 THEN REPEAT STRIP_TAC
746 THEN ASM_REWRITE_TAC[];
747 MRESA_TAC into_domain_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
748 THEN REPEAT STRIP_TAC
749 THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`)
751 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
752 THEN ASM_REWRITE_TAC[res];
753 MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
754 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
755 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
756 THEN REWRITE_TAC[res]
757 THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3`
758 THEN ASM_REWRITE_TAC[]
759 THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
760 THEN ASM_TAC THEN SET_TAC[]]]);;
763 let id_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3.
764 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
765 ==> (p e_fan) y=y /\ (p n_fan) y=y/\ (p f1_fan) y=y`,
767 THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
769 let id_power_enf_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3 n:num p.
770 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E))
771 ==> ((p e_fan) POWER n) y=y /\ ((p n_fan) POWER n)y=y/\ ((p f1_fan) POWER n) y=y`,
772 (let lem=prove(`!f:A->A x:A. f x = x ==> !m. (f POWER m) x = x`,
773 MRESA_TAC power_map_fix_point[`1:num`]
774 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[POWER_1;ARITH_RULE`m*1=m:num`]) in
776 THEN MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`y:real^3#real^3#real^3#real^3`]
777 THEN MRESA_TAC lem[`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
778 THEN MRESA_TAC lem[`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
779 THEN MRESA_TAC lem[`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]));;
784 let into_domain_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
785 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
786 ==> (!y. y IN d1_fan (x,V,E)==> (p e_fan ) y = e_fan x V E y)
787 /\ (!y. y IN d1_fan (x,V,E)==> (p n_fan ) y = n_fan x V E y)
788 /\(!y. y IN d1_fan (x,V,E)==> (p f1_fan ) y = f1_fan x V E y)
791 THEN ASM_REWRITE_TAC[res;]);;
796 let power_map_fix_set = prove(`!n f:A->A g:A->A s:A->bool. (!x:A. x IN s ==> f x= g x) /\ (!x:A. x IN s ==> g x IN s) ==> (!x. x IN s==>(f POWER n) x = (g POWER n) x)`,
797 INDUCT_TAC THENL[REWRITE_TAC[MULT; POWER; I_THM];
798 REWRITE_TAC[POWER; o_DEF] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
799 THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
800 POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_THEN(LABEL_TAC"NHO") THEN DISCH_TAC
801 THEN REMOVE_THEN "YEU" (fun th -> MRESA_TAC th[`f:A->A`;`g:A->A`;`s:A->bool`])
802 THEN POP_ASSUM (fun th-> MRESA1_TAC th `g (x:A):A`)
803 THEN POP_ASSUM MP_TAC
804 THEN REMOVE_THEN "EM" (fun th -> MRESA1_TAC th `x:A`)
805 THEN REMOVE_THEN "NHO" (fun th -> MRESA1_TAC th `x:A`)]);;
812 let into_domain_power_efn_fan=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num p.
813 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)))
814 ==> (!y. y IN d1_fan (x,V,E)==> ((p e_fan ) POWER n)y = ((e_fan x V E) POWER n) y)
815 /\ (!y. y IN d1_fan (x,V,E)==> ((p n_fan ) POWER n) y = ((n_fan x V E) POWER n) y)
816 /\(!y. y IN d1_fan (x,V,E)==> ((p f1_fan ) POWER n) y = ((f1_fan x V E) POWER n) y)`,
817 REPEAT GEN_TAC THEN REPEAT DISCH_TAC
818 THEN MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
819 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
820 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
821 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
822 THEN MRESA_TAC power_map_fix_set[`n:num`;
823 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
824 `(e_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
825 THEN MRESA_TAC power_map_fix_set[`n:num`;
826 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
827 `(n_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]
828 THEN MRESA_TAC power_map_fix_set[`n:num`;
829 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
830 `(f1_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]);;
835 let power_fun_in_domain=prove(`!n f:A->A s:A->bool.(!y. y IN s==> f y IN s)==> (!y. y IN s==> (f POWER n) y IN s)`,
836 INDUCT_TAC THENL[REWRITE_TAC[POWER_0; I_THM];
837 POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU")
838 THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`f:A->A`;`s:A->bool`])
839 THEN REWRITE_TAC[COM_POWER;o_DEF]
840 THEN POP_ASSUM (fun th-> MRESA1_TAC th`y:A`)]);;
844 let into_domain1_power_efn_fan= prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num.
845 FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (((e_fan x V E) POWER n) y IN d1_fan (x,V,E)))
846 /\ (!y. y IN d1_fan (x,V,E)==> (((n_fan x V E) POWER n) y IN d1_fan (x,V,E)))
847 /\(!y. y IN d1_fan (x,V,E)==> (((f1_fan x V E) POWER n) y IN d1_fan (x,V,E)))`,
848 REPEAT GEN_TAC THEN DISCH_TAC
849 THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
850 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
851 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;]
852 THEN MRESA_TAC power_fun_in_domain[`n:num`;`e_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
853 THEN MRESA_TAC power_fun_in_domain[`n:num`;`f1_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]
854 THEN MRESA_TAC power_fun_in_domain[`n:num`;`n_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]);;
861 let lemma_hypermap1_of_fanx=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool).
862 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==>
863 (p e_fan) o (p n_fan) o (p f1_fan)= I`,
865 THEN MATCH_MP_TAC EQ_EXT
866 THEN ASM_REWRITE_TAC[I_THM;o_DEF]
868 THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
870 MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x':real^3#real^3#real^3#real^3`];
871 MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
872 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
873 THEN REMOVE_ASSUM_TAC
874 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
875 THEN POP_ASSUM MP_TAC
876 THEN POP_ASSUM MP_TAC
877 THEN DISCH_THEN (LABEL_TAC"YEU")
878 THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
879 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )
881 THEN REMOVE_ASSUM_TAC
882 THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `(n_fan x V E (f1_fan x V E x')):real^3#real^3#real^3#real^3` )
883 THEN POP_ASSUM MP_TAC
884 THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
885 THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` )
887 THEN MRESA_TAC condition_hypermap_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`]
888 THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )]);;
898 let hypermap_of_fan_rep=prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) p.
899 FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==>
900 dart ( hypermap1_of_fanx (x,V,E)) =d_fan (x,V,E) /\ edge_map (hypermap1_of_fanx (x,V,E)) = p e_fan /\ node_map (hypermap1_of_fanx (x,V,E)) = p n_fan /\ face_map (hypermap1_of_fanx (x,V,E)) = p f1_fan `,
901 REPEAT GEN_TAC THEN DISCH_TAC
902 THEN REWRITE_TAC[hypermap1_of_fanx]
903 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
904 THEN ASM_REWRITE_TAC[]
905 THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
906 THEN MRESA_TAC e_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
907 THEN MRESA_TAC n_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
908 THEN MRESA_TAC f1_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
909 THEN MRESA_TAC lemma_hypermap1_of_fanx[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`]
910 THEN MRESA_TAC lemma_hypermap_rep[`d_fan (x:real^3,V,E):real^3#real^3#real^3#real^3->bool`;
911 `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
912 `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;
913 `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`]);;
915 let properties_of_f1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y y1.
916 FAN(x,V,E) /\ y = f1_fan x V E y1 /\ y1 IN d1_fan (x,V,E)
917 ==> pr3 y1 =pr2 y /\ {pr2 y1, pr3 y1} IN E /\ {pr2 y, pr3 y} IN E /\
918 pr2 y1= sigma_fan x V E (pr2 y) (pr3 y)`,
921 THEN POP_ASSUM MP_TAC
922 THEN REWRITE_TAC[d1_fan; IN_ELIM_THM]
924 THEN ASM_REWRITE_TAC[pr2;pr3;f1_fan]
925 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`w:real^3`]
926 THEN REMOVE_ASSUM_TAC
927 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
928 THEN POP_ASSUM MP_TAC
929 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
931 THEN REMOVE_ASSUM_TAC
932 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
933 THEN POP_ASSUM MP_TAC
934 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
936 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
937 THEN ASM_REWRITE_TAC[]);;
941 (* ========================================================================== *)
942 (* PROPERTIES OF HYPERMAP OF FAN (^_^) *)
943 (* ========================================================================== *)
947 let face_subset_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
949 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
950 ==> ds SUBSET d_fan (x,V,E)`,
951 REPEAT GEN_TAC THEN STRIP_TAC
952 THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`]
953 THEN MRESA_TAC hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
954 THEN MRESA_TAC lemma_face_subset[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]);;
959 let properties_of_elements_in_face_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y.
961 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
963 ==> {pr2 y, pr3 y} IN E\/ pr2 y= pr3 y`,
964 REPEAT GEN_TAC THEN STRIP_TAC
965 THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
966 THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`)
968 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM]
970 THEN ASM_REWRITE_TAC[pr2;pr3]);;
972 let fully_surrounded_is_non_isolated_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
974 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
975 ==> d20_fan(x,V,E)={}`,
977 THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU")
978 THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`]
979 THEN REWRITE_TAC[d20_fan;IN_ELIM_THM]
981 THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES])
982 THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
988 let AAUHTVE=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool).
989 FAN(x,V,E)/\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==>
990 FINITE (d_fan (x,V,E))
991 /\ (p e_fan) permutes (d_fan (x,V,E))
992 /\ (p n_fan) permutes (d_fan (x,V,E))
993 /\ (p f1_fan) permutes (d_fan (x,V,E))
994 /\(p e_fan) o (p n_fan) o (p f1_fan)= I
995 /\ (!a. a IN d1_fan(x,V,E)==> (e_fan x V E) (e_fan x V E a) =a)
996 /\ (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))
997 /\ (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))
998 /\ (!k:num l:num a. a IN d1_fan(x,V,E) ==>
999 (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)
1001 /\ (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a))`,
1003 MESON_TAC[lemma_hypermap1_of_fanx;e_fan_permutes;n_fan_permutes;finite_d_fan;f1_fan_permutes;plain_hypermap_fan;e_fan_no_fix_point;f_fan_no_fix_point;distinct_nodes;edge_lie_different_nodes]);;
1005 (********************************)