src/Provers/Arith/combine_numerals.ML
author huffman
Mon May 21 19:05:37 2007 +0200 (2007-05-21)
changeset 23058 c722004c5a22
parent 20114 a1bb4bc68ff3
child 35762 af3ff2ba4c54
permissions -rw-r--r--
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
     1 (*  Title:      Provers/Arith/combine_numerals.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     5 
     6 Combine coefficients in expressions:
     7 
     8      i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
     9 
    10 It works by (a) massaging the sum to bring the selected terms to the front:
    11 
    12      #m*u + (#n*u + (i + (j + k)))
    13 
    14 (b) then using left_distrib to reach
    15 
    16      #(m+n)*u + (i + (j + k))
    17 *)
    18 
    19 signature COMBINE_NUMERALS_DATA =
    20 sig
    21   (*abstract syntax*)
    22   eqtype coeff
    23   val iszero: coeff -> bool
    24   val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
    25   val mk_sum: typ -> term list -> term
    26   val dest_sum: term -> term list
    27   val mk_coeff: coeff * term -> term
    28   val dest_coeff: term -> coeff * term
    29   (*rules*)
    30   val left_distrib: thm
    31   (*proof tools*)
    32   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
    33   val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    34   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    35   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    36   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    37 end;
    38 
    39 
    40 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    41   sig
    42   val proc: simpset -> term -> thm option
    43   end
    44 =
    45 struct
    46 
    47 (*Remove the first occurrence of #m*u from the term list*)
    48 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
    49       raise TERM("combine_numerals: remove", [])
    50   | remove (m, u, t::terms) =
    51       case try Data.dest_coeff t of
    52           SOME(n,v) => if m=n andalso u aconv v then terms
    53                        else t :: remove (m, u, terms)
    54         | NONE      =>  t :: remove (m, u, terms);
    55 
    56 (*a left-to-right scan of terms, seeking another term of the form #n*u, where
    57   #m*u is already in terms for some m*)
    58 fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
    59   | find_repeated (tab, past, t::terms) =
    60       case try Data.dest_coeff t of
    61           SOME(n,u) =>
    62               (case Termtab.lookup tab u of
    63                   SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
    64                 | NONE => find_repeated (Termtab.update (u, n) tab,
    65                                          t::past,  terms))
    66         | NONE => find_repeated (tab, t::past, terms);
    67 
    68 (*the simplification procedure*)
    69 fun proc ss t =
    70   let
    71     val ctxt = Simplifier.the_context ss;
    72     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    73     val export = singleton (Variable.export ctxt' ctxt)
    74 
    75     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    76     val T = Term.fastype_of u
    77 
    78     val reshape =  (*Move i*u to the front and put j*u into standard form
    79                        i + #m + j + k == #m + i + (j + k) *)
    80       if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
    81         raise TERM("combine_numerals", [])
    82       else Data.prove_conv [Data.norm_tac ss] ctxt
    83         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
    84   in
    85     Option.map (export o Data.simplify_meta_eq ss)
    86       (Data.prove_conv
    87          [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    88           Data.numeral_simp_tac ss] ctxt
    89          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    90   end
    91   (* FIXME avoid handling of generic exceptions *)
    92   handle TERM _ => NONE
    93        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    94                              Undeclared type constructor "Numeral.bin"*)
    95 
    96 end;