(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)

(*
remaining conclusions from appendix to Local Fan chapter
*)


module Ayqjtmd = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;






open Xwitccn;;




let XWITCCN2=
prove_by_refinement(
` !s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s
/\  taustar_v39 s vv < &0
 ==> ~(BBprime2_v39 s = {})`,

  (* {{{ proof *)
[
REPEAT GEN_TAC
THEN  STRIP_TAC
THEN MRESA_TAC XWITCCN[`s:scs_v39`;`vv:num->real^3`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;]
THEN STRIP_TAC
THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\
     BBindex_v39 s vv1=n)` ASSUME_TAC;

EXISTS_TAC`BBindex_v39 s vv1`
THEN EXISTS_TAC`vv1:num->real^3`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[MINIMAL]
THEN STRIP_TAC
THEN EXISTS_TAC`vv1':num->real^3`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th))
THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`]
THEN STRIP_TAC
THEN MATCH_MP_TAC SELECT_UNIQUE
THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;]
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN EQ_TAC;

STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC;

EXISTS_TAC`vv1':num->real^3`
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`)
THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==>
BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`)
THEN RESA_TAC
THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN 
MRESA1_TAC th` BBindex_v39 s x`)
THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;

EXISTS_TAC`x:num->real^3`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;



EXISTS_TAC`vv1':num->real^3`
THEN ASM_REWRITE_TAC[];


REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1'   \/ BBindex_v39 s vv1' <= BBindex_v39 s x`)
THEN RESA_TAC;



REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN 
MRESA1_TAC th` BBindex_v39 s x`)
THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;

EXISTS_TAC`x:num->real^3`
THEN ASM_REWRITE_TAC[];


POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];
]);;
  (* }}} *)


let unadorned_MMs=
prove_by_refinement(
`  unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`
,

  (* {{{ proof *)
[
REWRITE_TAC[FUN_EQ_THM]
THEN REWRITE_TAC[unadorned_v39;MMs_v39;]
THEN REPEAT STRIP_TAC
THEN EQ_TAC
THEN RESA_TAC;

STRIP_TAC;

SET_TAC[];

STRIP_TAC;

SET_TAC[];

STRIP_TAC;

SET_TAC[];


POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;]
THEN RESA_TAC;
]);;
  (* }}} *)




let S_INIT_IS_UNADORNED=
prove(
`MEM s s_init_list_v39
==> unadorned_v39 s`,

REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;set_of_list;LET_DEF;LET_END_DEF
;SET_RULE`A IN {A1,A2,A3,A4,A5,A6,A7,A8} <=> A= A1 \/ A= A2 \/  A= A3 \/ A= A4 \/ A= A5 \/ A= A6 \/ A= A7 \/ A= A8`]
THEN REPEAT GEN_TAC
THEN RESA_TAC
THEN REWRITE_TAC[unadorned_v39]
THEN ASM_REWRITE_TAC[scs_lo_v39_explicit;scs_str_v39_explicit;scs_am_v39_explicit;scs_bm_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)/\ 3-1=2`;mk_unadorned_v39;CS_ADJ;scs_J_v39_explicit;change_type_v2;d_tame ;change_type_v3;scs_hi_v39_explicit;]);;


let AYQJTMD =
prove(
`!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
  taustar_v39 s vv < &0
 ==> ~(MMs_v39 s = {})`,

REPEAT GEN_TAC
THEN STRIP_TAC
THEN MP_TAC S_INIT_IS_UNADORNED
THEN RESA_TAC
THEN MP_TAC unadorned_MMs
THEN RESA_TAC
THEN MATCH_MP_TAC XWITCCN2
THEN EXISTS_TAC`vv:num->real^3`
THEN ASM_REWRITE_TAC[]);;


let EAPGLE =
prove(  `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`,

REPEAT STRIP_TAC
THEN MATCH_MP_TAC ZITHLQN
THEN REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`taustar_v39 s vv< &0\/ &0 <= taustar_v39 s vv`)
THEN RESA_TAC
THEN MRESA_TAC AYQJTMD[`s:scs_v39`;`vv:num->real^3`]
THEN ASM_TAC
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`s:scs_v39`));;


 end;;