# HG changeset patch # User huffman # Date 1238440079 25200 # Node ID f9e9e800d27e46c631263274cb60c34761013cb2 # Parent 1267011348116a60812709ee0a53f0b535e77273 simplify theorem references diff -r 126701134811 -r f9e9e800d27e src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Mar 30 10:47:41 2009 -0700 +++ b/src/HOL/Int.thy Mon Mar 30 12:07:59 2009 -0700 @@ -1525,6 +1525,17 @@ lemmas zle_int = of_nat_le_iff [where 'a=int] lemmas int_int_eq = of_nat_eq_iff [where 'a=int] +subsection {* Setting up simplification procedures *} + +lemmas int_arith_rules = + neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1 + minus_zero diff_minus left_minus right_minus + mult_zero_left mult_zero_right mult_Bit1 mult_1_right + mult_minus_left mult_minus_right + minus_add_distrib minus_minus mult_assoc + of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult + of_int_0 of_int_1 of_int_add of_int_mult + use "Tools/int_arith.ML" declaration {* K Int_Arith.setup *} diff -r 126701134811 -r f9e9e800d27e src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Mon Mar 30 10:47:41 2009 -0700 +++ b/src/HOL/Tools/int_arith.ML Mon Mar 30 12:07:59 2009 -0700 @@ -26,9 +26,6 @@ val reorient_simproc = Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc); -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; - (** Utilities **) @@ -176,10 +173,12 @@ val num_ss = HOL_ss settermless numtermless; +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) -val add_0s = thms "add_0s"; -val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"]; +val add_0s = @{thms add_0s}; +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; (*Simplify inverse Numeral1, a/Numeral1*) val inverse_1s = [@{thm inverse_numeral_1}]; @@ -208,16 +207,21 @@ (*push the unary minus down: - x * y = x * - y *) val minus_mult_eq_1_to_2 = - [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard; + [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard; (*to extract again any uncancelled minuses*) val minus_from_mult_simps = - [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym]; + [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; (*combine unary minus with numeric literals, however nested within a product*) val mult_minus_simps = [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + diff_simps @ minus_simps @ @{thms add_ac} +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} + structure CancelNumeralsCommon = struct val mk_sum = mk_sum @@ -227,10 +231,6 @@ val find_first_coeff = find_first_coeff [] val trans_tac = K Arith_Data.trans_tac - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms add_ac} - val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps - val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) @@ -310,10 +310,6 @@ val prove_conv = Arith_Data.prove_conv_nohyps val trans_tac = K Arith_Data.trans_tac - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms add_ac} - val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps - val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) @@ -340,12 +336,9 @@ val prove_conv = Arith_Data.prove_conv_nohyps val trans_tac = K Arith_Data.trans_tac - val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac} - val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps - val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} + val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) @@ -516,14 +509,7 @@ val add_rules = simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @ - [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}, - @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus}, - @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}, - @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym, - @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc}, - @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add}, - @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, - @{thm of_int_mult}] + @{thms int_arith_rules} val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]