rqe_num.ml

(* ---------------------------------------------------------------------- *)
(*  Nums                                                                  *)
(* ---------------------------------------------------------------------- *)

let neq = `(=):num->num->bool`;;
let nlt = `(<):num->num->bool`;;
let ngt = `(>):num->num->bool`;;
let nle = `(<=):num->num->bool`;;
let nge = `(>=):num->num->bool`;;
let nm = `( * ):num->num->num`;;
let np = `(+):num->num->num`;;
let nzero = `0`;;
let even_tm = `EVEN`;;
let odd_tm = `ODD`;;


let nmax = new_definition(
 `nmax (n:num) m = if n <= m then m else n`);;

let SUC_1 = prove(
  `1 + x = SUC x`,
(* {{{ Proof *)
  ARITH_TAC);;
(* }}} *)

let even_tm = `EVEN`;;
let odd_tm = `ODD`;;
let PARITY_CONV tm = 
  let k = dest_small_numeral tm in
  if even k then
    prove(mk_comb(even_tm,tm),ARITH_TAC)
  else 
    prove(mk_comb(odd_tm,tm),ARITH_TAC);;