paulson@8774: (*  Title:      Provers/Arith/combine_numerals.ML
paulson@8774:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8774:     Copyright   2000  University of Cambridge
paulson@8774: 
paulson@8774: Combine coefficients in expressions:
paulson@8774: 
paulson@8774:      i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
paulson@8774: 
paulson@8774: It works by (a) massaging the sum to bring the selected terms to the front:
paulson@8774: 
paulson@8774:      #m*u + (#n*u + (i + (j + k)))
paulson@8774: 
paulson@8774: (b) then using left_distrib to reach
paulson@8774: 
paulson@8774:      #(m+n)*u + (i + (j + k))
paulson@8774: *)
paulson@8774: 
paulson@8774: signature COMBINE_NUMERALS_DATA =
paulson@8774: sig
paulson@8774:   (*abstract syntax*)
huffman@23058:   eqtype coeff
huffman@23058:   val iszero: coeff -> bool
huffman@23058:   val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
paulson@14387:   val mk_sum: typ -> term list -> term
paulson@8774:   val dest_sum: term -> term list
huffman@23058:   val mk_coeff: coeff * term -> term
huffman@23058:   val dest_coeff: term -> coeff * term
paulson@8774:   (*rules*)
paulson@8774:   val left_distrib: thm
paulson@8774:   (*proof tools*)
wenzelm@20114:   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
haftmann@44947:   val trans_tac: thm option -> tactic            (*applies the initial lemma*)
wenzelm@51717:   val norm_tac: Proof.context -> tactic          (*proves the initial lemma*)
wenzelm@51717:   val numeral_simp_tac: Proof.context -> tactic  (*proves the final theorem*)
wenzelm@51717:   val simplify_meta_eq: Proof.context -> thm -> thm  (*simplifies the final theorem*)
paulson@8774: end;
paulson@8774: 
paulson@8774: 
paulson@8774: functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
paulson@8774:   sig
wenzelm@51717:   val proc: Proof.context -> term -> thm option
wenzelm@20114:   end
paulson@8774: =
paulson@8774: struct
paulson@8774: 
paulson@8774: (*Remove the first occurrence of #m*u from the term list*)
paulson@8774: fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
wenzelm@20114:       raise TERM("combine_numerals: remove", [])
paulson@8774:   | remove (m, u, t::terms) =
paulson@9646:       case try Data.dest_coeff t of
wenzelm@20114:           SOME(n,v) => if m=n andalso u aconv v then terms
wenzelm@20114:                        else t :: remove (m, u, terms)
wenzelm@20114:         | NONE      =>  t :: remove (m, u, terms);
paulson@8774: 
paulson@8774: (*a left-to-right scan of terms, seeking another term of the form #n*u, where
paulson@8774:   #m*u is already in terms for some m*)
wenzelm@20114: fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
paulson@8774:   | find_repeated (tab, past, t::terms) =
paulson@9646:       case try Data.dest_coeff t of
wenzelm@20114:           SOME(n,u) =>
wenzelm@20114:               (case Termtab.lookup tab u of
wenzelm@20114:                   SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
wenzelm@20114:                 | NONE => find_repeated (Termtab.update (u, n) tab,
wenzelm@20114:                                          t::past,  terms))
wenzelm@20114:         | NONE => find_repeated (tab, t::past, terms);
paulson@8774: 
paulson@8774: (*the simplification procedure*)
wenzelm@51717: fun proc ctxt t =
wenzelm@20044:   let
wenzelm@20114:     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
wenzelm@20114:     val export = singleton (Variable.export ctxt' ctxt)
wenzelm@51717:     (* FIXME ctxt vs. ctxt' (!?) *)
wenzelm@20114: 
wenzelm@20114:     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
wenzelm@20114:     val T = Term.fastype_of u
wenzelm@20114: 
wenzelm@20114:     val reshape =  (*Move i*u to the front and put j*u into standard form
wenzelm@20114:                        i + #m + j + k == #m + i + (j + k) *)
huffman@23058:       if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
wenzelm@20114:         raise TERM("combine_numerals", [])
wenzelm@51717:       else Data.prove_conv [Data.norm_tac ctxt] ctxt
wenzelm@20114:         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
paulson@8774:   in
wenzelm@51717:     Option.map (export o Data.simplify_meta_eq ctxt)
wenzelm@20114:       (Data.prove_conv
haftmann@44947:          [Data.trans_tac reshape, rtac Data.left_distrib 1,
wenzelm@51717:           Data.numeral_simp_tac ctxt] ctxt
wenzelm@20114:          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
paulson@8774:   end
wenzelm@20114:   (* FIXME avoid handling of generic exceptions *)
skalberg@15531:   handle TERM _ => NONE
skalberg@15531:        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
wenzelm@20114:                              Undeclared type constructor "Numeral.bin"*)
paulson@8774: 
paulson@8774: end;