(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Conclusions *)
(* Chapter: Fan                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-05-14                                                           *)
(* ========================================================================== *)

flyspeck_needs "fan/fan_defs.hl";;

module Fan_concl  = struct

  open Fan_defs;

  
let fan_card = new_definition `fan_card (V,E) <=> FINITE V /\ ~(V SUBSET {})`;;
  
  
let fan_origin = new_definition `fan_origin (V,E) <=> ~(vec 0 IN V)`;;
  
let fan_nonparallel = new_definition `fan_nonparallel (V,E) <=> (!e. (e IN E) ==> ~(collinear ({vec 0} UNION e)))`;;
  
let fan_intersection = new_definition `fan_intersection(V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
==> ((aff_ge {vec 0} e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;
  
let fan = new_definition `fan (V,E) <=>  ((UNIONS E) SUBSET V) /\ graph(E) /\ fan_card(V,E) /\ fan_origin(V,E)/\
fan_nonparallel(V,E)/\ fan_intersection(V,E)`;;

(* move to fan_misc.hl *)
  
let fan_of_FAN = 
prove(`!V E. FAN((vec 0), V,E) = fan(V,E)`,

        REWRITE_TAC[fan,fan_origin,fan_card,fan_nonparallel,fan_intersection,
             FAN, fan1,fan2,fan6,fan7] THEN MESON_TAC[]
	);;


 let CTVTAQA_concl = `!V E E'. fan (V,E) /\ (E' SUBSET E)  ==> fan (V,E')`;;

 let XOLHLED_concl = `!V E v. fan (V,E) /\ (v IN V) ==> cyclic_set(set_of_edge v V E) (vec 0) v`;;  (* introduction.hl:XOHLED *)

 let AAUHTVE_concl = `!V E. fan(V,E) ==>
    (hypermap_of_fan (V,E))
    (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fan_pair (V,E) d) = d)) /\
    (!d. d IN dart1_of_fan ==> (e_fan_pair (V,E) (e_fa


 let PIIJBJK_concl= `!x V E . FAN (x,V,E) /\ fan81 (x,V,E) ==> conforming_fan (x,V,E)`;;
 



end;;