(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)




module  Disjoint_fan = struct



open Sphere;;
open Fan_defs;;
open Hypermap_of_fan;;
open Tactic_fan;;
open Lemma_fan;;		
open Fan;;
open Hypermap_of_fan;;
open Node_fan;;
open Azim_node;;
open Sum_azim_node;;




(* ========================================================================== *)
(*                   DISJOINT IN   FAN                        *) 
(* ========================================================================== *)

let disjiont_union_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
==> 
 w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
 (aff{x,v} UNION aff_gt {x,v} {w1})={}`,


REPEAT STRIP_TAC THEN REWRITE_TAC[UNION_OVER_INTER]
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`  (v:real^3)`;` (w:real^3)`;` (w1:real^3)`] disjoint_set_fan) THEN ASM_REWRITE_TAC[]
  THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`  (v:real^3)`;` (w:real^3)`;] disjoint_fan1) THEN ASM_REWRITE_TAC[]
  THEN ASM_SET_TAC[]);;


let aff_ge_subset_aff_gt_union_aff=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3).
FAN(x,V,E)/\ {v,w} IN E 
==>
aff_ge {x} {v , w} SUBSET  (aff_gt {x , v} {w}) UNION (aff {x, v})`,


REPEAT STRIP_TAC THEN  MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;` (v:real^3)`] remark1_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GE_1_2)
		THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
		THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`]AFF_GT_2_1)
		THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
		THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`]affine_hull_2_fan)
		THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[SUBSET; UNION;IN_ELIM_THM]
  THEN GEN_TAC THEN
REWRITE_TAC[REAL_ARITH `(&0 <= (t3:real)) <=> (&0 < t3) \/ ( t3 = &0)`; TAUT `(a \/ b) /\ (c \/ d) /\ e /\ f <=> ((a \/ b)/\ c /\ e /\ f) \/ ((a \/ b) /\ d /\ e /\ f)`; EXISTS_OR_THM] THEN
MATCH_MP_TAC MONO_OR THEN
SUBGOAL_THEN `((?t1:real t2:real t3:real.
       (&0 < t2 \/ t2 = &0) /\
        &0< t3 /\
       t1 + t2 + t3 = &1 /\
       (x':real^3) = t1 % x + t2 % v + t3 % w)
  ==> (?t1 t2 t3.
            &0< t3 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v + t3 % w))` ASSUME_TAC
THENL  
[MESON_TAC[];
     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN
     REWRITE_TAC[REAL_ARITH `(&0< (t2:real) \/ (t2 = &0)) <=> ( &0<= t2)`] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN
     POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC [REAL_ARITH `(a:real)+ &0 = a`; VECTOR_ARITH  `&0 % (w:real^3) = vec 0`; 
     VECTOR_ARITH `  ((x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v:real^3) + vec 0)<=> ( x' = t1 % x + t2 % v )` ]
       THEN MESON_TAC[]]);;
	


let IBZWFFH=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)  (v:real^3) (w:real^3) (w1:real^3).
FAN(x,V,E)/\ ({v,w}IN E) /\ ({v,w1}IN E)
==> 
 w_dart_fan x V E (x,v,w,(sigma_fan x V E v w)) INTER
aff_ge {x} {v , w1}={}`,

REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;` (w1:real^3)`] aff_ge_subset_aff_gt_union_aff)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (v:real^3)`;`w:real^3`;` (w1:real^3)`] disjiont_union_fan)
  THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]);;


end;;