formal_lp/old/arith/nat.hl

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