formal_ineqs/arith/nat.hl

   1 (* =========================================================== *)\r
   2 (* Formal natural number arithmetic                            *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 (* Dependencies *)\r
   8 needs "arith_options.hl";;\r
   9 needs "arith/arith_cache.hl";;\r
  10 \r
  11 module Arith_nat = struct\r
  12 \r
  13 open Arith_options;;\r
  14 \r
  15 (* mk *)\r
  16 let mk_small_numeral_array = Arith_hash.mk_small_numeral_array;;\r
  17 let mk_numeral_array = Arith_hash.mk_numeral_array;;\r
  18 let NUMERAL_TO_NUM_CONV = Arith_hash.NUMERAL_TO_NUM_CONV;;\r
  19 let NUM_TO_NUMERAL_CONV = Arith_hash.NUM_TO_NUMERAL_CONV;;\r
  20 \r
  21 (* dest *)\r
  22 let raw_dest_hash = Arith_hash.raw_dest_hash;;\r
  23 \r
  24 (* SUC *)\r
  25 let raw_suc_conv_hash = \r
  26   if !cached then Arith_cache.raw_suc_conv_hash else Arith_hash.raw_suc_conv_hash;;\r
  27 \r
  28 let NUM_SUC_HASH_CONV = Arith_hash.NUM_SUC_HASH_CONV;;\r
  29 \r
  30 (* x = 0 *)\r
  31 let raw_eq0_hash_conv = \r
  32   if !cached then Arith_cache.raw_eq0_hash_conv else Arith_hash.raw_eq0_hash_conv;;\r
  33 \r
  34 let NUM_EQ0_HASH_CONV = Arith_hash.NUM_EQ0_HASH_CONV;;\r
  35 \r
  36 (* PRE *)\r
  37 let raw_pre_hash_conv = \r
  38   if !cached then Arith_cache.raw_pre_hash_conv else Arith_hash.raw_pre_hash_conv;;\r
  39 \r
  40 let NUM_PRE_HASH_CONV = Arith_hash.NUM_PRE_HASH_CONV;;\r
  41 \r
  42 (* x > 0 *)\r
  43 let raw_gt0_hash_conv = \r
  44   if !cached then Arith_cache.raw_gt0_hash_conv else Arith_hash.raw_gt0_hash_conv;;\r
  45 \r
  46 let NUM_GT0_HASH_CONV = Arith_hash.NUM_GT0_HASH_CONV;;\r
  47 \r
  48 (* x = y *)\r
  49 let raw_eq_hash_conv = Arith_hash.raw_eq_hash_conv;;\r
  50 let NUM_EQ_HASH_CONV = Arith_hash.NUM_EQ_HASH_CONV;;\r
  51 \r
  52 (* x < y, x <= y *)\r
  53 let raw_lt_hash_conv = \r
  54   if !cached then Arith_cache.raw_lt_hash_conv else Arith_hash.raw_lt_hash_conv;;\r
  55 \r
  56 let raw_le_hash_conv = \r
  57   if !cached then Arith_cache.raw_le_hash_conv else Arith_hash.raw_le_hash_conv;;\r
  58 \r
  59 let NUM_LT_HASH_CONV = Arith_hash.NUM_LT_HASH_CONV;;\r
  60 \r
  61 let NUM_LE_HASH_CONV = Arith_hash.NUM_LE_HASH_CONV;;\r
  62 \r
  63 (* x + y *)\r
  64 let raw_add_conv_hash = \r
  65   if !cached then Arith_cache.raw_add_conv_hash else Arith_hash.raw_add_conv_hash;;\r
  66 \r
  67 let NUM_ADD_HASH_CONV = Arith_hash.NUM_ADD_HASH_CONV;;\r
  68 \r
  69 (* x - y *)\r
  70 let raw_sub_hash_conv = \r
  71   if !cached then Arith_cache.raw_sub_hash_conv else Arith_hash.raw_sub_hash_conv;;\r
  72 \r
  73 let raw_sub_and_le_hash_conv = \r
  74   if !cached then Arith_cache.raw_sub_and_le_hash_conv else Arith_hash.raw_sub_and_le_hash_conv;;\r
  75 \r
  76 let NUM_SUB_HASH_CONV = Arith_hash.NUM_SUB_HASH_CONV;;\r
  77 \r
  78 (* x * y *)\r
  79 let raw_mul_conv_hash = \r
  80   if !cached then Arith_cache.raw_mul_conv_hash else Arith_hash.raw_mul_conv_hash;;\r
  81 \r
  82 let NUM_MULT_HASH_CONV = Arith_hash.NUM_MULT_HASH_CONV;;\r
  83 \r
  84 (* x / y *)\r
  85 let raw_div_hash_conv = \r
  86   if !cached then Arith_cache.raw_div_hash_conv else Arith_hash.raw_div_hash_conv;;\r
  87 \r
  88 let NUM_DIV_HASH_CONV = Arith_hash.NUM_DIV_HASH_CONV;;\r
  89 \r
  90 (* EVEN, ODD *)\r
  91 let raw_even_hash_conv = \r
  92   if !cached then Arith_cache.raw_even_hash_conv else Arith_hash.raw_even_hash_conv;;\r
  93 \r
  94 let raw_odd_hash_conv = \r
  95   if !cached then Arith_cache.raw_odd_hash_conv else Arith_hash.raw_odd_hash_conv;;\r
  96 \r
  97 let NUM_EVEN_HASH_CONV = Arith_hash.NUM_EVEN_HASH_CONV;;\r
  98 \r
  99 let NUM_ODD_HASH_CONV = Arith_hash.NUM_ODD_HASH_CONV;;\r
 100 \r
 101 \r
 102 let NUMERALS_TO_NUM = \r
 103         PURE_REWRITE_RULE[Arith_hash.NUM_THM] o CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;\r
 104 \r
 105 \r
 106 end;;\r