# File combine_numerals.ML

    (*  Title:      Provers/Arith/combine_numerals.ML
        ID:         $Id: combine_numerals.ML,v 1.15 2005/09/15 15:16:58 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   2000  University of Cambridge

    Combine coefficients in expressions:

         i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))

    It works by (a) massaging the sum to bring the selected terms to the front:

         #m*u + (#n*u + (i + (j + k)))

    (b) then using left_distrib to reach

         #(m+n)*u + (i + (j + k))
    *)

    signature COMBINE_NUMERALS_DATA =
    sig
      (*abstract syntax*)
      val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
      val mk_sum: typ -> term list -> term
      val dest_sum: term -> term list
      val mk_coeff: IntInf.int * term -> term
      val dest_coeff: term -> IntInf.int * term
      (*rules*)
      val left_distrib: thm
      (*proof tools*)
      val prove_conv: tactic list -> theory -> string list -> term * term -> thm option
      val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
      val norm_tac: simpset -> tactic                (*proves the initial lemma*)
      val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
      val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    end;

    functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
      sig
      val proc: theory -> simpset -> term -> thm option
      end
    =
    struct

    (*Remove the first occurrence of #m*u from the term list*)
    fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
          raise TERM("combine_numerals: remove", [])
      | remove (m, u, t::terms) =
          case try Data.dest_coeff t of
    	  SOME(n,v) => if m=n andalso u aconv v then terms
    		       else t :: remove (m, u, terms)
    	| NONE      =>  t :: remove (m, u, terms);

    (*a left-to-right scan of terms, seeking another term of the form #n*u, where
      #m*u is already in terms for some m*)
    fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
      | find_repeated (tab, past, t::terms) =
          case try Data.dest_coeff t of
    	  SOME(n,u) =>
    	      (case Termtab.lookup tab u of
    		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
    		| NONE => find_repeated (Termtab.update (u, n) tab,
    					 t::past,  terms))
    	| NONE => find_repeated (tab, t::past, terms);

    (*the simplification procedure*)
    fun proc thy ss t =
      let (*first freeze any Vars in the term to prevent flex-flex problems*)
          val (t', xs) = Term.adhoc_freeze_vars t
          val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
          val T = Term.fastype_of u
          val reshape =  (*Move i*u to the front and put j*u into standard form
    		       i + #m + j + k == #m + i + (j + k) *)
    	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    		raise TERM("combine_numerals", [])
    	    else Data.prove_conv [Data.norm_tac ss] thy xs
    			(t',
    			 Data.mk_sum T ([Data.mk_coeff(m,u),
    				         Data.mk_coeff(n,u)] @ terms))
      in
          Option.map (Data.simplify_meta_eq ss)
    	 (Data.prove_conv
    	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    	     Data.numeral_simp_tac ss] thy xs
    	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
      end
      handle TERM _ => NONE
           | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    			     Undeclared type constructor "Numeral.bin"*)

    end;