(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Tactic: AFF_SGN_TAC                                                       *)
(* Chapter: LEG                                                               *)
(* Author: John Harrison, with minor edits by T. Hales                        *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)

module type Aff_sgn_tac_type = sig
  val AFF_SGN_TAC : tactic
end;;

(*

  This is Harrison's 2009 workshop AFF_GE_TAC tactic, slightly adapted
  to handle signs other than GE.

  The tactic is documented at
  http://weyl.math.pitt.edu/hanoi2009/uploads/HOLLight/affsign_small.ml
  Examples appear at the indicated URL.

  It proves conv0, aff_gt, aff_ge, and aff_lt formulas in special cases.

*)

module Aff_sgn_tac : Aff_sgn_tac_type = struct


let AFF_SGN_TAC = 
    REWRITE_TAC[DISJOINT_INSERT; DISJOINT_EMPTY] THEN
 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
 REPEAT STRIP_TAC THEN
  REWRITE_TAC[aff_ge_def; sgn_ge; aff_gt_def;sgn_gt;conv0;aff_lt_def;sgn_lt;AFFSIGN_ALT] THEN
  REWRITE_TAC[SET_RULE `(x INSERT s) UNION t = x INSERT (s UNION t)`] THEN
  REWRITE_TAC[UNION_EMPTY] THEN
  SIMP_TAC[FINITE_INSERT; FINITE_UNION; AFFINE_HULL_FINITE_STEP_GEN;
           FINITE_EMPTY; RIGHT_EXISTS_AND_THM; 
           REAL_LE_ADD; REAL_LT_ADD;
           REAL_ARITH `a < &0 /\ b < &0 ==> a+ b< &0`;
           REAL_ARITH `&0 < a/ &2 <=> &0 < a`; REAL_ARITH `&0 <= a / &2 <=> &0 <= a`;
           REAL_ARITH `a/ &2 < &0 <=> a < &0`] THEN
  ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; real_ge;real_gt] THEN
  REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`;
              VECTOR_ARITH `x - y:real^N = z <=> x = y + z`] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; REAL_ADD_RID; VECTOR_ADD_RID] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `&1 = x <=> x = &1`] THEN
  REWRITE_TAC[] THEN SET_TAC[];;

end;;