# HG changeset patch # User paulson # Date 957436140 -7200 # Node ID 9aeca9a34cf4175ef6fbfe6b84e25e26a8f34606 # Parent 2f3412cd1b687193121b378b396b22267c24159a further tidying of integer simprocs diff -r 2f3412cd1b68 -r 9aeca9a34cf4 src/HOL/Integ/Bin.ML --- 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*) diff -r 2f3412cd1b68 -r 9aeca9a34cf4 src/HOL/Integ/IntArith.ML --- 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; diff -r 2f3412cd1b68 -r 9aeca9a34cf4 src/HOL/Integ/IntDiv.ML --- 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"; diff -r 2f3412cd1b68 -r 9aeca9a34cf4 src/HOL/Integ/NatSimprocs.ML --- 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)";