author | wenzelm |
Mon, 01 Aug 2005 19:20:26 +0200 | |
changeset 16973 | b2a894562b8f |
parent 15965 | f422f8283491 |
child 17223 | 430edc6b7826 |
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 |
||
14 |
#m*u + (i + j) ~~ #m'*u + (i' + j') |
|
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*) |
16973 | 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 |
8760 | 51 |
end |
52 |
= |
|
8736 | 53 |
struct |
54 |
||
8779 | 55 |
(*For t = #n*u then put u in the table*) |
8760 | 56 |
fun update_by_coeff (tab, t) = |
8779 | 57 |
Termtab.update ((#2 (Data.dest_coeff t), ()), tab); |
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) = |
|
15570 | 62 |
let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2) |
8760 | 63 |
fun seek [] = raise TERM("find_common", []) |
64 |
| seek (t::terms) = |
|
65 |
let val (_,u) = Data.dest_coeff t |
|
15570 | 66 |
in if isSome (Termtab.lookup (tab2, u)) then u |
8760 | 67 |
else seek terms |
68 |
end |
|
69 |
in seek terms1 end; |
|
8736 | 70 |
|
71 |
(*the simplification procedure*) |
|
16973 | 72 |
fun proc thy ss t = |
15027 | 73 |
let |
74 |
val hyps = prems_of_ss ss; |
|
75 |
(*first freeze any Vars in the term to prevent flex-flex problems*) |
|
13484 | 76 |
val (t', xs) = Term.adhoc_freeze_vars t; |
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset
|
77 |
val (t1,t2) = Data.dest_bal t' |
8760 | 78 |
val terms1 = Data.dest_sum t1 |
79 |
and terms2 = Data.dest_sum t2 |
|
80 |
val u = find_common (terms1,terms2) |
|
81 |
val (n1, terms1') = Data.find_first_coeff u terms1 |
|
82 |
and (n2, terms2') = Data.find_first_coeff u terms2 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
83 |
and T = Term.fastype_of u |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
84 |
fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
8779 | 85 |
val reshape = (*Move i*u to the front and put j*u into standard form |
86 |
i + #m + j + k == #m + i + (j + k) *) |
|
8772 | 87 |
if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
88 |
raise TERM("cancel_numerals", []) |
|
16973 | 89 |
else Data.prove_conv [Data.norm_tac ss] thy hyps xs |
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset
|
90 |
(t', |
8772 | 91 |
Data.mk_bal (newshape(n1,terms1'), |
8779 | 92 |
newshape(n2,terms2'))) |
8736 | 93 |
in |
16973 | 94 |
Option.map (Data.simplify_meta_eq ss) |
8799 | 95 |
(if n2<=n1 then |
96 |
Data.prove_conv |
|
16973 | 97 |
[Data.trans_tac ss reshape, rtac Data.bal_add1 1, |
98 |
Data.numeral_simp_tac ss] thy hyps xs |
|
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset
|
99 |
(t', Data.mk_bal (newshape(n1-n2,terms1'), |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
100 |
Data.mk_sum T terms2')) |
8799 | 101 |
else |
102 |
Data.prove_conv |
|
16973 | 103 |
[Data.trans_tac ss reshape, rtac Data.bal_add2 1, |
104 |
Data.numeral_simp_tac ss] thy hyps xs |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
105 |
(t', Data.mk_bal (Data.mk_sum T terms1', |
9191
300bd596d696
now freezes Vars in order to prevent errors in cases like these:
paulson
parents:
8799
diff
changeset
|
106 |
newshape(n2-n1,terms2')))) |
8736 | 107 |
end |
15531 | 108 |
handle TERM _ => NONE |
109 |
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
|
8779 | 110 |
Undeclared type constructor "Numeral.bin"*) |
8736 | 111 |
|
112 |
end; |