(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Tame Hypermap                                                     *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2013-01-22                                                           *)
(* JGTDEBU: general properties of a contravening packing                      *)
(* ========================================================================== *)

needs "fan/hypermap_iso-compiled.hl";;
needs "tame/TameGeneral.hl";;


module Jgtdebu = struct

parse_as_infix("iso",(24,"right"));;
open Tame_defs;;
open Fan_defs;;
open Hypermap_iso;;
open Hypermap_and_fan;;
open Tame_general;;

let contravening_imp_conforming = prove(`!V. contravening V ==>
					  conforming_fan (vec 0,V,ESTD V)`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC Conforming.PIIJBJK THEN
     MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN 
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     ASM_REWRITE_TAC[Planarity.fan80] THEN
     CONJ_TAC THEN REPEAT GEN_TAC THEN REPEAT DISCH_TAC THENL
     [
       MATCH_MP_TAC (ARITH_RULE `a >= 3 ==> a > 1`) THEN
	 MATCH_MP_TAC SURROUNDED_IMP_CARD_SET_OF_EDGE_GE_3 THEN
	 ASM_SIMP_TAC[CONTRAVENING_IMP_SURROUNDED];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `v,u IN dart_of_fan (V,ESTD V)` ASSUME_TAC THENL
     [
       REWRITE_TAC[dart_of_fan; IN_UNION; IN_ELIM_THM] THEN DISJ2_TAC THEN
	 EXISTS_TAC `v:real^3` THEN EXISTS_TAC `u:real^3` THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[GSYM CONTRAVENING_IMP_AZIM_DART_EQ_AZIM; AZIM_DART_POS] THEN
     MP_TAC (SPEC `V:real^3->bool` CONTRAVENING_IMP_FULLY_SURROUNDED) THEN
     ASM_SIMP_TAC[fully_surrounded]);;


(* 1 *)
let JGTDEBU1 = prove(`!V. contravening V 
		     ==> planar_hypermap (hypermap_of_fan (V, ESTD V))`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN 
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN
     ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_planar) THEN 
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     ASM_SIMP_TAC[Conforming.GGRLKHP; contravening_imp_conforming]);;


(* 2 *)
let JGTDEBU2 = prove(`!V. contravening V ==>
		       plain_hypermap (hypermap_of_fan (V,ESTD V))`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC PLAIN_HYPERMAP_OF_FAN THEN
     ASM_SIMP_TAC[CONTRAVENING_FAN]);;

	 
(* 3 *)
let JGTDEBU3 = prove(`!V. contravening V 
		     ==> connected_hypermap (hypermap_of_fan (V, ESTD V))`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN 
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN
     ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_connected) THEN 
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     ASM_SIMP_TAC[Conforming.WGVWSKE; contravening_imp_conforming]);;


(* 4 *)
let JGTDEBU4 = prove(`!V. contravening V ==> 
       simple_hypermap (hypermap_of_fan (V, ESTD V))`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC `V:real^3->bool` Tame_general.CONTRAVENING_FAN) THEN 
     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] fan_hypermaps_iso) THEN
     ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o MATCH_MP iso_simple) THEN 
     DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
     ASM_SIMP_TAC[Conforming.SRPRNPL; contravening_imp_conforming]);;


(* 5 *)
let JGTDEBU5 = prove(`!V. contravening V ==>
		       is_edge_nondegenerate (hypermap_of_fan (V,ESTD V))`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC HYPERMAP_OF_FAN_EDGE_NONDEGENERATE THEN
     ASM_SIMP_TAC[CONTRAVENING_FAN; CONTRAVENING_IMP_FULLY_SURROUNDED]);;


(* 6 *)
let JGTDEBU6 = prove(`!V. contravening V ==>
		       no_loops (hypermap_of_fan (V,ESTD V))`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC HYPERMAP_OF_FAN_NO_LOOPS THEN
     ASM_SIMP_TAC[CONTRAVENING_FAN]);;


