# HG changeset patch
# User paulson
# Date 930127049 -7200
# Node ID da8a393026868b54d56a5848f775b7654388fa36
# Parent  941c4f70db91d63ac57147e991c2222fc42c282e
new distributive laws involving * and -

diff -r 941c4f70db91 -r da8a39302686 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Wed Jun 23 10:36:59 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Wed Jun 23 10:37:29 1999 +0200
@@ -376,6 +376,15 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
+Goalw [zdiff_def] "((z1::int) - z2) * w = (z1 * w) - (z2 * w)";
+by (stac zadd_zmult_distrib 1);
+by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
+qed "zdiff_zmult_distrib";
+
+Goal "(w::int) * (z1 - z2) = (w * z1) - (w * z2)";
+by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
+qed "zdiff_zmult_distrib2";
+
 Goalw [int_def] "int 0 * z = int 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);