1(*  Title:      Provers/Arith/combine_numerals.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   2000  University of Cambridge
4
5Combine coefficients in expressions:
6
7     i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
8
9It works by (a) massaging the sum to bring the selected terms to the front:
10
11     #m*u + (#n*u + (i + (j + k)))
12
13(b) then using left_distrib to reach
14
15     #(m+n)*u + (i + (j + k))
16*)
17
18signature COMBINE_NUMERALS_DATA =
19sig
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: Proof.context -> thm option -> tactic            (*applies the initial lemma*)
33  val norm_tac: Proof.context -> tactic          (*proves the initial lemma*)
34  val numeral_simp_tac: Proof.context -> tactic  (*proves the final theorem*)
35  val simplify_meta_eq: Proof.context -> thm -> thm  (*simplifies the final theorem*)
36end;
37
38
39functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
40  sig
41  val proc: Proof.context -> cterm -> thm option
42  end
43=
44struct
45
46(*Remove the first occurrence of #m*u from the term list*)
47fun 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);
54
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*)
57fun 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);
66
67(*the simplification procedure*)
68fun proc ctxt ct =
69  let
70    val t = Thm.term_of ct
71    val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
72
73    val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
74    val T = Term.fastype_of u
75
76    val reshape =  (*Move i*u to the front and put j*u into standard form
77                       i + #m + j + k == #m + i + (j + k) *)
78      if Data.iszero m orelse Data.iszero n then   (*trivial, so do nothing*)
79        raise TERM("combine_numerals", [])
80      else Data.prove_conv [Data.norm_tac ctxt'] ctxt'
81        (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
82  in
83    Data.prove_conv
84       [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1,
85        Data.numeral_simp_tac ctxt'] ctxt'
86       (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))
87    |> Option.map
88      (Data.simplify_meta_eq ctxt' #>
89        singleton (Variable.export ctxt' ctxt))
90  end
91  (* FIXME avoid handling of generic exceptions *)
92  handle TERM _ => NONE
93       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
94                             Undeclared type constructor "Numeral.bin"*)
95
96end;
97