src/Provers/Arith/combine_coeff.ML

new simprocs assoc_fold and combine_coeff

(*  Title:      Provers/Arith/combine_coeff.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1999  University of Cambridge

Simplification procedure to combine literal coefficients in sums of products

Example, #3*x + y - (x*#2) goes to x + y

For the relations <, <= and =, the difference is simplified

[COULD BE GENERALIZED to products of exponentials?]
*)

signature COMBINE_COEFF_DATA =
sig
  val ss		: simpset	(*basic simpset of object-logtic*)
  val eq_reflection	: thm		(*object-equality to meta-equality*)
  val thy		: theory	(*the theory of the group*)
  val T			: typ		(*the type of group elements*)

  val trans             : thm           (*transitivity of equals*)
  val add_ac		: thm list      (*AC-rules for the addition operator*)
  val diff_def		: thm		(*Defines x-y as x + -y *)
  val minus_add_distrib	: thm           (* -(x+y) = -x + -y *)        
  val minus_minus	: thm           (* - -x = x *)
  val mult_commute 	: thm		(*commutative law for the product*)
  val mult_1_right 	: thm           (*the law x*1=x *)
  val add_mult_distrib  : thm           (*law w*(x+y) = w*x + w*y *)
  val diff_mult_distrib : thm           (*law w*(x-y) = w*x - w*y *)
  val mult_minus_right  : thm           (*law x * -y = -(x*y) *)

  val rel_iff_rel_0_rls : thm list      (*e.g. (x < y) = (x-y < 0) *)
  val dest_eqI		: thm -> term   (*to get patterns from the rel rules*)
end;


