(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definitions                                                                  *)
(* Chapter: Tame Hypermap                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-07                                                           *)
(* ========================================================================== *)

(*

Definitions file for Local Fans

This file was split off from tame/tame_defs.hl in July 2010
when it was discovered that there are many incompatible
definitions betwen the Local Fans chapter and the Tame chapter.

This file is not currently part of the build.
*)

flyspeck_needs "hypermap/hypermap.hl";;
flyspeck_needs "fan/fan_defs.hl";;
flyspeck_needs "packing/pack_defs.hl";;

module Local_fan_defs  = struct



let cwedge = new_definition `cwedge v0 v1 w1 w2 =
         {y |  &0 <= azim v0 v1 w1 y /\
              azim v0 v1 w1 y <= azim v0 v1 w1 w2}`;;


let cw_dart_fan=new_definition
`cw_dart_fan (V:real^3->bool) (E:(real^3->bool)->bool) ((v:real^3),(w:real^3))=  
if (CARD (set_of_edge v V E) > 1) 
then cwedge (vec 0) v w (sigma_fan (vec 0) V E v w)
else (:real^3)`;;


let local_fan = new_definition `local_fan (V,E,f) <=>
   FAN (vec 0,V,E) /\ 
   f IN face_set_of_fan (V,E) /\
   (hypermap_of_fan (V,E)) iso (cyclic_hypermap I I (CARD f))`;;


let convex_local_fan = new_definition `convex_local_fan (V,E,f) <=>
    local_fan (V,E,f) /\
    (!x. (x IN f) ==> azim_dart (V,E) x <= pi) /\
    (!x. (x IN f) ==> V SUBSET cw_dart_fan V E x)`;;


let rho_node1 = new_definition 
  `rho_node1 (V:A1,E:A2,f:A3#A4->bool) v = @w. (v,w) IN f`;;


let order_permutation = new_definition
  `order_permutation (p:A->A) = (minimal) { m | (p POWER m = I) /\ (m > 0) }`;;


let is_cyclic_permutation = new_definition
  `is_cyclic_permutation rho s <=> 
   rho permutes s /\ s HAS_SIZE (order_permutation rho)`;;


let interior_angle = new_definition 
  `interior_angle (V,E,f) v = azim_dart (V,E) (v,(rho_node1 (V,E,f) v))`;;


let cw_node_fan = new_definition
  `cw_node_fan (V,E,f) v = cw_dart_fan V E (v,rho_node1(V,E,f) v)`;;


let w_node_fan = new_definition (* 4th component is ignored *)
  `w_node_fan (V,E,f) v = w_dart_fan (vec 0) V E (vec 0,v,rho_node1(V,E,f) v,v)`;;


let localization = new_definition `localization (V,E,f) = 
  {v | v IN V /\ (?w. w IN V /\ (v,w) IN f)},
   { {v,w} | {v,w} IN E /\  (v,w) IN f},
   f`;;


let is_generic_clf = new_definition `is_generic_clf (V,E,f:A) <=> 
  (! v w (u:real^3).  (u IN V) /\ {v,w} IN E ==>   
    aff_ge { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {})`;;


let is_circular_clf = new_definition `is_circular_clf (V,E,f:A) <=> 
  (? v w (u:real^3). (u IN V) /\ {v,w} IN E /\
     ~( aff_gt { vec 0 } { v , w} INTER aff_lt { vec 0 } {u } = {}))`;;


let is_lunar_clf = new_definition `is_lunar_clf (V,E,f:A) (v,w) <=> 
  v IN V /\ w IN V /\ ~(is_circular_clf (V,E,f)) /\
    collinear {(vec 0) , v, w}`;;


let is_flat = new_definition `is_flat (V,E,f) v <=>
  interior_angle (V,E,f) v = pi`;;



let is_deformation_clf  = new_definition 
  `is_deformation_clf  phi V s = (!v x. v IN V ==> (phi v) continuous at x within s)`;;


let node_deform = new_definition
  `node_deform phi V t = { phi v t | v IN V}`;;


let edge_deform = new_definition
  `edge_deform phi V E t = { {phi v t, phi w t} | {v,w} IN E}`;;


let face_deform = new_definition
  `face_deform phi V f t = { (phi v t, phi w t) | (v,w) IN f}`;;


let per = new_definition
`per(V,E,f) v k = sum (0..k-1) 
   ( \ i. arcV (vec 0) ((rho_node1 (V,E,f) POWER i) v) ((rho_node1 (V,E,f) POWER (i+1)) v))`;;


let perimeter = new_definition
`perimeter(V,E,f)  = per(V,E,f) (CHOICE V)  (CARD(f))`;;



let perimeterbound = new_definition `perimeterbound (V,E) = 
  (!f. f IN face_set_of_fan (V,E) ==> 
       sum f (\ (v,w).  arcV (vec 0) (v:real^3) w ) <= &2 * pi)`;;



