Rqe/rqe_num.ml

   1
   2 (* ---------------------------------------------------------------------- *)
   3 (*  Nums                                                                  *)
   4 (* ---------------------------------------------------------------------- *)
   5
   6 let neq = `(=):num->num->bool`;;
   7 let nlt = `(<):num->num->bool`;;
   8 let ngt = `(>):num->num->bool`;;
   9 let nle = `(<=):num->num->bool`;;
  10 let nge = `(>=):num->num->bool`;;
  11 let nm = `( * ):num->num->num`;;
  12 let np = `(+):num->num->num`;;
  13 let nzero = `0`;;
  14 let even_tm = `EVEN`;;
  15 let odd_tm = `ODD`;;
  16
  17
  18 let nmax = new_definition(
  19  `nmax (n:num) m = if n <= m then m else n`);;
  20
  21 let SUC_1 = prove(
  22   `1 + x = SUC x`,
  23 (* {{{ Proof *)
  24   ARITH_TAC);;
  25 (* }}} *)
  26
  27 let even_tm = `EVEN`;;
  28 let odd_tm = `ODD`;;
  29 let PARITY_CONV tm =
  30   let k = dest_small_numeral tm in
  31   if even k then
  32     prove(mk_comb(even_tm,tm),ARITH_TAC)
  33   else
  34     prove(mk_comb(odd_tm,tm),ARITH_TAC);;