7072
|
1 |
(* Title: Provers/Arith/assoc_fold.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1999 University of Cambridge
|
|
5 |
|
|
6 |
Simplification procedure for associative operators + and * on numeric types
|
|
7 |
|
|
8 |
Performs constant folding when the literals are separated, as in 3+n+4.
|
|
9 |
*)
|
|
10 |
|
|
11 |
|
|
12 |
signature ASSOC_FOLD_DATA =
|
|
13 |
sig
|
|
14 |
val ss : simpset (*basic simpset of object-logtic*)
|
|
15 |
val eq_reflection : thm (*object-equality to meta-equality*)
|
|
16 |
val thy : theory (*the operator's theory*)
|
|
17 |
val T : typ (*the operator's numeric type*)
|
|
18 |
val plus : term (*the operator being folded*)
|
|
19 |
val add_ac : thm list (*AC-rewrites for plus*)
|
|
20 |
end;
|
|
21 |
|
|
22 |
|
|
23 |
functor Assoc_Fold (Data: ASSOC_FOLD_DATA) =
|
|
24 |
struct
|
|
25 |
|
|
26 |
val assoc_ss = Data.ss addsimps Data.add_ac;
|
|
27 |
|
|
28 |
(*prove while suppressing timing information*)
|
|
29 |
fun prove name ct tacf =
|
8999
|
30 |
setmp Library.timing false (prove_goalw_cterm [] ct) tacf
|
7072
|
31 |
handle ERROR =>
|
|
32 |
error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
|
|
33 |
|
|
34 |
exception Assoc_fail;
|
|
35 |
|
|
36 |
fun mk_sum [] = raise Assoc_fail
|
|
37 |
| mk_sum tms = foldr1 (fn (x,y) => Data.plus $ x $ y) tms;
|
|
38 |
|
|
39 |
(*Separate the literals from the other terms being combined*)
|
|
40 |
fun sift_terms (t, (lits,others)) =
|
|
41 |
case t of
|
|
42 |
Const("Numeral.number_of", _) $ _ =>
|
|
43 |
(t::lits, others) (*new literal*)
|
|
44 |
| (f as Const _) $ x $ y =>
|
|
45 |
if f = Data.plus
|
|
46 |
then sift_terms (x, sift_terms (y, (lits,others)))
|
|
47 |
else (lits, t::others) (*arbitrary summand*)
|
|
48 |
| _ => (lits, t::others);
|
|
49 |
|
|
50 |
val trace = ref false;
|
|
51 |
|
|
52 |
(*Make a simproc to combine all literals in a associative nest*)
|
|
53 |
fun proc sg _ lhs =
|
|
54 |
let fun show t = string_of_cterm (Thm.cterm_of sg t)
|
|
55 |
val _ = if !trace then writeln ("assoc_fold simproc: LHS = " ^ show lhs)
|
|
56 |
else ()
|
|
57 |
val (lits,others) = sift_terms (lhs, ([],[]))
|
|
58 |
val _ = if length lits < 2
|
|
59 |
then raise Assoc_fail (*we can't reduce the number of terms*)
|
|
60 |
else ()
|
|
61 |
val rhs = Data.plus $ mk_sum lits $ mk_sum others
|
|
62 |
val _ = if !trace then writeln ("RHS = " ^ show rhs) else ()
|
|
63 |
val th = prove "assoc_fold"
|
|
64 |
(Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
|
|
65 |
(fn _ => [rtac Data.eq_reflection 1,
|
|
66 |
simp_tac assoc_ss 1])
|
|
67 |
in Some th end
|
|
68 |
handle Assoc_fail => None;
|
|
69 |
|
|
70 |
val conv =
|
8857
|
71 |
Simplifier.mk_simproc "assoc_fold"
|
7072
|
72 |
[Thm.cterm_of (Theory.sign_of Data.thy)
|
|
73 |
(Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
|
|
74 |
proc;
|
|
75 |
|
|
76 |
end;
|
|
77 |
|
|
78 |
|
|
79 |
(*test data:
|
8999
|
80 |
set timing;
|
7072
|
81 |
|
|
82 |
Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)";
|
|
83 |
|
|
84 |
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)";
|
|
85 |
*)
|