functor Combine_Coeff (Data: COMBINE_COEFF_DATA) =
struct

 local open Data 
 in
 val rhs_ss = ss addsimps
                    [add_mult_distrib, diff_mult_distrib,
		     mult_minus_right, mult_1_right];

 val lhs_ss = ss addsimps
		 add_ac @
		 [diff_def, minus_add_distrib, minus_minus, mult_commute];
 end;

 (*prove while suppressing timing information*)
 fun prove name ct tacf = 
     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
     handle ERROR =>
	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
                
 val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
 val minus = Const ("op -", [Data.T,Data.T] ---> Data.T);
 val uminus = Const ("uminus", Data.T --> Data.T);
 val times = Const ("op *", [Data.T,Data.T] ---> Data.T);

 val number_of = Const ("Numeral.number_of", 
			Type ("Numeral.bin", []) --> Data.T);

 val zero = number_of $ HOLogic.pls_const;
 val one =  number_of $ (HOLogic.bit_const $ 
			 HOLogic.pls_const $ 
			 HOLogic.true_const);

 (*We map -t to t and (in other cases) t to -t.  No need to check the type of
   uminus, since the simproc is only called on sums of type T.*)
 fun negate (Const("uminus",_) $ t) = t
   | negate t                       = uminus $ t;

 fun mk_sum []  = zero
   | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;

 fun attach_coeff (Bound ~1,ns) = mk_sum ns  (*just a literal*)
   | attach_coeff (x,ns) = times $ x $ (mk_sum ns);

 fun add_atom (x, (neg,m)) pairs = 
   let val m' = if neg then negate m else m
   in 
       case gen_assoc (op aconv) (pairs, x) of
	   Some n => gen_overwrite (op aconv) (pairs, (x, m'::n))
	 | None => (x,[m']) :: pairs
   end;

 (**STILL MISSING: a treatment of nested coeffs, e.g. a*(b*3) **)
 (*Convert a formula built from +, * and - (binary and unary) to a
   (atom, coeff) association list.  Handles t+t, t-t, -t, a*n, n*a, n, a
   where n denotes a numeric literal and a is any other term.
   No need to check types PROVIDED they are checked upon entry!*)
 fun add_terms neg (Const("op +", _) $ x $ y, pairs) =
	 add_terms neg (x, add_terms neg (y, pairs))
   | add_terms neg (Const("op -", _) $ x $ y, pairs) =
	 add_terms neg (x, add_terms (not neg) (y, pairs))
   | add_terms neg (Const("uminus", _) $ x, pairs) = 
	 add_terms (not neg) (x, pairs)
   | add_terms neg (lit as Const("Numeral.number_of", _) $ _, pairs) =
	 (*literal: make it the coefficient of a dummy term*)
	 add_atom (Bound ~1, (neg, lit)) pairs
   | add_terms neg (Const("op *", _) $ x 
		             $ (lit as Const("Numeral.number_of", _) $ _),
		    pairs) =
	 (*coefficient on the right*)
	 add_atom (x, (neg, lit)) pairs
   | add_terms neg (Const("op *", _) 
		             $ (lit as Const("Numeral.number_of", _) $ _)
                             $ x, pairs) =
	 (*coefficient on the left*)
	 add_atom (x, (neg, lit)) pairs
   | add_terms neg (x, pairs) = add_atom (x, (neg, one)) pairs;

 fun terms fml = add_terms false (fml, []);

 exception CC_fail;

 (*The number of terms in t, assuming no collapsing takes place*)
 fun term_count (Const("op +", _) $ x $ y) = term_count x + term_count y
   | term_count (Const("op -", _) $ x $ y) = term_count x + term_count y
   | term_count (Const("uminus", _) $ x) = term_count x
   | term_count x = 1;


 val trace = ref false;

 (*The simproc for sums*)
 fun sum_proc sg _ lhs =
   let fun show t = string_of_cterm (Thm.cterm_of sg t)
       val _ = if !trace then writeln 
	                   ("combine_coeff sum simproc: LHS = " ^ show lhs)
	       else ()
       val ts = terms lhs
       val _ = if term_count lhs = length ts 
               then raise CC_fail (*we can't reduce the number of terms*)
               else ()  
       val rhs = mk_sum (map attach_coeff ts)
       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
       val th = prove "combine_coeff" 
	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
		   (fn _ => [rtac Data.eq_reflection 1,
			     simp_tac rhs_ss 1,
			     IF_UNSOLVED (simp_tac lhs_ss 1)])
   in Some th end
   handle CC_fail => None;

 val sum_conv = 
     Simplifier.mk_simproc "combine_coeff_sums"
       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
	[("x + y", Data.T), ("x - y", Data.T)])
       sum_proc;


 (*The simproc for relations, which just replaces x<y by x-y<0 and simplifies*)

 val trans_eq_reflection = Data.trans RS Data.eq_reflection |> standard;

 fun rel_proc sg asms (lhs as (rel$lt$rt)) =
   let val _ = if !trace then writeln
                               ("cc_rel simproc: LHS = " ^ 
				string_of_cterm (cterm_of sg lhs))
	       else ()
       val _ = if lt=zero orelse rt=zero then raise CC_fail 
               else ()   (*this simproc can do nothing if either side is zero*)
       val cc_th = the (sum_proc sg asms (minus $ lt $ rt))
                   handle OPTION => raise CC_fail
       val _ = if !trace then 
		 writeln ("cc_th = " ^ string_of_thm cc_th)
	       else ()
       val cc_lr = #2 (Logic.dest_equals (concl_of cc_th))

       val rhs = rel $ cc_lr $ zero
       val _ = if !trace then 
		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
	       else ()
       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))

       val th = prove "cc_rel" ct 
                  (fn _ => [rtac trans_eq_reflection 1,
			    resolve_tac Data.rel_iff_rel_0_rls 1,
			    simp_tac (Data.ss addsimps [cc_th]) 1])
   in Some th end
   handle CC_fail => None;

 val rel_conv = 
     Simplifier.mk_simproc "cc_relations"
       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI)
            Data.rel_iff_rel_0_rls)
       rel_proc;

end;