src/Provers/Arith/combine_numerals.ML
author wenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 58838 59203adfc33f
parent 51717 9e7d1c139569
child 59498 50b60f501b05
permissions -rw-r--r--
eliminated aliases;
     1 (*  Title:      Provers/Arith/combine_numerals.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2000  University of Cambridge
     4 
     5 Combine coefficients in expressions:
     6 
     7      i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
     8 
     9 It 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 
    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: 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*)
    36 end;
    37 
    38 
    39 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    40   sig
    41   val proc: Proof.context -> term -> thm option
    42   end
    43 =
    44 struct
    45 
    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);
    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*)
    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);
    66 
    67 (*the simplification procedure*)
    68 fun proc ctxt t =
    69   let
    70     val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    71     val export = singleton (Variable.export ctxt' ctxt)
    72     (* FIXME ctxt vs. ctxt' (!?) *)
    73 
    74     val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
    75     val T = Term.fastype_of u
    76 
    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 ctxt] 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 ctxt)
    85       (Data.prove_conv
    86          [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
    87           Data.numeral_simp_tac ctxt] 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"*)
    94 
    95 end;