--- a/src/HOL/Complex/ComplexBin.ML Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Complex/ComplexBin.ML Tue Jul 22 11:03:42 2003 +0200
@@ -264,6 +264,11 @@
minus_complex_number_of, diff_complex_number_of, mult_complex_number_of,
complex_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+ during re-arrangement*)
+val non_add_bin_simps =
+ bin_simps \\ [complex_add_number_of_left, add_complex_number_of];
+
(*To evaluate binary negations of coefficients*)
val complex_minus_simps = NCons_simps @
[complex_minus_1_eq_m1,minus_complex_number_of,
@@ -309,7 +314,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
complex_minus_simps@complex_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
complex_add_ac@complex_mult_ac))
@@ -349,7 +354,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
complex_minus_simps@complex_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@complex_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps@
complex_add_ac@complex_mult_ac))
val numeral_simp_tac = ALLGOALS
--- a/src/HOL/Complex/NSComplexBin.ML Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Complex/NSComplexBin.ML Tue Jul 22 11:03:42 2003 +0200
@@ -296,6 +296,11 @@
minus_hcomplex_number_of, diff_hcomplex_number_of, mult_hcomplex_number_of,
hcomplex_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+ during re-arrangement*)
+val non_add_bin_simps =
+ bin_simps \\ [hcomplex_add_number_of_left, add_hcomplex_number_of];
+
(*To evaluate binary negations of coefficients*)
val hcomplex_minus_simps = NCons_simps @
[hcomplex_minus_1_eq_m1,minus_hcomplex_number_of,
@@ -342,7 +347,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hcomplex_minus_simps@hcomplex_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
hcomplex_add_ac@hcomplex_mult_ac))
@@ -382,7 +387,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hcomplex_minus_simps@hcomplex_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hcomplex_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps@
hcomplex_add_ac@hcomplex_mult_ac))
val numeral_simp_tac = ALLGOALS
--- a/src/HOL/Hyperreal/HyperBin.ML Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Tue Jul 22 11:03:42 2003 +0200
@@ -328,6 +328,11 @@
diff_hypreal_number_of, mult_hypreal_number_of,
hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+ during re-arrangement*)
+val non_add_bin_simps =
+ bin_simps \\ [hypreal_add_number_of_left, add_hypreal_number_of];
+
(*To evaluate binary negations of coefficients*)
val hypreal_minus_simps = NCons_simps @
[hypreal_minus_1_eq_m1, minus_hypreal_number_of,
@@ -372,7 +377,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hypreal_minus_simps@hypreal_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
hypreal_add_ac@hypreal_mult_ac))
@@ -440,7 +445,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hypreal_minus_simps@hypreal_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
hypreal_add_ac@hypreal_mult_ac))
val numeral_simp_tac = ALLGOALS
--- a/src/HOL/Real/RealBin.ML Mon Jul 21 17:27:23 2003 +0200
+++ b/src/HOL/Real/RealBin.ML Tue Jul 22 11:03:42 2003 +0200
@@ -349,6 +349,11 @@
diff_real_number_of, mult_real_number_of, real_mult_number_of_left] @
bin_arith_simps @ bin_rel_simps;
+(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
+ during re-arrangement*)
+val non_add_bin_simps =
+ bin_simps \\ [real_add_number_of_left, add_real_number_of];
+
(*To evaluate binary negations of coefficients*)
val real_minus_simps = NCons_simps @
[real_minus_1_eq_m1, minus_real_number_of,
@@ -396,7 +401,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
real_minus_simps@real_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
real_add_ac@real_mult_ac))
@@ -464,7 +469,7 @@
val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@real_minus_simps@real_add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@real_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
real_add_ac@real_mult_ac))
val numeral_simp_tac = ALLGOALS