--- a/src/HOL/Integ/Bin.ML Wed May 03 18:34:09 2000 +0200
+++ b/src/HOL/Integ/Bin.ML Thu May 04 12:29:00 2000 +0200
@@ -256,15 +256,6 @@
zmult_1, zmult_1_right,
zmult_minus1, zmult_minus1_right];
-(*For specialist use: NOT as default simprules*)
-Goal "#2 * z = (z+z::int)";
-by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
-qed "zmult_2";
-
-Goal "z * #2 = (z+z::int)";
-by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
-qed "zmult_2_right";
-
(*Negation of a coefficient*)
Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
@@ -406,7 +397,12 @@
(*Hide the binary representation of integer constants*)
Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
-(*simplification of arithmetic operations on integer constants*)
+(*Simplification of arithmetic operations on integer constants.
+ Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
+
+val NCons_simps = [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1,
+ NCons_BIT];
+
val bin_arith_extra_simps =
[number_of_add RS sym,
number_of_minus RS sym,
@@ -417,9 +413,7 @@
bin_add_Pls_right, bin_add_Min_right,
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
diff_number_of_eq,
- bin_mult_1, bin_mult_0,
- NCons_Pls_0, NCons_Pls_1,
- NCons_Min_0, NCons_Min_1, NCons_BIT];
+ bin_mult_1, bin_mult_0] @ NCons_simps;
(*For making a minimal simpset, one must include these default simprules
of thy. Also include simp_thms, or at least (~False)=True*)
--- a/src/HOL/Integ/IntArith.ML Wed May 03 18:34:09 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Thu May 04 12:29:00 2000 +0200
@@ -169,6 +169,12 @@
val bin_simps = [number_of_add RS sym, add_number_of_left] @
bin_arith_simps @ bin_rel_simps;
+(*To evaluate binary negations of coefficients*)
+val zminus_simps = NCons_simps @
+ [number_of_minus RS sym,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+
(*To let us treat subtraction as addition*)
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
@@ -204,7 +210,7 @@
val find_first_coeff = find_first_coeff []
val subst_tac = subst_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
- zadd_ac))
+ zminus_simps@zadd_ac))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
bin_simps@zadd_ac@zmult_ac))
@@ -239,16 +245,6 @@
val bal_add2 = le_add_iff2 RS trans
);
-structure DiffCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
- val prove_conv = prove_conv "intdiff_cancel_numerals"
- val mk_bal = HOLogic.mk_binop "op -"
- val dest_bal = HOLogic.dest_bin "op -" HOLogic.intT
- val bal_add1 = diff_add_eq1 RS trans
- val bal_add2 = diff_add_eq2 RS trans
-);
-
-
val cancel_numerals =
map prep_simproc
[("inteq_cancel_numerals",
@@ -265,12 +261,7 @@
prep_pats ["(l::int) + m <= n", "(l::int) <= m + n",
"(l::int) - m <= n", "(l::int) <= m - n",
"(l::int) * m <= n", "(l::int) <= m * n"],
- LeCancelNumerals.proc),
- ("intdiff_cancel_numerals",
- prep_pats ["((l::int) + m) - n", "(l::int) - (m + n)",
- "((l::int) - m) - n", "(l::int) - (m - n)",
- "(l::int) * m - n", "(l::int) - m * n"],
- DiffCancelNumerals.proc)];
+ LeCancelNumerals.proc)];
structure CombineNumeralsData =
@@ -284,7 +275,7 @@
val subst_tac = subst_tac
val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
- zadd_ac))
+ zminus_simps@zadd_ac))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
bin_simps@zadd_ac@zmult_ac))
@@ -296,8 +287,7 @@
val combine_numerals =
prep_simproc ("int_combine_numerals",
- prep_pats ["(i::int) + (j+k)", "(i::int) + (j*k)",
- "(j+k) + (i::int)", "(j*k) + (i::int)"],
+ prep_pats ["(i::int) + j", "(i::int) - j"],
CombineNumerals.proc);
end;
--- a/src/HOL/Integ/IntDiv.ML Wed May 03 18:34:09 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Thu May 04 12:29:00 2000 +0200
@@ -94,7 +94,7 @@
(*Proving posDivAlg's termination condition*)
val [tc] = posDivAlg.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by (auto_tac (claset(), simpset() addsimps [zmult_2]));
+by Auto_tac;
val lemma = result();
(* removing the termination condition from the generated theorems *)
@@ -135,7 +135,7 @@
(*Proving negDivAlg's termination condition*)
val [tc] = negDivAlg.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by (auto_tac (claset(), simpset() addsimps [zmult_2]));
+by Auto_tac;
val lemma = result();
(* removing the termination condition from the generated theorems *)
@@ -814,7 +814,7 @@
div_pos_pos_trivial]) 1);
by (stac div_pos_pos_trivial 1);
by (asm_simp_tac (simpset()
- addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
+ addsimps zadd_ac@ [mod_pos_pos_trivial,
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
@@ -851,7 +851,7 @@
addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
- addsimps [zmult_2 RS sym, zdiv_zmult_zmult1,
+ addsimps [zdiv_zmult_zmult1,
pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
qed "zdiv_number_of_BIT";
@@ -876,7 +876,7 @@
mod_pos_pos_trivial]) 1);
by (rtac mod_pos_pos_trivial 1);
by (asm_simp_tac (simpset()
- addsimps zadd_ac@ [zmult_2_right, mod_pos_pos_trivial,
+ addsimps zadd_ac@ [mod_pos_pos_trivial,
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
@@ -912,7 +912,7 @@
addsimps [zadd_assoc, number_of_BIT]) 1);
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
- addsimps [zmult_2 RS sym, zmod_zmult_zmult1,
+ addsimps [zmod_zmult_zmult1,
pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);
qed "zmod_number_of_BIT";
--- a/src/HOL/Integ/NatSimprocs.ML Wed May 03 18:34:09 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Thu May 04 12:29:00 2000 +0200
@@ -267,9 +267,7 @@
val combine_numerals =
prep_simproc ("nat_combine_numerals",
- prep_pats ["(i::nat) + (j+k)", "(i::nat) + (j*k)",
- "(j+k) + (i::nat)", "(j*k) + (i::nat)",
- "Suc (i + j)"],
+ prep_pats ["(i::nat) + j", "Suc (i + j)"],
CombineNumerals.proc);
end;
@@ -285,6 +283,7 @@
fun test s = (Goal s; by (Simp_tac 1));
(*cancel_numerals*)
+test "l +( #2) + (#2) + #2 + (l + #2) + (oo + #2) = (uu::nat)";
test "(#2*length xs < #2*length xs + j)";
test "(#2*length xs < length xs * #2 + j)";
test "#2*u = (u::nat)";