Rqe/rewrites.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Num                                                                   *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 let NUM_REWRITES = ref [
   6 LT_TRANS;
   7 LET_TRANS;
   8 LTE_TRANS;
   9 LE_TRANS;
  10 GT;
  11 GE;
  12 PRE;
  13 ARITH_RULE `x + 0 = x`;
  14 ARITH_RULE `0 + x = x`;
  15 ARITH_RULE `1 * x = x`;
  16 ARITH_RULE `x * 1 = x`;
  17 ];;
  18
  19 let NUM_SIMP_TAC = REWRITE_TAC !NUM_REWRITES;;
  20
  21 let extend_num_rewrites l =
  22   NUM_REWRITES := !NUM_REWRITES @ l;;
  23
  24 (* ---------------------------------------------------------------------- *)
  25 (*  Real                                                                  *)
  26 (* ---------------------------------------------------------------------- *)
  27
  28 (*
  29 search [`(pow)`;rp]
  30 *)
  31
  32 let REAL_REWRITES = ref [
  33 REAL_MUL_LID;
  34 REAL_MUL_RID;
  35 REAL_MUL_RZERO;
  36 REAL_MUL_LZERO;
  37 REAL_LT_TRANS;
  38 REAL_LET_TRANS;
  39 REAL_LTE_TRANS;
  40 REAL_LE_TRANS;
  41 REAL_LE_MUL;
  42 REAL_NOT_LT;
  43 REAL_LT_REFL;
  44 REAL_LE_REFL;
  45 REAL_ADD_RID;
  46 REAL_ADD_LID;
  47 REAL_ADD_LDISTRIB;
  48 REAL_ADD_RDISTRIB;
  49 REAL_NEG_0;
  50 REAL_NEG_MUL2;
  51 REAL_OF_NUM_LT;
  52 REAL_MAX_MAX;
  53 real_pow;
  54 REAL_ARITH `x - &0 = x`;
  55 REAL_NOT_LT;
  56 REAL_NOT_LE;
  57 REAL_INV_INV;
  58 REAL_INV_MUL;
  59 real_gt;
  60 real_ge;
  61 REAL_POW_1;
  62 ARITH_RULE `-- &1 * x = -- x`;
  63 ARITH_RULE `-- &1 * -- &1 = &1`;
  64 ARITH_RULE `-- (-- x * y) = x * y`;
  65 ARITH_RULE `x - x = &0`;
  66 REAL_POW_ONE;
  67 REAL_NEG_NEG;
  68 ];;
  69
  70 let REAL_ELIM = ref [
  71 REAL_LT_INV;
  72 REAL_ADD_SYM;
  73 REAL_ADD_ASSOC;
  74 REAL_MUL_SYM;
  75 REAL_MUL_ASSOC;
  76 REAL_LT_LE;
  77 REAL_LE_LT;
  78 real_div;
  79 ];;
  80
  81 let REAL_SIMP_TAC = REWRITE_TAC (
  82   !REAL_REWRITES
  83 );;
  84
  85 let REAL_SOLVE_TAC = ASM_MESON_TAC (!REAL_REWRITES @ !REAL_ELIM);;
  86
  87 let extend_real_rewrites l =
  88   REAL_REWRITES := !REAL_REWRITES @ l;;
  89
  90 let BASIC_REWRITES = ref (!REAL_REWRITES @ !NUM_REWRITES);;