src/Provers/Arith/assoc_fold.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 60754 02924903a6fd
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Provers/Arith/assoc_fold.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 
     5 Simplification procedure for associative operators + and * on numeric
     6 types.  Performs constant folding when the literals are separated, as
     7 in 3+n+4.
     8 *)
     9 
    10 signature ASSOC_FOLD_DATA =
    11 sig
    12   val assoc_ss: simpset
    13   val eq_reflection: thm
    14   val is_numeral: term -> bool
    15 end;
    16 
    17 signature ASSOC_FOLD =
    18 sig
    19   val proc: Proof.context -> term -> thm option
    20 end;
    21 
    22 functor Assoc_Fold(Data: ASSOC_FOLD_DATA): ASSOC_FOLD =
    23 struct
    24 
    25 exception Assoc_fail;
    26 
    27 fun mk_sum plus []  = raise Assoc_fail
    28   | mk_sum plus tms = foldr1 (fn (x, y) => plus $ x $ y) tms;
    29 
    30 (*Separate the literals from the other terms being combined*)
    31 fun sift_terms plus (t, (lits,others)) =
    32   if Data.is_numeral t then (t::lits, others) (*new literal*) else
    33   (case t of
    34     (f as Const _) $ x $ y =>
    35       if f = plus
    36       then sift_terms plus (x, sift_terms plus (y, (lits,others)))
    37       else (lits, t::others)    (*arbitrary summand*)
    38   | _ => (lits, t::others));
    39 
    40 (*A simproc to combine all literals in a associative nest*)
    41 fun proc ctxt lhs =
    42   let
    43     val plus = (case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern")
    44     val (lits, others) = sift_terms plus (lhs, ([],[]))
    45     val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*)
    46     val rhs = plus $ mk_sum plus lits $ mk_sum plus others
    47     val th =
    48       Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs)) (fn _ =>
    49         resolve_tac ctxt [Data.eq_reflection] 1 THEN
    50         simp_tac (put_simpset Data.assoc_ss ctxt) 1)
    51   in SOME th end handle Assoc_fail => NONE;
    52 
    53 end;