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.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.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;
```