(* 7 *)
let JGTDEBU7 = prove(`!V.  contravening V ==>
		       is_no_double_joints (hypermap_of_fan (V,ESTD V))`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC HYPERMAP_OF_FAN_NO_DOUBLE_JOINTS THEN
     ASM_SIMP_TAC[CONTRAVENING_FAN]);;


(* number_of_faces  (hypermap_of_fan (V, ESTD V)) >= 3 *)
let CONTRAVENING_HAS_SIZE_lemma = prove(`!V. contravening V ==> ?n. n > 0 /\ V HAS_SIZE n`,
   GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     REMOVE_THEN "A" MP_TAC THEN
     REWRITE_TAC[contravening] THEN
     REPLICATE_TAC 4 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
     EXISTS_TAC `CARD (V:real^3->bool)` THEN
     ASM_SIMP_TAC[ARITH_RULE `a = 13 \/ a = 14 \/ a = 15 ==> a > 0`] THEN
     REWRITE_TAC[HAS_SIZE] THEN
     REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
     REWRITE_TAC[Fan_defs.FAN; Fan_defs.fan1] THEN
     SIMP_TAC[]);;
     

(* 8 *)
let JGTDEBU8 = prove(`!V. contravening V ==>
		       number_of_faces (hypermap_of_fan (V,ESTD V)) >= 3`,
   GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN
     MP_TAC (SPEC `V:real^3->bool` JGTDEBU4) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     USE_THEN "A" MP_TAC THEN
     REWRITE_TAC[contravening] THEN
     REPLICATE_TAC 5 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
     REWRITE_TAC[Hypermap.number_of_faces] THEN
     SUBGOAL_THEN `?v:real^3. v IN V` MP_TAC THENL
     [
       MP_TAC (SPEC `V:real^3->bool` CONTRAVENING_HAS_SIZE_lemma) THEN
	 ASM_REWRITE_TAC[ARITH_RULE `n > 0 <=> ~(n = 0)`] THEN
	 STRIP_TAC THEN
	 MP_TAC (SPEC `n:num` num_CASES) THEN
	 ASM_REWRITE_TAC[] THEN
	 STRIP_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o check (is_binary "HAS_SIZE" o concl)) THEN
	 ASM_REWRITE_TAC[HAS_SIZE_CLAUSES] THEN
	 STRIP_TAC THEN
	 EXISTS_TAC `a:real^3` THEN
	 POP_ASSUM MP_TAC THEN
	 SIMP_TAC[INSERT; EXTENSION; IN_ELIM_THM];
       ALL_TAC
     ] THEN
     STRIP_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `v:real^3`] DART_EXISTS) THEN
     ASM_REWRITE_TAC[] THEN
     STRIP_TAC THEN
     ABBREV_TAC `H = hypermap_of_fan (V,ESTD V)` THEN 
     SUBGOAL_THEN `v,w IN dart1_of_fan (V:real^3->bool,ESTD V)` ASSUME_TAC THENL
     [
       MATCH_MP_TAC SURROUNDED_IMP_IN_DART1_OF_FAN THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN
     ABBREV_TAC `A = {face H y | y | y IN dart H /\ T /\ y IN node H (v:real^3,w:real^3)}` THEN
     SUBGOAL_THEN `A SUBSET face_set (H:(real^3#real^3)hypermap)` ASSUME_TAC THENL
     [
       EXPAND_TAC "A" THEN
	 REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
	 GEN_TAC THEN STRIP_TAC THEN
	 ASM_REWRITE_TAC[GSYM Hypermap.lemma_in_face_set] THEN
	 EXPAND_TAC "H" THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN];
       ALL_TAC
     ] THEN
     ONCE_REWRITE_TAC[GE] THEN
     MATCH_MP_TAC LE_TRANS THEN
     EXISTS_TAC `CARD (A:(real^3#real^3->bool)->bool)` THEN
     CONJ_TAC THENL
     [
       EXPAND_TAC "A" THEN
	 MP_TAC (ISPECL [`H:(real^3#real^3)hypermap`; `v:real^3,w:real^3`; `(\x:real^3#real^3. T)`] SIMPLE_HYPERMAP_lemma) THEN
	 REMOVE_ASSUM THEN REMOVE_ASSUM THEN
	 ASM_REWRITE_TAC[ETA_AX] THEN
	 EXPAND_TAC "H" THEN
	 ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
	 SIMP_TAC[SIMPLE_HYPERMAP_lemma] THEN
	 DISCH_THEN (fun th -> ALL_TAC) THEN
	 SUBGOAL_THEN `{y:real^3#real^3 | y IN node H (v,w)} = node H (v,w)` MP_TAC THENL
	 [
	   REWRITE_TAC[EXTENSION; IN_ELIM_THM];
	   ALL_TAC
	 ] THEN
	 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
	 REWRITE_TAC[GSYM GE] THEN
	 EXPAND_TAC "H" THEN
	 MATCH_MP_TAC SURROUNDED_IMP_CARD_NODE_GE_3 THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN


     MATCH_MP_TAC CARD_SUBSET THEN
     ASM_REWRITE_TAC[Hypermap.FINITE_HYPERMAP_ORBITS]
		    );;
 

