anchor.diff:          ((parse_term "!x. &0 <= x <=> (&(num_of_int x) = x)"), 
            MESON_TAC [INT_OF_NUM_OF_INT; INT_POS])
   
  +(* ------------------------------------------------------------------------- *)
  +(* Now define similar notions over the natural numbers.                      *)
  +(* ------------------------------------------------------------------------- *)
   overload_interface("divides", (parse_term "num_divides:num->num->bool"))
   overload_interface("mod", (parse_term "num_mod:num->num->num->bool"))
   overload_interface("coprime", (parse_term "num_coprime:num#num->bool"))
   overload_interface("gcd", (parse_term "num_gcd:num#num->num"))
   
  -(* ------------------------------------------------------------------------- *)
  -(* Now define similar notions over the natural numbers.                      *)
  -(* ------------------------------------------------------------------------- *)
   let num_divides = new_definition(parse_term "a divides b <=> &a divides &b")
   
   let num_mod = new_definition(parse_term "(mod n) x y <=> (mod &n) (&x) (&y)")
  
positive.code:                             "min", (parse_term "int_min:int->int->int")
                              "&", (parse_term "int_of_num:num->int")]
  
  (* ------------------------------------------------------------------------- *)
  (* Set up interface map.                                                     *)
  (* ------------------------------------------------------------------------- *)
  let prioritize_int() = prioritize_overload(mk_type("int", []))
  
  (* ------------------------------------------------------------------------- *)
  
negative.code: let num_coprime = new_definition(parse_term "coprime(a,b) <=> coprime(&a,&b)")
  let num_gcd = new_definition(parse_term "gcd(a,b) = num_of_int(gcd(&a,&b))")
  
  (* ------------------------------------------------------------------------- *)
  (* Map an assertion over N to an integer equivalent.                         *)
  (* To make this work nicely, all variables of type num should be quantified. *)
  (* ------------------------------------------------------------------------- *)
  
  let NUM_TO_INT_CONV =
    let pth_relativize = 
     prove ((parse_term "((!n. P(&n)) <=> (!i. ~(&0 <= i) \/ P i)) /\
       ((?n. P(&n)) <=> (?i. &0 <= i /\ P i))"),
      REWRITE_TAC[INT_EXISTS_POS; INT_FORALL_POS] |>THEN<| MESON_TAC[])
    let relation_conv = 
     (GEN_REWRITE_CONV TOP_SWEEP_CONV << map GSYM) [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE; INT_OF_NUM_GT;
      INT_OF_NUM_SUC; INT_OF_NUM_ADD; INT_OF_NUM_MUL; INT_OF_NUM_POW]
    let quantifier_conv = GEN_REWRITE_CONV DEPTH_CONV [pth_relativize]
    NUM_SIMPLIFY_CONV |>THENC<| relation_conv |>THENC<| quantifier_conv
  
  (* ------------------------------------------------------------------------- *)
  (* Linear decision procedure for the naturals at last!                       *)
  (* ------------------------------------------------------------------------- *)
  
  let ARITH_RULE =
    let init_conv =
      NUM_SIMPLIFY_CONV |>THENC<|
      GEN_REWRITE_CONV DEPTH_CONV [ADD1] |>THENC<|
      PROP_ATOM_CONV (BINOP_CONV NUM_NORMALIZE_CONV) |>THENC<|
      PRENEX_CONV |>THENC<|
      (GEN_REWRITE_CONV TOP_SWEEP_CONV << map GSYM)
        [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE;
         INT_OF_NUM_GT; INT_OF_NUM_ADD; SPEC (parse_term "NUMERAL k") INT_OF_NUM_MUL;
         INT_OF_NUM_MAX; INT_OF_NUM_MIN]
    let is_numimage t =
      match t with
        Comb(Const("int_of_num",_),n) when not(is_numeral n) -> true
      | _ -> false in
    fun tm ->
      let th1 = init_conv tm in
      let tm1 = rand(concl th1) in
      let avs,bod = strip_forall tm1 in
      let nim = setify(find_terms is_numimage bod) in
      let gvs = map (genvar << type_of) nim in
      let pths = map (fun v -> SPEC (rand v) INT_POS) nim in
      let ibod = itlist (curry mk_imp << concl) pths bod in
      let gbod = subst (zip gvs nim) ibod in
      let th2 = INST (zip nim gvs) (INT_ARITH gbod) in
      let th3 = GENL avs (rev_itlist (C MP) pths th2) in
      EQ_MP (SYM th1) th3;;
  
  let ARITH_TAC = CONV_TAC(EQT_INTRO << ARITH_RULE);;
  
  let ASM_ARITH_TAC =
    REPEAT(FIRST_X_ASSUM(MP_TAC << check (not << is_forall << concl))) |>THEN<|
    ARITH_TAC;;
  
  (* ------------------------------------------------------------------------- *)
  (* Also a similar divisibility procedure for natural numbers.                *)
  (* ------------------------------------------------------------------------- *)
  
  let NUM_GCD = 
   prove ((parse_term "!a b. &(gcd(a,b)) = gcd(&a,&b)"),
    REWRITE_TAC[num_gcd; GSYM NUM_OF_INT; int_gcd]);;
  
  let NUMBER_TAC =
    let pth_relativize = 
     prove ((parse_term "((!n. P(&n)) <=> (!i. &0 <= i ==> P i)) /\
       ((?n. P(&n)) <=> (?i. &0 <= i /\ P i))"),
      GEN_REWRITE_TAC RAND_CONV [TAUT (parse_term "(a <=> b) <=> (~a <=> ~b)")] |>THEN<|
      REWRITE_TAC[NOT_EXISTS_THM; INT_FORALL_POS] |>THEN<| MESON_TAC[])
    let relation_conv =
     GEN_REWRITE_CONV TOP_SWEEP_CONV
      (num_divides::num_congruent::num_coprime::NUM_GCD::(map GSYM [INT_OF_NUM_EQ; INT_OF_NUM_LE; INT_OF_NUM_LT; INT_OF_NUM_GE; INT_OF_NUM_GT;
       INT_OF_NUM_SUC; INT_OF_NUM_ADD; INT_OF_NUM_MUL; INT_OF_NUM_POW]))
    let quantifier_conv = GEN_REWRITE_CONV DEPTH_CONV [pth_relativize]
    W(fun (_,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) |>THEN<|
    CONV_TAC(relation_conv |>THENC<| quantifier_conv) |>THEN<|
    REWRITE_TAC[RIGHT_IMP_FORALL_THM] |>THEN<| REPEAT GEN_TAC |>THEN<|
    INTEGER_TAC;;
  
  let NUMBER_RULE tm = prove(tm,NUMBER_TAC);;
  
  (* ------------------------------------------------------------------------- *)
  (* Make sure we give priority to N.                                          *)
  (* ------------------------------------------------------------------------- *)
  
  
  prioritize_num()