--- 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 *)