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;