--- 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;
--- 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 \
--- 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";
--- /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;
--- /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;
--- /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;