1(* ===================================================================== *)
2(* FILE          : Num_conv.sml                                          *)
3(* DESCRIPTION   : num_CONV maps a numeric literal to a theorem equating *)
4(*                 it with the successor of its predecessor.             *)
5(*                                                                       *)
6(* AUTHOR        : T.Melham                                              *)
7(* TRANSLATOR    : Konrad Slind, University of Calgary                   *)
8(* DATE          : 87.08.23                                              *)
9(*                 September 11, 1991                                    *)
10(* REVISED       : Michael Norrish 1999, for numerals                    *)
11(*                 (this code formerly used mk_thm, but no longer:       *)
12(*                  numbers are built-up in a binary fashion)            *)
13(* ===================================================================== *)
14
15
16structure Num_conv :> Num_conv =
17struct
18
19open HolKernel Parse boolLib;
20
21val (Type,Term) = parse_from_grammars arithmeticTheory.arithmetic_grammars
22
23(* |- !m n. 0 < n ==> ((m = PRE n) = SUC m = n) *)
24
25val PRE_SUC_EQ      = arithmeticTheory.PRE_SUC_EQ
26
27val numeral_pre     = numeralTheory.numeral_pre
28val numeral_lt      = numeralTheory.numeral_lt
29val numeral_distrib = numeralTheory.numeral_distrib
30val save_zero =
31  prove(Term`NUMERAL ZERO = 0`,
32   REWRITE_TAC [arithmeticTheory.NUMERAL_DEF, arithmeticTheory.ALT_ZERO]);
33
34
35local val RW_CONV1 = REWRITE_CONV [numeral_pre, numeral_distrib, save_zero]
36      val RW_CONV2 = REWRITE_CONV [numeral_lt, numeral_distrib]
37      val ZERO = numSyntax.zero_tm
38      val PRE  = numSyntax.pre_tm
39      val lt_0 = mk_comb(numSyntax.less_tm, ZERO)
40      val one  = numSyntax.mk_numeral(Arbnum.fromInt 1)
41      val two  = numSyntax.mk_numeral(Arbnum.fromInt 2)
42in
43fun num_CONV t =
44 if aconv t one then arithmeticTheory.ONE else
45 if aconv t two then arithmeticTheory.TWO else
46 if Literal.is_numeral t andalso not (aconv t ZERO)
47 then let val pre_t    = mk_comb(PRE, t)
48          val pre_thm  = SYM (RW_CONV1 pre_t)
49          val result_t = lhs (concl pre_thm)
50          val less_thm = EQT_ELIM (RW_CONV2 (mk_comb(lt_0, t)))
51          val thm0     = MP (SPECL [result_t, t] PRE_SUC_EQ) less_thm
52      in
53         SYM (EQ_MP thm0 pre_thm)
54      end
55 else raise (mk_HOL_ERR "Num_conv" "num_CONV"
56                        "Term either not a numeral or zero")
57end;
58
59end; (* Num_conv *)
60