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