1 (* Main estimate file*)
\r
2 (* Author: PHAN HOANG CHON *)
\r
3 (*========================================================*)
\r
6 needs "database_more.ml";;
\r
7 needs "definitions_kepler.ml";;
\r
8 (* removed convex.ml by thales, not compatible with other loads *)
\r
9 (* needs "Multivariate/convex.ml";; *)
\r
10 needs "geomdetail.ml";; (* Writen by Nguyen Quang TRuong *)
\r
13 (*========================================================*)
\r
14 (* These definitions are defined by other authors*)
\r
15 (*========================================================*)
\r
18 (*arctan2 function is defined in definition_kepler.ml*)
\r
20 let delta_tet = new_definition (`delta_tet = sqrt8 * atn2(&5, sqrt2)`);;
\r
22 let delta_oct = new_definition (`delta_oct = (( &3* pi_rt18 - delta_tet)*( &1 / &2 ))`);;
\r
24 (*========================================================*)
\r
26 let lambda_v = new_definition (`lambda_v = (-- &4)* delta_oct `);;
\r
28 let lambda_s = new_definition (`lambda_s = (&1)/(&3) `);;
\r
30 let lambda_oct = new_definition (`lambda_oct = (lambda_v , lambda_s) `);;
\r
32 (*========================================================*)
\r
34 (* benign redefinition *)
\r
35 let open_ball = new_definition `open_ball (x:real^3) (r:real)= { y | norm(y-x)< r }`;;
\r
39 (*========================================================*)
\r
41 (* There is a mistake in this definition. For example: let d={x,y,z,t} be a quarter with 2*t0<dist(x,y)<=sqrt8
\r
42 and dist(z,t)=2*t0, then diagonal {z ,t} d s is true, that means {z,t} is diagonal of d. But here {x,y} is really
\r
45 let diagonal = new_definition ` diagonal dgcheo d s = ( quarter d s /\
\r
46 ( ? x y. x IN d /\ y IN d /\ { x, y } = dgcheo /\ d3 x y >= &2 * t0 ))`;;
\r
49 (*========================================================*)
\r
52 let diag = new_definition ` diag d q s = ( quarter q s /\
\r
56 v1 IN q /\ v2 IN q /\
\r
57 { x, y } = d /\ d3 x y >= &2 * t0 /\
\r
58 d3 x y >= d3 v1 v2 ))`;;
\r
61 let find_diagonal = new_definition ` find_diagonal q s:real^3->bool = @{x, y}. {x , y} SUBSET q /\ diag {x , y} q s `;;
\r
63 let find_dia = new_definition ` find_dia q (s:real^3->bool) =
\r
64 let d = find_diagonal q s in
\r
65 @(u,v). u IN d /\ v IN d /\ ~( u = v ) `;;
\r
67 (* thales, nov 11. anchor is already defined in geomdetail.ml *)
\r
68 let anchor_alt = new_definition ` anchor_alt (v:real^3) v1 v2 = ( d3 v1 v2 <= sqrt ( &8 ) /\
\r
69 d3 v1 v2 >= &2 * t0 /\ d3 v v1 <= &2 * t0 /\ d3 v v2 <= &2 * t0 )`;;
\r
71 (* Definition 7.20 =============================================*)
\r
73 let context = new_definition ` context (v , w) s (p:num, r) = (
\r
74 CARD { d | diag { v , w } d s } = p /\
\r
75 CARD { t | &2 * t0 <= d3 v w /\ anchor_alt t v w } = (p + r ))`;;
\r
77 let cotext = new_definition ` cotext (v , w) (s:real^3->bool) = @( (p:num) , (r:num) ).
\r
78 CARD { d | diag { v , w } d s } = p /\
\r
79 CARD { t | &2 * t0 <= d3 v w /\ anchor_alt t v w } = (p + r )`;;
\r
81 (* Definition 7.21 =============================================*)
\r
83 let VC1 = new_definition ` VC1 v s d = VC v d INTER conv s `;;
\r
85 let VCt = new_definition ` VCt x t s d
\r
86 = VC1 x s d INTER open_ball x t `;;
\r
88 (* Definition 7.22 =============================================*)
\r
90 let sv = new_definition ` sv x p d = lambda_v * vol(VC1 x p d) + lambda_s * solid x (conv0 p) `;;
\r
92 let gamma = new_definition ` gamma (v1 , v2 , v3 , v4) d =
\r
93 ( &1 / &4 ) * ( sv v1 { v1 , v2 , v3 , v4 } d +
\r
94 sv v2 { v1 , v2 , v3 , v4 } d +
\r
95 sv v3 { v1 , v2 , v3 , v4 } d +
\r
96 sv v4 { v1 , v2 , v3 , v4 } d )`;;
\r
98 let volan = new_definition ` volan v0 (v0 , v1, v2, v3 ) =
\r
99 let x01 = dist(v0,v1) pow 2 in
\r
100 let x02 = dist(v0,v2) pow 2 in
\r
101 let x03 = dist(v0,v3) pow 2 in
\r
102 let x12 = dist(v1,v2) pow 2 in
\r
103 let x13 = dist(v1,v3) pow 2 in
\r
104 let x23 = dist(v2,v3) pow 2 in
\r
105 ( x01 * ( x02 + x12 - x01 ) * ( chi_x x23 x13 x03 x01 x02 x12 ) ) /
\r
106 ( &48 * (ups_x x01 x02 x12) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) +
\r
107 ( x01 * ( x03 + x13 - x01 ) * ( chi_x x23 x12 x02 x01 x03 x13 ) ) /
\r
108 ( &48 * (ups_x x01 x03 x13) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) +
\r
109 ( x02 * ( x01 + x12 - x02 ) * ( chi_x x13 x23 x03 x02 x01 x12 ) ) /
\r
110 ( &48 * (ups_x x02 x01 x12) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) +
\r
111 ( x01 * ( x03 + x23 - x02 ) * ( chi_x x13 x12 x01 x02 x03 x23 ) ) /
\r
112 ( &48 * (ups_x x02 x03 x23) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) +
\r
113 ( x02 * ( x01 + x13 - x03 ) * ( chi_x x12 x23 x02 x03 x01 x13 ) ) /
\r
114 ( &48 * (ups_x x03 x01 x13) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) +
\r
115 ( x02 * ( x02 + x23 - x03 ) * ( chi_x x12 x13 x01 x03 x02 x23 ) ) /
\r
116 ( &48 * (ups_x x03 x02 x23) * sqrt( delta_x x01 x02 x03 x23 x13 x12 )) `;;
\r
118 let svan =new_definition ` svan v0 ( v0 , v1, v2, v3) =
\r
119 lambda_v * volan v0 ( v0 , v1, v2, v3) +
\r
120 lambda_s * solid v0 ( conv0 { v0 , v1, v2, v3}) `;;
\r
122 (* Definition 7.23 =================================================*)
\r
124 let eta_pos = new_definition ` eta_pos (q:real^3->bool) (s:real^3->bool) =
\r
125 let d = find_diagonal q s in
\r
126 let f1 = d UNION ( @{u}. ( q DIFF d ) u ) in
\r
127 let f2 = d UNION ( @{v}. ( q DIFF f1) v ) in
\r
128 ( max_real ( radV f1 ) ( radV f2) )`;;
\r
130 (* The definition 7.24 =============================================*)
\r
132 let sv0 = new_definition ` sv0 v s d = sovo v (VCt v t0 s d) lambda_oct `;;
\r
134 let v_hat = new_definition `v_hat v q s = if ( quarter q s ) /\ ( v IN find_diagonal q s )
\r
135 then ( @u. u IN (find_diagonal q s DIFF {v} ))
\r
138 let sigma = new_definition ` sigma v0 ( v0 , v1 , v2, v3 ) ( s:real^3->bool ) =
\r
139 let q = { v0 , v1 , v2 , v3 } in
\r
140 if ( quasi_reg_tet q s ) then
\r
141 if radV q < sqrt2 then gamma ( v0 , v1 , v2, v3 ) s
\r
142 else svan v0 ( v0 , v1 , v2, v3 )
\r
143 else if ( eta_pos q s ) < sqrt2 then
\r
144 if ( cotext ( find_dia q s ) s = (1,1) ) \/( cotext ( find_dia q s ) s = (4,0) ) then
\r
145 gamma (v0 , v1 , v2, v3 ) s
\r
146 else gamma ( v0 , v1 , v2, v3 ) s + ( &1 / &2 )* ( ( sv0 v0 q s ) - ( sv0 ( v_hat v0 q s ) q s ))
\r
147 else if ( cotext ( find_dia q s ) s = (1,1) ) then svan v0 ( v0 , v1, v2, v3 )
\r
148 else ( if ( cotext ( find_dia q s ) s = (4,0) ) then
\r
149 ( &1 / &2 )* ( ( svan v0 ( v0 , v1, v2, v3 )) + ( svan ( v_hat v0 q s ) ( v0 , v1, v2, v3 )))
\r
150 else ( &1 / &2 )* ( ( svan v0 ( v0 , v1, v2, v3 )) + ( svan ( v_hat v0 q s ) ( v0 , v1, v2, v3 ))) +
\r
151 ( &1 / &2 )* ( ( sv0 v0 q s - sv0 ( v_hat v0 q s) q s ))) `;;
\r
153 let A_1 = new_definition ` A_1 v0 ( v0 , v1 , v2 , v3 ) (s:real^3->bool) =
\r
154 let q = { v0 , v1 , v2 , v3 } in
\r
155 -- vol( VC1 v0 q s ) + (( solid v0 q )/ ( &3 * delta_oct ))
\r
156 + (( sigma v0 ( v0 , v1 , v2, v3 ) s ) / (&4 * delta_oct )) `;;
\r
157 (*=====================================================================*)
\r
158 (* this definition is writen by anhtamct ==============================*)
\r
159 let ball3_lambda = new_definition ` ball3_lambda (x:real^3) (r:real) (Lambda:real^3 -> bool) =
\r
160 ((open_ball x r ) INTER ( UNIONS ( IMAGE (\v. open_ball v (&1) ) Lambda ) ))`;;
\r
161 let truncated_packing = new_definition ` truncated_packing x r Lambda = Lambda INTER (ball3_lambda x r Lambda) `;;
\r
162 (*=====================================================================*)
\r
163 (* these definition are writen by Hoang Le Truong =====================*)
\r
164 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
\r
165 let fan1 = new_definition`fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {}) `;;
\r
166 let fan2 = new_definition`fan2(x,V,E):bool <=> ~(x IN V)`;;
\r
168 let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
\r
170 let fan4 = new_definition`fan4(x,V,E):bool<=> (!e. (e IN E) ==> (aff_gt {x} e INTER V={}))`;;
\r
172 let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
\r
173 let fan = new_definition`fan(x,V,E)<=> ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;;
\r
174 let X= new_definition`X fan(x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
\r
175 let Y= new_definition`Y fan(x,V,E)={v:real^3 | ?e. (E e)/\(~(v IN aff_ge {x} e))}`;;
\r
176 (*=====================================================================*)
\r
177 (* Definition 8.9 =====================================================*)
\r
178 let tru_pack =new_definition ` tru_pack (v:real^3) (r:real) (s:real^3->bool) =
\r
179 { x | center_pac s v /\ x IN s /\ x IN open_ball v r }`;;
\r
180 let v_std = new_definition ` v_std (s:real^3->bool) (v0:real^3) = ( tru_pack v0 ( &2 * t0 ) s ) DIFF {v0}`;;
\r
181 let e_std = new_definition ` e_std (s:real^3->bool) (v0:real^3) =
\r
182 { { u , v } | u IN (tru_pack v0 ( &2 * t0 ) s ) DIFF {v0} /\
\r
183 v IN (tru_pack v0 ( &2 * t0 ) s ) DIFF {v0} /\
\r
184 ~(u = v) /\ d3 u v <= ( &2 * t0 ) }`;;
\r
186 (*=====================================================================*)
\r
187 (* Definition 26 in collection_geom file ==============================*)
\r
188 let condC = new_definition ` condC (M13:real) (m12:real) (m14:real) (M24:real) (m34:real) (m23:real) =
\r
189 (( m12 + m23 >= M13 ) /\ ( m14 + m34 >= M13 ) /\ ( m12 + m14 > M24 ) /\ ( m23 + m34 > M24 ) /\
\r
190 ( delta_x (M13 pow 2) (m12 pow 2) (m14 pow 2) (M24 pow 2) (m34 pow 2) (m23 pow 2) >= &0 ))` ;;
\r
191 (*=====================================================================*)
\r
192 (* Begin to prove lemma 8.30 *)
\r
193 (*=====================================================================*)
\r
197 let in_lemma2 = REWRITE_CONV[IN_ELIM_THM]
\r
198 `e IN {{u, v} | u IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
199 v IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
201 d3 u v <= &2 * t0}`;;
\r
203 let in_inv = prove (`{{u, v} | u IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
204 v IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
206 d3 u v <= &2 * t0} e <=> e IN {{u, v} | u IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
207 v IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
209 d3 u v <= &2 * t0}`,SET_TAC[]);;
\r
211 let lemma_graph = prove(`center_pac (s:real^3->bool) (v0:real^3) ==> graph (e_std s v0)`, REWRITE_TAC[e_std;tru_pack;graph]
\r
212 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
\r
213 THEN REWRITE_TAC[SET_RULE `{x | x IN s /\ x IN open_ball v0 (&2 * t0)}= s INTER open_ball v0 (&2 * t0)`]
\r
214 THEN GEN_TAC THEN REWRITE_TAC[in_inv] THEN REWRITE_TAC[in_lemma2]
\r
215 THEN REWRITE_TAC[ARITH_RULE `2 = SUC (SUC 0)`;HAS_SIZE_CLAUSES]THEN REPEAT STRIP_TAC
\r
216 THEN EXISTS_TAC`u:real^3` THEN EXISTS_TAC`{v:real^3}`
\r
217 THEN ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY] THEN EXISTS_TAC `v:real^3` THEN EXISTS_TAC `{}:real^3->bool`
\r
218 THEN ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);;
\r
219 (*==============================================================================*)
\r
220 (* end lemma_graph*)
\r
221 (*==============================================================================*)
\r
225 let uni_lemma1 = prove( ` UNIONS
\r
226 {{u, v} | u IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
227 v IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
229 d3 u v <= &2 * t0} =UNIONS
\r
230 {{u1, v1} | u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
231 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
233 d3 u1 v1 <= &2 * t0}`,SET_TAC[]);;
\r
235 let in_lemma1 = REWRITE_CONV[IN_ELIM_THM]
\r
237 {{u1, v1} | u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
238 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
240 d3 u1 v1 <= &2 * t0}`;;
\r
242 let in_lemma = ONCE_REWRITE_CONV[IN_ELIM_THM]
\r
245 {{u1, v1} | u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
246 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
248 d3 u1 v1 <= &2 * t0} /\
\r
251 let exist_lemma = prove(` (?u. (?u1 v1.
\r
252 (u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
253 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
255 d3 u1 v1 <= &2 * t0) /\
\r
257 x IN u) <=> (?u1 v1.
\r
258 (u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
259 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
261 d3 u1 v1 <= &2 * t0 /\
\r
262 x IN { u1, v1 }))`, MESON_TAC[]);;
\r
264 let cha_lemma1 = prove (`{x | ?u. u IN
\r
265 {{u1, v1} | u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
266 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
268 d3 u1 v1 <= &2 * t0} /\
\r
269 x IN u} = {y | ?u. u IN
\r
270 {{u1, v1} | u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
271 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
273 d3 u1 v1 <= &2 * t0} /\
\r
274 y IN u}`,SET_TAC[]);;
\r
276 let exist_lemma1 = prove(` (?u1 v1.
\r
277 u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
278 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
280 d3 u1 v1 <= &2 * t0 /\
\r
282 u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
283 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
285 d3 u1 v1 <= &2 * t0 /\
\r
288 x IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
289 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
291 d3 x v1 <= &2 * t0 ) \/
\r
293 u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
294 x IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
296 d3 u1 x <= &2 * t0 )`,MESON_TAC[]);;
\r
298 let unions_lemma = prove (`!(v0:real^3) (s:real^3->bool). center_pac (s:real^3->bool) (v0:real^3) ==> UNIONS (e_std s v0) SUBSET v_std s v0`,
\r
299 REPEAT GEN_TAC THEN REWRITE_TAC[e_std;v_std;tru_pack]
\r
300 THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
301 REWRITE_TAC[SET_RULE` {x | x IN s /\ x IN open_ball v0 (&2 * t0)}= s INTER open_ball v0 (&2 * t0)`] THEN
\r
302 ONCE_REWRITE_TAC[uni_lemma1] THEN REWRITE_TAC[SUBSET;UNIONS] THEN ONCE_REWRITE_TAC[cha_lemma1] THEN
\r
303 ONCE_REWRITE_TAC[in_lemma] THEN GEN_TAC THEN ONCE_REWRITE_TAC[in_lemma1] THEN REWRITE_TAC[exist_lemma] THEN
\r
304 REWRITE_TAC[SET_RULE ` x IN {u1 , v1} <=> x = u1 \/ x = v1`] THEN
\r
305 REWRITE_TAC[TAUT ` u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
306 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
308 d3 u1 v1 <= &2 * t0 /\
\r
309 (x = u1 \/ x = v1) <=> ( u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
310 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
312 d3 u1 v1 <= &2 * t0 /\
\r
313 x = u1) \/ ( u1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
314 v1 IN s INTER open_ball v0 (&2 * t0) DIFF {v0} /\
\r
316 d3 u1 v1 <= &2 * t0 /\
\r
318 REWRITE_TAC[exist_lemma1] THEN STRIP_TAC);;
\r
319 (*==================================================================================*)
\r
320 (* end of unions_lemma*)
\r
321 (*==================================================================================*)
\r
325 let lemma7_1 = new_axiom `!(v0:real^3) (s:real^3->bool) r:real. center_pac (s:real^3->bool) (v0:real^3) ==>
\r
326 FINITE (tru_pack v0 r s )`;;
\r
328 let fini_lemma = prove(` FINITE (tru_pack v0 (&2 * t0) s)
\r
329 ==> FINITE (tru_pack v0 (&2 * t0) s DIFF {v0})`, REWRITE_TAC[FINITE_DIFF]);;
\r
331 let infi_lemma2 = prove(`center_pac s v0 ==> FINITE (tru_pack v0 (&2 * t0) s) `, REWRITE_TAC[lemma7_1]);;
\r
333 let fini_lemma1 = prove(`!(v0:real^3) (s:real^3->bool). center_pac s v0 ==> FINITE ( v_std s v0 )`,
\r
334 REPEAT GEN_TAC THEN REWRITE_TAC[v_std] THEN DISCH_TAC THEN
\r
335 MATCH_MP_TAC ( fini_lemma) THEN
\r
336 UNDISCH_TAC `center_pac (s:real^3->bool) (v0:real^3)` THEN REWRITE_TAC[infi_lemma2]);;
\r
338 let fan1_lemma = prove(`!(v0:real^3) (s:real^3->bool). center_pac (s:real^3->bool) (v0:real^3) /\ ~( v_std s v0 = {}) ==>
\r
339 fan1 (v0 , v_std s v0 , e_std s v0 )` , REPEAT GEN_TAC THEN REWRITE_TAC[fan1] THEN
\r
340 REWRITE_TAC[TAUT `center_pac s v0 /\ ~(v_std s v0 = {} ) ==> FINITE ( v_std s v0 ) /\ ~(v_std s v0 SUBSET {}) <=>
\r
341 ( center_pac s v0 /\ ~( v_std s v0 = {}) ==> FINITE ( v_std s v0 ) ) /\
\r
342 ( center_pac s v0 /\ ~( v_std s v0 = {}) ==> ~(v_std s v0 SUBSET {}))`] THEN
\r
343 REWRITE_TAC[SET_RULE ` ~( v_std s v0 SUBSET {}) <=> ~( v_std s v0 = {})`] THEN
\r
344 MESON_TAC[fini_lemma1]);;
\r
345 (*======================================================================================*)
\r
346 (* end of fan1_lemma*)
\r
347 (*======================================================================================*)
\r
351 let fan2_lemma = prove(`!(v0:real^3) (s:real^3->bool). center_pac s v0 ==> fan2 (v0,v_std s v0,e_std s v0 )`,
\r
352 REPEAT GEN_TAC THEN REWRITE_TAC[fan2;v_std;DIFF] THEN SET_TAC[]);;
\r
353 (*======================================================================================*)
\r
354 (*end of fan2_lemma*)
\r
355 (*======================================================================================*)
\r
359 let lemmaf3 = prove(`{v, w} IN
\r
360 {{x, y} | x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
361 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
363 d3 x y <= &2 * t0} <=>
\r
365 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
366 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
368 d3 x y <= &2 * t0) /\
\r
369 {v, w} = {x, y})`, REWRITE_TAC[IN_ELIM_THM]);;
\r
371 let lemma_subset = prove ( `{w | ?x y.
\r
372 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
373 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
375 d3 x y <= &2 * t0) /\
\r
376 {v, w} = {x, y}} SUBSET tru_pack v0 (&2 * t0) s DIFF {v0}`, SET_TAC[]);;
\r
378 let lemmaf32 = prove (` FINITE (tru_pack v0 (&2 * t0) s DIFF {v0})
\r
381 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
382 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
384 d3 x y <= &2 * t0) /\
\r
385 {v, w} = {x, y}} <=> ( FINITE (tru_pack v0 (&2 * t0) s DIFF {v0}) /\ {w | ?x y.
\r
386 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
387 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
389 d3 x y <= &2 * t0) /\
\r
390 {v, w} = {x, y}} SUBSET
\r
391 tru_pack v0 (&2 * t0) s DIFF {v0} )
\r
394 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
395 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
397 d3 x y <= &2 * t0) /\
\r
398 {v, w} = {x, y}}`, MESON_TAC[lemma_subset]);;
\r
400 let lemmaf33 = prove(` FINITE (tru_pack v0 (&2 * t0) s DIFF {v0})
\r
403 (x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
404 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
406 d3 x y <= &2 * t0) /\
\r
407 {v, w} = {x, y}}`, REWRITE_TAC[lemmaf32] THEN REWRITE_TAC[FINITE_SUBSET]);;
\r
409 let lemmaf34 = prove (` condC (#2.6) (&2) (&2) (#2.6) (&2) (&2)`, REWRITE_TAC[condC;delta_x] THEN REAL_ARITH_TAC);;
\r
411 (* prove lemma have_not_prove*)
\r
413 let lemma_c = REWRITE_CONV[IN_ELIM_THM]`&1 / (h + &1) % p + h / (h + &1) % v IN
\r
414 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % p + b % v}`;;
\r
416 let lemma_2 = REWRITE_CONV[IN_ELIM_THM]`&1 / (h + &1) % p + h / (h + &1) % v IN
\r
417 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % q + b % v0}`;;
\r
419 let lemma_c1 = prove (` &0 <= h ==> &0 <= &1 / (h + &1)`, DISCH_TAC THEN MATCH_MP_TAC (REAL_LE_DIV) THEN UNDISCH_TAC `&0 <= h`
\r
420 THEN REWRITE_TAC[MESON[]` &0 <= h ==> &0 <= &1 /\ &0 <= h + &1 <=> ( &0 <= h ==> &0 <= &1 ) /\ (&0 <= h ==> &0 <= h + &1 )`]
\r
421 THEN REAL_ARITH_TAC);;
\r
423 let lemma_c11 = prove (`&0 < &1 / ( h + &1) ==> &0 <= &1 / (h + &1) `, REAL_ARITH_TAC);;
\r
425 let lemma_c111 = prove (`h >= &0 ==> &0 <= &1 / (h + &1)`, DISCH_TAC THEN MATCH_MP_TAC (lemma_c1)
\r
426 THEN UNDISCH_TAC `h:real >= &0` THEN REAL_ARITH_TAC);;
\r
428 let lemma_ch = prove (` &0 <= h ==> &0 <= h / (h + &1)`, DISCH_TAC THEN MATCH_MP_TAC (REAL_LE_DIV) THEN UNDISCH_TAC `&0 <= h`
\r
429 THEN REWRITE_TAC[MESON[]` &0 <= h ==> &0 <= h /\ &0 <= h + &1 <=> ( &0 <= h ==> &0 <= h ) /\ (&0 <= h ==> &0 <= h + &1 )`]
\r
430 THEN REAL_ARITH_TAC);;
\r
432 let lemma_ch1 = prove (`&0 < h / ( h + &1) ==> &0 <= h / (h + &1) `, REAL_ARITH_TAC);;
\r
434 let lemma_ch11 = prove (`h >= &0 ==> &0 <= h / (h + &1)`, DISCH_TAC THEN MATCH_MP_TAC (lemma_ch)
\r
435 THEN UNDISCH_TAC `h:real >= &0` THEN REAL_ARITH_TAC);;
\r
437 let lemma_1 = prove (` h >= &0 ==> &1 / (h + &1) + h / (h + &1) = &1`, STRIP_TAC THEN
\r
438 REWRITE_TAC[REAL_ARITH `&1 / (h + &1) + h / (h + &1) = (h + &1)/ (h + &1)`] THEN
\r
439 MATCH_MP_TAC (REAL_DIV_REFL) THEN UNDISCH_TAC `h >= &0` THEN REAL_ARITH_TAC);;
\r
441 let le1_diag_trape = prove (` p:real^3 = q + (h:real) % (v0 - v) /\ h >= &0
\r
442 ==> &1 / (h + &1) % p + h / (h + &1) % v IN {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % p + b % v}`,
\r
443 REWRITE_TAC[lemma_c]THEN STRIP_TAC THEN EXISTS_TAC ` &1 / (h+ &1)` THEN EXISTS_TAC ` h:real / (h+ &1)` THEN
\r
444 UNDISCH_TAC `h:real >= &0` THEN
\r
445 REWRITE_TAC[MESON[] ` h >= &0
\r
446 ==> &0 <= &1 / (h + &1) /\
\r
447 &0 <= h / (h + &1) /\
\r
448 &1 / (h + &1) + h / (h + &1) = &1 /\
\r
449 &1 / (h + &1) % p + h / (h + &1) % v =
\r
450 &1 / (h + &1) % p + h / (h + &1) % v <=>
\r
451 ( h >= &0 ==> &0 <= &1 / (h + &1) ) /\
\r
452 ( h >= &0 ==> &0 <= h / (h + &1) ) /\
\r
453 ( h >= &0 ==> &1 / (h + &1) + h / (h + &1) = &1 ) /\
\r
454 ( h >= &0 ==> &1 / (h + &1) % p + h / (h + &1) % v =
\r
455 &1 / (h + &1) % p + h / (h + &1) % v )`] THEN
\r
456 REWRITE_TAC[lemma_c111;lemma_ch11;lemma_1]);;
\r
458 let diag_trape = prove (` !(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real). p = q + h % (v0 - v) /\ h >= &0 ==>
\r
459 ~(conv {p, v} INTER conv {q, v0} = {})`, REPEAT GEN_TAC THEN DISCH_TAC THEN
\r
460 REWRITE_TAC[SET_RULE ` ~(conv {p, v} INTER conv {q, v0} = {}) <=> ? x. x IN conv {p, v} /\ x IN conv {q, v0}`] THEN
\r
461 EXISTS_TAC ` (&1/(h + &1)) % (p:real^3) + ((h:real)/(h + &1)) % (v:real^3)` THEN
\r
462 UNDISCH_TAC `p:real^3 = q + h % (v0 - v) /\ h >= &0 ` THEN REWRITE_TAC[CONV_SET2] THEN
\r
463 REWRITE_TAC[MESON[] ` p = q + h % (v0 - v) /\ h >= &0
\r
464 ==> &1 / (h + &1) % p + h / (h + &1) % v IN
\r
465 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % p + b % v} /\
\r
466 &1 / (h + &1) % p + h / (h + &1) % v IN
\r
467 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % q + b % v0} <=>
\r
468 ( p = q + h % (v0 - v) /\ h >= &0
\r
469 ==> &1 / (h + &1) % p + h / (h + &1) % v IN
\r
470 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % p + b % v} ) /\
\r
471 ( p = q + h % (v0 - v) /\ h >= &0
\r
472 ==> &1 / (h + &1) % p + h / (h + &1) % v IN
\r
473 {w | ?a b. &0 <= a /\ &0 <= b /\ a + b = &1 /\ w = a % q + b % v0} )`] THEN
\r
474 REWRITE_TAC[le1_diag_trape] THEN REWRITE_TAC[lemma_2] THEN STRIP_TAC THEN
\r
475 EXISTS_TAC ` &1 / (h+ &1)` THEN EXISTS_TAC ` h:real / (h+ &1)` THEN UNDISCH_TAC `h >= &0` THEN
\r
476 REWRITE_TAC[MESON[] ` h >= &0
\r
477 ==> &0 <= &1 / (h + &1) /\
\r
478 &0 <= h / (h + &1) /\
\r
479 &1 / (h + &1) + h / (h + &1) = &1 /\
\r
480 &1 / (h + &1) % p + h / (h + &1) % v =
\r
481 &1 / (h + &1) % q + h / (h + &1) % v0 <=>
\r
482 ( h >= &0 ==> &0 <= &1 / (h + &1) ) /\
\r
483 ( h >= &0 ==> &0 <= h / (h + &1) ) /\
\r
484 ( h >= &0 ==> &1 / (h + &1) + h / (h + &1) = &1 ) /\
\r
485 ( h >= &0 ==> &1 / (h + &1) % p + h / (h + &1) % v =
\r
486 &1 / (h + &1) % q + h / (h + &1) % v0 )`] THEN
\r
487 REWRITE_TAC[lemma_c111; lemma_ch11; lemma_1] THEN DISCH_TAC THEN
\r
488 REWRITE_TAC[VECTOR_ARITH `&1 / (h + &1) % p + h / (h + &1) % v = &1 / (h + &1) % q + h / (h + &1) % v0 <=>
\r
489 &1 / (h + &1) % p = &1 / (h + &1) % q + h / (h + &1) % v0 - ( h / (h + &1) % v )`] THEN
\r
490 REWRITE_TAC[VECTOR_ARITH `&1 / (h + &1) % p = &1 / (h + &1) % q + h / (h + &1) % v0 - h / (h + &1) % v
\r
491 <=> &1 / (h + &1) % p = &1 / (h + &1) % q + h / (h + &1) % (v0 - v)`] THEN ASM_REWRITE_TAC[] THEN
\r
492 VECTOR_ARITH_TAC ) ;;
\r
494 let inv_diag = prove(`!(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real). p = q + h % (v0 - v) /\ conv {p, v} INTER conv {q, v0} = {} ==> ~(h >= &0)`,
\r
495 REWRITE_TAC[TAUT `p = q + h % (v0 - v) /\ conv {p, v} INTER conv {q, v0} = {}
\r
496 ==> ~(h >= &0) <=> p = q + h % (v0 - v) ==> ( conv {p, v} INTER conv {q, v0} = {} ==> ~(h >= &0) )`] THEN
\r
497 REWRITE_TAC[TAUT ` conv {p, v} INTER conv {q, v0} = {}
\r
498 ==> ~(h >= &0) <=> ( h >= &0 ==> ~(conv {p, v} INTER conv {q, v0} = {}))`] THEN
\r
499 REWRITE_TAC[TAUT `p = q + h % (v0 - v)==> h >= &0
\r
500 ==> ~(conv {p, v} INTER conv {q, v0} = {}) <=> ( p = q + h % (v0 - v) /\ h >= &0 ) ==> ~(conv {p, v} INTER conv {q, v0} = {})`] THEN
\r
501 REWRITE_TAC[diag_trape]);;
\r
503 let inv1_diag = prove (`!(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real).
\r
504 conv {p, v} INTER conv {q, v0} = {} /\ h >= &0 ==> ~(p = q + h % (v0 - v))`, MESON_TAC[diag_trape]);;
\r
506 let vec_le = prove (` (h:real) % ( v0:real^3 - v ) = -- h % (v - v0)`, VECTOR_ARITH_TAC);;
\r
509 let diag_trape1 = prove ( ` !(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real). p = q + h % (v0 - v) /\ h <= &0 ==>
\r
510 ~(conv {p, v0} INTER conv {q, v} = {})`, REWRITE_TAC[REAL_ARITH ` h <= &0 <=> -- h >= &0`] THEN
\r
511 ONCE_REWRITE_TAC[vec_le] THEN REWRITE_TAC[diag_trape]);;
\r
513 let inv_diag1 = prove(`!(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real). p = q + h % (v0 - v) /\ conv {p, v0} INTER conv {q, v} = {} ==> ~(h <= &0)`,
\r
514 REWRITE_TAC[TAUT `p = q + h % (v0 - v) /\ conv {p, v0} INTER conv {q, v} = {}
\r
515 ==> ~(h <= &0) <=> p = q + h % (v0 - v) ==> ( conv {p, v0} INTER conv {q, v} = {} ==> ~(h <= &0) )`] THEN
\r
516 REWRITE_TAC[TAUT ` conv {p, v0} INTER conv {q, v} = {}
\r
517 ==> ~(h <= &0) <=> ( h <= &0 ==> ~(conv {p, v0} INTER conv {q, v} = {}))`] THEN
\r
518 REWRITE_TAC[TAUT `p = q + h % (v0 - v)==> h <= &0
\r
519 ==> ~(conv {p, v0} INTER conv {q, v} = {}) <=> ( p = q + h % (v0 - v) /\ h <= &0 ) ==> ~(conv {p, v0} INTER conv {q, v} = {})`] THEN
\r
520 REWRITE_TAC[diag_trape1]);;
\r
522 let inv1_diag1 = prove (`!(p:real^3) (q:real^3) (v0:real^3) (v:real^3) (h:real).
\r
523 conv {p, v0} INTER conv {q, v} = {} /\ h <= &0 ==> ~(p = q + h % (v0 - v))`, MESON_TAC[diag_trape1]);;
\r
525 let lemma_3_4 = new_axiom (` !(v1:real^3) (v2:real^3) (v3:real^3) (v4:real^3).
\r
526 !(m12:real) (m23:real) (m34:real) (m14:real) (M13:real) (M24:real).
\r
533 condC M13 m12 m14 M24 m34 m23
\r
534 ==> conv {v1 , v3} INTER conv {v2 , v4} = {}`);;
\r
536 let lemma_3_4_c = new_axiom (` !(p:real^3) (q:real^3) (v:real^3) (v0:real^3).
\r
543 condC M13 m12 m14 M24 m34 m23
\r
544 ==> conv {p , v} INTER conv {q , v0} = {}`);;
\r
546 let affine_two_points = prove (`!(x:real^3) (y:real^3). affine {z | ?u v. u + v = &1 /\ z = u % x + v % y}`, REPEAT GEN_TAC THEN
\r
547 REWRITE_TAC[affine] THEN REPEAT GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
\r
548 ASM_REWRITE_TAC[] THEN EXISTS_TAC `( u:real) * u' + v * u''` THEN EXISTS_TAC ` u:real * v' + v * v''` THEN
\r
549 REWRITE_TAC[REAL_RING `(u * u' + v * u'') + u * v' + v * v'' = u * (u' + v') + v * (u'' + v'')`] THEN
\r
550 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_RING `u * &1 + v * &1 = u + v`] THEN ASM_REWRITE_TAC[] THEN
\r
551 VECTOR_ARITH_TAC);;
\r
553 let ch_le = prove (`(!x y u v. x IN t /\ y IN t /\ u + v = &1 ==> u % x + v % y IN t) <=>
\r
554 (!v1 v2 r s. v1 IN t /\ v2 IN t /\ r + s = &1 ==> r % v1 + s % v2 IN t)`, MESON_TAC[]);;
\r
556 let sub_aff = prove ( ` ! (t:real^3->bool) v1:real^3 v2:real^3 . affine t /\ {v1 , v2} SUBSET t ==>
\r
557 {w | ?r s. r + s = &1 /\ w = r % v1 + s % v2} SUBSET t`, REPEAT GEN_TAC THEN REWRITE_TAC[affine] THEN
\r
558 REWRITE_TAC[SET_RULE `{v1, v2} SUBSET t <=> v1 IN t /\ v2 IN t`] THEN STRIP_TAC THEN REWRITE_TAC[SUBSET] THEN
\r
559 GEN_TAC THEN ONCE_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
560 UNDISCH_TAC `!x:real^3 y:real^3 u:real v. x IN (t:real^3->bool) /\ y IN t /\ u + v = &1 ==> u % x + v % y IN t` THEN
\r
561 ONCE_REWRITE_TAC[ch_le] THEN UNDISCH_TAC `v1:real^3 IN t:real^3->bool` THEN UNDISCH_TAC `v2:real^3 IN t:real^3->bool` THEN
\r
562 UNDISCH_TAC `r + s = &1 ` THEN MESON_TAC[]);;
\r
564 let ans = prove (` INTERS {t:real^3->bool | affine t /\ {v1:real^3, v2} SUBSET t} = {w:real^3 | ?r:real s. r + s = &1 /\ w = r % v1 + s % v2}
\r
565 <=> INTERS {t | affine t /\ {v1, v2} SUBSET t} SUBSET {w | ?r s. r + s = &1 /\ w = r % v1 + s % v2} /\
\r
566 {w | ?r s. r + s = &1 /\ w = r % v1 + s % v2} SUBSET INTERS {t | affine t /\ {v1, v2} SUBSET t} `, SET_TAC[]);;
\r
568 let anss = SET_RULE `(!t:real^3->bool. affine t /\ {v1, v2} SUBSET t ==> {w | ?r s. r + s = &1 /\ w = r % v1 + s % v2} SUBSET t ) ==>
\r
569 {w | ?r s. r + s = &1 /\ w = r % v1 + s % v2} SUBSET INTERS {t | affine t /\ {v1, v2} SUBSET t}`;;
\r
571 let chon = SET_RULE `!s:A->bool. s IN { t | P t} ==> INTERS { t| P t} SUBSET s`;;
\r
573 let subset_two_points = SET_RULE `{a , b } SUBSET s <=> a IN s /\ b IN s`;;
\r
575 let sub_1 = prove (`{w | ?r s. r + s = &1 /\ w = r % (v1:real^3) + s % (v2:real^3)} SUBSET
\r
576 INTERS {(t:real^3->bool) | affine t /\ {v1, v2} SUBSET t}`, MATCH_MP_TAC(anss) THEN REWRITE_TAC[sub_aff]);;
\r
578 let AFF_HULL_TWO_POINTS = prove (` ! v1:real^3 v2:real^3 . affine hull {v1 , v2} = { w | ? r s . r + s = &1 /\ w = r % v1 + s % v2 }`,
\r
579 REPEAT GEN_TAC THEN REWRITE_TAC[hull] THEN REWRITE_TAC[ans] THEN REWRITE_TAC[sub_1] THEN MATCH_MP_TAC(chon) THEN
\r
580 REWRITE_TAC[IN_ELIM_THM] THEN REWRITE_TAC[affine_two_points] THEN REWRITE_TAC[subset_two_points] THEN
\r
581 REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL [EXISTS_TAC `&1`; EXISTS_TAC `&0`] THENL [EXISTS_TAC `&0`; EXISTS_TAC `&1`]
\r
582 THENL [REWRITE_TAC[REAL_ARITH ` &1 + &0 = &1`]; REWRITE_TAC[REAL_ARITH ` &0 + &1 = &1`]] THEN VECTOR_ARITH_TAC);;
\r
584 let fa4 = prove(`(p:real^3) = (q:real^3) + (h:real) % ((v0:real^3) - (v:real^3)) /\ h = &0 ==> p = q`,
\r
585 REWRITE_TAC[TAUT` p = q + h % (v0 - v) /\ h = &0 ==> p = q <=> h = &0 /\ p = q + h % (v0 - v) ==> p = q`]THEN
\r
586 REWRITE_TAC[TAUT `h = &0 /\ p = q + h % (v0 - v) ==> p = q <=> h = &0 ==> p = q + h % (v0 - v) ==> p = q`] THEN
\r
587 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);;
\r
589 let tam = prove (` (p:real^3) = (q:real^3) + (h:real) % ((v0:real^3) - (v:real^3)) /\ ~(h = &0) ==>
\r
590 ~(conv {p, v} INTER conv {q, v0} = {}) \/ ~(conv {p, v0} INTER conv {q, v} = {})`,
\r
591 REWRITE_TAC[REAL_ARITH `~(h = &0) <=> (h > &0 \/ h < &0)`] THEN
\r
592 REWRITE_TAC[TAUT ` p = q + h % (v0 - v) /\ (h > &0 \/ h < &0) <=> p = q + h % (v0 - v) /\ h > &0 \/
\r
593 p = q + h % (v0 - v) /\ h < &0 `] THEN STRIP_TAC
\r
594 THENL[ MATCH_MP_TAC(TAUT ` ~(conv {(p:real^3) , (v:real^3)} INTER conv {(q:real^3), (v0:real^3)} = {}) ==>
\r
595 ~(conv {p, v} INTER conv {q, v0} = {}) \/ ~(conv {p, v0} INTER conv {q, v} = {})`);
\r
596 MATCH_MP_TAC(TAUT ` ~(conv {(p:real^3) , (v0:real^3)} INTER conv {(q:real^3), (v:real^3)} = {}) ==>
\r
597 ~(conv {p, v} INTER conv {q, v0} = {}) \/ ~(conv {p, v0} INTER conv {q, v} = {})`)]
\r
598 THENL[MATCH_MP_TAC(diag_trape);MATCH_MP_TAC(diag_trape1)] THEN EXISTS_TAC ` h:real`
\r
599 THENL[STRIP_TAC THENL[ASM_REWRITE_TAC[]; UNDISCH_TAC ` h > &0 ` ] THEN REAL_ARITH_TAC ;
\r
600 STRIP_TAC THENL[ASM_REWRITE_TAC[]; UNDISCH_TAC ` h < &0 ` ] THEN REAL_ARITH_TAC]);;
\r
602 let tam1 = prove (` (p:real^3) = (q:real^3) + (h:real) % ( (v0:real^3) - (v:real^3)) /\ ~(p = q )
\r
603 ==> ~(conv {p, v} INTER conv {q, v0} = {}) \/ ~(conv {p, v0} INTER conv {q, v} = {})`,
\r
604 STRIP_TAC THEN MATCH_MP_TAC(tam) THEN STRIP_TAC
\r
605 THENL[ASM_REWRITE_TAC[];UNDISCH_TAC `~(p:real^3 = q)` THEN UNDISCH_TAC `p:real^3 = q + h % (v0 - v)`]
\r
606 THEN REWRITE_TAC[TAUT` ~(p = q) ==> ~(h = &0) <=> h = &0 ==> p = q`] THEN MESON_TAC[fa4]);;
\r
608 let tam2 = prove (` ~(p:real^3 = q) /\ conv {p, v:real^3} INTER conv {q, v0:real^3} = {} /\ conv {p, v0} INTER conv {q, v} = {}
\r
609 ==> ~(p = q + (h:real) % (v0 - v) )`, MESON_TAC[tam1]);;
\r
611 let c_nov16 = prove (` ~(p:real^3 = q) ==> (!(x:real^3) (y:real^3). x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\
\r
612 (v0:real^3) IN s ==> (v:real^3) IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)
\r
613 ==> (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
614 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
615 ~(v = p) /\ norm (v - p) <= &2 * t0) \/
\r
616 ((p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
617 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
618 ~(p = v) /\ norm (p - v) <= &2 * t0))
\r
619 ==> (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
620 (q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
621 ~(v = q) /\ norm (v - q) <= &2 * t0) \/
\r
622 ((q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
623 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
624 ~(q = v) /\ norm (q - v) <= &2 * t0))
\r
625 ==> ~(p = q + h % (v0 - v))`,
\r
626 REWRITE_TAC[MESON[NORM_SUB]` (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
627 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
628 ~(v = p) /\ norm (v - p) <= &2 * t0 \/
\r
629 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
630 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
631 ~(p = v) /\ norm (p - v) <= &2 * t0
\r
632 <=> (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
633 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
634 ~(p = v) /\ norm (p - v) <= &2 * t0 `] THEN REPEAT STRIP_TAC THEN
\r
635 UNDISCH_TAC `p:real^3 = q + (h:real) % (v0 - v)` THEN
\r
636 REWRITE_TAC[MESON[]`p = q + h % (v0 - v) ==> F <=> ~(p = q + h % (v0 - v))`] THEN
\r
637 MATCH_MP_TAC(tam2) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MATCH_MP_TAC(lemma_3_4) THEN
\r
638 EXISTS_TAC ` &2` THEN EXISTS_TAC ` &2` THEN EXISTS_TAC ` &2` THEN EXISTS_TAC ` &2` THEN
\r
639 EXISTS_TAC ` #2.6` THEN EXISTS_TAC ` #2.6` THEN REWRITE_TAC[lemmaf34] THEN REWRITE_TAC[d3;dist]
\r
640 THENL[UNDISCH_TAC ` norm (q:real^3 - v0) < &2 * t0` ; UNDISCH_TAC` norm (q:real^3 - v) <= &2 * t0` ] THEN
\r
641 REWRITE_TAC[t0] THEN REWRITE_TAC[REAL_ARITH ` &2 * #1.255 = #2.51`]
\r
642 THENL[REWRITE_TAC[TAUT ` norm (q - v0) < #2.51
\r
643 ==> norm (p - q) >= &2 /\
\r
644 norm (q - v) >= &2 /\
\r
645 norm (v - v0) >= &2 /\
\r
646 norm (v0 - p) >= &2 /\
\r
647 norm (p - v) < #2.6 /\
\r
648 norm (q - v0) <= #2.6
\r
649 <=> ( norm (q - v0) < #2.51
\r
650 ==> norm (p - q) >= &2 /\
\r
651 norm (q - v) >= &2 /\
\r
652 norm (v - v0) >= &2 /\
\r
653 norm (v0 - p) >= &2 /\
\r
654 norm (p - v) < #2.6) /\
\r
655 (norm (q - v0) < #2.51
\r
656 ==> norm (q - v0) <= #2.6 )`] THEN CONJ_TAC THENL [DISCH_TAC ; REAL_ARITH_TAC];
\r
657 REWRITE_TAC[TAUT `norm (q - v) <= #2.51
\r
658 ==> norm (p - q) >= &2 /\
\r
659 norm (q - v0) >= &2 /\
\r
660 norm (v0 - v) >= &2 /\
\r
661 norm (v - p) >= &2 /\
\r
662 norm (p - v0) < #2.6 /\
\r
663 norm (q - v) <= #2.6
\r
664 <=> ( norm (q - v) <= #2.51
\r
665 ==> norm (p - q) >= &2 /\
\r
666 norm (q - v0) >= &2 /\
\r
667 norm (v0 - v) >= &2 /\
\r
668 norm (v - p) >= &2 /\
\r
669 norm (p - v0) < #2.6 ) /\
\r
670 ( norm (q - v) <= #2.51
\r
671 ==> norm (q - v) <= #2.6 ) `] THEN CONJ_TAC THENL [DISCH_TAC ; REAL_ARITH_TAC]]
\r
672 THENL[UNDISCH_TAC `norm (p:real^3 - v) <= &2 * t0` THEN REWRITE_TAC[t0] THEN REWRITE_TAC[REAL_ARITH ` &2 * #1.255 = #2.51`] THEN
\r
673 REWRITE_TAC[TAUT ` norm (p - v) <= #2.51
\r
674 ==> norm (p - q) >= &2 /\
\r
675 norm (q - v) >= &2 /\
\r
676 norm (v - v0) >= &2 /\
\r
677 norm (v0 - p) >= &2 /\
\r
678 norm (p - v) < #2.6 <=> ( norm (p - v) <= #2.51
\r
679 ==> norm (p - q) >= &2 /\
\r
680 norm (q - v) >= &2 /\
\r
681 norm (v - v0) >= &2 /\
\r
682 norm (v0 - p) >= &2 ) /\ (norm (p - v) <= #2.51 ==>
\r
683 norm (p - v) < #2.6 )`] THEN CONJ_TAC THENL [DISCH_TAC; REAL_ARITH_TAC] THEN
\r
684 UNDISCH_TAC ` ~(p:real^3 = v0)` THEN UNDISCH_TAC ` v0:real^3 IN s:real^3->bool` THEN
\r
685 UNDISCH_TAC` !x:real^3 y:real^3. x IN s:real^3->bool /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2` THEN
\r
686 UNDISCH_TAC ` p:real^3 IN s:real^3->bool` THEN UNDISCH_TAC `q:real^3 IN (s:real^3->bool)` THEN
\r
687 UNDISCH_TAC ` ~(p:real^3 = q)` THEN UNDISCH_TAC ` v:real^3 IN (s:real^3->bool)`
\r
688 THEN UNDISCH_TAC ` ~(q:real^3 = v)` THEN UNDISCH_TAC ` ~(v:real^3 = v0)` ;
\r
689 UNDISCH_TAC` norm (p:real^3 - v0) < &2 * t0` THEN REWRITE_TAC[t0] THEN REWRITE_TAC[REAL_ARITH ` &2 * #1.255 = #2.51`] THEN
\r
690 REWRITE_TAC[TAUT ` norm (p - v0) < #2.51
\r
691 ==> norm (p - q) >= &2 /\
\r
692 norm (q - v0) >= &2 /\
\r
693 norm (v0 - v) >= &2 /\
\r
694 norm (v - p) >= &2 /\
\r
695 norm (p - v0) < #2.6 <=> (norm (p - v0) < #2.51
\r
696 ==> norm (p - q) >= &2 /\
\r
697 norm (q - v0) >= &2 /\
\r
698 norm (v0 - v) >= &2 /\
\r
699 norm (v - p) >= &2 ) /\ (norm (p - v0) < #2.51
\r
700 ==> norm (p - v0) < #2.6)`] THEN CONJ_TAC THENL [DISCH_TAC; REAL_ARITH_TAC] THEN
\r
701 UNDISCH_TAC ` p:real^3 IN (s:real^3->bool) ` THEN UNDISCH_TAC ` q:real^3 IN (s:real^3->bool) ` THEN
\r
702 UNDISCH_TAC ` v:real^3 IN (s:real^3->bool) ` THEN UNDISCH_TAC ` v0:real^3 IN (s:real^3->bool) ` THEN
\r
703 UNDISCH_TAC ` ~(p:real^3 = q) ` THEN UNDISCH_TAC ` ~(p:real^3 = v) ` THEN
\r
704 UNDISCH_TAC ` ~(v:real^3 = v0) ` THEN UNDISCH_TAC ` ~(q:real^3 = v0) ` THEN
\r
705 UNDISCH_TAC ` !x:real^3 y:real^3. x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2 `]
\r
706 THEN MESON_TAC[NORM_SUB]);;
\r
708 let c_nov17 = prove (` ( ~(p:real^3 = q) /\ (!(x:real^3) (y:real^3). x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\
\r
709 (v0:real^3) IN s /\ (v:real^3) IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)
\r
710 /\ (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
711 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
712 ~(v = p) /\ norm (v - p) <= &2 * t0) \/
\r
713 ((p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
714 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
715 ~(p = v) /\ norm (p - v) <= &2 * t0))
\r
716 /\ (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
717 (q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
718 ~(v = q) /\ norm (v - q) <= &2 * t0) \/
\r
719 ((q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
720 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
721 ~(q = v) /\ norm (q - v) <= &2 * t0)) )
\r
722 ==> ~(p = q + h % (v0 - v))`,
\r
723 REWRITE_TAC[TAUT ` ~(p = q) /\
\r
724 (!x y. x IN s /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\
\r
727 norm (v - v0) < &2 * t0 /\
\r
729 ((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
730 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
732 norm (v - p) <= &2 * t0 \/
\r
733 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
734 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
736 norm (p - v) <= &2 * t0) /\
\r
737 ((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
738 (q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
740 norm (v - q) <= &2 * t0 \/
\r
741 (q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
742 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
744 norm (q - v) <= &2 * t0)
\r
745 ==> ~(p = q + h % (v0 - v)) <=>
\r
747 ==> (!(x:real^3) (y:real^3). x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\
\r
748 (v0:real^3) IN s ==> (v:real^3) IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)
\r
749 ==> (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
750 (p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
751 ~(v = p) /\ norm (v - p) <= &2 * t0) \/
\r
752 ((p IN s /\ norm (p - v0) < &2 * t0 /\ ~(p = v0)) /\
\r
753 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
754 ~(p = v) /\ norm (p - v) <= &2 * t0))
\r
755 ==> (((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
756 (q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
757 ~(v = q) /\ norm (v - q) <= &2 * t0) \/
\r
758 ((q IN s /\ norm (q - v0) < &2 * t0 /\ ~(q = v0)) /\
\r
759 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
760 ~(q = v) /\ norm (q - v) <= &2 * t0))
\r
761 ==> ~(p = q + h % (v0 - v))`] THEN REWRITE_TAC[c_nov16]);;
\r
763 let fa2 = REWRITE_CONV[IN_ELIM_THM] `{v, q} IN
\r
764 {{u, v'} | (u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
765 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
767 norm (u - v') <= &2 * t0}`;;
\r
769 let fa1 = REWRITE_CONV[IN_ELIM_THM]`p IN {w | {v, w} IN e_std s v0}`;;
\r
771 let c_nov1_17 = prove( ` center_pac (s:real^3->bool) (v0:real^3)
\r
772 ==> (v IN v_std s v0
\r
774 {w | {v, w} IN e_std s v0} p /\
\r
775 {w | {v, w} IN e_std s v0} q /\
\r
776 p = q + h % (v0 - v)
\r
778 REWRITE_TAC[SET_RULE `{w | {v, w} IN e_std s v0} p <=> p IN {w | {v, w} IN e_std s v0}`] THEN
\r
779 REWRITE_TAC[fa1] THEN REPEAT DISCH_TAC THEN REPEAT GEN_TAC THEN
\r
780 UNDISCH_TAC `(v:real^3) IN v_std (s:real^3->bool) v0` THEN UNDISCH_TAC `center_pac (s:real^3->bool) v0` THEN
\r
781 REWRITE_TAC[TAUT `center_pac s v0
\r
782 ==> v IN v_std s v0
\r
783 ==> {v, p} IN e_std s v0 /\ {v, q} IN e_std s v0 /\ p = q + h % (v0 - v)
\r
785 ~(p = q ) /\ center_pac s v0 /\ v IN v_std s v0 /\ {v, p} IN e_std s v0 /\ {v, q} IN e_std s v0
\r
786 ==> ~(p = q + h % (v0 - v))`] THEN
\r
787 REWRITE_TAC[TAUT ` ~(p = q) /\
\r
790 {v, p} IN e_std s v0 /\
\r
791 {v, q} IN e_std s v0
\r
792 ==> ~(p = q + h % (v0 - v)) <=>
\r
793 ~(p = q) ==> ( center_pac s v0 ==> ( v IN v_std s v0 /\
\r
794 {v, p} IN e_std s v0 /\
\r
795 {v, q} IN e_std s v0
\r
796 ==> ~(p = q + h % (v0 - v)))) `] THEN DISCH_TAC THEN DISCH_TAC THEN
\r
797 REWRITE_TAC[v_std;e_std;tru_pack] THEN ASM_REWRITE_TAC[] THEN
\r
798 REWRITE_TAC[SET_RULE ` v IN {x | x IN s /\ x IN open_ball v0 (&2 * t0)} DIFF {v0} <=>
\r
799 v IN s /\ v IN open_ball v0 (&2 * t0) /\ ~ ( v = v0)`] THEN
\r
800 ONCE_REWRITE_TAC[SET_RULE `{{u, v} | (u IN s /\ u IN open_ball v0 (&2 * t0) /\ ~(u = v0)) /\
\r
801 (v IN s /\ v IN open_ball v0 (&2 * t0) /\ ~(v = v0)) /\
\r
803 d3 u v <= &2 * t0} =
\r
804 {{u, v'} | (u IN s /\ u IN open_ball v0 (&2 * t0) /\ ~(u = v0)) /\
\r
805 (v' IN s /\ v' IN open_ball v0 (&2 * t0) /\ ~(v' = v0)) /\
\r
807 d3 u v' <= &2 * t0}`] THEN UNDISCH_TAC ` center_pac (s:real^3->bool) v0` THEN
\r
808 REWRITE_TAC[center_pac;packing_trg;d3;dist;open_ball] THEN
\r
809 REWRITE_TAC[SET_RULE `u IN {y | norm (y - v0) < &2 * t0} <=> norm (u - v0) < &2 * t0`] THEN
\r
810 REWRITE_TAC[SET_RULE ` (s:real^3->bool) x <=> x IN s`] THEN REWRITE_TAC[SET_RULE ` ~(v0 IN (=) u) <=> ~ (u = v0)`] THEN
\r
811 REWRITE_TAC[fa2] THEN REWRITE_TAC[SET_RULE ` {v, p} = {u, v'} <=> ( v = u /\ p = v') \/ ( v = v' /\ p = u )`] THEN
\r
812 REPEAT DISCH_TAC THEN UNDISCH_TAC `(p:real^3) = (q:real^3) + (h:real) % ((v0:real^3) - (v:real^3))` THEN
\r
813 REWRITE_TAC[TAUT ` p = q + h % (v0 - v) ==> F <=> ~(p = q + h % (v0 - v))`] THEN MATCH_MP_TAC(c_nov17) THEN
\r
814 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]);;
\r
816 let c_nov18 = prove(` ! x:real^3. x IN affine hull {v1:real^3 , v2:real^3} ==> norm ( x - v1) = norm (x - v2) + norm (v2 - v1) \/
\r
817 norm ( x - v2) = norm (x - v1) + norm (v2 - v1) \/ norm ( v1 - v2) = norm ( x - v1) + norm (x - v2)`,
\r
818 GEN_TAC THEN REWRITE_TAC[AFF_HULL_TWO_POINTS] THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
\r
819 ASM_REWRITE_TAC[] THEN UNDISCH_TAC ` (r:real) + (s:real) = &1 ` THEN
\r
820 REWRITE_TAC [REAL_ARITH ` r + s = &1 <=> r = &1 - s`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
821 REWRITE_TAC[VECTOR_ARITH ` ((&1 - s) % v1 + s % v2) - v1 = s % ( v2 - v1) `] THEN
\r
822 REWRITE_TAC[VECTOR_ARITH ` ((&1 - s) % v1 + s % v2) - v2 = (&1 - s) % (v1 - v2)`] THEN REWRITE_TAC[NORM_MUL] THEN
\r
823 REWRITE_TAC[TAUT ` abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1) \/
\r
824 abs (&1 - s) * norm (v1 - v2) = abs s * norm (v2 - v1) + norm (v2 - v1) \/
\r
825 norm (v1 - v2) = abs s * norm (v2 - v1) + abs (&1 - s) * norm (v1 - v2) <=>
\r
826 ~( abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1)) /\
\r
827 ~( abs (&1 - s) * norm (v1 - v2) = abs s * norm (v2 - v1) + norm (v2 - v1)) ==>
\r
828 norm (v1 - v2) = abs s * norm (v2 - v1) + abs (&1 - s) * norm (v1 - v2)`] THEN
\r
829 DISCH_TAC THEN REWRITE_TAC[NORM_SUB] THEN
\r
830 REWRITE_TAC[REAL_ARITH ` abs s * norm (v1 - v2) + abs (&1 - s) * norm (v1 - v2)
\r
831 = (abs s + abs (&1 - s))*norm (v1 - v2)`] THEN
\r
832 MATCH_MP_TAC(REAL_ARITH` (abs s + abs (&1 - s)) = &1 ==> norm (v1 - v2) = (abs s + abs (&1 - s)) * norm (v1 - v2)`) THEN
\r
833 MATCH_MP_TAC(REAL_ARITH ` abs s = s /\ abs (&1 - s) = (&1 - s) ==> abs s + abs (&1 - s) = &1`) THEN
\r
834 REWRITE_TAC[REAL_ABS_REFL] THEN
\r
835 UNDISCH_TAC ` ~(abs (s:real) * norm (v2:real^3 - v1:real^3) =
\r
836 abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1)) /\
\r
837 ~(abs (&1 - s) * norm (v1 - v2) =
\r
838 abs s * norm (v2 - v1) + norm (v2 - v1))` THEN
\r
839 REWRITE_TAC[TAUT ` ~(abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1)) /\
\r
840 ~(abs (&1 - s) * norm (v1 - v2) = abs s * norm (v2 - v1) + norm (v2 - v1))
\r
841 ==> &0 <= s /\ &0 <= &1 - s <=>
\r
842 ~(&0 <= s /\ &0 <= &1 - s ) /\ ~(abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1))
\r
843 ==> (abs (&1 - s) * norm (v1 - v2) = abs s * norm (v2 - v1) + norm (v2 - v1))`] THEN
\r
844 STRIP_TAC THEN REWRITE_TAC[NORM_SUB] THEN
\r
845 REWRITE_TAC[REAL_ARITH ` abs (&1 - s) * norm (v1 - v2) = abs s * norm (v1 - v2) + norm (v1 - v2) <=>
\r
846 abs (&1 - s) * norm (v1 - v2) - abs s * norm (v1 - v2) = norm (v1 - v2)`] THEN
\r
847 REWRITE_TAC[REAL_ARITH `abs (&1 - s) * norm (v1 - v2) - abs s * norm (v1 - v2) =
\r
848 ( abs (&1 - s) - abs s ) * norm (v1 - v2)`] THEN
\r
849 REWRITE_TAC[REAL_ARITH ` (abs (&1 - s) - abs s) * norm (v1 - v2) = norm (v1 - v2) <=>
\r
850 norm (v1 - v2) = (abs (&1 - s) - abs s) * norm (v1 - v2)`] THEN
\r
851 MATCH_MP_TAC( REAL_RING `(abs (&1 - s:real) - abs s) = &1 ==>
\r
852 norm (v1 - v2) = (abs (&1 - s) - abs s) * norm (v1 - v2)`) THEN
\r
853 MATCH_MP_TAC(REAL_ARITH ` abs (&1 - s) = (&1 - s) /\ abs s = -- s ==> abs (&1 - s) - abs s = &1`) THEN
\r
854 REWRITE_TAC[REAL_ARITH ` abs s = --s <=> abs (--s) = --s`] THEN REWRITE_TAC[REAL_ABS_REFL] THEN
\r
855 UNDISCH_TAC ` ~(abs s * norm ((v2:real^3) - (v1:real^3)) =
\r
856 abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1))` THEN
\r
857 REWRITE_TAC[TAUT ` ~(abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1))
\r
858 ==> &0 <= &1 - s /\ &0 <= --s <=> ~(&0 <= &1 - s /\ &0 <= --s) ==>
\r
859 abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1)`] THEN
\r
860 REWRITE_TAC[REAL_ARITH ` abs s * norm (v2 - v1) = abs (&1 - s) * norm (v1 - v2) + norm (v2 - v1)
\r
861 <=> norm (v2 - v1) = abs s * norm (v2 - v1) - abs (&1 - s) * norm (v1 - v2)`] THEN
\r
862 REWRITE_TAC[NORM_SUB] THEN
\r
863 REWRITE_TAC[REAL_ARITH ` abs s * norm (v1 - v2) - abs (&1 - s) * norm (v1 - v2) = ( abs s - abs (&1 - s)) * norm (v1 - v2)`] THEN
\r
864 DISCH_TAC THEN MATCH_MP_TAC(REAL_RING ` (abs s - abs (&1 - s)) = &1 ==> norm (v1 - v2) = (abs s - abs (&1 - s)) * norm (v1 - v2)`) THEN
\r
865 REWRITE_TAC[REAL_ARITH ` abs (&1 - s) = abs (s - &1)`] THEN
\r
866 MATCH_MP_TAC(REAL_ARITH ` abs s = s /\ abs (s - &1) = (s - &1) ==> abs s - abs (s - &1) = &1`) THEN REWRITE_TAC[REAL_ABS_REFL] THEN
\r
867 UNDISCH_TAC `~(&0 <= &1 - s /\ &0 <= --s)` THEN UNDISCH_TAC ` ~(&0 <= s /\ &0 <= &1 - s)` THEN REAL_ARITH_TAC);;
\r
869 let c_inv_nov18 = prove (` ~(norm ( x:real^3 - v1:real^3) = norm (x - v2:real^3) + norm (v2 - v1)) /\
\r
870 ~(norm ( x - v2) = norm (x - v1) + norm (v2 - v1)) /\
\r
871 ~(norm ( v1 - v2) = norm ( x - v1) + norm (x - v2)) ==> ~(x IN affine hull {v1 , v2})`, MESON_TAC[c_nov18]);;
\r
873 let fa5 = prove( `!a:real b:real c:real. a >= &2 /\ a <= #2.51 /\ b >= &2 /\ b <= #2.51 /\ c >= &2 /\ c <= #2.51
\r
874 ==> ~(a = b + c) /\ ~(b = a + c) /\ ~(c = a + b)`, REAL_ARITH_TAC);;
\r
876 let c_nov18e = prove( `(!x:real^3 y:real^3. x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\ v0:real^3 IN s
\r
877 ==> v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)
\r
878 ==> (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
879 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
880 ~(v = w) /\ norm (v - w) <= &2 * t0 \/
\r
881 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
882 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
883 ~(w = v) /\ norm (w - v) <= &2 * t0
\r
884 ==> ~(w IN affine hull {v0, v})`,
\r
885 REWRITE_TAC[MESON[NORM_SUB] ` (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
886 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
887 ~(v = w) /\ norm (v - w) <= &2 * t0 \/
\r
888 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
889 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
890 ~(w = v) /\ norm (w - v) <= &2 * t0 <=> (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
891 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
892 ~(w = v) /\ norm (w - v) <= &2 * t0 `] THEN REPEAT STRIP_TAC THEN
\r
893 UNDISCH_TAC ` w:real^3 IN affine hull {v0:real^3, v:real^3}` THEN
\r
894 REWRITE_TAC[TAUT ` w IN affine hull {v0, v} ==> F <=> ~(w IN affine hull {v0, v})`] THEN
\r
895 MATCH_MP_TAC(c_inv_nov18) THEN
\r
896 UNDISCH_TAC ` !x:real^3 y:real^3. x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2` THEN
\r
897 UNDISCH_TAC ` v0:real^3 IN (s:real^3->bool)` THEN UNDISCH_TAC ` v:real^3 IN (s:real^3->bool)` THEN
\r
898 UNDISCH_TAC ` w:real^3 IN (s:real^3->bool)` THEN UNDISCH_TAC ` norm (v:real^3 - v0) < &2 * t0` THEN
\r
899 UNDISCH_TAC ` norm (w:real^3 - v0) < &2 * t0` THEN UNDISCH_TAC ` norm (w:real^3 - v) <= &2 * t0` THEN
\r
900 UNDISCH_TAC ` ~(v:real^3 = v0)` THEN UNDISCH_TAC ` ~(w:real^3 = v0)` THEN UNDISCH_TAC ` ~(w:real^3 = v)` THEN
\r
901 REWRITE_TAC[t0] THEN REWRITE_TAC[REAL_ARITH ` &2 * #1.255 = #2.51`] THEN REWRITE_TAC[NORM_SUB] THEN
\r
902 REPEAT DISCH_TAC THEN MATCH_MP_TAC(fa5) THEN UNDISCH_TAC `norm (v0:real^3 - w) < #2.51` THEN
\r
903 REWRITE_TAC[TAUT ` norm (v0 - w) < #2.51
\r
904 ==> norm (v0 - w) >= &2 /\
\r
905 norm (v0 - w) <= #2.51 /\
\r
906 norm (v - w) >= &2 /\
\r
907 norm (v - w) <= #2.51 /\
\r
908 norm (v - v0) >= &2 /\
\r
909 norm (v - v0) <= #2.51
\r
910 <=> (norm (v0 - w) < #2.51
\r
911 ==> norm (v0 - w) >= &2 /\
\r
912 norm (v - w) >= &2 /\
\r
913 norm (v - w) <= #2.51 /\
\r
914 norm (v - v0) >= &2 /\
\r
915 norm (v - v0) <= #2.51 ) /\
\r
916 (norm (v0 - w) < #2.51
\r
917 ==> norm (v0 - w) <= #2.51 )`] THEN
\r
918 CONJ_TAC THENL[DISCH_TAC; REAL_ARITH_TAC] THEN UNDISCH_TAC ` norm (v:real^3 - v0) < #2.51` THEN
\r
919 REWRITE_TAC[TAUT ` norm (v - v0) < #2.51
\r
920 ==> norm (v0 - w) >= &2 /\
\r
921 norm (v - w) >= &2 /\
\r
922 norm (v - w) <= #2.51 /\
\r
923 norm (v - v0) >= &2 /\
\r
924 norm (v - v0) <= #2.51
\r
925 <=> (norm (v - v0) < #2.51
\r
926 ==> norm (v0 - w) >= &2 /\
\r
927 norm (v - w) >= &2 /\
\r
928 norm (v - w) <= #2.51 /\
\r
929 norm (v - v0) >= &2 ) /\
\r
930 (norm (v - v0) < #2.51
\r
931 ==> norm (v - v0) <= #2.51 )`] THEN CONJ_TAC THENL[DISCH_TAC;REAL_ARITH_TAC] THEN
\r
932 ASM_MESON_TAC[NORM_SUB]);;
\r
934 let c_nov18e1 = prove ( `((!x:real^3 y:real^3. x IN (s:real^3->bool) /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\ v0:real^3 IN s ) /\
\r
935 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
936 ((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
937 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
938 ~(v = w) /\ norm (v - w) <= &2 * t0 \/
\r
939 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
940 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
941 ~(w = v) /\ norm (w - v) <= &2 * t0 )
\r
942 ==> ~(w IN affine hull {v0, v})`,
\r
943 REWRITE_TAC[TAUT ` ((!x y. x IN s /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\ v0 IN s) /\
\r
944 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
945 ((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
946 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
948 norm (v - w) <= &2 * t0 \/
\r
949 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
950 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
952 norm (w - v) <= &2 * t0)
\r
953 ==> ~(w IN affine hull {v0, v})
\r
955 ((!x y. x IN s /\ y IN s /\ ~(x = y) ==> norm (x - y) >= &2) /\ v0 IN s)
\r
956 ==> (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0))
\r
957 ==> ((v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
958 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
960 norm (v - w) <= &2 * t0 \/
\r
961 (w IN s /\ norm (w - v0) < &2 * t0 /\ ~(w = v0)) /\
\r
962 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
964 norm (w - v) <= &2 * t0)
\r
965 ==> ~(w IN affine hull {v0, v})`] THEN REWRITE_TAC[c_nov18e]);;
\r
967 let c_nov18e2 = prove( `center_pac (s:real^3->bool) (v0:real^3) ==>
\r
968 (v:real^3 IN v_std s v0
\r
969 ==> {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {})`,
\r
970 DISCH_TAC THEN REWRITE_TAC[v_std;e_std;tru_pack] THEN ASM_REWRITE_TAC[] THEN
\r
971 REWRITE_TAC[SET_RULE ` u IN {x | x IN s /\ x IN open_ball v0 (&2 * t0)} DIFF {v0} <=>
\r
972 u IN s /\ u IN open_ball v0 (&2 * t0) /\ ~(u = v0)`] THEN
\r
973 REWRITE_TAC[open_ball] THEN REWRITE_TAC[SET_RULE ` v IN {y | norm (y - v0) < &2 * t0} <=> norm (v - v0) < &2 * t0 `] THEN
\r
974 ONCE_REWRITE_TAC[SET_RULE ` {{u, v} | (u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
975 (v IN s /\ norm (v - v0) < &2 * t0 /\ ~(v = v0)) /\
\r
976 ~(u = v) /\ d3 u v <= &2 * t0} =
\r
977 {{u, v'} | (u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
978 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
979 ~(u = v') /\ d3 u v' <= &2 * t0}`] THEN
\r
980 UNDISCH_TAC ` center_pac (s:real^3->bool) (v0:real^3)` THEN REWRITE_TAC[center_pac; packing_trg;d3;dist] THEN
\r
981 REWRITE_TAC[SET_RULE ` {w | {v, w} IN
\r
982 {{u, v'} | (u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
983 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
984 ~(u = v') /\ norm (u - v') <= &2 * t0}} INTER affine hull {v0, v} = {}
\r
985 <=> !w. w IN {w | {v, w} IN
\r
986 {{u, v'} | (u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
987 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
988 ~(u = v') /\ norm (u - v') <= &2 * t0}}
\r
989 ==> ~(w IN affine hull {v0, v})`] THEN DISCH_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
\r
990 UNDISCH_TAC ` (!x:real^3 y:real^3. (s:real^3->bool) x /\ s y /\ ~(x = y) ==> norm (x - y) >= &2) /\ s (v0:real^3)` THEN
\r
991 REWRITE_TAC[SET_RULE ` (s:real^3->bool) x <=> x IN s `] THEN REWRITE_TAC[SET_RULE `~(y IN (=) x) <=> ~(x = y)`] THEN DISCH_TAC THEN
\r
992 UNDISCH_TAC `(w:real^3) IN
\r
993 {w | {v:real^3, w} IN
\r
994 {{u:real^3, v'} | (u IN (s:real^3->bool) /\ norm (u - v0:real^3) < &2 * t0 /\ ~(u = v0)) /\
\r
995 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
996 ~(u = v') /\ norm (u - v') <= &2 * t0}}` THEN ONCE_REWRITE_TAC[IN_ELIM_THM] THEN
\r
997 REWRITE_TAC[fa2] THEN REWRITE_TAC[SET_RULE ` {v, w} = {u, v'} <=> ( v = u /\ w = v') \/ (v = v' /\ w = u)`] THEN
\r
998 REWRITE_TAC[TAUT ` ((u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
999 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
1000 ~(u = v') /\ norm (u - v') <= &2 * t0) /\
\r
1001 (v = u /\ w = v' \/ v = v' /\ w = u)
\r
1002 <=> (((u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
1003 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
1004 ~(u = v') /\ norm (u - v') <= &2 * t0) /\
\r
1005 v = u /\ w = v') \/ (((u IN s /\ norm (u - v0) < &2 * t0 /\ ~(u = v0)) /\
\r
1006 (v' IN s /\ norm (v' - v0) < &2 * t0 /\ ~(v' = v0)) /\
\r
1007 ~(u = v') /\ norm (u - v') <= &2 * t0) /\
\r
1008 v = v' /\ w = u)`] THEN DISCH_TAC THEN MATCH_MP_TAC(c_nov18e1) THEN ASM_MESON_TAC[]);;
\r
1010 let c_nov18e3 = prove( `center_pac (s:real^3->bool) (v0:real^3)
\r
1011 ==> (v:real^3 IN v_std s v0
\r
1013 {w | {v, w} IN e_std s v0} p /\
\r
1014 {w | {v, w} IN e_std s v0} q /\
\r
1015 p = q + h % (v0 - v)
\r
1018 ==> {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {})`,
\r
1019 REWRITE_TAC[TAUT ` center_pac s v0
\r
1020 ==> (v IN v_std s v0
\r
1022 {w | {v, w} IN e_std s v0} p /\
\r
1023 {w | {v, w} IN e_std s v0} q /\
\r
1024 p = q + h % (v0 - v)
\r
1027 ==> {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {})
\r
1028 <=> ( center_pac s v0
\r
1029 ==> (v IN v_std s v0
\r
1031 {w | {v, w} IN e_std s v0} p /\
\r
1032 {w | {v, w} IN e_std s v0} q /\
\r
1033 p = q + h % (v0 - v)
\r
1036 ==> (v IN v_std s v0
\r
1037 ==> {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {}))`] THEN
\r
1038 REWRITE_TAC[c_nov18e2;c_nov1_17]);;
\r
1040 let fan3_lemma = prove(`!(v0:real^3) (s:real^3->bool). center_pac s v0 ==> fan3 (v0,v_std s v0,e_std s v0 )`, REPEAT GEN_TAC THEN
\r
1041 REWRITE_TAC[fan3;cyclic_set] THEN DISCH_TAC THEN GEN_TAC THEN
\r
1042 REWRITE_TAC[TAUT ` v IN v_std s v0
\r
1044 FINITE {w | {v, w} IN e_std s v0} /\
\r
1046 {w | {v, w} IN e_std s v0} p /\
\r
1047 {w | {v, w} IN e_std s v0} q /\
\r
1048 p = q + h % (v0 - v)
\r
1050 {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {} <=>
\r
1051 ( v IN v_std s v0 ==> ~(v0 = v)) /\ ( v IN v_std s v0 ==> FINITE {w | {v, w} IN e_std s v0}) /\
\r
1052 ( v IN v_std s v0 ==> (!p q h.
\r
1053 {w | {v, w} IN e_std s v0} p /\
\r
1054 {w | {v, w} IN e_std s v0} q /\
\r
1055 p = q + h % (v0 - v)
\r
1057 ( v IN v_std s v0 ==> {w | {v, w} IN e_std s v0} INTER affine hull {v0, v} = {})`] THEN
\r
1058 CONJ_TAC THENL[REWRITE_TAC[v_std;DIFF] THEN SET_TAC[]; ALL_TAC] THEN
\r
1059 CONJ_TAC THENL[REWRITE_TAC[e_std] THEN ONCE_REWRITE_TAC[SET_RULE `{{u, v} | u IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
1060 v IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
1062 d3 u v <= &2 * t0} = {{x, y} | x IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
1063 y IN tru_pack v0 (&2 * t0) s DIFF {v0} /\
\r
1065 d3 x y <= &2 * t0}`] THEN DISCH_TAC THEN ONCE_REWRITE_TAC[lemmaf3] THEN
\r
1066 MATCH_MP_TAC (lemmaf33) THEN MATCH_MP_TAC (fini_lemma) THEN
\r
1067 UNDISCH_TAC `center_pac (s:real^3->bool) (v0:real^3)` THEN REWRITE_TAC[infi_lemma2];
\r
1068 UNDISCH_TAC `center_pac (s:real^3->bool) (v0:real^3)` THEN REWRITE_TAC[c_nov18e3]]);;
\r
1070 (*=====================================================================*)
\r
1071 (* end of fan3_lemma*)
\r
1072 (*=====================================================================*)
\r