1(*****************************************************************************) 2(* FILE : arith_cons.sml *) 3(* DESCRIPTION : Constructor, destructor and discriminator functions for *) 4(* arithmetic terms. *) 5(* *) 6(* READS FILES : <none> *) 7(* WRITES FILES : <none> *) 8(* *) 9(* AUTHOR : R.J.Boulton, University of Cambridge *) 10(* DATE : 4th March 1991 *) 11(* *) 12(* TRANSLATOR : R.J.Boulton, University of Cambridge *) 13(* DATE : 4th February 1993 *) 14(* *) 15(* LAST MODIFIED : R.J.Boulton *) 16(* DATE : 16th November 1995 *) 17(*****************************************************************************) 18 19structure Arith_cons :> Arith_cons = 20struct 21 22open HolKernel Arbint Abbrev; 23 24local open arithmeticTheory in end; 25 26(*===========================================================================*) 27(* Constructors, destructors and discriminators for +,-,* *) 28(*===========================================================================*) 29 30val num_ty = numSyntax.num 31 32(*---------------------------------------------------------------------------*) 33(* mk_plus, mk_minus, mk_mult *) 34(*---------------------------------------------------------------------------*) 35 36val mk_plus = numSyntax.mk_plus 37and mk_minus = numSyntax.mk_minus 38and mk_mult = numSyntax.mk_mult 39 40(*---------------------------------------------------------------------------*) 41(* dest_plus, dest_minus, dest_mult *) 42(*---------------------------------------------------------------------------*) 43 44val dest_plus = numSyntax.dest_plus 45and dest_minus = numSyntax.dest_minus 46and dest_mult = numSyntax.dest_mult 47 48(*---------------------------------------------------------------------------*) 49(* is_plus, is_minus, is_mult, is_arith_op *) 50(*---------------------------------------------------------------------------*) 51 52val is_plus = numSyntax.is_plus 53and is_minus = numSyntax.is_minus 54and is_mult = numSyntax.is_mult 55 56(*===========================================================================*) 57(* Constructors, destructors and discriminators for <,<=,>,>= *) 58(*===========================================================================*) 59 60(*---------------------------------------------------------------------------*) 61(* mk_less, mk_leq, mk_great, mk_geq *) 62(*---------------------------------------------------------------------------*) 63 64val mk_less = numSyntax.mk_less 65and mk_leq = numSyntax.mk_leq 66and mk_great = numSyntax.mk_greater 67and mk_geq = numSyntax.mk_geq 68 69(*---------------------------------------------------------------------------*) 70(* dest_less, dest_leq, dest_great, dest_geq *) 71(*---------------------------------------------------------------------------*) 72 73val dest_less = numSyntax.dest_less 74and dest_leq = numSyntax.dest_leq 75and dest_great = numSyntax.dest_greater 76and dest_geq = numSyntax.dest_geq 77 78(*---------------------------------------------------------------------------*) 79(* is_less, is_leq, is_great, is_geq, is_num_reln *) 80(*---------------------------------------------------------------------------*) 81 82val is_less = numSyntax.is_less 83and is_leq = numSyntax.is_leq 84and is_great = numSyntax.is_greater 85and is_geq = numSyntax.is_geq; 86 87(*===========================================================================*) 88(* Constructor, destructor and discriminator for SUC *) 89(*===========================================================================*) 90 91val mk_suc = numSyntax.mk_suc 92val dest_suc = numSyntax.dest_suc 93val is_suc = numSyntax.is_suc; 94 95(*===========================================================================*) 96(* Constructor, destructor and discriminator for PRE *) 97(*===========================================================================*) 98 99val mk_pre = numSyntax.mk_pre 100val dest_pre = numSyntax.dest_pre 101val is_pre = numSyntax.is_pre 102 103(*===========================================================================*) 104(* Discriminators for numbers *) 105(*===========================================================================*) 106 107val is_num_const = numSyntax.is_numeral 108val zero = numSyntax.zero_tm 109fun is_zero tm = (tm = zero) 110 111 112(*===========================================================================*) 113(* Conversions between ML integers and numeric constant terms *) 114(*===========================================================================*) 115 116val int_of_term = fromNat o numSyntax.dest_numeral 117val term_of_int = numSyntax.mk_numeral o toNat 118 119(*===========================================================================*) 120(* Generation of a numeric variable from a name *) 121(*===========================================================================*) 122 123fun mk_num_var s = mk_var(s,num_ty); 124 125(*===========================================================================*) 126(* Functions to extract the arguments from an application of a binary op. *) 127(*===========================================================================*) 128 129val arg1 = rand o rator 130and arg2 = rand; 131 132(*===========================================================================*) 133(* Is a term a full application of a numerical relation? *) 134(*===========================================================================*) 135 136local infixr --> 137 val num_reln_type = num_ty --> num_ty --> bool 138in 139fun is_num_reln tm = 140 (num_reln_type = type_of(rator(rator tm))) handle HOL_ERR _ => false 141end; 142 143end 144