src/Provers/Arith/combine_numerals.ML
changeset 14387 e96d5c42c4b0
parent 13484 d8f5d3391766
child 15027 d23887300b96
     1.1 --- a/src/Provers/Arith/combine_numerals.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/Provers/Arith/combine_numerals.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  sig
     1.5    (*abstract syntax*)
     1.6    val add: int * int -> int          (*addition (or multiplication) *)
     1.7 -  val mk_sum: term list -> term
     1.8 +  val mk_sum: typ -> term list -> term
     1.9    val dest_sum: term -> term list
    1.10    val mk_coeff: int * term -> term
    1.11    val dest_coeff: term -> int * term
    1.12 @@ -66,22 +66,23 @@
    1.13  (*the simplification procedure*)
    1.14  fun proc sg _ t =
    1.15    let (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.16 -      val (t', xs) = Term.adhoc_freeze_vars t;
    1.17 +      val (t', xs) = Term.adhoc_freeze_vars t
    1.18        val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    1.19 +      val T = Term.fastype_of u
    1.20        val reshape =  (*Move i*u to the front and put j*u into standard form
    1.21  		       i + #m + j + k == #m + i + (j + k) *)
    1.22  	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    1.23  		raise TERM("combine_numerals", []) 
    1.24  	    else Data.prove_conv [Data.norm_tac] sg xs
    1.25  			(t', 
    1.26 -			 Data.mk_sum ([Data.mk_coeff(m,u),
    1.27 -				       Data.mk_coeff(n,u)] @ terms))
    1.28 +			 Data.mk_sum T ([Data.mk_coeff(m,u),
    1.29 +				         Data.mk_coeff(n,u)] @ terms))
    1.30    in
    1.31        apsome Data.simplify_meta_eq
    1.32  	 (Data.prove_conv 
    1.33  	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    1.34  	     Data.numeral_simp_tac] sg xs
    1.35 -	    (t', Data.mk_sum (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    1.36 +	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    1.37    end
    1.38    handle TERM _ => None
    1.39         | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)