(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Conclusions                                                                  *)
(* Chapter: Tame Hypermap                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-27                                                           *)
(* ========================================================================== *)

(*
Conclusions file for Tame Hypermap 
*)


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

module Tame_concl  = struct

  let PPHEUFG_concl = `!(H:(A)hypermap). tame_hypermap H <=> tame_hypermap (opposite_hypermap H)`;;

  let RUNOQPQ_concl = `!(H:(A)hypermap). tame_hypermap H ==> restricted_hypermap H`;;

  (* WTEMDTA_concl skipped. Tame hypermap classification theorem. *)

  let UBHDEUU1_concl = `! V.  packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ESTD V)`;;

  let UBHDEUU2_concl = `! V.  packing V /\ V SUBSET ball_annulus ==> FAN(vec 0, V, ECTC V)`;;

  let FATUGPD_concl = `!V. packing V /\ V SUBSET ball_annulus ==>
   (?W phi.  BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\ 
        (!w. w IN W ==>  (set_of_edge w W (ECTC W) = {}) \/ (surrounded_node (W,(ECTC W)) w)))`;;

  let FJLBXS_concl = `!V. packing V /\ V SUBSET ball_annulus ==>
    (?W phi. BIJ phi V W /\ (!v. v IN V ==> norm(v) = norm(phi v)) /\ 
        (!w. w IN W ==>  (set_of_edge w W (ESTD W) = {}) \/ (surrounded_node (W,(ESTD W)) w)))`;;

  let FCDJDOT_concl = `(?W. packing W /\ W SUBSET ball_annulus /\ scriptL W > &12) ==>
       (?V. contravening V)`;;

  let HRXEFDM_concl = `!V.  contravening V  ==>
     (  sum (face_set_of_fan (V,ESTD V)) (\ f.  tauVEF (V,ESTD V,f) ) < &4 * pi - &20 * sol0 )`;;

  let JGTDEBU1_concl = `!V. contravening V ==> 
       planar_hypermap (hypermap_of_fan (V, ESTD V))`;;

  let JGTDEBU2_concl = `!V. contravening V ==> 
       plain_hypermap (hypermap_of_fan (V, ESTD V))`;;

  let JGTDEBU3_concl = `!V. contravening V ==> 
       connected_hypermap (hypermap_of_fan (V, ESTD V))`;;

  let JGTDEBU4_concl = `!V. contravening V ==> 
       simple_hypermap (hypermap_of_fan (V, ESTD V))`;;

  let JGTDEBU5_concl = `!V. contravening V ==> 
       is_edge_nondegenerate  (hypermap_of_fan (V, ESTD V))`;;

  let  JGTDEBU6_concl = `!V. contravening V ==> 
       no_loops  (hypermap_of_fan (V, ESTD V))`;;

  let  JGTDEBU7_concl = `!V. contravening V ==> 
       is_no_double_joints  (hypermap_of_fan (V, ESTD V))`;;

  let  JGTDEBU8_concl = `!V. contravening V ==> 
       number_of_faces  (hypermap_of_fan (V, ESTD V)) >= 3 `;;

  let  JGTDEBU10_concl = `!V. contravening V ==> 
       tame_10  (hypermap_of_fan (V, ESTD V))`;;

  let  JGTDEBU11_concl = `!V. contravening V ==> 
       tame_11a  (hypermap_of_fan (V, ESTD V))`;;

  let CDTETAT_concl = `!V x. contravening V /\ x IN dart_of_fan (V,ESTD V) /\ tame_hypermap_calcs ==>
       (let (p,q,r) = type_of_node (hypermap_of_fan (V, ESTD V)) x in
             ((p,q+r) IN { (0,3), (0,4), (0,5), (1,2), (1,3), (1,4), 
             (2,1), (2,2), (2,3), (3,1), (3,2), (3,3), 
             (4,0), (4,1),(4,2), (5,0), (5,1), 
             (6,0), (6,1), (7,0)  }))`;;

  let  SZIPOAS_concl = `!V. contravening V /\ tame_hypermap_calcs ==> 
       tame_11b  (hypermap_of_fan (V, ESTD V))`;;

  let KCBLRQC_concl = `!V x. contravening V /\ x IN dart_of_fan (V,ESTD V) /\ tame_hypermap_calcs ==> 
    (let H = hypermap_of_fan (V,ESTD V) in
    let (p,q,r) = type_of_node H x in
       (r > 0) \/ (sum (set_of_face_meeting_node H x) (\ f. tauVEF (V,ESTD V,f)) >= b_tame p q))`;;

  let BDJYFFB1_concl = `!V x. contravening V /\ x IN dart_of_fan (V, ESTD V) /\ tame_hypermap_calcs ==>
     tame_12o ( hypermap_of_fan (V,ESTD V) ) `;;

    let BDJYFFB2_concl = `!V x. contravening V /\ x IN dart_of_fan (V, ESTD V) /\ tame_hypermap_calcs ==>
     (let H = hypermap_of_fan (V,ESTD V) in
      (type_of_node H x = (5,0,1)) ==> 
        sum {f | f IN set_of_face_meeting_node H x /\ CARD(f)=3 }  (\f. tauVEF (V, ESTD V,f)) > #0.63)`;;

  let  CRTTXAT_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==> 
       tame_9a  (hypermap_of_fan (V, ESTD V))`;;


(* main result of the chapter. *)

  let MQMSMAB_concl = `!V. contravening V /\ tame_hypermap_calcs /\ (perimeterbound (V, ESTD V))==> 
        tame_hypermap (hypermap_of_fan (V, ESTD V))`;;

end;;