src/Provers/Arith/cancel_numerals.ML
changeset 8736 0bfd6678a5fa
child 8760 9139453d7033
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Tue Apr 18 15:51:59 2000 +0200
     1.3 @@ -0,0 +1,61 @@
     1.4 +(*  Title:      Provers/Arith/cancel_sums.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2000  University of Cambridge
     1.8 +
     1.9 +Cancel common literals in balanced expressions:
    1.10 +
    1.11 +     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
    1.12 +
    1.13 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
    1.14 +*)
    1.15 +
    1.16 +signature CANCEL_NUMERALS_DATA =
    1.17 +sig
    1.18 +  (*abstract syntax*)
    1.19 +  val mk_numeral: int -> term
    1.20 +  val find_first_numeral: term list -> int * term * term list
    1.21 +  val mk_sum: term list -> term
    1.22 +  val dest_sum: term -> term list
    1.23 +  val mk_bal: term * term -> term
    1.24 +  val dest_bal: term -> term * term
    1.25 +  (*proof tools*)
    1.26 +  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    1.27 +  val subst_tac: term -> tactic
    1.28 +  val all_simp_tac: tactic
    1.29 +end;
    1.30 +
    1.31 +signature CANCEL_NUMERALS =
    1.32 +sig
    1.33 +  val proc: Sign.sg -> thm list -> term -> thm option
    1.34 +end;
    1.35 +
    1.36 +
    1.37 +functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
    1.38 +struct
    1.39 +
    1.40 +(*predicting the outputs of other simprocs given a term of the form
    1.41 +   (i + ... #m + ... j) - #n   *)
    1.42 +fun cancelled m n terms =
    1.43 +    if m = n then (*cancel_sums: sort the terms*)
    1.44 +	sort Term.term_ord terms 
    1.45 +    else          (*inverse_fold: subtract, keeping original term order*)
    1.46 +	Data.mk_numeral (m - n) :: terms;
    1.47 +
    1.48 +(*the simplification procedure*)
    1.49 +fun proc sg _ t =
    1.50 +  let val (t1,t2) = Data.dest_bal t 
    1.51 +      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
    1.52 +      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
    1.53 +      val lit_n = if n1<n2 then lit1 else lit2
    1.54 +      and n     = BasisLibrary.Int.min (n1,n2)
    1.55 +          (*having both the literals and their integer values makes it
    1.56 +            more robust against negative natural number literals*)
    1.57 +  in
    1.58 +      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
    1.59 +	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
    1.60 +			  Data.mk_sum (cancelled n2 n terms2)))
    1.61 +  end
    1.62 +  handle _ => None;
    1.63 +
    1.64 +end;