new simprocs assoc_fold and combine_coeff
authorpaulson
Fri Jul 23 17:24:48 1999 +0200 (1999-07-23)
changeset 7072c3f3fd86e11c
parent 7071 55b80ec1927d
child 7073 a959b4391fd8
new simprocs assoc_fold and combine_coeff
src/HOL/ROOT.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/combine_coeff.ML
     1.1 --- a/src/HOL/ROOT.ML	Fri Jul 23 16:54:28 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri Jul 23 17:24:48 1999 +0200
     1.3 @@ -27,10 +27,12 @@
     1.4  use "~~/src/Provers/Arith/cancel_sums.ML";
     1.5  use "~~/src/Provers/Arith/cancel_factor.ML";
     1.6  use "~~/src/Provers/Arith/abel_cancel.ML";
     1.7 +use "~~/src/Provers/Arith/assoc_fold.ML";
     1.8  use "~~/src/Provers/quantifier1.ML";
     1.9  
    1.10  use_thy "HOL";
    1.11  use "hologic.ML";
    1.12 +use "~~/src/Provers/Arith/combine_coeff.ML";
    1.13  use "cladata.ML";
    1.14  use "simpdata.ML";
    1.15  
    1.16 @@ -70,6 +72,7 @@
    1.17  use_thy "IntDef";
    1.18  use "simproc.ML";
    1.19  use_thy "NatBin";
    1.20 +use "bin_simprocs.ML";
    1.21  cd "..";
    1.22  
    1.23  (*the all-in-one theory*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Provers/Arith/assoc_fold.ML	Fri Jul 23 17:24:48 1999 +0200
     2.3 @@ -0,0 +1,85 @@
     2.4 +(*  Title:      Provers/Arith/assoc_fold.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1999  University of Cambridge
     2.8 +
     2.9 +Simplification procedure for associative operators + and * on numeric types
    2.10 +
    2.11 +Performs constant folding when the literals are separated, as in 3+n+4.
    2.12 +*)
    2.13 +
    2.14 +
    2.15 +signature ASSOC_FOLD_DATA =
    2.16 +sig
    2.17 +  val ss		: simpset	(*basic simpset of object-logtic*)
    2.18 +  val eq_reflection	: thm		(*object-equality to meta-equality*)
    2.19 +  val thy		: theory	(*the operator's theory*)
    2.20 +  val T			: typ		(*the operator's numeric type*)
    2.21 +  val plus		: term		(*the operator being folded*)
    2.22 +  val add_ac		: thm list      (*AC-rewrites for plus*)
    2.23 +end;
    2.24 +
    2.25 +
    2.26 +functor Assoc_Fold (Data: ASSOC_FOLD_DATA) =
    2.27 +struct
    2.28 +
    2.29 + val assoc_ss = Data.ss addsimps Data.add_ac;
    2.30 +
    2.31 + (*prove while suppressing timing information*)
    2.32 + fun prove name ct tacf = 
    2.33 +     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
    2.34 +     handle ERROR =>
    2.35 +	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    2.36 +                
    2.37 + exception Assoc_fail;
    2.38 +
    2.39 + fun mk_sum []  = raise Assoc_fail
    2.40 +   | mk_sum tms = foldr1 (fn (x,y) => Data.plus $ x $ y) tms;
    2.41 +
    2.42 + (*Separate the literals from the other terms being combined*)
    2.43 + fun sift_terms (t, (lits,others)) =
    2.44 +     case t of
    2.45 +	  Const("Numeral.number_of", _) $ _ =>
    2.46 +	      (t::lits, others)         (*new literal*)
    2.47 +	| (f as Const _) $ x $ y =>
    2.48 +	      if f = Data.plus 
    2.49 +              then sift_terms (x, sift_terms (y, (lits,others)))
    2.50 +	      else (lits, t::others)    (*arbitrary summand*)
    2.51 +	| _ => (lits, t::others);
    2.52 +
    2.53 + val trace = ref false;
    2.54 +
    2.55 + (*Make a simproc to combine all literals in a associative nest*)
    2.56 + fun proc sg _ lhs =
    2.57 +   let fun show t = string_of_cterm (Thm.cterm_of sg t)
    2.58 +       val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
    2.59 +	       else ()
    2.60 +       val (lits,others) = sift_terms (lhs, ([],[]))
    2.61 +       val _ = if length lits < 2
    2.62 +               then raise Assoc_fail (*we can't reduce the number of terms*)
    2.63 +               else ()  
    2.64 +       val rhs = Data.plus $ mk_sum lits $ mk_sum others
    2.65 +       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
    2.66 +       val th = prove "assoc_fold" 
    2.67 +	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
    2.68 +		   (fn _ => [rtac Data.eq_reflection 1,
    2.69 +			     simp_tac assoc_ss 1])
    2.70 +   in Some th end
    2.71 +   handle Assoc_fail => None;
    2.72 + 
    2.73 + val conv = 
    2.74 +     Simplifier.mk_simproc "assoc_fold_sums"
    2.75 +       [Thm.cterm_of (Theory.sign_of Data.thy)
    2.76 +	             (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
    2.77 +       proc;
    2.78 +
    2.79 +end;
    2.80 +
    2.81 +
    2.82 +(*test data:
    2.83 +set proof_timing;
    2.84 +
    2.85 +Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
    2.86 +
    2.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)";
    2.88 +*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Provers/Arith/combine_coeff.ML	Fri Jul 23 17:24:48 1999 +0200
     3.3 @@ -0,0 +1,193 @@
     3.4 +(*  Title:      Provers/Arith/combine_coeff.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1999  University of Cambridge
     3.8 +
     3.9 +Simplification procedure to combine literal coefficients in sums of products
    3.10 +
    3.11 +Example, #3*x + y - (x*#2) goes to x + y
    3.12 +
    3.13 +For the relations <, <= and =, the difference is simplified
    3.14 +
    3.15 +[COULD BE GENERALIZED to products of exponentials?]
    3.16 +*)
    3.17 +
    3.18 +signature COMBINE_COEFF_DATA =
    3.19 +sig
    3.20 +  val ss		: simpset	(*basic simpset of object-logtic*)
    3.21 +  val eq_reflection	: thm		(*object-equality to meta-equality*)
    3.22 +  val thy		: theory	(*the theory of the group*)
    3.23 +  val T			: typ		(*the type of group elements*)
    3.24 +
    3.25 +  val trans             : thm           (*transitivity of equals*)
    3.26 +  val add_ac		: thm list      (*AC-rules for the addition operator*)
    3.27 +  val diff_def		: thm		(*Defines x-y as x + -y *)
    3.28 +  val minus_add_distrib	: thm           (* -(x+y) = -x + -y *)        
    3.29 +  val minus_minus	: thm           (* - -x = x *)
    3.30 +  val mult_commute 	: thm		(*commutative law for the product*)
    3.31 +  val mult_1_right 	: thm           (*the law x*1=x *)
    3.32 +  val add_mult_distrib  : thm           (*law w*(x+y) = w*x + w*y *)
    3.33 +  val diff_mult_distrib : thm           (*law w*(x-y) = w*x - w*y *)
    3.34 +  val mult_minus_right  : thm           (*law x * -y = -(x*y) *)
    3.35 +
    3.36 +  val rel_iff_rel_0_rls : thm list      (*e.g. (x < y) = (x-y < 0) *)
    3.37 +  val dest_eqI		: thm -> term   (*to get patterns from the rel rules*)
    3.38 +end;
    3.39 +
    3.40 +
    3.41 +functor Combine_Coeff (Data: COMBINE_COEFF_DATA) =
    3.42 +struct
    3.43 +
    3.44 + local open Data 
    3.45 + in
    3.46 + val rhs_ss = ss addsimps
    3.47 +                    [add_mult_distrib, diff_mult_distrib,
    3.48 +		     mult_minus_right, mult_1_right];
    3.49 +
    3.50 + val lhs_ss = ss addsimps
    3.51 +		 add_ac @
    3.52 +		 [diff_def, minus_add_distrib, minus_minus, mult_commute];
    3.53 + end;
    3.54 +
    3.55 + (*prove while suppressing timing information*)
    3.56 + fun prove name ct tacf = 
    3.57 +     setmp Goals.proof_timing false (prove_goalw_cterm [] ct) tacf
    3.58 +     handle ERROR =>
    3.59 +	 error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
    3.60 +                
    3.61 + val plus = Const ("op +", [Data.T,Data.T] ---> Data.T);
    3.62 + val minus = Const ("op -", [Data.T,Data.T] ---> Data.T);
    3.63 + val uminus = Const ("uminus", Data.T --> Data.T);
    3.64 + val times = Const ("op *", [Data.T,Data.T] ---> Data.T);
    3.65 +
    3.66 + val number_of = Const ("Numeral.number_of", 
    3.67 +			Type ("Numeral.bin", []) --> Data.T);
    3.68 +
    3.69 + val zero = number_of $ HOLogic.pls_const;
    3.70 + val one =  number_of $ (HOLogic.bit_const $ 
    3.71 +			 HOLogic.pls_const $ 
    3.72 +			 HOLogic.true_const);
    3.73 +
    3.74 + (*We map -t to t and (in other cases) t to -t.  No need to check the type of
    3.75 +   uminus, since the simproc is only called on sums of type T.*)
    3.76 + fun negate (Const("uminus",_) $ t) = t
    3.77 +   | negate t                       = uminus $ t;
    3.78 +
    3.79 + fun mk_sum []  = zero
    3.80 +   | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;
    3.81 +
    3.82 + fun attach_coeff (Bound ~1,ns) = mk_sum ns  (*just a literal*)
    3.83 +   | attach_coeff (x,ns) = times $ x $ (mk_sum ns);
    3.84 +
    3.85 + fun add_atom (x, (neg,m)) pairs = 
    3.86 +   let val m' = if neg then negate m else m
    3.87 +   in 
    3.88 +       case gen_assoc (op aconv) (pairs, x) of
    3.89 +	   Some n => gen_overwrite (op aconv) (pairs, (x, m'::n))
    3.90 +	 | None => (x,[m']) :: pairs
    3.91 +   end;
    3.92 +
    3.93 + (**STILL MISSING: a treatment of nested coeffs, e.g. a*(b*3) **)
    3.94 + (*Convert a formula built from +, * and - (binary and unary) to a
    3.95 +   (atom, coeff) association list.  Handles t+t, t-t, -t, a*n, n*a, n, a
    3.96 +   where n denotes a numeric literal and a is any other term.
    3.97 +   No need to check types PROVIDED they are checked upon entry!*)
    3.98 + fun add_terms neg (Const("op +", _) $ x $ y, pairs) =
    3.99 +	 add_terms neg (x, add_terms neg (y, pairs))
   3.100 +   | add_terms neg (Const("op -", _) $ x $ y, pairs) =
   3.101 +	 add_terms neg (x, add_terms (not neg) (y, pairs))
   3.102 +   | add_terms neg (Const("uminus", _) $ x, pairs) = 
   3.103 +	 add_terms (not neg) (x, pairs)
   3.104 +   | add_terms neg (lit as Const("Numeral.number_of", _) $ _, pairs) =
   3.105 +	 (*literal: make it the coefficient of a dummy term*)
   3.106 +	 add_atom (Bound ~1, (neg, lit)) pairs
   3.107 +   | add_terms neg (Const("op *", _) $ x 
   3.108 +		             $ (lit as Const("Numeral.number_of", _) $ _),
   3.109 +		    pairs) =
   3.110 +	 (*coefficient on the right*)
   3.111 +	 add_atom (x, (neg, lit)) pairs
   3.112 +   | add_terms neg (Const("op *", _) 
   3.113 +		             $ (lit as Const("Numeral.number_of", _) $ _)
   3.114 +                             $ x, pairs) =
   3.115 +	 (*coefficient on the left*)
   3.116 +	 add_atom (x, (neg, lit)) pairs
   3.117 +   | add_terms neg (x, pairs) = add_atom (x, (neg, one)) pairs;
   3.118 +
   3.119 + fun terms fml = add_terms false (fml, []);
   3.120 +
   3.121 + exception CC_fail;
   3.122 +
   3.123 + (*The number of terms in t, assuming no collapsing takes place*)
   3.124 + fun term_count (Const("op +", _) $ x $ y) = term_count x + term_count y
   3.125 +   | term_count (Const("op -", _) $ x $ y) = term_count x + term_count y
   3.126 +   | term_count (Const("uminus", _) $ x) = term_count x
   3.127 +   | term_count x = 1;
   3.128 +
   3.129 +
   3.130 + val trace = ref false;
   3.131 +
   3.132 + (*The simproc for sums*)
   3.133 + fun sum_proc sg _ lhs =
   3.134 +   let fun show t = string_of_cterm (Thm.cterm_of sg t)
   3.135 +       val _ = if !trace then writeln 
   3.136 +	                   ("combine_coeff sum simproc: LHS = " ^ show lhs)
   3.137 +	       else ()
   3.138 +       val ts = terms lhs
   3.139 +       val _ = if term_count lhs = length ts 
   3.140 +               then raise CC_fail (*we can't reduce the number of terms*)
   3.141 +               else ()  
   3.142 +       val rhs = mk_sum (map attach_coeff ts)
   3.143 +       val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
   3.144 +       val th = prove "combine_coeff" 
   3.145 +	           (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
   3.146 +		   (fn _ => [rtac Data.eq_reflection 1,
   3.147 +			     simp_tac rhs_ss 1,
   3.148 +			     IF_UNSOLVED (simp_tac lhs_ss 1)])
   3.149 +   in Some th end
   3.150 +   handle CC_fail => None;
   3.151 +
   3.152 + val sum_conv = 
   3.153 +     Simplifier.mk_simproc "combine_coeff_sums"
   3.154 +       (map (Thm.read_cterm (Theory.sign_of Data.thy)) 
   3.155 +	[("x + y", Data.T), ("x - y", Data.T)])
   3.156 +       sum_proc;
   3.157 +
   3.158 +
   3.159 + (*The simproc for relations, which just replaces x<y by x-y<0 and simplifies*)
   3.160 +
   3.161 + val trans_eq_reflection = Data.trans RS Data.eq_reflection |> standard;
   3.162 +
   3.163 + fun rel_proc sg asms (lhs as (rel$lt$rt)) =
   3.164 +   let val _ = if !trace then writeln
   3.165 +                               ("cc_rel simproc: LHS = " ^ 
   3.166 +				string_of_cterm (cterm_of sg lhs))
   3.167 +	       else ()
   3.168 +       val _ = if lt=zero orelse rt=zero then raise CC_fail 
   3.169 +               else ()   (*this simproc can do nothing if either side is zero*)
   3.170 +       val cc_th = the (sum_proc sg asms (minus $ lt $ rt))
   3.171 +                   handle OPTION => raise CC_fail
   3.172 +       val _ = if !trace then 
   3.173 +		 writeln ("cc_th = " ^ string_of_thm cc_th)
   3.174 +	       else ()
   3.175 +       val cc_lr = #2 (Logic.dest_equals (concl_of cc_th))
   3.176 +
   3.177 +       val rhs = rel $ cc_lr $ zero
   3.178 +       val _ = if !trace then 
   3.179 +		 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
   3.180 +	       else ()
   3.181 +       val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
   3.182 +
   3.183 +       val th = prove "cc_rel" ct 
   3.184 +                  (fn _ => [rtac trans_eq_reflection 1,
   3.185 +			    resolve_tac Data.rel_iff_rel_0_rls 1,
   3.186 +			    simp_tac (Data.ss addsimps [cc_th]) 1])
   3.187 +   in Some th end
   3.188 +   handle CC_fail => None;
   3.189 +
   3.190 + val rel_conv = 
   3.191 +     Simplifier.mk_simproc "cc_relations"
   3.192 +       (map (Thm.cterm_of (Theory.sign_of Data.thy) o Data.dest_eqI)
   3.193 +            Data.rel_iff_rel_0_rls)
   3.194 +       rel_proc;
   3.195 +
   3.196 +end;