let special_fan = new_definition
`special_fan (V,E,f,S) <=> packing V /\ V SUBSET ball_annulus /\ convex_local_fan (V,E,f) /\
    S SUBSET E /\ 
   (! v w.  {v,w} IN S ==>( dist(v,w) = &2 * h0)) /\
   (! v w.  {v,w} IN E ==> (dist(v,w) <= &2 * h0)) /\
   (! v w.  v IN V /\ w IN V /\ ~(v=w) /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w))`;;


let r_special = new_definition
  `r_special (V,E,f,S) = CARD(E) - CARD(S)`;;


let s_special = new_definition
  `s_special (V,E,f,S) = CARD(S)`;;


let d2_tame = new_definition  (* deprecate *)
  `d2_tame r s = if (r + 2*s > 3) 
  then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4)
  else #0.0`;;


let tame_table_d = new_definition
  `tame_table_d r s = if (r + 2*s > 3) 
  then #0.103 * (&2 - &s) + #0.2759 * (&r + &2* &s - &4)
  else #0.0`;;
  (* preferred term *)



let d2_special = new_definition
   `d2_special (V,E,f,S) = d2_tame (r_special (V,E,f,S)) (s_special (V,E,f,S))`;;


let vertex_datum = new_definition
  `vertex_datum p k = IMAGE p (0..(k-1))`;;


let edge_datum = new_definition
  `edge_datum p k  = { { p i, p ((i+1) MOD k) }  |i| i IN (0..(k-1)) }`;;


let face_datum = new_definition
  `face_datum p k = { (p i, p ((i+1) MOD k)) |i|  i IN (0..(k-1)) }`;;
 


let special_datum = new_definition
  `special_datum p k J = { (p i, (p((i+1) MOD k))) | i | i IN J }`;;


let fan_datum = new_definition
  `fan_datum p k J <=> 
      IMAGE p (0..(k-1)) SUBSET ball_annulus /\
      (!i j. (i < k) /\ (j < k) /\ dist(p i,p j) < &2 ==> (i=j)) /\
      (!i. (i<k) /\ (i IN J) ==> dist(p i, p ((i+1) MOD k)) = &2 * h0) /\
      (!i. (i<k) ==> dist(p i, p ((i+1) MOD k)) <= &2 * h0) /\
      (!i j. (i+1<j) /\ (j<k) /\ (j +1 < i+k) ==> &2 * h0 <= dist(p i, p j)) /\
      (CARD(J) <= 3) /\  (3 <= k) /\ (k + CARD(J) <= 6) /\
    (!i. (i<k) ==> azim (vec 0) (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) <= pi) /\
     (!i j. (i<k) /\ (j<k) ==> p j IN cwedge (vec 0)  (p i) (p ((i+1) MOD k)) (p ((i + k - 1) MOD k)) )`;;


let vertex_slice = new_definition
  `vertex_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER i) v | i IN (1..j)  }`;;


let edge_slice = new_definition
   `edge_slice (V,E,f) v j = { (rho_node1 (V,E,f) POWER j) v,  v } INSERT 
  { {(rho_node1 (V,E,f) POWER i) v  ,  (rho_node1 (V,E,f) POWER (i+1)) v } | i IN (1..(j-1)) }`;;
  

let face_slice = new_definition
   `face_slice (V,E,f) v j = ( (rho_node1 (V,E,f) POWER j) v,  v ) INSERT 
  { ((rho_node1 (V,E,f) POWER i) v  ,  (rho_node1 (V,E,f) POWER (i+1)) v ) | i IN (1..(j-1)) }`;;


let kmin = new_definition
  `kmin = (minimal) 
   ({ k | (k=0) /\ (! V E f S. special_fan (V,E,f,S) ==>
       tauVEF (V,E,f) >= d2_special (V,E,f,S) ) } UNION 
    { k | ? V E f S. (k= CARD(E)) /\ special_fan (V,E,f,S) /\ tauVEF(V,E,f) < d2_special (V,E,f,S) } )`;;


let taumin = new_definition
  `taumin = inf (
     { tauVEF (V,E,f) - d2_special (V,E,f,S) | special_fan (V,E,f,S) /\ (kmin = CARD E) } UNION 
     { t | (t= &0) /\ (kmin = 0) })`;;


let minimal_fan = new_definition
  `minimal_fan (V,E,f,S) <=> special_fan (V,E,f,S) /\ (kmin = CARD E) /\ 
    (taumin =  tauVEF (V,E,f) - d2_special (V,E,f,S))`;;


let s_extremal_edge = new_definition
  `s_extremal_edge (V,E,f,S) (v,w) <=> (v,w ) IN S \/ (dist(v,w) IN {&2, &2 * h0 }) `;;


let s_minimal_edge = new_definition
   `s_minimal_edge (V,E,f,S) (v,w) <=> (v,w) IN S \/ (dist(v,w) = &2) `;;


let special_feature_extreme_edge = new_definition
   `special_feature_extreme_edge (V,E,f,S) = (!v w. {v,w} IN E ==> s_extremal_edge (V,E,f,S) (v,w))`;;




end;;