# HG changeset patch # User haftmann # Date 1660888150 0 # Node ID 24b17460ee60109b43986d610b98d6324a82ec95 # Parent fcd118d9242f8a1343aa2dddeeed50af68c82c7a streamlined simpset building, avoiding duplicated rewrite rules diff -r fcd118d9242f -r 24b17460ee60 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:09 2022 +0000 +++ b/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:10 2022 +0000 @@ -15,7 +15,7 @@ lemmas semiring_norm = Let_def arith_simps diff_nat_numeral rel_simps if_False if_True - add_0 add_Suc add_numeral_left + add_Suc add_numeral_left add_neg_numeral_left mult_numeral_left numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1 eq_numeral_iff_iszero not_iszero_Numeral1 @@ -92,16 +92,16 @@ lemma nat_mult_eq_cancel_disj: fixes k m n :: nat shows "k * m = k * n \ k = 0 \ m = n" - by auto + by (fact mult_cancel_left) -lemma nat_mult_div_cancel_disj [simp]: +lemma nat_mult_div_cancel_disj: fixes k m n :: nat shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)" by (fact div_mult_mult1_if) lemma numeral_times_minus_swap: fixes x:: "'a::comm_ring_1" shows "numeral w * -x = x * - numeral w" - by (simp add: mult.commute) + by (simp add: ac_simps) ML_file \Tools/numeral_simprocs.ML\ diff -r fcd118d9242f -r 24b17460ee60 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Aug 19 05:49:09 2022 +0000 +++ b/src/HOL/Tools/lin_arith.ML Fri Aug 19 05:49:10 2022 +0000 @@ -104,6 +104,15 @@ val neq_limit = Attrib.setup_config_int \<^binding>\linarith_neq_limit\ (K 9); val trace = Attrib.setup_config_bool \<^binding>\linarith_trace\ (K false); +fun nnf_simpset ctxt = + (empty_simpset ctxt + |> Simplifier.set_mkeqTrue mk_eq_True + |> Simplifier.set_mksimps (mksimps mksimps_pairs)) + addsimps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj + de_Morgan_conj not_all not_ex not_not} + +fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt) + structure LA_Data: LIN_ARITH_DATA = struct @@ -764,6 +773,7 @@ result end; + (* takes the i-th subgoal [| A1; ...; An |] ==> B to *) (* An --> ... --> A1 --> B, performs splitting with the given 'split_thms' *) (* (resulting in a different subgoal P), takes P to ~P ==> False, *) @@ -773,16 +783,6 @@ (* general form [| Q1; ...; Qm |] ==> False. Fails if more than *) (* !split_limit splits are possible. *) -local - fun nnf_simpset ctxt = - (empty_simpset ctxt - |> Simplifier.set_mkeqTrue mk_eq_True - |> Simplifier.set_mksimps (mksimps mksimps_pairs)) - addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, - @{thm de_Morgan_conj}, not_all, not_ex, not_not] - fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt) -in - fun split_once_tac ctxt split_thms = let val thy = Proof_Context.theory_of ctxt @@ -813,8 +813,6 @@ ] end; -end; (* local *) - (* remove irrelevant premises, then split the i-th subgoal (and all new *) (* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *) (* subgoals and finally attempt to solve them by finding an immediate *) @@ -897,16 +895,6 @@ where the Ai are atomic, i.e. no top-level &, | or EX *) -local - fun nnf_simpset ctxt = - (empty_simpset ctxt - |> Simplifier.set_mkeqTrue mk_eq_True - |> Simplifier.set_mksimps (mksimps mksimps_pairs)) - addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj}, - @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}]; - fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt); -in - fun refute_tac ctxt test prep_tac ref_tac = let val refute_prems_tac = REPEAT_DETERM @@ -921,8 +909,6 @@ SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; -end; - (* arith proof method *) diff -r fcd118d9242f -r 24b17460ee60 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri Aug 19 05:49:09 2022 +0000 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri Aug 19 05:49:10 2022 +0000 @@ -166,7 +166,7 @@ simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.set_term_ord numterm_ord); (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*) -val numeral_syms = [@{thm numeral_One} RS sym]; +val numeral_syms = @{thms numeral_One [symmetric]}; (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) val add_0s = @{thms add_0_left add_0_right}; @@ -174,57 +174,54 @@ (* For post-simplification of the rhs of simproc-generated rules *) val post_simps = - [@{thm numeral_One}, - @{thm add_0_left}, @{thm add_0_right}, - @{thm mult_zero_left}, @{thm mult_zero_right}, - @{thm mult_1_left}, @{thm mult_1_right}, - @{thm mult_minus1}, @{thm mult_minus1_right}] + @{thms numeral_One + add_0_left add_0_right + mult_zero_left mult_zero_right + mult_1_left mult_1_right + mult_minus1 mult_minus1_right} val field_post_simps = - post_simps @ [@{thm div_0}, @{thm div_by_1}] + post_simps @ @{thms div_0 div_by_1} (*Simplify inverse Numeral1*) -val inverse_1s = [@{thm inverse_numeral_1}]; +val inverse_1s = @{thms inverse_numeral_1} (*To perform binary arithmetic. The "left" rewriting handles patterns created by the Numeral_Simprocs, such as 3 * (5 * x). *) val simps = - [@{thm numeral_One} RS sym] @ - @{thms add_numeral_left} @ - @{thms add_neg_numeral_left} @ - @{thms mult_numeral_left} @ - @{thms arith_simps} @ @{thms rel_simps}; + @{thms numeral_One [symmetric] + add_numeral_left + add_neg_numeral_left + mult_numeral_left + arith_simps rel_simps} (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms during re-arrangement*) val non_add_simps = subtract Thm.eq_thm - (@{thms add_numeral_left} @ - @{thms add_neg_numeral_left} @ - @{thms numeral_plus_numeral} @ - @{thms add_neg_numeral_simps}) simps; - -(*To evaluate binary negations of coefficients*) -val minus_simps = [@{thm minus_zero}, @{thm minus_minus}]; + @{thms add_numeral_left + add_neg_numeral_left + numeral_plus_numeral + add_neg_numeral_simps} simps; (*To let us treat subtraction as addition*) -val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}]; +val diff_simps = @{thms diff_conv_add_uminus minus_add_distrib minus_minus}; (*To let us treat division as multiplication*) -val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; +val divide_simps = @{thms divide_inverse inverse_mult_distrib inverse_inverse_eq}; (*to extract again any uncancelled minuses*) val minus_from_mult_simps = - [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; + @{thms minus_minus mult_minus_left mult_minus_right}; (*combine unary minus with numeric literals, however nested within a product*) val mult_minus_simps = - [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}]; + @{thms mult.assoc minus_mult_right minus_mult_commute numeral_times_minus_swap}; val norm_ss1 = simpset_of (put_simpset num_ss \<^context> addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms ac_simps}) + diff_simps @ @{thms minus_zero ac_simps}) val norm_ss2 = simpset_of (put_simpset num_ss \<^context> @@ -232,7 +229,7 @@ val norm_ss3 = simpset_of (put_simpset num_ss \<^context> - addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute}) + addsimps minus_from_mult_simps @ @{thms ac_simps minus_mult_commute}) structure CancelNumeralsCommon = struct @@ -249,7 +246,7 @@ THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) + simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps @@ -303,7 +300,7 @@ THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) val numeral_simp_ss = - simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) + simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps @@ -326,7 +323,7 @@ val trans_tac = trans_tac val norm_ss1a = - simpset_of (put_simpset norm_ss1 \<^context> addsimps inverse_1s @ divide_simps) + simpset_of (put_simpset norm_ss1 \<^context> addsimps (inverse_1s @ divide_simps)) fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt)) THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) @@ -334,7 +331,7 @@ val numeral_simp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}]) + addsimps (simps @ @{thms add_frac_eq not_False_eq_True})) fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps @@ -386,7 +383,7 @@ fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) val simplify_meta_eq = Arith_Data.simplify_meta_eq - ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps) + (@{thms Nat.add_0 Nat.add_0_right} @ post_simps) val prove_conv = Arith_Data.prove_conv end @@ -588,9 +585,9 @@ val type_tvar = tvar \<^sort>\type\; val geq = cterm_of (Const (\<^const_name>\HOL.eq\, TVar type_tvar --> TVar type_tvar --> \<^typ>\bool\)); -val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} -val add_frac_num = mk_meta_eq @{thm "add_frac_num"} -val add_num_frac = mk_meta_eq @{thm "add_num_frac"} +val add_frac_eq = mk_meta_eq @{thm add_frac_eq} +val add_frac_num = mk_meta_eq @{thm add_frac_num} +val add_num_frac = mk_meta_eq @{thm add_num_frac} fun prove_nz ctxt T t = let @@ -706,35 +703,37 @@ \<^term>\(a::'a::{field, ord}) / b = c\], proc = K proc3} -val ths = - [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_numeral_1"}, - @{thm "div_by_0"}, @{thm div_0}, - @{thm "divide_divide_eq_left"}, - @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_times_eq"}, - @{thm "divide_divide_eq_right"}, - @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"}, - @{thm "add_divide_distrib"} RS sym, - @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, - Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute})))) - (@{thm Fields.field_divide_inverse} RS sym)] - val field_comp_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms "semiring_norm"} - addsimps ths addsimps @{thms simp_thms} + addsimps @{thms semiring_norm + mult_numeral_1 + mult_numeral_1_right + divide_numeral_1 + div_by_0 + div_0 + divide_divide_eq_left + times_divide_eq_left + times_divide_eq_right + times_divide_times_eq + divide_divide_eq_right + diff_conv_add_uminus + minus_divide_left + add_divide_distrib [symmetric] + Fields.field_divide_inverse [symmetric] + inverse_divide + divide_inverse_commute [symmetric] + simp_thms} addsimprocs field_cancel_numeral_factors addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] - |> Simplifier.add_cong @{thm "if_weak_cong"}) + |> Simplifier.add_cong @{thm if_weak_cong}) in fun field_comp_conv ctxt = Simplifier.rewrite (put_simpset field_comp_ss ctxt) then_conv - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}]) + Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}) end