1(*  Title:      Provers/Arith/assoc_fold.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1999  University of Cambridge
4
5Simplification procedure for associative operators + and * on numeric
6types.  Performs constant folding when the literals are separated, as
7in 3+n+4.
8*)
9
10signature ASSOC_FOLD_DATA =
11sig
12  val assoc_ss: simpset
13  val eq_reflection: thm
14  val is_numeral: term -> bool
15end;
16
17signature ASSOC_FOLD =
18sig
19  val proc: Proof.context -> term -> thm option
20end;
21
22functor Assoc_Fold(Data: ASSOC_FOLD_DATA): ASSOC_FOLD =
23struct
24
25exception Assoc_fail;
26
27fun 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*)
31fun 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*)
41fun 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
53end;
54