--- 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 \<longleftrightarrow> k = 0 \<or> 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 \<open>Tools/numeral_simprocs.ML\<close>
--- 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>\<open>linarith_neq_limit\<close> (K 9);
val trace = Attrib.setup_config_bool \<^binding>\<open>linarith_trace\<close> (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 *)
--- 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>\<open>type\<close>;
val geq = cterm_of (Const (\<^const_name>\<open>HOL.eq\<close>, TVar type_tvar --> TVar type_tvar --> \<^typ>\<open>bool\<close>));
-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>\<open>(a::'a::{field, ord}) / b = c\<close>],
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