text_formalization/local/HXHYTIJ.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Hxhytij = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73 open Uxckfpe;;
  74 open Sgtrnaf;;
  75
  76
  77
  78
  79 let HXHYTIJ= prove_by_refinement(`!s vv ww.
  80   is_scs_v39 s /\
  81   BBprime2_v39 s vv /\
  82   BBs_v39 s ww ==>
  83   (taustar_v39 s vv < taustar_v39 s ww  \/
  84      BBindex_v39 s vv <= BBindex_v39 s ww)`,
  85 [REPEAT STRIP_TAC
  86 THEN MP_TAC(REAL_ARITH`(taustar_v39 s vv < taustar_v39 s ww)\/ taustar_v39 s ww <= taustar_v39 s vv`)
  87 THEN RESA_TAC
  88 THEN SUBGOAL_THEN`BBprime_v39 s ww` ASSUME_TAC;
  89
  90 ASM_TAC
  91 THEN ASM_REWRITE_TAC[IN;BBprime_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
  92 THEN REPEAT RESA_TAC;
  93
  94 REPLICATE_TAC (7-2)(POP_ASSUM MP_TAC)
  95 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
  96 THEN MRESA1_TAC th`ww':num->real^3`)
  97 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
  98 THEN REAL_ARITH_TAC;
  99
 100 REPLICATE_TAC (6-2)(POP_ASSUM MP_TAC)
 101 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 102 THEN MRESA1_TAC th`ww:num->real^3`)
 103 THEN ASM_TAC
 104 THEN REAL_ARITH_TAC;
 105
 106 ASM_TAC
 107 THEN ASM_REWRITE_TAC[IN;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39;BBindex_min_v39]
 108 THEN REPEAT RESA_TAC
 109 THEN SUBGOAL_THEN`(BBindex_v39 s ww) IN IMAGE (BBindex_v39 s) (BBprime_v39 s)` ASSUME_TAC;
 110
 111 REWRITE_TAC[IMAGE;IN_ELIM_THM;IN]
 112 THEN EXISTS_TAC`ww:num->real^3`
 113 THEN ASM_REWRITE_TAC[];
 114
 115 POP_ASSUM MP_TAC
 116 THEN REWRITE_TAC[IN]
 117 THEN STRIP_TAC
 118 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s ww`]]);;
 119
 120
 121  end;;
 122
 123
 124 (*
 125 let check_completeness_claimA_concl =
 126   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 127 *)
 128
 129
 130
 131