(* ========================================================================== *)
(* 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;;