src/Provers/Arith/cancel_numerals.ML
author paulson
Tue Apr 18 15:51:59 2000 +0200 (2000-04-18)
changeset 8736 0bfd6678a5fa
child 8760 9139453d7033
permissions -rw-r--r--
new simprocs for numerals of type "nat"
paulson@8736
     1
(*  Title:      Provers/Arith/cancel_sums.ML
paulson@8736
     2
    ID:         $Id$
paulson@8736
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8736
     4
    Copyright   2000  University of Cambridge
paulson@8736
     5
paulson@8736
     6
Cancel common literals in balanced expressions:
paulson@8736
     7
paulson@8736
     8
     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
paulson@8736
     9
paulson@8736
    10
where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
paulson@8736
    11
*)
paulson@8736
    12
paulson@8736
    13
signature CANCEL_NUMERALS_DATA =
paulson@8736
    14
sig
paulson@8736
    15
  (*abstract syntax*)
paulson@8736
    16
  val mk_numeral: int -> term
paulson@8736
    17
  val find_first_numeral: term list -> int * term * term list
paulson@8736
    18
  val mk_sum: term list -> term
paulson@8736
    19
  val dest_sum: term -> term list
paulson@8736
    20
  val mk_bal: term * term -> term
paulson@8736
    21
  val dest_bal: term -> term * term
paulson@8736
    22
  (*proof tools*)
paulson@8736
    23
  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
paulson@8736
    24
  val subst_tac: term -> tactic
paulson@8736
    25
  val all_simp_tac: tactic
paulson@8736
    26
end;
paulson@8736
    27
paulson@8736
    28
signature CANCEL_NUMERALS =
paulson@8736
    29
sig
paulson@8736
    30
  val proc: Sign.sg -> thm list -> term -> thm option
paulson@8736
    31
end;
paulson@8736
    32
paulson@8736
    33
paulson@8736
    34
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
paulson@8736
    35
struct
paulson@8736
    36
paulson@8736
    37
(*predicting the outputs of other simprocs given a term of the form
paulson@8736
    38
   (i + ... #m + ... j) - #n   *)
paulson@8736
    39
fun cancelled m n terms =
paulson@8736
    40
    if m = n then (*cancel_sums: sort the terms*)
paulson@8736
    41
	sort Term.term_ord terms 
paulson@8736
    42
    else          (*inverse_fold: subtract, keeping original term order*)
paulson@8736
    43
	Data.mk_numeral (m - n) :: terms;
paulson@8736
    44
paulson@8736
    45
(*the simplification procedure*)
paulson@8736
    46
fun proc sg _ t =
paulson@8736
    47
  let val (t1,t2) = Data.dest_bal t 
paulson@8736
    48
      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
paulson@8736
    49
      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
paulson@8736
    50
      val lit_n = if n1<n2 then lit1 else lit2
paulson@8736
    51
      and n     = BasisLibrary.Int.min (n1,n2)
paulson@8736
    52
          (*having both the literals and their integer values makes it
paulson@8736
    53
            more robust against negative natural number literals*)
paulson@8736
    54
  in
paulson@8736
    55
      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
paulson@8736
    56
	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
paulson@8736
    57
			  Data.mk_sum (cancelled n2 n terms2)))
paulson@8736
    58
  end
paulson@8736
    59
  handle _ => None;
paulson@8736
    60
paulson@8736
    61
end;