author | wenzelm |
Thu, 01 Sep 2005 22:15:10 +0200 | |
changeset 17223 | 430edc6b7826 |
parent 16973 | b2a894562b8f |
child 17412 | e26cb20ef0cc |
permissions | -rw-r--r-- |
8760 | 1 |
(* Title: Provers/Arith/cancel_numerals.ML |
8736 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 2000 University of Cambridge |
|
5 |
||
8760 | 6 |
Cancel common coefficients in balanced expressions: |
8736 | 7 |
|
8760 | 8 |
i + #m*u + j ~~ i' + #m'*u + j' == #(m-m')*u + i + j ~~ i' + j' |
8736 | 9 |
|
10 |
where ~~ is an appropriate balancing operation (e.g. =, <=, <, -). |
|
8760 | 11 |
|
12 |
It works by (a) massaging both sides to bring the selected term to the front: |
|
13 |
||
17223 | 14 |
#m*u + (i + j) ~~ #m'*u + (i' + j') |
8760 | 15 |
|
16 |
(b) then using bal_add1 or bal_add2 to reach |
|
17 |
||
18 |
#(m-m')*u + i + j ~~ i' + j' (if m'<=m) |
|
19 |
||
20 |
or |
|
21 |
||
22 |
i + j ~~ #(m'-m)*u + i' + j' (otherwise) |
|
8736 | 23 |
*) |
24 |
||
25 |
signature CANCEL_NUMERALS_DATA = |
|
26 |
sig |
|
27 |
(*abstract syntax*) |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
28 |
val mk_sum: typ -> term list -> term |
8736 | 29 |
val dest_sum: term -> term list |
30 |
val mk_bal: term * term -> term |
|
31 |
val dest_bal: term -> term * term |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
32 |
val mk_coeff: IntInf.int * term -> term |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
33 |
val dest_coeff: term -> IntInf.int * term |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
34 |
val find_first_coeff: term -> term list -> IntInf.int * term list |
8760 | 35 |
(*rules*) |
36 |
val bal_add1: thm |
|
37 |
val bal_add2: thm |
|
8736 | 38 |
(*proof tools*) |
17223 | 39 |
val prove_conv: tactic list -> theory -> |
13484 | 40 |
thm list -> string list -> term * term -> thm option |
16973 | 41 |
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
42 |
val norm_tac: simpset -> tactic (*proves the initial lemma*) |
|
43 |
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
|
44 |
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
|
8736 | 45 |
end; |
46 |
||
47 |
||
8760 | 48 |
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): |
49 |
sig |
|
16973 | 50 |
val proc: theory -> simpset -> term -> thm option |
17223 | 51 |
end |
8760 | 52 |
= |
8736 | 53 |
struct |
54 |
||
8779 | 55 |
(*For t = #n*u then put u in the table*) |
17223 | 56 |
fun update_by_coeff t = |
57 |
Termtab.curried_update (#2 (Data.dest_coeff t), ()); |
|
8760 | 58 |
|
59 |
(*a left-to-right scan of terms1, seeking a term of the form #n*u, where |
|
60 |
#m*u is in terms2 for some m*) |
|
61 |
fun find_common (terms1,terms2) = |
|
17223 | 62 |
let val tab2 = fold update_by_coeff terms2 Termtab.empty |
63 |
fun seek [] = raise TERM("find_common", []) |
|
64 |
| seek (t::terms) = |
|
65 |
let val (_,u) = Data.dest_coeff t |
|
66 |
in if Termtab.defined tab2 u then u else seek terms end |
|
8760 | 67 |
in seek terms1 end; |
8736 | 68 |
|
69 |
(*the simplification procedure*) |
|
16973 | 70 |
fun proc thy ss t = |
15027 | 71 |
let |
72 |
val hyps = prems_of_ss ss; |
|
73 |
(*first freeze any Vars in the term to prevent flex-flex problems*) |
|
13484 | 74 |
val (t', xs) = Term.adhoc_freeze_vars t; |
17223 | 75 |
val (t1,t2) = Data.dest_bal t' |
8760 | 76 |
val terms1 = Data.dest_sum t1 |
77 |
and terms2 = Data.dest_sum t2 |
|
78 |
val u = find_common (terms1,terms2) |
|
79 |
val (n1, terms1') = Data.find_first_coeff u terms1 |
|
80 |
and (n2, terms2') = Data.find_first_coeff u terms2 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
81 |
and T = Term.fastype_of u |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
82 |
fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
8779 | 83 |
val reshape = (*Move i*u to the front and put j*u into standard form |
17223 | 84 |
i + #m + j + k == #m + i + (j + k) *) |
85 |
if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
|
86 |
raise TERM("cancel_numerals", []) |
|
87 |
else Data.prove_conv [Data.norm_tac ss] thy hyps xs |
|
88 |
(t', |
|
89 |
Data.mk_bal (newshape(n1,terms1'), |
|
90 |
newshape(n2,terms2'))) |
|
8736 | 91 |
in |
16973 | 92 |
Option.map (Data.simplify_meta_eq ss) |
17223 | 93 |
(if n2<=n1 then |
94 |
Data.prove_conv |
|
95 |
[Data.trans_tac ss reshape, rtac Data.bal_add1 1, |
|
96 |
Data.numeral_simp_tac ss] thy hyps xs |
|
97 |
(t', Data.mk_bal (newshape(n1-n2,terms1'), |
|
98 |
Data.mk_sum T terms2')) |
|
99 |
else |
|
100 |
Data.prove_conv |
|
101 |
[Data.trans_tac ss reshape, rtac Data.bal_add2 1, |
|
102 |
Data.numeral_simp_tac ss] thy hyps xs |
|
103 |
(t', Data.mk_bal (Data.mk_sum T terms1', |
|
104 |
newshape(n2-n1,terms2')))) |
|
8736 | 105 |
end |
15531 | 106 |
handle TERM _ => NONE |
107 |
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
|
17223 | 108 |
Undeclared type constructor "Numeral.bin"*) |
8736 | 109 |
|
110 |
end; |