# HG changeset patch
# User paulson
# Date 932744975 -7200
# Node ID b551a5a8966c07bf62e2696699ee11fd889e4861
# Parent  eec20608c791bd46c9bf583a2f70b15b963483d1
new simprocs assoc_fold and combine_coeff

diff -r eec20608c791 -r b551a5a8966c src/HOL/Integ/bin_simprocs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/bin_simprocs.ML	Fri Jul 23 17:49:35 1999 +0200
@@ -0,0 +1,104 @@
+(*  Title:      HOL/Integ/bin_simproc
+    ID:         $Id$
+    Author:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+
+Installation of simprocs that work on numeric literals
+*)
+
+
+(** Combining of literal coefficients in sums of products **)
+
+Goal "(x < y) = (x-y < (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zless_iff_zdiff_zless_0";
+
+Goal "(x = y) = (x-y = (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "eq_iff_zdiff_eq_0";
+
+Goal "(x <= y) = (x-y <= (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zle_iff_zdiff_zle_0";
+
+
+structure Int_CC_Data : COMBINE_COEFF_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val thy	= Bin.thy
+  val T		= Type ("IntDef.int", [])
+
+  val trans		= trans
+  val add_ac		= zadd_ac
+  val diff_def		= zdiff_def
+  val minus_add_distrib	= zminus_zadd_distrib
+  val minus_minus	= zminus_zminus
+  val mult_commute	= zmult_commute
+  val mult_1_right	= zmult_1_right
+  val add_mult_distrib = zadd_zmult_distrib2
+  val diff_mult_distrib = zdiff_zmult_distrib2
+  val mult_minus_right = zmult_zminus_right
+
+  val rel_iff_rel_0_rls = [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
+			   zle_iff_zdiff_zle_0]
+  fun dest_eqI th = 
+      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
+	      (HOLogic.dest_Trueprop (concl_of th)))
+
+end;
+
+structure Int_CC = Combine_Coeff (Int_CC_Data);
+
+Addsimprocs [Int_CC.sum_conv, Int_CC.rel_conv];
+
+
+(** Constant folding for integer plus and times **)
+
+(*We do not need
+    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
+  because cancel_coeffs does the same thing*)
+
+structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val thy    = Bin.thy
+  val T	     = HOLogic.intT
+  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
+  val add_ac = zmult_ac
+end;
+
+structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
+
+Addsimprocs [Int_Times_Assoc.conv];
+
+
+(** The same for the naturals **)
+
+structure Nat_Plus_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val thy    = Bin.thy
+  val T	     = HOLogic.natT
+  val plus   = Const ("op +", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
+  val add_ac = add_ac
+end;
+
+structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
+
+structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val thy    = Bin.thy
+  val T	     = HOLogic.natT
+  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
+  val add_ac = mult_ac
+end;
+
+structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
+
+Addsimprocs [Nat_Plus_Assoc.conv, Nat_Times_Assoc.conv];
+