author | wenzelm |
Wed, 09 Sep 2015 20:57:21 +0200 | |
changeset 61144 | 5e94dfead1c2 |
parent 59530 | 2a20354c0877 |
child 70315 | 2f9623aa1eeb |
permissions | -rw-r--r-- |
8760 | 1 |
(* Title: Provers/Arith/cancel_numerals.ML |
8736 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 2000 University of Cambridge |
|
4 |
||
8760 | 5 |
Cancel common coefficients in balanced expressions: |
8736 | 6 |
|
8760 | 7 |
i + #m*u + j ~~ i' + #m'*u + j' == #(m-m')*u + i + j ~~ i' + j' |
8736 | 8 |
|
9 |
where ~~ is an appropriate balancing operation (e.g. =, <=, <, -). |
|
8760 | 10 |
|
11 |
It works by (a) massaging both sides to bring the selected term to the front: |
|
12 |
||
17223 | 13 |
#m*u + (i + j) ~~ #m'*u + (i' + j') |
8760 | 14 |
|
15 |
(b) then using bal_add1 or bal_add2 to reach |
|
16 |
||
17 |
#(m-m')*u + i + j ~~ i' + j' (if m'<=m) |
|
18 |
||
19 |
or |
|
20 |
||
21 |
i + j ~~ #(m'-m)*u + i' + j' (otherwise) |
|
8736 | 22 |
*) |
23 |
||
24 |
signature CANCEL_NUMERALS_DATA = |
|
25 |
sig |
|
26 |
(*abstract syntax*) |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13484
diff
changeset
|
27 |
val mk_sum: typ -> term list -> term |
8736 | 28 |
val dest_sum: term -> term list |
29 |
val mk_bal: term * term -> term |
|
30 |
val dest_bal: term -> term * term |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
20114
diff
changeset
|
31 |
val mk_coeff: int * term -> term |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
20114
diff
changeset
|
32 |
val dest_coeff: term -> int * term |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
20114
diff
changeset
|
33 |
val find_first_coeff: term -> term list -> int * term list |
8760 | 34 |
(*rules*) |
35 |
val bal_add1: thm |
|
36 |
val bal_add2: thm |
|
8736 | 37 |
(*proof tools*) |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
38 |
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option |
59530 | 39 |
val trans_tac: Proof.context -> thm option -> tactic (*applies the initial lemma*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
40 |
val norm_tac: Proof.context -> tactic (*proves the initial lemma*) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
41 |
val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
42 |
val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*) |
8736 | 43 |
end; |
44 |
||
42462 | 45 |
signature CANCEL_NUMERALS = |
46 |
sig |
|
61144 | 47 |
val proc: Proof.context -> cterm -> thm option |
42462 | 48 |
end; |
8736 | 49 |
|
42462 | 50 |
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS = |
8736 | 51 |
struct |
52 |
||
8779 | 53 |
(*For t = #n*u then put u in the table*) |
17223 | 54 |
fun update_by_coeff t = |
17412 | 55 |
Termtab.update (#2 (Data.dest_coeff t), ()); |
8760 | 56 |
|
57 |
(*a left-to-right scan of terms1, seeking a term of the form #n*u, where |
|
58 |
#m*u is in terms2 for some m*) |
|
59 |
fun find_common (terms1,terms2) = |
|
17223 | 60 |
let val tab2 = fold update_by_coeff terms2 Termtab.empty |
61 |
fun seek [] = raise TERM("find_common", []) |
|
62 |
| seek (t::terms) = |
|
63 |
let val (_,u) = Data.dest_coeff t |
|
64 |
in if Termtab.defined tab2 u then u else seek terms end |
|
8760 | 65 |
in seek terms1 end; |
8736 | 66 |
|
67 |
(*the simplification procedure*) |
|
61144 | 68 |
fun proc ctxt ct = |
15027 | 69 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
70 |
val prems = Simplifier.prems_of ctxt |
61144 | 71 |
val t = Thm.term_of ct |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
72 |
val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
73 |
val export = singleton (Variable.export ctxt' ctxt) |
54565 | 74 |
(* FIXME ctxt vs. ctxt' (!?) *) |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
75 |
|
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
76 |
val (t1,t2) = Data.dest_bal t' |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
77 |
val terms1 = Data.dest_sum t1 |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
78 |
and terms2 = Data.dest_sum t2 |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
79 |
|
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
80 |
val u = find_common (terms1, terms2) |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
81 |
val (n1, terms1') = Data.find_first_coeff u terms1 |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
82 |
and (n2, terms2') = Data.find_first_coeff u terms2 |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
83 |
and T = Term.fastype_of u |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
84 |
|
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
85 |
fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
86 |
val reshape = (*Move i*u to the front and put j*u into standard form |
17223 | 87 |
i + #m + j + k == #m + i + (j + k) *) |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
88 |
if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
89 |
raise TERM("cancel_numerals", []) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
90 |
else Data.prove_conv [Data.norm_tac ctxt] ctxt prems |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
91 |
(t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2'))) |
8736 | 92 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
93 |
Option.map (export o Data.simplify_meta_eq ctxt) |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
94 |
(if n2 <= n1 then |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
95 |
Data.prove_conv |
59530 | 96 |
[Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
97 |
Data.numeral_simp_tac ctxt] ctxt prems |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
98 |
(t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
99 |
else |
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
100 |
Data.prove_conv |
59530 | 101 |
[Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
44947
diff
changeset
|
102 |
Data.numeral_simp_tac ctxt] ctxt prems |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
103 |
(t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) |
8736 | 104 |
end |
20114
a1bb4bc68ff3
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
wenzelm
parents:
20044
diff
changeset
|
105 |
(* FIXME avoid handling of generic exceptions *) |
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; |