# HG changeset patch
# User paulson
# Date 956065919 -7200
# Node ID 0bfd6678a5fa6a880ef16bec0e8522cb1bf1281a
# Parent  bb2250ac955767e26412c44e318f518c8e1700b0
new simprocs for numerals of type "nat"

diff -r bb2250ac9557 -r 0bfd6678a5fa NEWS
--- a/NEWS	Tue Apr 18 14:57:18 2000 +0200
+++ b/NEWS	Tue Apr 18 15:51:59 2000 +0200
@@ -110,6 +110,9 @@
 basically a generalized version of de-Bruijn representation; very
 useful in avoiding lifting all operations;
 
+* greatly improved simplification involving numerals of type "nat", e.g. in
+   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k;
+
 * new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
diff -r bb2250ac9557 -r 0bfd6678a5fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Apr 18 14:57:18 2000 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 18 15:51:59 2000 +0200
@@ -35,6 +35,9 @@
   $(SRC)/Provers/Arith/cancel_sums.ML		\
   $(SRC)/Provers/Arith/assoc_fold.ML		\
   $(SRC)/Provers/Arith/combine_coeff.ML		\
+  $(SRC)/Provers/Arith/inverse_fold.ML		\
+  $(SRC)/Provers/Arith/fold_Suc.ML		\
+  $(SRC)/Provers/Arith/cancel_numerals.ML		\
   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
diff -r bb2250ac9557 -r 0bfd6678a5fa src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Apr 18 14:57:18 2000 +0200
+++ b/src/HOL/ROOT.ML	Tue Apr 18 15:51:59 2000 +0200
@@ -31,6 +31,9 @@
 use "~~/src/Provers/Arith/assoc_fold.ML";
 use "~~/src/Provers/quantifier1.ML";
 use "~~/src/Provers/Arith/combine_coeff.ML";
+use "~~/src/Provers/Arith/inverse_fold.ML";
+use "~~/src/Provers/Arith/cancel_numerals.ML";
+use "~~/src/Provers/Arith/fold_Suc.ML";
 
 with_path "Integ" use_thy "Main";
 
