(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definitions File *)
(* Chapter: Local Fan                                                      *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-25                                                           *)
(* ========================================================================== *)




module Local_defs  = struct

(* the definition of hypermap *)

let exist_hypermap = 
prove(`?H:((A->bool)#(A->A)#(A->A)#(A->A)). FINITE (FST H) /\ (FST(SND H)) permutes (FST H) /\ (FST(SND(SND H))) permutes (FST H) /\ (SND(SND(SND H))) permutes (FST H) /\ (FST(SND H)) o (FST(SND(SND  H))) o (SND(SND(SND H))) = I`,
EXISTS_TAC
`({},I,I,I):(A->bool)#(A->A)#(A->A)#(A->A)` THEN REWRITE_TAC[FINITE_RULES; PERMUTES_I; I_O_ID]);;

let hypermap_tybij = (new_type_definition "hypermap" ("hypermap", "tuple_hypermap")exist_hypermap);;

let dart = new_definition `dart (H:(A)hypermap) = FST (tuple_hypermap H)`;;

let edge_map = new_definition `edge_map (H:(A)hypermap) = FST(SND(tuple_hypermap H))`;;

let node_map = new_definition `node_map (H:(A)hypermap) = FST(SND(SND(tuple_hypermap H)))`;;

let face_map = new_definition `face_map (H:(A)hypermap) = SND(SND(SND(tuple_hypermap H)))`;;

(* edges, nodes and faces of a hypermap *)

parse_as_infix("POWER",(24,"right"));;

let POWER = new_recursive_definition num_RECURSION 
  `(!(f:A->A). f POWER 0  = I) /\  
   (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;

let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;

let edge = new_definition `edge (H:(A)hypermap) (x:A) = orbit_map (edge_map H) x`;;

let node = new_definition `node (H:(A)hypermap) (x:A) = orbit_map (node_map H) x`;;

let face = new_definition `face (H:(A)hypermap) (x:A) = orbit_map (face_map H) x`;;

(* some definitions on orbits *)

let set_of_orbits = new_definition `set_of_orbits (D:A->bool) (f:A->A) = {orbit_map f x | x IN D}`;;

let number_of_orbits = new_definition `number_of_orbits (D:A->bool) (f:A->A) = CARD(set_of_orbits D f)`;;


(* the orbits on hypermaps*)

let edge_set = new_definition `edge_set (H:(A)hypermap) = set_of_orbits (dart H) (edge_map H)`;;

let node_set = new_definition `node_set  (H:(A)hypermap) = set_of_orbits (dart H) (node_map H)`;;

let face_set = new_definition `face_set (H:(A)hypermap) = set_of_orbits (dart H) (face_map H)`;;


(* some special kinds of hypergraphs *)

let plain_hypermap = new_definition `plain_hypermap (H:(A)hypermap) <=> edge_map H o edge_map H = I`;;


let simple_hypermap = new_definition `simple_hypermap (H:(A)hypermap) <=>
    (!x:A. x IN dart H ==> (node H x) INTER (face H x) = {x})`;;

(* fan definitions *)

let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;

let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;

let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;

let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;

let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;

let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
fan6(x,V,E)/\ fan7(x,V,E)`;;


let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;

let set_of_edges=new_definition`set_of_edges v E={w|{v,w} IN E}`;;

let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;

(* local fan def. To Here. *)

let zfan = new_definition `zfan (V,E) = FAN (vec 0 ,V,E)`;;

let hypermap_of_fan = `hypermap_of_zfan
  (V,E) = `;;

let tuple_of_dart = `tuple_of_dart (V,E) 
  (v,w) = 
  (vec 0 , v , w, ...)`;;

let azim_fandart = `azim_fandart H (v,w) =
  (let (v0,v1,v2,v3) = tuple_of_dart H (v,w)
   in azim v0 v1 v2 v3)  `;;

let WRGCVDR1_concl = `!(V,E,f). convex_local_fan (V,E,f) ==> BIJ (\ (v,w). v) f V`;;

let WRGCVDR2_concl = `!(V,E,f). convex_local_fan (V,E,f) ==> cyclic_permutation rho_convex_local_fan V`;;

(* nd = FST *)


let LVDUCXU1_concl = `!V E f. zfan (V,E) /\
  (f IN face_set(hypermap_of_zfan (V,E))) 
   ==> local_fan (localization(V,E,f))
   `;;

let LVDUCXU2_concl = `!V E f x. zfan (V,E) /\
  (f IN face_set(hypermap_of_zfan (V,E))) /\
  (x IN f) 
   ==> (tuple_of_dart H x = tuple_of_dart


end;;