(*********************************)
(* The natural number arithmetic *)
(*********************************)

(* Dependencies *)
needs "../formal_lp/arith/arith_options.hl";;
needs "../formal_lp/arith/arith_cache.hl";;

module Arith_nat = struct

open Arith_options;;

(* mk *)
let mk_small_numeral_array = Arith_hash.mk_small_numeral_array;;
let mk_numeral_array = Arith_hash.mk_numeral_array;;
let NUMERAL_TO_NUM_CONV = Arith_hash.NUMERAL_TO_NUM_CONV;;
let NUM_TO_NUMERAL_CONV = Arith_hash.NUM_TO_NUMERAL_CONV;;

(* dest *)
let raw_dest_hash = Arith_hash.raw_dest_hash;;

(* SUC *)
let raw_suc_conv_hash = 
  if cached then Arith_cache.raw_suc_conv_hash else Arith_hash.raw_suc_conv_hash;;

let NUM_SUC_HASH_CONV = Arith_hash.NUM_SUC_HASH_CONV;;

(* x = 0 *)
let raw_eq0_hash_conv = 
  if cached then Arith_cache.raw_eq0_hash_conv else Arith_hash.raw_eq0_hash_conv;;

let NUM_EQ0_HASH_CONV = Arith_hash.NUM_EQ0_HASH_CONV;;

(* PRE *)
let raw_pre_hash_conv = 
  if cached then Arith_cache.raw_pre_hash_conv else Arith_hash.raw_pre_hash_conv;;

let NUM_PRE_HASH_CONV = Arith_hash.NUM_PRE_HASH_CONV;;

(* x > 0 *)
let raw_gt0_hash_conv = 
  if cached then Arith_cache.raw_gt0_hash_conv else Arith_hash.raw_gt0_hash_conv;;

let NUM_GT0_HASH_CONV = Arith_hash.NUM_GT0_HASH_CONV;;

(* x < y, x <= y *)
let raw_lt_hash_conv = 
  if cached then Arith_cache.raw_lt_hash_conv else Arith_hash.raw_lt_hash_conv;;

let raw_le_hash_conv = 
  if cached then Arith_cache.raw_le_hash_conv else Arith_hash.raw_le_hash_conv;;

let NUM_LT_HASH_CONV = Arith_hash.NUM_LT_HASH_CONV;;

let NUM_LE_HASH_CONV = Arith_hash.NUM_LE_HASH_CONV;;

(* x + y *)
let raw_add_conv_hash = 
  if cached then Arith_cache.raw_add_conv_hash else Arith_hash.raw_add_conv_hash;;

let NUM_ADD_HASH_CONV = Arith_hash.NUM_ADD_HASH_CONV;;

(* x - y *)
let raw_sub_hash_conv = 
  if cached then Arith_cache.raw_sub_hash_conv else Arith_hash.raw_sub_hash_conv;;

let raw_sub_and_le_hash_conv = 
  if cached then Arith_cache.raw_sub_and_le_hash_conv else Arith_hash.raw_sub_and_le_hash_conv;;

let NUM_SUB_HASH_CONV = Arith_hash.NUM_SUB_HASH_CONV;;

(* x * y *)
let raw_mul_conv_hash = 
  if cached then Arith_cache.raw_mul_conv_hash else Arith_hash.raw_mul_conv_hash;;

let NUM_MULT_HASH_CONV = Arith_hash.NUM_MULT_HASH_CONV;;

(* x / y *)
let raw_div_hash_conv = 
  if cached then Arith_cache.raw_div_hash_conv else Arith_hash.raw_div_hash_conv;;

let NUM_DIV_HASH_CONV = Arith_hash.NUM_DIV_HASH_CONV;;

(* EVEN, ODD *)
let raw_even_hash_conv = 
  if cached then Arith_cache.raw_even_hash_conv else Arith_hash.raw_even_hash_conv;;

let raw_odd_hash_conv = 
  if cached then Arith_cache.raw_odd_hash_conv else Arith_hash.raw_odd_hash_conv;;

let NUM_EVEN_HASH_CONV = Arith_hash.NUM_EVEN_HASH_CONV;;

let NUM_ODD_HASH_CONV = Arith_hash.NUM_ODD_HASH_CONV;;


let NUMERALS_TO_NUM = 
	PURE_REWRITE_RULE[Arith_hash.NUM_THM] o CONV_RULE (DEPTH_CONV NUMERAL_TO_NUM_CONV);;


end;;