src/Provers/Arith/combine_numerals.ML
 author haftmann Sat Sep 17 15:08:55 2011 +0200 (2011-09-17) changeset 44947 8ae418dfe561 parent 35762 af3ff2ba4c54 child 51717 9e7d1c139569 permissions -rw-r--r--
dropped unused argument – avoids problem with SML/NJ
1 (*  Title:      Provers/Arith/combine_numerals.ML
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   2000  University of Cambridge
5 Combine coefficients in expressions:
7      i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
9 It works by (a) massaging the sum to bring the selected terms to the front:
11      #m*u + (#n*u + (i + (j + k)))
13 (b) then using left_distrib to reach
15      #(m+n)*u + (i + (j + k))
16 *)
18 signature COMBINE_NUMERALS_DATA =
19 sig
20   (*abstract syntax*)
21   eqtype coeff
22   val iszero: coeff -> bool
23   val add: coeff * coeff -> coeff     (*addition (or multiplication) *)
24   val mk_sum: typ -> term list -> term
25   val dest_sum: term -> term list
26   val mk_coeff: coeff * term -> term
27   val dest_coeff: term -> coeff * term
28   (*rules*)
29   val left_distrib: thm
30   (*proof tools*)
31   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
32   val trans_tac: thm option -> tactic            (*applies the initial lemma*)
33   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
34   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
35   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
36 end;
39 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
40   sig
41   val proc: simpset -> term -> thm option
42   end
43 =
44 struct
46 (*Remove the first occurrence of #m*u from the term list*)
47 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
48       raise TERM("combine_numerals: remove", [])
49   | remove (m, u, t::terms) =
50       case try Data.dest_coeff t of
51           SOME(n,v) => if m=n andalso u aconv v then terms
52                        else t :: remove (m, u, terms)
53         | NONE      =>  t :: remove (m, u, terms);
55 (*a left-to-right scan of terms, seeking another term of the form #n*u, where
56   #m*u is already in terms for some m*)
57 fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
58   | find_repeated (tab, past, t::terms) =
59       case try Data.dest_coeff t of
60           SOME(n,u) =>
61               (case Termtab.lookup tab u of
62                   SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
63                 | NONE => find_repeated (Termtab.update (u, n) tab,
64                                          t::past,  terms))
65         | NONE => find_repeated (tab, t::past, terms);
67 (*the simplification procedure*)
68 fun proc ss t =
69   let
70     val ctxt = Simplifier.the_context ss;
71     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
72     val export = singleton (Variable.export ctxt' ctxt)
74     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
75     val T = Term.fastype_of u
77     val reshape =  (*Move i*u to the front and put j*u into standard form
78                        i + #m + j + k == #m + i + (j + k) *)
79       if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
80         raise TERM("combine_numerals", [])
81       else Data.prove_conv [Data.norm_tac ss] ctxt
82         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
83   in
84     Option.map (export o Data.simplify_meta_eq ss)
85       (Data.prove_conv
86          [Data.trans_tac reshape, rtac Data.left_distrib 1,
87           Data.numeral_simp_tac ss] ctxt
88          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
89   end
90   (* FIXME avoid handling of generic exceptions *)
91   handle TERM _ => NONE
92        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
93                              Undeclared type constructor "Numeral.bin"*)
95 end;