src/Provers/Arith/cancel_numerals.ML
changeset 8760 9139453d7033
parent 8736 0bfd6678a5fa
child 8772 ebb07113c4f7
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Fri Apr 21 11:29:57 2000 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Fri Apr 21 11:31:03 2000 +0200
     1.3 @@ -1,61 +1,103 @@
     1.4 -(*  Title:      Provers/Arith/cancel_sums.ML
     1.5 +(*  Title:      Provers/Arith/cancel_numerals.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   2000  University of Cambridge
     1.9  
    1.10 -Cancel common literals in balanced expressions:
    1.11 +Cancel common coefficients in balanced expressions:
    1.12  
    1.13 -     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
    1.14 +     i + #m*u + j ~~ i' + #m'*u + j'  ==  #(m-m')*u + i + j ~~ i' + j'
    1.15  
    1.16  where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
    1.17 +
    1.18 +It works by (a) massaging both sides to bring the selected term to the front:
    1.19 +
    1.20 +     #m*u + (i + j) ~~ #m'*u + (i' + j') 
    1.21 +
    1.22 +(b) then using bal_add1 or bal_add2 to reach
    1.23 +
    1.24 +     #(m-m')*u + i + j ~~ i' + j'       (if m'<=m)
    1.25 +
    1.26 +or
    1.27 +
    1.28 +     i + j ~~ #(m'-m)*u + i' + j'       (otherwise)
    1.29  *)
    1.30  
    1.31  signature CANCEL_NUMERALS_DATA =
    1.32  sig
    1.33    (*abstract syntax*)
    1.34 -  val mk_numeral: int -> term
    1.35 -  val find_first_numeral: term list -> int * term * term list
    1.36    val mk_sum: term list -> term
    1.37    val dest_sum: term -> term list
    1.38    val mk_bal: term * term -> term
    1.39    val dest_bal: term -> term * term
    1.40 +  val mk_coeff: int * term -> term
    1.41 +  val dest_coeff: term -> int * term
    1.42 +  val find_first_coeff: term -> term list -> int * term list
    1.43 +  (*rules*)
    1.44 +  val bal_add1: thm
    1.45 +  val bal_add2: thm
    1.46    (*proof tools*)
    1.47    val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
    1.48 -  val subst_tac: term -> tactic
    1.49 -  val all_simp_tac: tactic
    1.50 -end;
    1.51 -
    1.52 -signature CANCEL_NUMERALS =
    1.53 -sig
    1.54 -  val proc: Sign.sg -> thm list -> term -> thm option
    1.55 +  val norm_tac: tactic
    1.56 +  val numeral_simp_tac: tactic
    1.57  end;
    1.58  
    1.59  
    1.60 -functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
    1.61 +functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
    1.62 +  sig
    1.63 +  val proc: Sign.sg -> thm list -> term -> thm option
    1.64 +  end 
    1.65 +=
    1.66  struct
    1.67  
    1.68 -(*predicting the outputs of other simprocs given a term of the form
    1.69 -   (i + ... #m + ... j) - #n   *)
    1.70 -fun cancelled m n terms =
    1.71 -    if m = n then (*cancel_sums: sort the terms*)
    1.72 -	sort Term.term_ord terms 
    1.73 -    else          (*inverse_fold: subtract, keeping original term order*)
    1.74 -	Data.mk_numeral (m - n) :: terms;
    1.75 +fun listof None = []
    1.76 +  | listof (Some x) = [x];
    1.77 +
    1.78 +(*If t = #n*u then put u in the table*)
    1.79 +fun update_by_coeff (tab, t) =
    1.80 +  Termtab.update ((#2 (Data.dest_coeff t), ()), tab)
    1.81 +  handle TERM _ => tab;
    1.82 +
    1.83 +(*a left-to-right scan of terms1, seeking a term of the form #n*u, where
    1.84 +  #m*u is in terms2 for some m*)
    1.85 +fun find_common (terms1,terms2) =
    1.86 +  let val tab2 = foldl update_by_coeff (Termtab.empty, terms2)
    1.87 +      fun seek [] = raise TERM("find_common", []) 
    1.88 +	| seek (t::terms) =
    1.89 +	      let val (_,u) = Data.dest_coeff t 
    1.90 +	      in  if is_some (Termtab.lookup (tab2, u)) then u
    1.91 +		  else seek terms
    1.92 +	      end
    1.93 +	      handle TERM _ => seek terms
    1.94 +  in  seek terms1 end;
    1.95  
    1.96  (*the simplification procedure*)
    1.97  fun proc sg _ t =
    1.98    let val (t1,t2) = Data.dest_bal t 
    1.99 -      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
   1.100 -      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
   1.101 -      val lit_n = if n1<n2 then lit1 else lit2
   1.102 -      and n     = BasisLibrary.Int.min (n1,n2)
   1.103 -          (*having both the literals and their integer values makes it
   1.104 -            more robust against negative natural number literals*)
   1.105 +      val terms1 = Data.dest_sum t1
   1.106 +      and terms2 = Data.dest_sum t2
   1.107 +      val u = find_common (terms1,terms2)
   1.108 +      val (n1, terms1') = Data.find_first_coeff u terms1
   1.109 +      and (n2, terms2') = Data.find_first_coeff u terms2
   1.110 +      fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms)
   1.111 +      val reshapes =  (*Move i*u to the front and put j*u into standard form
   1.112 +		      i + #m + j + k == #m + i + (j + k) *)
   1.113 +	    listof (Data.prove_conv [Data.norm_tac] sg 
   1.114 +		    (t, 
   1.115 +		     Data.mk_bal (newshape(n1,terms1'), 
   1.116 +				  newshape(n2,terms2'))))
   1.117    in
   1.118 -      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
   1.119 -	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
   1.120 -			  Data.mk_sum (cancelled n2 n terms2)))
   1.121 +
   1.122 +      if n2<=n1 then 
   1.123 +	  Data.prove_conv 
   1.124 +	     [rewrite_goals_tac reshapes, rtac Data.bal_add1 1,
   1.125 +	      Data.numeral_simp_tac] sg
   1.126 +	     (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
   1.127 +      else
   1.128 +	  Data.prove_conv 
   1.129 +	     [rewrite_goals_tac reshapes, rtac Data.bal_add2 1,
   1.130 +	      Data.numeral_simp_tac] sg
   1.131 +	     (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))
   1.132    end
   1.133 -  handle _ => None;
   1.134 +  handle TERM _ => None;
   1.135  
   1.136  end;