author | wenzelm |
Fri, 17 Jun 2005 18:33:03 +0200 | |
changeset 16423 | 24abe4c0e4b4 |
parent 15531 | 08c8dad8e399 |
child 16973 | b2a894562b8f |
permissions | -rw-r--r-- |
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 |
|
13462 | 14 |
val ss : simpset (*basic simpset of object-logtic*) |
15 |
val eq_reflection : thm (*object-equality to meta-equality*) |
|
16423 | 16 |
val thy_ref : theory_ref (*the operator's signature*) |
13462 | 17 |
val add_ac : thm list (*AC-rewrites for plus*) |
7072 | 18 |
end; |
19 |
||
20 |
||
21 |
functor Assoc_Fold (Data: ASSOC_FOLD_DATA) = |
|
22 |
struct |
|
23 |
||
24 |
val assoc_ss = Data.ss addsimps Data.add_ac; |
|
25 |
||
26 |
exception Assoc_fail; |
|
27 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
28 |
fun mk_sum plus [] = raise Assoc_fail |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
29 |
| mk_sum plus tms = foldr1 (fn (x,y) => plus $ x $ y) tms; |
7072 | 30 |
|
31 |
(*Separate the literals from the other terms being combined*) |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
32 |
fun sift_terms plus (t, (lits,others)) = |
7072 | 33 |
case t of |
13462 | 34 |
Const("Numeral.number_of", _) $ _ => |
35 |
(t::lits, others) (*new literal*) |
|
36 |
| (f as Const _) $ x $ y => |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
37 |
if f = plus |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
38 |
then sift_terms plus (x, sift_terms plus (y, (lits,others))) |
13462 | 39 |
else (lits, t::others) (*arbitrary summand*) |
40 |
| _ => (lits, t::others); |
|
7072 | 41 |
|
42 |
val trace = ref false; |
|
43 |
||
44 |
(*Make a simproc to combine all literals in a associative nest*) |
|
16423 | 45 |
fun proc thy _ lhs = |
46 |
let fun show t = string_of_cterm (Thm.cterm_of thy t) |
|
12262 | 47 |
val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs) |
13462 | 48 |
else () |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
49 |
val plus = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
50 |
(case lhs of f $ _ $ _ => f | _ => error "Assoc_fold: bad pattern") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
51 |
val (lits,others) = sift_terms plus (lhs, ([],[])) |
7072 | 52 |
val _ = if length lits < 2 |
53 |
then raise Assoc_fail (*we can't reduce the number of terms*) |
|
13462 | 54 |
else () |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13480
diff
changeset
|
55 |
val rhs = plus $ mk_sum plus lits $ mk_sum plus others |
12262 | 56 |
val _ = if !trace then tracing ("RHS = " ^ show rhs) else () |
16423 | 57 |
val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs)) |
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
58 |
(fn _ => rtac Data.eq_reflection 1 THEN |
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset
|
59 |
simp_tac assoc_ss 1) |
15531 | 60 |
in SOME th end |
61 |
handle Assoc_fail => NONE; |
|
13462 | 62 |
|
7072 | 63 |
end; |
64 |
||
65 |
||
66 |
(*test data: |
|
8999 | 67 |
set timing; |
7072 | 68 |
|
69 |
Goal "(#3 * (a * #34)) * (#2 * b * #9) = (x::int)"; |
|
70 |
||
71 |
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)"; |
|
72 |
*) |