# HG changeset patch
# User paulson
# Date 931941566 -7200
# Node ID 1833bdd83ebfabdcd3174059ca37570bb21c0147
# Parent  1a28d968c5aaaff8d2c796cac7d3b70fb474bae6
new constant folding rewrites

diff -r 1a28d968c5aa -r 1833bdd83ebf src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Tue Jul 13 13:54:08 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Jul 14 10:39:26 1999 +0200
@@ -278,7 +278,11 @@
 Goal "(w + (#1::int) <= z) = (w<z)";
 by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
 qed "add1_zle_eq";
-Addsimps [add1_zle_eq];
+
+Goal "((#1::int) + w <= z) = (w<z)";
+by (stac zadd_commute 1);
+by (rtac add1_zle_eq 1);
+qed "add1_left_zle_eq";
 
 Goal "neg x = (x < #0)";
 by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
@@ -321,7 +325,8 @@
 (** Equals (=) **)
 
 Goalw [iszero_def]
-  "((number_of x::int) = number_of y) = iszero(number_of (bin_add x (bin_minus y)))"; 
+  "((number_of x::int) = number_of y) = \
+\  iszero (number_of (bin_add x (bin_minus y)))"; 
 by (simp_tac (simpset() addsimps
               (zcompare_rls @ [number_of_add, number_of_minus])) 1); 
 qed "eq_number_of_eq"; 
@@ -427,6 +432,36 @@
 Addsimps bin_arith_extra_simps;
 Addsimps bin_rel_simps;
 
+
+(** Constant folding inside parentheses **)
+
+Goal "number_of v + (number_of w + c) = number_of(bin_add v w) + (c::int)";
+by (stac (zadd_assoc RS sym) 1);
+by (stac number_of_add 1);
+by Auto_tac;
+qed "nested_number_of_add";
+
+Goalw [zdiff_def]
+    "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)";
+by (rtac nested_number_of_add 1);
+qed "nested_diff1_number_of_add";
+
+Goal "number_of v + (c - number_of w) = \
+\    number_of (bin_add v (bin_minus w)) + (c::int)";
+by (stac (diff_number_of_eq RS sym) 1);
+by Auto_tac;
+qed "nested_diff2_number_of_add";
+
+Goal "number_of v * (number_of w * c) = number_of(bin_mult v w) * (c::int)";
+by (stac (zmult_assoc RS sym) 1);
+by (stac number_of_mult 1);
+by Auto_tac;
+qed "nested_number_of_mult";
+Addsimps [nested_number_of_add, nested_diff1_number_of_add,
+	  nested_diff2_number_of_add, nested_number_of_mult]; 
+
+
+
 (*---------------------------------------------------------------------------*)
 (* Linear arithmetic                                                         *)
 (*---------------------------------------------------------------------------*)