legacy/oldleg/assembly.ml

   1 (* Main estimate file*)\r
   2 (* Author: PHAN HOANG CHON *)\r
   3 (*========================================================*)\r
   4 \r
   5 (*\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
  11 *)\r
  12 \r
  13 (*========================================================*)\r
  14 (* These definitions are defined by other authors*)\r
  15 (*========================================================*)\r
  16 (*Some constant*)\r
  17 \r
  18 (*arctan2 function is defined in definition_kepler.ml*)\r
  19 \r
  20 let delta_tet = new_definition (`delta_tet = sqrt8 * atn2(&5, sqrt2)`);;\r
  21 \r
  22 let delta_oct = new_definition (`delta_oct = (( &3* pi_rt18 - delta_tet)*( &1 / &2 ))`);;\r
  23 \r
  24 (*========================================================*)\r
  25 \r
  26 let lambda_v = new_definition (`lambda_v = (-- &4)* delta_oct `);;\r
  27 \r
  28 let lambda_s = new_definition (`lambda_s = (&1)/(&3) `);;\r
  29 \r
  30 let lambda_oct = new_definition (`lambda_oct = (lambda_v , lambda_s) `);;\r
  31 \r
  32 (*========================================================*)\r
  33 \r
  34 (* benign redefinition *)\r
  35 let open_ball = new_definition `open_ball (x:real^3) (r:real)= { y | norm(y-x)< r }`;;\r
  36 \r
  37 \r
  38 \r
  39 (*========================================================*)\r
  40 \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
  43 diagonal of d.\r
  44 \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
  47 *)\r
  48 \r
  49 (*========================================================*)\r
  50 \r
  51 (* benign redef *)\r
  52 let diag = new_definition ` diag d q s = ( quarter q s /\\r
  53                  ( ? x y. \r
  54                       ! v1 v2.\r
  55                            x IN q /\ y IN q /\\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
  59 \r
  60 (* benign *)\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
  62 \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
  66 \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
  70 \r
  71 (* Definition 7.20 =============================================*)\r
  72 \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
  76 \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
  80                     \r
  81 (* Definition 7.21 =============================================*)\r
  82 \r
  83 let VC1 = new_definition ` VC1 v s d =  VC v d INTER conv s `;;\r
  84 \r
  85 let VCt = new_definition ` VCt x t s d \r
  86                         = VC1 x s d INTER open_ball x t `;;\r
  87 \r
  88 (* Definition 7.22 =============================================*)\r
  89 \r
  90 let sv = new_definition ` sv x p d = lambda_v * vol(VC1 x p d) + lambda_s * solid x (conv0 p) `;;\r
  91 \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
  97 \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
 117 \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
 121                   \r
 122 (* Definition 7.23 =================================================*)\r
 123 \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
 129                             \r
 130 (* The definition 7.24 =============================================*)\r
 131 \r
 132 let sv0 = new_definition ` sv0 v s d = sovo v (VCt v t0 s d) lambda_oct `;;\r
 133 \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
 136                                       else v `;;\r
 137 \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
 152 \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
 167 \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
 169 \r
 170 let fan4 = new_definition`fan4(x,V,E):bool<=> (!e. (e IN E) ==> (aff_gt {x} e INTER V={}))`;;\r
 171 \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
 185 \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
 194 \r
 195 (* lemma_grap*)\r
 196 \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
 200                ~(u = v) /\\r
 201                d3 u v <= &2 * t0}`;;\r
 202 \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
 205            ~(u = v) /\\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
 208            ~(u = v) /\\r
 209            d3 u v <= &2 * t0}`,SET_TAC[]);;\r
 210 \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
 222 \r
 223 (*unions_lemma*)\r
 224 \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
 228            ~(u = v) /\\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
 232            ~(u1 = v1) /\\r
 233            d3 u1 v1 <= &2 * t0}`,SET_TAC[]);;\r
 234 \r
 235 let in_lemma1 = REWRITE_CONV[IN_ELIM_THM]\r
 236 `u IN\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
 239                   ~(u1 = v1) /\\r
 240                   d3 u1 v1 <= &2 * t0}`;;\r
 241 \r
 242 let in_lemma = ONCE_REWRITE_CONV[IN_ELIM_THM]\r
 243 `x IN\r
 244      {y | ?u. u IN\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
 247                           ~(u1 = v1) /\\r
 248                           d3 u1 v1 <= &2 * t0} /\\r
 249               y IN u}`;;\r
 250 \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
 254             ~(u1 = v1) /\\r
 255             d3 u1 v1 <= &2 * t0) /\\r
 256            u = {u1, v1}) /\\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
 260             ~(u1 = v1) /\\r
 261             d3 u1 v1 <= &2 * t0 /\\r
 262            x IN { u1, v1 }))`, MESON_TAC[]);;\r
 263 \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
 267                           ~(u1 = v1) /\\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
 272                           ~(u1 = v1) /\\r
 273                           d3 u1 v1 <= &2 * t0} /\\r
 274               y IN u}`,SET_TAC[]);;\r
 275 \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
 279       ~(u1 = v1) /\\r
 280       d3 u1 v1 <= &2 * t0 /\\r
 281       x = u1 \/\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
 284       ~(u1 = v1) /\\r
 285       d3 u1 v1 <= &2 * t0 /\\r
 286       x = v1) <=> \r
 287   ( ?v1.\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
 290       ~(x = v1) /\\r
 291       d3 x v1 <= &2 * t0 ) \/\r
 292   ( ?u1.\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
 295       ~(u1 = x) /\\r
 296       d3 u1 x <= &2 * t0 )`,MESON_TAC[]);;\r
 297 \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
 307                                         ~(u1 = v1) /\\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
 311                                          ~(u1 = v1) /\\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
 315                                         ~(u1 = v1) /\\r
 316                                          d3 u1 v1 <= &2 * t0 /\\r
 317                                          x = v1 )`] THEN \r
 318                                      REWRITE_TAC[exist_lemma1] THEN STRIP_TAC);;\r
 319 (*==================================================================================*)\r
 320 (* end of unions_lemma*)\r
 321 (*==================================================================================*)\r
 322 \r
 323 (*fan1_lemma*)\r
 324 \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
 327 \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
 330 \r
 331 let infi_lemma2 = prove(`center_pac s v0 ==> FINITE (tru_pack v0 (&2 * t0) s) `, REWRITE_TAC[lemma7_1]);;\r
 332 \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
 337 \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
 348 \r
 349 (* fan2_lemma*)\r
 350 \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
 356 \r
 357 (* fan3_lemma*)\r
 358 \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
 362                ~(x = y) /\\r
 363                d3 x y <= &2 * t0} <=>\r
 364      (?x y.\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
 367            ~(x = y) /\\r
 368            d3 x y <= &2 * t0) /\\r
 369           {v, w} = {x, y})`, REWRITE_TAC[IN_ELIM_THM]);;\r
 370 \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
 374                ~(x = y) /\\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
 377 \r
 378 let lemmaf32 = prove (` FINITE (tru_pack v0 (&2 * t0) s DIFF {v0})\r
 379  ==> FINITE\r
 380      {w | ?x y.\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
 383                ~(x = y) /\\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
 388                ~(x = y) /\\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
 392  ==> FINITE\r
 393      {w | ?x y.\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
 396                ~(x = y) /\\r
 397                d3 x y <= &2 * t0) /\\r
 398               {v, w} = {x, y}}`, MESON_TAC[lemma_subset]);;\r
 399 \r
 400 let lemmaf33 = prove(` FINITE (tru_pack v0 (&2 * t0) s DIFF {v0})\r
 401      ==> FINITE\r
 402          {w | ?x y.\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
 405                    ~(x = y) /\\r
 406                    d3 x y <= &2 * t0) /\\r
 407                   {v, w} = {x, y}}`, REWRITE_TAC[lemmaf32] THEN REWRITE_TAC[FINITE_SUBSET]);;\r
 408 \r
 409 let lemmaf34 = prove (` condC (#2.6) (&2) (&2) (#2.6) (&2) (&2)`, REWRITE_TAC[condC;delta_x] THEN REAL_ARITH_TAC);;\r
 410 \r
 411 (* prove lemma have_not_prove*)\r
 412 \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
 415 \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
 418 \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
 422 \r
 423 let lemma_c11 = prove (`&0 < &1 / ( h + &1) ==> &0 <= &1 / (h + &1) `, REAL_ARITH_TAC);;\r
 424 \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
 427 \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
 431 \r
 432 let lemma_ch1 = prove (`&0 < h / ( h + &1) ==> &0 <= h / (h + &1) `, REAL_ARITH_TAC);;\r
 433 \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
 436 \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
 440 \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
 457 \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
 493 \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
 502 \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
 505 \r
 506 let vec_le = prove (` (h:real) % ( v0:real^3 - v ) = -- h % (v - v0)`, VECTOR_ARITH_TAC);;\r
 507 \r
 508 \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
 512 \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
 521 \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
 524 \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
 527                                d3 v1 v2 >= m12 /\\r
 528                                d3 v2 v3 >= m23 /\\r
 529                                d3 v3 v4 >= m34 /\\r
 530                                d3 v4 v1 >= m14 /\\r
 531                                d3 v1 v3 <  M13 /\\r
 532                                d3 v2 v4 <= M24 /\\r
 533                                condC M13 m12 m14 M24 m34 m23 \r
 534                             ==> conv {v1 , v3} INTER conv {v2 , v4} = {}`);;\r
 535 \r
 536 let lemma_3_4_c = new_axiom (` !(p:real^3) (q:real^3) (v:real^3) (v0:real^3).\r
 537                                d3 p q >= m12 /\\r
 538                                d3 q v >= m23 /\\r
 539                                d3 v v0 >= m34 /\\r
 540                                d3 v0 p >= m14 /\\r
 541                                d3 p v <  M13 /\\r
 542                                d3 q v0 <= M24 /\\r
 543                                condC M13 m12 m14 M24 m34 m23 \r
 544                             ==> conv {p , v} INTER conv {q , v0} = {}`);;\r
 545 \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
 552 \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
 555 \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
 563 \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
 567 \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
 570 \r
 571 let chon = SET_RULE `!s:A->bool. s IN { t | P t} ==> INTERS { t| P t} SUBSET s`;;\r
 572 \r
 573 let subset_two_points = SET_RULE `{a , b } SUBSET s <=> a IN s /\ b IN s`;;\r
 574 \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
 577 \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
 583 \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
 588 \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
 601 \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
 607 \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
 610 \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
 707 \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
 725                                      v0 IN s /\\r
 726                                      v IN s /\\r
 727                                      norm (v - v0) < &2 * t0 /\\r
 728                                      ~(v = v0) /\\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
 731                                     ~(v = p) /\\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
 735                                     ~(p = v) /\\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
 739                                     ~(v = q) /\\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
 743                                    ~(q = v) /\\r
 744                                     norm (q - v) <= &2 * t0)\r
 745                                      ==> ~(p = q + h % (v0 - v)) <=> \r
 746                                      ~(p:real^3 = q) \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
 762 \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
 766                 ~(u = v') /\\r
 767                 norm (u - v') <= &2 * t0}`;;\r
 768 \r
 769 let fa1 = REWRITE_CONV[IN_ELIM_THM]`p IN {w | {v, w} IN e_std s v0}`;;\r
 770 \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
 773                                ==> (!p q h.\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
 777                                    ==> p = q))`, \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
 784                                         ==> p = q <=> \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
 788                                        center_pac s v0 /\\r
 789                                        v IN v_std s v0 /\\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
 802                                              ~(u = v) /\\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
 806                                             ~(u = v') /\\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
 815 \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
 868 \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
 872 \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
 875 \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
 933 \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
 947                                              ~(v = w) /\\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
 951                                             ~(w = v) /\\r
 952                                              norm (w - v) <= &2 * t0)\r
 953                                              ==> ~(w IN affine hull {v0, v})\r
 954                                      <=>\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
 959                                              ~(v = w) /\\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
 963                                             ~(w = v) /\\r
 964                                               norm (w - v) <= &2 * t0)\r
 965                                          ==> ~(w IN affine hull {v0, v})`] THEN REWRITE_TAC[c_nov18e]);;\r
 966 \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
1009 \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
1012                             ==> (!p q h.\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
1016                                      ==> p = q)) /\\r
1017                            (v IN v_std s v0\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
1021                                            ==> (!p q h.\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
1025                                                        ==> p = q)) /\\r
1026                                          (v IN v_std s v0\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
1030                                              ==> (!p q h.\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
1034                                                         ==> p = q))) /\\r
1035                                       ( center_pac s v0\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
1039 \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
1043                                       ==> ~(v0 = v) /\\r
1044                                            FINITE {w | {v, w} IN e_std s v0} /\\r
1045                                           (!p q h.\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
1049                                                  ==> p = q) /\\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
1056                                                           ==> p = q)) /\\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
1061                                                       ~(u = v) /\\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
1064                                                      ~(x = y) /\\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
1069 \r
1070 (*=====================================================================*)\r
1071 (* end of fan3_lemma*)\r
1072 (*=====================================================================*)\r