2 module Node_fan = struct
10 open Hypermap_of_fan;;
14 (* ========================================================================== *)
15 (* NODE OF HYPERMAP OF FAN (^_^) *)
16 (* ========================================================================== *)
20 let CARD_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3).
22 CARD( IMAGE (sigma_fan x V E v) (set_of_edge v V E))= CARD(set_of_edge v V E)
25 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN STRIP_TAC
27 REPEAT GEN_TAC THEN STRIP_TAC THEN
28 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`x':real^3`]properties_of_set_of_edge_fan)
29 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
30 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`y:real^3`]properties_of_set_of_edge_fan)
31 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
32 ASM_MESON_TAC[MONO_SIGMA_FAN];
33 POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN MESON_TAC[remark_finite_fan1]]);;
35 let MONO_AZIM_SIGMA_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
36 FAN(x,V,E) /\ ({v,u} IN E)
37 /\ ({v,w} IN E) /\ ~(sigma_fan x V E v w =u)
38 ==> (azim x v u w <= azim x v u (sigma_fan x V E v w))`,
40 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1")
41 THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6]
43 THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN
44 DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b")
45 THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
46 THEN DISJ_CASES_TAC(SET_RULE`({(w:real^3)}=set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) \/ ~({(w:real^3)}=set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`)
48 ASM_REWRITE_TAC[sigma_fan] THEN REAL_ARITH_TAC;(*1*)
50 DISJ_CASES_TAC(SET_RULE`((u:real^3)=(w:real^3))\/ ~(u=w)`)
53 ASM_REWRITE_TAC[AZIM_REFL] THEN MESON_TAC[azim];(*2*)
55 DISJ_CASES_TAC(SET_RULE`(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) <= azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) ) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) <= azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) )`)
57 ASM_REWRITE_TAC[];(*3*)
59 SUBGOAL_THEN`azim (x:real^3) (v:real^3) (u:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))
60 <= azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) ` ASSUME_TAC
62 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*)
64 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge)
65 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
66 MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge)
67 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
68 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN)
69 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
70 THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "c") THEN
71 SUBGOAL_THEN `{(u:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(w:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC
73 ASM_TAC THEN SET_TAC[];(*5*)
75 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
76 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
77 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(u:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(w:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
78 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
79 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (w:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
80 THEN SUBGOAL_THEN `azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (w:real^3)<= azim x v u w` ASSUME_TAC
83 MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`]azim) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*)
85 POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[])THEN ASM_REWRITE_TAC[] THEN
86 MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge)
87 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
88 THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
89 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
90 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))}`th) THEN ASSUME_TAC(th))
91 THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`]
92 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]
94 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
96 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN)
97 THEN ASM_TAC THEN SET_TAC[];(*7*)
99 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3) = &0)`)
102 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
103 THEN ASM_TAC THEN SET_TAC[];(*8*)
105 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`w:real^3`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]AZIM_COMPL)
106 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
107 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL)
108 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - a<= &2 * pi - (b:real) <=> b<= (a:real)`]
109 THEN REMOVE_THEN "c" (fun th -> MP_TAC(ISPEC `u:real^3` th) ) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN STRIP_TAC
110 THEN SUBGOAL_THEN `azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = azim x v w u` ASSUME_TAC
113 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*9*)
115 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;`u:real^3`]UNIQUE_AZIM_POINT_FAN)
116 THEN ASM_REWRITE_TAC[]]]]]]]]]]);;
121 let MONO_POWER_SIGMA_FAN=prove(`!(i:num) (j:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
122 FAN(x,V,E) /\ ({v,u} IN E)/\(j<i)/\
123 (power_map_points sigma_fan x V E v u i)= (power_map_points sigma_fan x V E v u j)
124 ==> u=power_map_points sigma_fan x V E v u (i-j)`,
129 [REWRITE_TAC[ARITH_RULE `SUC i- 0 =SUC (i:num)`;power_map_points] THEN ASM_TAC THEN SET_TAC[];
131 REWRITE_TAC[ARITH_RULE `SUC (i:num)-SUC (j:num)= i - j`; ARITH_RULE `SUC(j:num) < SUC (i) <=> j < i`;power_map_points]
132 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC
133 THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
134 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]properties_of_set_of_edge_fan)
135 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
136 THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
138 THEN MP_TAC(ISPECL[`(j:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
140 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`]properties_of_set_of_edge_fan)
141 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
142 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (j:num)`]properties_of_set_of_edge_fan)
143 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
144 THEN MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (j:num)`]MONO_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
146 THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPECL[`(j:num) `;`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]th))
147 THEN ASM_REWRITE_TAC[]]]);;
154 let MONO_POWER_MAP_POINTS1_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
155 FAN(x,V,E) /\ (u IN set_of_edge v V E) /\ ~(set_of_edge v V E={u})
156 ==> ~(power_map_points (sigma_fan) x V E v u i=power_map_points (sigma_fan) x V E v u (SUC i))
159 REWRITE_TAC[power_map_points] THEN REPEAT GEN_TAC THEN STRIP_TAC
160 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN) THEN ASM_MESON_TAC[];
161 REPEAT GEN_TAC THEN POP_ASSUM
162 (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 REWRITE_TAC[power_map_points]
163 THEN STRIP_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC)
164 THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b")
165 THEN USE_THEN "b" MP_TAC THEN REWRITE_TAC[FAN]
167 THEN DISCH_TAC THEN DISCH_TAC
168 THEN REMOVE_THEN "a" MP_TAC THEN MP_TAC(ARITH_RULE `SUC (i:num)< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> i < CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`)
169 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
170 THEN MATCH_MP_TAC MONO_NOT THEN DISCH_TAC
171 THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
173 THEN MP_TAC(ISPECL[`SUC (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]
175 THEN MP_TAC(ISPECL[` (v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`] properties_of_set_of_edge)
176 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
177 THEN MP_TAC(ISPECL[` (v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (SUC (i:num)))`] properties_of_set_of_edge)
178 THEN ASM_REWRITE_TAC[power_map_points] THEN DISCH_TAC
179 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num)`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))`]MONO_SIGMA_FAN)
180 THEN ASM_MESON_TAC[]]);;
190 let set_of_orbits_points_fan = new_definition `set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = {power_map_points sigma_fan x V E v u i| 0<=i }`;;
192 let number_of_orbits_fan = new_definition `number_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;;
196 let addition_sigma_fan = prove(`!(m:num) (n:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
197 power_map_points sigma_fan x V E v u (m + n) = (power_map_points sigma_fan x V E v (power_map_points sigma_fan x V E v u n) m) `,
200 REWRITE_TAC[power_map_points; ARITH_RULE`0 + n:num =n`];
201 REWRITE_TAC[ARITH_RULE` SUC (m:num) + n= SUC(m+n)`; power_map_points] THEN REPEAT GEN_TAC
202 THEN POP_ASSUM(ASSUME_TAC o GSYM o (ISPECL[`(n:num) `;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]))
203 THEN ASM_TAC THEN SET_TAC[]]);;
210 let fix_point_sigma_fan=prove(`! (q:num) (i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
211 (power_map_points (sigma_fan) x V E v u i=u)
212 ==>power_map_points sigma_fan x V E v u (q * i)=u
215 ASM_REWRITE_TAC[ARITH_RULE`0 * i:num = 0`;power_map_points];
216 REWRITE_TAC[ARITH_RULE`SUC q * i:num= q * i + i`] THEN REPEAT GEN_TAC THEN
217 POP_ASSUM(MP_TAC o (ISPECL[`(i:num) `;`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]))
218 THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[addition_sigma_fan]]);;
220 let i_IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num).
221 power_map_points (sigma_fan) x V E v u i IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
222 REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN EXISTS_TAC`i:num` THEN REWRITE_TAC[power_map_points] THEN SIMP_TAC[] THEN ARITH_TAC);;
224 let u_IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
225 u IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
226 REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN EXISTS_TAC`0` THEN REWRITE_TAC[power_map_points] THEN SIMP_TAC[] THEN ARITH_TAC);;
229 let IN_ORBITS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3).
230 w IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
231 ==> sigma_fan x V E v w IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
233 REPEAT GEN_TAC THEN REWRITE_TAC[set_of_orbits_points_fan; IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`SUC i` THEN ASM_REWRITE_TAC[power_map_points] THEN ARITH_TAC);;
236 let ORBITS_SUBSET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
237 FAN(x,V,E) /\ ({v,u} IN E)
238 ==> set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
239 SUBSET set_of_edge v V E`,
240 REPEAT GEN_TAC THEN STRIP_TAC
241 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]properties_of_set_of_edge_fan)
242 THEN ASM_REWRITE_TAC[set_of_orbits_points_fan;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN GEN_TAC THEN STRIP_TAC
243 THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]image_power_map_points) THEN ASM_REWRITE_TAC[]);;
246 let CARD_ORBITS_EDGE_FAN_LE=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
247 FAN(x,V,E) /\ ({v,u} IN E)
248 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) )
249 <=CARD( set_of_edge v V E)`,
250 REPEAT GEN_TAC THEN STRIP_TAC
251 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]ORBITS_SUBSET_EDGE_FAN)
252 THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC)
253 THEN REWRITE_TAC[FAN;fan1] THEN REPEAT STRIP_TAC
254 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`] remark_finite_fan1)
255 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]CARD_SUBSET)
256 THEN ASM_REWRITE_TAC[]);;
261 let FINITE_ORBITS_SIGMA_FAN=prove( `!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
262 FAN(x,V,E) /\ ({v,u} IN E)
263 ==> FINITE(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) `,
265 REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`] ORBITS_SUBSET_EDGE_FAN)THEN ASM_REWRITE_TAC[]
266 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC
267 THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`] remark_finite_fan1)
268 THEN ASM_REWRITE_TAC[] THEN MESON_TAC[FINITE_SUBSET]);;
272 let ORBITS_SIGMA_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
273 FAN(x,V,E) /\ ({v,u} IN E)/\
274 (power_map_points (sigma_fan) x V E v u i=u) /\ ~(i=0)
275 ==> set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) =
276 {power_map_points sigma_fan x V E v u j| j < i }
278 REPEAT STRIP_TAC THEN REWRITE_TAC[set_of_orbits_points_fan; EXTENSION; IN_ELIM_THM]
279 THEN GEN_TAC THEN EQ_TAC
281 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
282 FIND_ASSUM (MP_TAC o (SPEC `i':num`) o MATCH_MP DIVMOD_EXIST) `~(i:num = 0)`
283 THEN REPEAT STRIP_TAC
284 THEN EXISTS_TAC`r:num` THEN ASM_REWRITE_TAC[ARITH_RULE`q * (i:num) + r = r+ q * i`;addition_sigma_fan]
285 THEN MP_TAC (SPECL [`(q:num)`;` (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`]fix_point_sigma_fan) THEN ASM_REWRITE_TAC[]
286 THEN DISCH_TAC THEN ASM_REWRITE_TAC[];
288 STRIP_TAC THEN EXISTS_TAC `j:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC]);;
290 (***********lemmas in hypermap.ml***************)
293 let IMAGE_SEG = prove(`!(n:num) (f:num->A). IMAGE f {i:num | i < n:num} = {f (i:num) | i < n}`,
295 THEN REWRITE_TAC[IMAGE; IN_ELIM_THM] THEN ASM_SET_TAC[]);;
297 let FINITE_SERIES = prove(`!(n:num) (f:num->A). FINITE {f(i) | i < n}`,
299 THEN ONCE_REWRITE_TAC[SYM(SPECL[`n:num`; `f:num->A`] IMAGE_SEG)]
300 THEN MATCH_MP_TAC FINITE_IMAGE
301 THEN REWRITE_TAC[FINITE_NUMSEG_LT]);;
303 let CARD_FINITE_SERIES_LE = prove(`!(n:num) (f:num->A). CARD {f(i) | i < n} <= n`,
305 THEN ONCE_REWRITE_TAC[SYM(SPECL[`n:num`; `f:num->A`] IMAGE_SEG)]
306 THEN MP_TAC(ISPEC `f:num ->A` (MATCH_MP CARD_IMAGE_LE (SPEC `n:num` FINITE_NUMSEG_LT)))
307 THEN REWRITE_TAC[CARD_NUMSEG_LT]);;
309 let LEMMA_INJ = prove(`!(n:num) (f:num->A).(!i:num j:num. i < n /\ j < i ==> ~(f i = f j)) ==> (!i:num j:num. i < n /\ j < n /\ f i = f j ==> i = j)`,
311 THEN DISCH_TAC THEN MATCH_MP_TAC WLOG_LT
312 THEN STRIP_TAC THENL[ARITH_TAC; ALL_TAC]
313 THEN STRIP_TAC THENL[MESON_TAC[]; ALL_TAC]
314 THEN ASM_MESON_TAC[]);;
316 let CARD_FINITE_SERIES_EQ = prove(`!(n:num) (f:num->A). (!i:num j:num. i < n /\ j < i ==> ~(f i = f j)) ==> CARD {f(i) | i < n} = n`,
318 THEN DISCH_THEN (LABEL_TAC "F1" o MATCH_MP LEMMA_INJ)
319 THEN ONCE_REWRITE_TAC[GSYM IMAGE_SEG]
320 THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV) [GSYM (SPEC `n:num` CARD_NUMSEG_LT)]
321 THEN MATCH_MP_TAC CARD_IMAGE_INJ
322 THEN REWRITE_TAC[FINITE_NUMSEG_LT]
323 THEN REWRITE_TAC[IN_ELIM_THM]
324 THEN ASM_REWRITE_TAC[]);;
328 (**************************************)
331 let CARD_ORBITS_SIGMA_FAN_LE=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
332 FAN(x,V,E) /\ ({v,u} IN E)/\
333 (power_map_points (sigma_fan) x V E v u i=u) /\ ~(i=0)
334 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))<=i`,
336 REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
337 THEN MP_TAC(ISPECL[`i:num`;`power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_LE) THEN ASM_TAC THEN SET_TAC[]);;
342 let exists_inverse_in_orbits_sigma_fan=prove(`
343 !(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (y:real^3).
344 FAN(x,V,E) /\({v,u} IN E)/\ ~(y IN set_of_orbits_points_fan x V E v u)
346 (?(w:real^3). (w IN (set_of_orbits_points_fan x V E v u)) /\ ~(w=y) /\
347 (!(w1:real^3). (w1 IN (set_of_orbits_points_fan x V E v u))/\ ~(w1=y) ==> azim1 x v y w <= azim1 x v y w1))
352 FINITE X /\ ~(X = {})
353 ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
354 MESON_TAC[INF_FINITE]) in
356 MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC
357 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "ba")
358 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan)
359 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
360 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
362 SUBGOAL_THEN `FINITE ((set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) (v:real^3) (u:real^3) DELETE (y:real^3))` ASSUME_TAC
365 ASM_MESON_TAC[FINITE_DELETE_IMP];(*1*)
366 DISJ_CASES_TAC(SET_RULE`(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE (y:real^3)={})\/
367 ~(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE (y:real^3)={})`)
369 MP_TAC (ISPECL[`y:real^3`;`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]DELETE_NON_ELEMENT)
370 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
371 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`v:real^3`;` (u:real^3)`]u_IN_ORBITS_FAN)
372 THEN ASM_TAC THEN SET_TAC[];(*2*)
373 SUBGOAL_THEN`~(IMAGE ( azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE (y:real^3))={})` ASSUME_TAC
375 REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*3*)
377 SUBGOAL_THEN` FINITE (IMAGE (azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE (y:real^3)))` ASSUME_TAC
379 ASM_MESON_TAC[FINITE_IMAGE];(*4*)
381 REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v y) (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) DELETE (y:real^3)))` th))
382 THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
383 THEN EXISTS_TAC`x':real^3`
384 THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]]]]));;
393 let key_lemma_cyclic_fan=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
394 FAN(x,V,E) /\ (0 < i) /\(i< CARD(set_of_edge v V E)) /\ ({v,u} IN E)
395 ==> ~(power_map_points (sigma_fan) x V E v u i=u)
398 THENL(*1*)[ARITH_TAC;(*1*)
399 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points] THEN
400 MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]ORBITS_SUBSET_EDGE_FAN)
401 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
402 THEN DISJ_CASES_TAC(SET_RULE`(sigma_fan x V E v (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))= u)\/ ~(sigma_fan x V E v (power_map_points sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num))= u)`)
404 ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`SUC (i:num)`;` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_ORBITS_SIGMA_FAN_LE)
405 THEN ASM_REWRITE_TAC[power_map_points; ARITH_RULE`~(SUC i = 0)`] THEN STRIP_TAC
406 THEN SUBGOAL_THEN `CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) <CARD(set_of_edge v V E)` ASSUME_TAC
408 REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC;(*3*)
410 SUBGOAL_THEN `set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) PSUBSET set_of_edge v V E` ASSUME_TAC
412 ASM_REWRITE_TAC[PSUBSET] THEN DISJ_CASES_TAC(SET_RULE`(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = set_of_edge v V E)\/ ~(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) = set_of_edge v V E)`)
414 SUBGOAL_THEN`CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) =CARD( set_of_edge v V E)`ASSUME_TAC
416 POP_ASSUM(fun th->REWRITE_TAC[th]);(*6*)
417 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC](*6*);(*5*)
419 POP_ASSUM(fun th->REWRITE_TAC[th])](*5*);(*4*)
422 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSUBSET_MEMBER] THEN STRIP_TAC
423 THEN MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`y:real^3`]
424 exists_inverse_in_orbits_sigma_fan)
425 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)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`)
427 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
428 THEN DISCH_THEN(LABEL_TAC "b") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN DISCH_TAC
429 THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[u_IN_ORBITS_FAN];(*5*)
431 ASM_REWRITE_TAC[] THEN STRIP_TAC
432 THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
433 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:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})`)
436 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")
437 THEN DISCH_THEN(LABEL_TAC "b") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[IN_SING] THEN DISCH_TAC
438 THEN REMOVE_THEN "b" MP_TAC THEN ASM_REWRITE_TAC[];(*6*)
440 MP_TAC(ISPECL[` (x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`u:real^3`;` (w:real^3)`]IN_ORBITS_FAN)
441 THEN ASM_REWRITE_TAC[]
442 THEN STRIP_TAC THEN STRIP_TAC
443 THEN POP_ASSUM(fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)` th))
444 THEN ASM_REWRITE_TAC[]
445 THEN DISJ_CASES_TAC(SET_RULE`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)=(y:real^3) \/ ~(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)=(y:real^3))`)
447 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC
448 THEN ASM_REWRITE_TAC[];(*7*)
450 ASM_REWRITE_TAC[azim1;REAL_ARITH` (a:real) - b <= a - c <=> c<=b`] THEN STRIP_TAC
452 SUBGOAL_THEN `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3) IN set_of_edge v V E` ASSUME_TAC
454 ASM_TAC THEN SET_TAC[];(*8*)
456 SUBGOAL_THEN `(w:real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ASSUME_TAC
458 ASM_TAC THEN SET_TAC[];(*9*)
460 SUBGOAL_THEN `{(y:real^3),sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3),(w:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC
463 ASM_TAC THEN SET_TAC[];(*10*)
465 FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN
466 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
467 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN)
468 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
469 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(y:real^3),sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3),(w:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan)
470 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
471 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`y:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`;`w:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[]
472 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`y:real^3`;`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`]azim)
473 THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (w:real^3) <= azim (x:real^3) (v:real^3) (y:real^3) (w:real^3)`
476 REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*11*)
478 POP_ASSUM MP_TAC THEN POP_ASSUM(fun th ->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN
479 MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (y:real^3)`]properties_of_set_of_edge_fan)
480 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
481 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan)
482 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
483 THEN MP_TAC (ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge_fan)
484 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
486 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (y:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (y:real^3) = &0)`)
488 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(y:real^3)`]UNIQUE_AZIM_0_POINT_FAN)
489 THEN ASM_REWRITE_TAC[];(*12*)
491 DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`)
493 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`; ` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ]UNIQUE_AZIM_0_POINT_FAN)
494 THEN ASM_REWRITE_TAC[]
495 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`] SIGMA_FAN)
496 THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN SET_TAC[];(*13*)
498 REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
499 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(y:real^3)}`th) THEN ASSUME_TAC(th))
500 THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))}`th) THEN ASSUME_TAC(th))
501 THEN REWRITE_TAC[SET_RULE`{(a:real^3)} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[]
502 THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
503 MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]AZIM_COMPL)
504 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
505 THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (y:real^3)`]AZIM_COMPL) THEN
506 ASM_REWRITE_TAC[] THEN DISCH_TAC
507 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH`(a - (b:real) <= (a:real)- (c:real))<=> c <= b`]
509 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`; `(w:real^3)`] SIGMA_FAN)
510 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(y:real^3)`th))
511 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
512 THEN SUBGOAL_THEN`azim (x:real^3) (v:real^3) (w:real^3) (y:real^3) = azim x v w (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ASSUME_TAC
514 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*14*)
516 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(w:real^3)`;` (y:real^3)`; ` (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))` ]UNIQUE_AZIM_POINT_FAN)
517 THEN ASM_REWRITE_TAC[]
520 ASM_REWRITE_TAC[]]]);;
526 let cyclic_power_sigma_fan=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) (j:num).
527 FAN(x,V,E) /\ (i< CARD(set_of_edge v V E)) /\ (j<i) /\ ({v,u} IN E)
528 ==> ~(power_map_points (sigma_fan) x V E v u i= power_map_points (sigma_fan) x V E v u j)
531 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
532 MP_TAC(ISPECL[`(i:num)`;` (j:num)`;` (x:real^3)`;` (V:real^3->bool)`;
533 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]MONO_POWER_SIGMA_FAN)
534 THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE` j < i ==> 0 < (i:num)-(j:num)`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
535 THEN MP_TAC(ARITH_RULE` (j:num) <(i:num)==> i-j <= i`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
536 THEN MP_TAC(ARITH_RULE` (i :num )-(j:num) <= i /\ i< CARD(set_of_edge (v:real^3)(V:real^3->bool) (E:(real^3->bool)->bool))==> i-j <CARD(set_of_edge (v:real^3)(V:real^3->bool) (E:(real^3->bool)->bool))`) THEN ASM_REWRITE_TAC[]
538 THEN MP_TAC(ISPECL[`(i:num)-(j:num)`;` (x:real^3)`;` (V:real^3->bool)`;
539 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]key_lemma_cyclic_fan)
540 THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);;
546 let CARD_SET_OF_ORBITS_POINTS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
547 FAN(x,V,E) /\ ({v,u} IN E)
548 ==> CARD(set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))= CARD(set_of_edge v V E)`,
550 REPEAT GEN_TAC THEN STRIP_TAC THEN
551 SUBGOAL_THEN`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i| (i< CARD(set_of_edge v V E))}
552 SUBSET set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
554 THENL[ REWRITE_TAC[set_of_orbits_points_fan;SUBSET;IN_ELIM_THM]
555 THEN GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
557 SUBGOAL_THEN`CARD {power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i| (i< CARD(set_of_edge v V E))}
558 <= CARD (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`
561 MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
562 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`] FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
564 THEN MP_TAC(ISPECL[`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i| (i< CARD(set_of_edge v V E))}`;`set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_SUBSET) THEN ASM_REWRITE_TAC[];
566 MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
567 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
568 THEN MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_EQ)
569 THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
570 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
571 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_ORBITS_EDGE_FAN_LE)
572 THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC]]);;
575 let ORBITS_EQ_SET_EDGE_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
576 FAN(x,V,E) /\ ({v,u} IN E)
579 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`,
581 REWRITE_TAC[SET_RULE`(set_of_edge v V E
582 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))<=> (set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)= set_of_edge v V E) `] THEN
583 REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_SUBSET_EQ THEN
584 STRIP_TAC THENL[REPEAT (POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan1] THEN MESON_TAC[remark_finite_fan1];
585 ASM_MESON_TAC[ORBITS_SUBSET_EDGE_FAN;CARD_SET_OF_ORBITS_POINTS_FAN]]);;
588 let SIMP_ORBITS_POINTS_FAN=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3).
589 FAN(x,V,E) /\ ({v,u} IN E)
591 {power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i| (i< CARD(set_of_edge v V E))}
592 = set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
595 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`{power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) |i| (i< CARD(set_of_edge v V E))}
596 SUBSET set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)
599 REWRITE_TAC[set_of_orbits_points_fan;SUBSET;IN_ELIM_THM]
600 THEN GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
602 POP_ASSUM MP_TAC THEN MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
603 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]cyclic_power_sigma_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
604 THEN MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)`]CARD_FINITE_SERIES_EQ)
605 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"a")
606 THEN MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
607 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]CARD_SET_OF_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[SET_RULE`a=b<=> b=a`] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[]
608 THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;
609 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`] FINITE_ORBITS_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
610 THEN MESON_TAC[CARD_SUBSET_EQ]]);;
613 let ORDER_POWER_SIGMA_FAN=prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) .
614 FAN(x,V,E) /\ (i=CARD(set_of_edge v V E)) /\ ({v,u} IN E)
615 ==> power_map_points (sigma_fan) x V E v u i= u
617 REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `power_map_points (sigma_fan) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (i:num) IN set_of_orbits_points_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` ASSUME_TAC
619 REWRITE_TAC[ set_of_orbits_points_fan; IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
621 POP_ASSUM MP_TAC THEN MP_TAC(SPECL[`(x:real^3)`;` (V:real^3->bool)`;
622 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIMP_ORBITS_POINTS_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
623 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th);]) THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC
624 THEN ASM_REWRITE_TAC[] THEN
625 MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`;`i':num`;`(x:real^3)`;` (V:real^3->bool)`;
626 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]MONO_POWER_SIGMA_FAN) THEN ASM_REWRITE_TAC[]
627 THEN DISJ_CASES_TAC(ARITH_RULE`(0<(i':num))\/ i'=0`)
630 MP_TAC(ARITH_RULE`0 < (i':num)/\ i'< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) ==> (CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))- (i':num) < CARD (set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
631 THEN MP_TAC(ARITH_RULE`(i':num)< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))==> 0< CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))-i'`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
633 MP_TAC(ISPECL[`CARD(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))-(i':num)`; `(x:real^3)`;` (V:real^3->bool)`;
634 ` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]key_lemma_cyclic_fan)
635 THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[];
637 ASM_REWRITE_TAC[power_map_points]]]);;