needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";; needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";; needs "tame/CDTETAT.hl";; needs "tame/ssreflect/KCBLRQC-compiled.hl";; (* Module Mqmsmab*) module Mqmsmab = struct open Ssrbool;; open Ssrnat;; open Hypermap;; open Tame_lemmas;; open Tame_defs;; open Tame_general;; open Hypermap_and_fan;; open Hypermap_iso;; open Kcblrqc;; open Jgtdebu;; open Cdtetat_tame;; open Lp_ineqs_proofs;; open Lp_main_estimate;; (* Section MQMSMAB *) Sections.begin_section "MQMSMAB";; (Sections.add_section_hyp "ineqs" (`kcblrqc_ineq_def`));; (Sections.add_section_hyp "h_main" (`lp_main_estimate`));; (* Lemma MQMSMAB *) let MQMSMAB = Sections.section_proof ["V"] `contravening V ==> tame_hypermap (hypermap_of_fan (V, ESTD V))` [ ((((use_arg_then2 ("tame_hypermap", [tame_hypermap]))(thm_tac (new_rewrite [] [])))) THEN (move ["contrV"])); ((fun arg_tac -> (use_arg_then2 ("contravening_lp_fan", [contravening_lp_fan])) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["h_fan"]))); ((((use_arg_then2 ("h_fan", [])) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_fan", [lp_fan]))(thm_tac (new_rewrite [] [])))) THEN ALL_TAC THEN (case THEN (move ["fanV"])) THEN (case THEN (move ["f_surr"])) THEN (case THEN (move ["subV"])) THEN (move ["packV"]))); ((fun arg_tac -> (use_arg_then2 ("COMPONENTS_HYPERMAP_OF_FAN", [COMPONENTS_HYPERMAP_OF_FAN])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (case THEN ((move ["dartH"]) THEN (move ["_"]))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("Crttxat_tame.CRTTXAT", [Crttxat_tame.CRTTXAT])) (fun fst_arg -> (use_arg_then2 ("JGTDEBU4", [JGTDEBU4])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("fully_surrounded_perimeter_bound", [fully_surrounded_perimeter_bound])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN (move ["card"]))); ((((use_arg_then2 ("card", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("card", [])) (disch_tac [])) THEN (clear_assumption "card") THEN BETA_TAC) THEN ((((use_arg_then2 ("tame_9a", [tame_9a]))(thm_tac (new_rewrite [] [])))) THEN (move ["card_ineq"]))); ((((use_arg_then2 ("JGTDEBU10", [JGTDEBU10]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU11", [JGTDEBU11]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("SZIPOAS", [SZIPOAS]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("BDJYFFB1", [BDJYFFB1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_1", [tame_1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU1", [JGTDEBU1]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU2", [JGTDEBU2]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_2", [tame_2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU3", [JGTDEBU3]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (((use_arg_then2 ("JGTDEBU4", [JGTDEBU4]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_3", [tame_3]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU5", [JGTDEBU5]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_4", [tame_4]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU6", [JGTDEBU6]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_5a", [tame_5a]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU7", [JGTDEBU7]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))); ((((use_arg_then2 ("tame_8", [tame_8]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("JGTDEBU8", [JGTDEBU8]))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 12 0 (((use_arg_then2 ("andTb", [andTb]))(thm_tac (new_rewrite [] [])))))); ((((use_arg_then2 ("tame_13a", [tame_13a]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("admissible_weight", [admissible_weight]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("total_weight", [total_weight]))(thm_tac (new_rewrite [] []))))); ((fun arg_tac -> arg_tac (Arg_term (`hypermap_of_fan _`))) (term_tac (set_tac "H"))); ((THENL_ROT (-1)) (((fun arg_tac -> arg_tac (Arg_term (`\f. tauVEF (V,ESTD V,f)`))) (term_tac exists_tac)) THEN (split_tac))); ((((use_arg_then2 ("REAL_LET_TRANS", [REAL_LET_TRANS])) (disch_tac [])) THEN (clear_assumption "REAL_LET_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`&4 * pi - &20 * sol0`))) (term_tac exists_tac)) THEN (((use_arg_then2 ("tgt", [tgt]))(thm_tac (new_rewrite [] []))))); ((THENL_LAST) (split_tac) ((((use_arg_then2 ("Flyspeck_constants.bounds", [Flyspeck_constants.bounds])) (disch_tac [])) THEN (clear_assumption "Flyspeck_constants.bounds") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac))); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then2 ("sum_tauVEF_upper_bound", [sum_tauVEF_upper_bound])) (fun fst_arg -> (use_arg_then2 ("fanV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("f_surr", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))); ((((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("contrV", [])) (disch_tac [])) THEN (clear_assumption "contrV") THEN BETA_TAC) THEN (((((use_arg_then2 ("contravening", [contravening]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_gt", [real_gt]))(thm_tac (new_rewrite [] []))))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("adm_1", [adm_1]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("adm_2", [adm_2]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("adm_3", [adm_3]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (split_tac)); (BETA_TAC THEN (move ["d"]) THEN (move ["d_in"])); ((fun arg_tac -> arg_tac (Arg_term (`CARD (face H d) = k ==> d IN darts_k k H`))) (term_tac (have_gen_tac ["k"](move ["d_in_k"])))); (((((use_arg_then2 ("List_hypermap.darts_k", [List_hypermap.darts_k]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`a >= 3 /\ a <= 6 ==> a = 3 \/ a = 4 \/ a = 5 \/ a = 6`))) (term_tac (have_gen_tac ["a"](move ["ineq"])))) ((arith_tac) THEN (done_tac))); (((fun arg_tac -> (use_arg_then2 ("card_ineq", [])) (fun fst_arg -> (use_arg_then2 ("d_in", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN (fun snd_th -> (use_arg_then2 ("ineq", [])) (thm_tac (match_mp_then snd_th MP_TAC)))) THEN BETA_TAC); ((repeat_tactic 1 9 (case)) THEN (BETA_TAC THEN (move ["card_eq"])) THEN ((((use_arg_then2 ("card_eq", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_tame", [d_tame]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_ge", [real_ge]))(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 20 (((use_arg_then2 ("ARITH_EQ", [ARITH_EQ]))(fun arg -> ONCE_REWRITE_TAC[get_arg_thm arg]))))); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau3_tauVEF_std", [ineq_tau3_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau4_tauVEF_std", [ineq_tau4_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau5_tauVEF_std", [ineq_tau5_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((((use_arg_then2 ("H_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((fun arg_tac -> (use_arg_then2 ("ineq_tau6_tauVEF_std", [ineq_tau6_tauVEF_std])) (fun fst_arg -> (use_arg_then2 ("h_fan", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REFL_CLAUSE", [REFL_CLAUSE]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("d_in_k", []))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)) THEN (repeat_tactic 1 9 (((use_arg_then2 ("andbT", [andbT]))(thm_tac (new_rewrite [] [])))))); ((BETA_TAC THEN (move ["a"]) THEN (move ["b"]) THEN (move ["c"]) THEN (move ["cond"])) THEN (((use_arg_then2 ("h_main", [])) (disch_tac [])) THEN (clear_assumption "h_main") THEN BETA_TAC) THEN ((((use_arg_then2 ("lp_main_estimate", [lp_main_estimate]))(thm_tac (new_rewrite [] [])))) THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((split_tac) THEN (move ["d"])); (((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "r"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "p"))) THEN ((fun arg_tac -> arg_tac (Arg_term (`CARD _`))) (term_tac (set_tac "q"))) THEN (BETA_TAC THEN (case THEN (move ["d_in"])) THEN (move ["r0"]))); ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`type_of_node H d = p,q,0`))) (term_tac (have_gen_tac [](move ["type_eq"])))) ((((use_arg_then2 ("type_of_node", [type_of_node]))(thm_tac (new_rewrite [] [])))) THEN (done_tac))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE KCBLRQC))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h_main", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); (((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("d_in", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("LET_DEF", [LET_DEF]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LET_END_DEF", [LET_END_DEF]))(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then2 ("GT", [GT]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("LT_REFL", [LT_REFL]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("orFb", [orFb]))(thm_tac (new_rewrite [] []))))) THEN (done_tac)); ((BETA_TAC THEN (case THEN (move ["d_in"])) THEN (move ["type_eq"])) THEN ((((use_arg_then2 ("a_tame", [a_tame]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("real_ge", [real_ge]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("REAL_LT_IMP_LE", [REAL_LT_IMP_LE]))(thm_tac (new_rewrite [] [])))))); ((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (let_RULE BDJYFFB2))) (fun fst_arg -> (use_arg_then2 ("contrV", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("h_main", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("ineqs", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then2 ("d", [])) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun arg -> thm_tac MP_TAC arg THEN ALL_TAC)); ((THENL_FIRST) (((((use_arg_then2 ("H_def", []))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("type_eq", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (ANTS_TAC)) ((((use_arg_then2 ("dartH", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac))); ((fun arg_tac -> arg_tac (Arg_term (`GSPEC _`))) (term_tac (set_tac "s"))); ((THENL_FIRST) (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`s = set_of_triangles_meeting_node H d`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))))) ((ALL_TAC) THEN (done_tac))); ((((use_arg_then2 ("s_def", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then2 ("set_of_triangles_meeting_node", [set_of_triangles_meeting_node]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("set_of_face_meeting_node", [set_of_face_meeting_node]))(thm_tac (new_rewrite [] []))))); (((((use_arg_then2 ("EXTENSION", [EXTENSION]))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then2 ("inE", [inE]))(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then2 ("IN_ELIM_THM", [IN_ELIM_THM]))(thm_tac (new_rewrite [] []))))) THEN (simp_tac)) THEN (move ["f"])); ((THENL) (split_tac) [((case THEN ALL_TAC) THEN (case THEN (move ["y"])) THEN (case THEN (move ["y_in"])) THEN (move ["f_eq"]) THEN (move ["card_f"])); ((case THEN (move ["y"])) THEN (case THEN ALL_TAC) THEN (case THEN (move ["y_in"])) THEN (case THEN (move ["card_f"])) THEN (move ["y_in_n"]) THEN (move ["f_eq"]))]); (((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (((use_arg_then2 ("f_eq", []))(gsym_then (thm_tac (new_rewrite [] []))))) THEN (done_tac)); (((((use_arg_then2 ("f_eq", []))(thm_tac (new_rewrite [2] [])))) THEN (((use_arg_then2 ("card_f", []))(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN ((use_arg_then2 ("y", [])) (term_tac exists_tac)) THEN (done_tac)); ];; (* Finalization of the section MQMSMAB *) let MQMSMAB = Sections.finalize_theorem MQMSMAB;; Sections.end_section "MQMSMAB";; (* Close the module *) end;;