(* 10 *)
(* tame_10  (hypermap_of_fan (V, ESTD V)) *)
let JGTDEBU10 = prove(`!V. contravening V ==> tame_10 (hypermap_of_fan (V,ESTD V))`,
   GEN_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     REMOVE_THEN "A" MP_TAC THEN
     REWRITE_TAC[contravening; tame_10; Hypermap.number_of_nodes] THEN
     REPLICATE_TAC 4 (DISCH_THEN (CONJUNCTS_THEN2 (fun th -> ALL_TAC) MP_TAC)) THEN
     DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (fun th -> ALL_TAC)) THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD V`] NODE_SET_AS_IMAGE) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     SUBGOAL_THEN `CARD(IMAGE (f:real^3 -> ((real^3#real^3) -> bool)) V) = CARD V` (fun th -> REWRITE_TAC[th]) THENL
     [
       MATCH_MP_TAC CARD_IMAGE_INJ THEN
	 FIRST_X_ASSUM (MP_TAC o check (fun th -> rand (concl th) = `(vec 0:real^3,V:real^3->bool,ESTD V)`)) THEN
	 REWRITE_TAC[Fan_defs.FAN; Fan_defs.fan1] THEN
	 ASM_SIMP_TAC[] THEN
	 DISCH_THEN (fun th -> ALL_TAC) THEN
	 REPEAT STRIP_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o SPECL [`x:real^3`; `y:real^3`]) THEN
	 ASM_SIMP_TAC[];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]);;
     

(* 11 *)
(* tame_11a  (hypermap_of_fan (V, ESTD V)) *)
let JGTDEBU11 = prove(`!V. contravening V ==> tame_11a (hypermap_of_fan (V,ESTD V))`,
   REPEAT STRIP_TAC THEN
     MP_TAC (SPEC_ALL CONTRAVENING_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
     REWRITE_TAC[tame_11a] THEN
     ASM_SIMP_TAC[Hypermap.dart; HYPERMAP_OF_FAN] THEN
     REPEAT STRIP_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `x:real^3#real^3`] IN_DART_OF_FAN) THEN
     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
     MP_TAC (SPECL [`V:real^3->bool`; `ESTD (V:real^3->bool)`; `v:real^3`; `w:real^3`] SURROUNDED_IMP_IN_DART1_OF_FAN) THEN
     MP_TAC (SPEC_ALL CONTRAVENING_IMP_SURROUNDED) THEN
     ASM_SIMP_TAC[] THEN REPEAT DISCH_TAC THEN
     MATCH_MP_TAC SURROUNDED_IMP_CARD_NODE_GE_3 THEN
     ASM_REWRITE_TAC[]);;
	 

end;;