src/HOL/Tools/lin_arith.ML

    discrete = discrete});
 
 val split_limit = Attrib.setup_config_int \<^binding>\<open>linarith_split_limit\<close> (K 9);
 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
 

     val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm
   in
     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,         *)
 (* performs NNF-normalization of ~P, and eliminates conjunctions,            *)
 (* disjunctions and existential quantifiers from the premises, possibly (in  *)
 (* the case of disjunctions) resulting in several new subgoals, each of the  *)
 (* 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
     val cond_split_tac = SUBGOAL (fn (subgoal, i) =>

       TRY o REPEAT_ALL_NEW
         (DETERM o (eresolve_tac ctxt [conjE, exE] ORELSE' eresolve_tac ctxt [disjE]))
     ]
   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        *)
 (* contradiction (i.e., a term and its negation) in their premises.          *)
 

    the actual refutation tactic. Should be able to deal with goals
    [| A1; ...; An |] ==> False
    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
               (eresolve_tac ctxt [@{thm conjE}, @{thm exE}] 1 ORELSE
                filter_prems_tac ctxt test 1 ORELSE

   in EVERY'[TRY o filter_prems_tac ctxt test,
             REPEAT_DETERM o eresolve_tac ctxt @{thms rev_mp}, prep_tac,
               resolve_tac ctxt @{thms ccontr}, prem_nnf_tac ctxt,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
-
-end;
 
 
 (* arith proof method *)
 
 local