diff -r bb2250ac9557 -r 0bfd6678a5fa src/Provers/Arith/cancel_numerals.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/cancel_numerals.ML	Tue Apr 18 15:51:59 2000 +0200
@@ -0,0 +1,61 @@
+(*  Title:      Provers/Arith/cancel_sums.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Cancel common literals in balanced expressions:
+
+     i + #m + j ~~ i' + #m' + j'  ==  #(m-m') + i + j ~~ i' + j'
+
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, -).
+*)
+
+signature CANCEL_NUMERALS_DATA =
+sig
+  (*abstract syntax*)
+  val mk_numeral: int -> term
+  val find_first_numeral: term list -> int * term * term list
+  val mk_sum: term list -> term
+  val dest_sum: term -> term list
+  val mk_bal: term * term -> term
+  val dest_bal: term -> term * term
+  (*proof tools*)
+  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val subst_tac: term -> tactic
+  val all_simp_tac: tactic
+end;
+
+signature CANCEL_NUMERALS =
+sig
+  val proc: Sign.sg -> thm list -> term -> thm option
+end;
+
+
+functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
+struct
+
+(*predicting the outputs of other simprocs given a term of the form
+   (i + ... #m + ... j) - #n   *)
+fun cancelled m n terms =
+    if m = n then (*cancel_sums: sort the terms*)
+	sort Term.term_ord terms 
+    else          (*inverse_fold: subtract, keeping original term order*)
+	Data.mk_numeral (m - n) :: terms;
+
+(*the simplification procedure*)
+fun proc sg _ t =
+  let val (t1,t2) = Data.dest_bal t 
+      val (n1, lit1, terms1) = Data.find_first_numeral (Data.dest_sum t1)
+      and (n2, lit2, terms2) = Data.find_first_numeral (Data.dest_sum t2)
+      val lit_n = if n1<n2 then lit1 else lit2
+      and n     = BasisLibrary.Int.min (n1,n2)
+          (*having both the literals and their integer values makes it
+            more robust against negative natural number literals*)
+  in
+      Data.prove_conv [Data.subst_tac lit_n, Data.all_simp_tac] sg
+	 (t, Data.mk_bal (Data.mk_sum (cancelled n1 n terms1),
+			  Data.mk_sum (cancelled n2 n terms2)))
+  end
+  handle _ => None;
+
+end;
diff -r bb2250ac9557 -r 0bfd6678a5fa src/Provers/Arith/fold_Suc.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/fold_Suc.ML	Tue Apr 18 15:51:59 2000 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Provers/Arith/fold_Suc.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Simplifies  Suc (i + ... #m + ... j) == #(m+1) + i + ... j
+*)
+
+
+signature FOLD_SUC_DATA =
+sig
+  (*abstract syntax*)
+  val mk_numeral: int -> term
+  val find_first_numeral: term list -> int * term * term list
+  val mk_sum: term list -> term
+  val dest_sum: term -> term list
+  val dest_Suc: term -> term
+  (*proof tools*)
+  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val add_norm_tac: tactic
+  val numeral_simp_tac: thm list -> tactic
+end;
+
+
+functor FoldSucFun(Data: FOLD_SUC_DATA):
+		sig
+		  val proc: Sign.sg -> thm list -> term -> thm option
+		end
+=
+struct
+
+fun proc sg _ t =
+  let val sum = Data.dest_Suc t 
+      val terms = Data.dest_sum sum
+      val (m, lit_m, terms') = Data.find_first_numeral terms
+      val assocs =  (*If needed, rewrite the literal m to the front:
+		     i + #m + j + k == #m + i + (j + k) *)
+	  [the (Data.prove_conv [Data.add_norm_tac] sg
+		(sum, Data.mk_sum (lit_m::terms')))]
+	  handle _ => []
+  in
+      Data.prove_conv 
+        [Data.numeral_simp_tac assocs] sg
+	(t, Data.mk_sum (Data.mk_numeral (m+1) :: terms'))
+  end
+  handle _ => None;
+
+end;
diff -r bb2250ac9557 -r 0bfd6678a5fa src/Provers/Arith/inverse_fold.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/Arith/inverse_fold.ML	Tue Apr 18 15:51:59 2000 +0200
@@ -0,0 +1,65 @@
+(*  Title:      Provers/Arith/inverse_fold.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+For things like  (i + #m + j) - #n   == #(m-n) + i + j    (n<m)
+                                     == i + j - #(n-m)    (m<n)
+
+and maybe        (i * #m * j) div #n == #(m div n) * i * j   (n divides m)
+
+This simproc is needed for cancel_numerals.ML
+*)
+
+
+signature INVERSE_FOLD_DATA =
+sig
+  (*abstract syntax*)
+  val mk_numeral: int -> term
+  val dest_numeral: term -> int
+  val find_first_numeral: term list -> int * term * term list
+  val mk_sum: term list -> term
+  val dest_sum: term -> term list
+  val mk_diff: term * term -> term
+  val dest_diff: term -> term * term
+  (*rules*)
+  val double_diff_eq: thm
+  val move_diff_eq: thm
+  (*proof tools*)
+  val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val add_norm_tac: tactic
+  val numeral_simp_tac: thm list -> tactic
+end;
+
+
+functor InverseFoldFun(Data: INVERSE_FOLD_DATA): 
+		sig
+		  val proc: Sign.sg -> thm list -> term -> thm option
+		end
+=
+struct
+
+fun proc sg _ t =
+  let val (sum,lit_n) = Data.dest_diff t 
+      val terms = Data.dest_sum sum
+      val (m, lit_m, terms') = Data.find_first_numeral terms
+      val n = Data.dest_numeral lit_n
+      and sum' = Data.mk_sum terms'
+      val assocs =  (*If needed, rewrite the literal m to the front:
+		      i + #m + j + k == #m + i + (j + k) *)
+	    [the (Data.prove_conv [Data.add_norm_tac] sg 
+		  (sum, Data.mk_sum [lit_m, sum']))]
+            handle _ => []
+  in
+      if m < n then
+	    Data.prove_conv 
+	     [Data.numeral_simp_tac (Data.double_diff_eq::assocs)] sg
+	     (t, Data.mk_diff (sum', Data.mk_numeral (n-m)))
+      else (*n < m, since equality would have been cancelled*)
+	    Data.prove_conv 
+	     [Data.numeral_simp_tac (Data.move_diff_eq::assocs)] sg
+	     (t, Data.mk_sum [Data.mk_numeral (m-n), sum'])
+  end
+  handle _ => None;
+
+end;