1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Provers/Arith/assoc_fold.ML	Fri Jul 23 17:24:48 1999 +0200
     1.3 @@ -0,0 +1,85 @@
     1.4 +(*  Title:      Provers/Arith/assoc_fold.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Simplification procedure for associative operators + and * on numeric types
    1.10 +
    1.11 +Performs constant folding when the literals are separated, as in 3+n+4.
    1.12 +*)
    1.13 +
    1.14 +
    1.15 +signature ASSOC_FOLD_DATA =
    1.16 +sig
    1.17 +  val ss		: simpset	(*basic simpset of object-logtic*)
    1.18 +  val eq_reflection	: thm		(*object-equality to meta-equality*)
    1.19 +  val thy		: theory	(*the operator's theory*)
    1.20 +  val T			: typ		(*the operator's numeric type*)
    1.21 +  val plus		: term		(*the operator being folded*)
    1.22 +  val add_ac		: thm list      (*AC-rewrites for plus*)
    1.23 +end;
    1.24 +
    1.25 +
    1.26 +functor Assoc_Fold (Data: ASSOC_FOLD_DATA) =
    1.27 +struct
    1.28 +
    1.29 + val assoc_ss = Data.ss addsimps Data.add_ac;
    1.30 +
    1.31 + (*prove while suppressing timing information*)
    1.32 + fun prove name ct tacf = 
    1.33 +     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
    1.34 +     handle ERROR =>
    1.35 +	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    1.36 +                
    1.37 + exception Assoc_fail;
    1.38 +
    1.39 + fun mk_sum []  = raise Assoc_fail
    1.40 +   | mk_sum tms = foldr1 (fn (x,y) => Data.plus $ x $ y) tms;
    1.41 +
    1.42 + (*Separate the literals from the other terms being combined*)
    1.43 + fun sift_terms (t, (lits,others)) =
    1.44 +     case t of
    1.45 +	  Const("Numeral.number_of", _) $ _ =>
    1.46 +	      (t::lits, others)         (*new literal*)
    1.47 +	| (f as Const _) $ x $ y =>
    1.48 +	      if f = Data.plus 
    1.49 +              then sift_terms (x, sift_terms (y, (lits,others)))
    1.50 +	      else (lits, t::others)    (*arbitrary summand*)
    1.51 +	| _ => (lits, t::others);
    1.52 +
    1.53 + val trace = ref false;
    1.54 +
    1.55 + (*Make a simproc to combine all literals in a associative nest*)
    1.56 + fun proc sg _ lhs =
    1.57 +   let fun show t = string_of_cterm (Thm.cterm_of sg t)
    1.58 +       val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
    1.59 +	       else ()
    1.60 +       val (lits,others) = sift_terms (lhs, ([],[]))
    1.61 +       val _ = if length lits < 2
    1.62 +               then raise Assoc_fail (*we can't reduce the number of terms*)
    1.63 +               else ()  
    1.64 +       val rhs = Data.plus $ mk_sum lits $ mk_sum others
    1.65 +       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
    1.66 +       val th = prove "assoc_fold" 
    1.67 +	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
    1.68 +		   (fn _ => [rtac Data.eq_reflection 1,
    1.69 +			     simp_tac assoc_ss 1])
    1.70 +   in Some th end
    1.71 +   handle Assoc_fail => None;
    1.72 + 
    1.73 + val conv = 
    1.74 +     Simplifier.mk_simproc "assoc_fold_sums"
    1.75 +       [Thm.cterm_of (Theory.sign_of Data.thy)
    1.76 +	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
    1.77 +       proc;
    1.78 +
    1.79 +end;
    1.80 +
    1.81 +
    1.82 +(*test data:
    1.83 +set proof_timing;
    1.84 +
    1.85 +Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
    1.86 +
    1.87 +Goal "a + b + c + d + e + f + g + h + i + j + k + l + m + n + oo + p + q + r + s + t + u + v + (w + x + y + z + a + #2 + b + #2 + c + #2 + d + #2 + e) + #2 + f + (#2 + g + #2 + h + #2 + i) + #2 + (j + #2 + k + #2 + l + #2 + m + #2) + n + #2 + (oo + #2 + p + #2 + q + #2 + r) + #2 + s + #2 + t + #2 + u + #2 + v + #2 + w + #2 + x + #2 + y + #2 + z + #2 = (uu::nat)";
    1.88 +*)