text_formalization/leg/AFF_SGN_TAC.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Tactic: AFF_SGN_TAC                                                       *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: John Harrison, with minor edits by T. Hales                        *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10 module type Aff_sgn_tac_type = sig
  11   val AFF_SGN_TAC : tactic
  12 end;;
  13
  14 (*
  15
  16   This is Harrison's 2009 workshop AFF_GE_TAC tactic, slightly adapted
  17   to handle signs other than GE.
  18
  19   The tactic is documented at
  20   http://weyl.math.pitt.edu/hanoi2009/uploads/HOLLight/affsign_small.ml
  21   Examples appear at the indicated URL.
  22
  23   It proves conv0, aff_gt, aff_ge, and aff_lt formulas in special cases.
  24
  25 *)
  26
  27 module Aff_sgn_tac : Aff_sgn_tac_type = struct
  28
  29
  30 let AFF_SGN_TAC =
  31     REWRITE_TAC[DISJOINT_INSERT; DISJOINT_EMPTY] THEN
  32  REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
  33  REPEAT STRIP_TAC THEN
  34   REWRITE_TAC[aff_ge_def; sgn_ge; aff_gt_def;sgn_gt;conv0;aff_lt_def;sgn_lt;AFFSIGN_ALT] THEN
  35   REWRITE_TAC[SET_RULE `(x INSERT s) UNION t = x INSERT (s UNION t)`] THEN
  36   REWRITE_TAC[UNION_EMPTY] THEN
  37   SIMP_TAC[FINITE_INSERT; FINITE_UNION; AFFINE_HULL_FINITE_STEP_GEN;
  38            FINITE_EMPTY; RIGHT_EXISTS_AND_THM;
  39            REAL_LE_ADD; REAL_LT_ADD;
  40            REAL_ARITH `a < &0 /\ b < &0 ==> a+ b< &0`;
  41            REAL_ARITH `&0 < a/ &2 <=> &0 < a`; REAL_ARITH `&0 <= a / &2 <=> &0 <= a`;
  42            REAL_ARITH `a/ &2 < &0 <=> a < &0`] THEN
  43   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; real_ge;real_gt] THEN
  44   REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`;
  45               VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
  46   REWRITE_TAC[RIGHT_AND_EXISTS_THM; REAL_ADD_RID; VECTOR_ADD_RID] THEN
  47   ONCE_REWRITE_TAC[REAL_ARITH `&1 = x <=> x = &1`] THEN
  48   REWRITE_TAC[] THEN SET_TAC[];;
  49
  50 end;;