src/Provers/Arith/combine_numerals.ML
author paulson
Fri Jun 16 13:13:55 2000 +0200 (2000-06-16)
changeset 9073 40d8dfac96b8
parent 8816 31b4fb3d8d60
child 9191 300bd596d696
permissions -rw-r--r--
tracing flag for arith_tac
     1 (*  Title:      Provers/Arith/combine_numerals.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     5 
     6 Combine coefficients in expressions:
     7 
     8      i + #m*u + j ... + #n*u + k  ==  #(m+n)*u + (i + (j + k))
     9 
    10 It works by (a) massaging the sum to bring the selected terms to the front:
    11 
    12      #m*u + (#n*u + (i + (j + k)))
    13 
    14 (b) then using left_distrib to reach
    15 
    16      #(m+n)*u + (i + (j + k))
    17 *)
    18 
    19 signature COMBINE_NUMERALS_DATA =
    20 sig
    21   (*abstract syntax*)
    22   val mk_sum: term list -> term
    23   val dest_sum: term -> term list
    24   val mk_coeff: int * term -> term
    25   val dest_coeff: term -> int * term
    26   (*rules*)
    27   val left_distrib: thm
    28   (*proof tools*)
    29   val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    30   val trans_tac: thm option -> tactic (*applies the initial lemma*)
    31   val norm_tac: tactic                (*proves the initial lemma*)
    32   val numeral_simp_tac: tactic        (*proves the final theorem*)
    33   val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
    34 end;
    35 
    36 
    37 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    38   sig
    39   val proc: Sign.sg -> thm list -> term -> thm option
    40   end 
    41 =
    42 struct
    43 
    44 (*Remove the first occurrence of #m*u from the term list*)
    45 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
    46       raise TERM("combine_numerals: remove", [])  
    47   | remove (m, u, t::terms) =
    48       let val (n,v) = Data.dest_coeff t 
    49       in  if m=n andalso u aconv v then terms
    50           else t :: remove (m, u, terms)
    51       end;
    52 
    53 (*a left-to-right scan of terms, seeking another term of the form #n*u, where
    54   #m*u is already in terms for some m*)
    55 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
    56   | find_repeated (tab, past, t::terms) =
    57       let val (n,u) = Data.dest_coeff t 
    58       in  
    59 	  case Termtab.lookup (tab, u) of
    60 	      Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
    61 	    | None => find_repeated (Termtab.update ((u,n), tab), 
    62 				     t::past,  terms)
    63       end;
    64 
    65 (*the simplification procedure*)
    66 fun proc sg _ t =
    67   let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t)
    68       val reshape =  (*Move i*u to the front and put j*u into standard form
    69 		       i + #m + j + k == #m + i + (j + k) *)
    70 	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
    71 		raise TERM("combine_numerals", []) 
    72 	    else Data.prove_conv [Data.norm_tac] sg 
    73 			(t, 
    74 			 Data.mk_sum ([Data.mk_coeff(m,u),
    75 				       Data.mk_coeff(n,u)] @ terms))
    76   in
    77       apsome Data.simplify_meta_eq
    78 	 (Data.prove_conv 
    79 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
    80 	     Data.numeral_simp_tac] sg
    81 	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
    82   end
    83   handle TERM _ => None
    84        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
    85 			     Undeclared type constructor "Numeral.bin"*)
    86 
    87 end;