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