src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

update for release;

(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction.thy
    Author:     Nik Sultana, Cambridge University Computer Laboratory

Proof reconstruction for Leo-II.

USAGE:
* Simple call the "reconstruct_leo2" function.
* For more advanced use, you could use the component functions used in
  "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for
  examples of this.

This file contains definitions describing how to interpret LEO-II's
calculus in Isabelle/HOL, as well as more general proof-handling
functions. The definitions in this file serve to build an intermediate
proof script which is then evaluated into a tactic -- both these steps
are independent of LEO-II, and are defined in the TPTP_Reconstruct SML
module.

CONFIG:
The following attributes are mainly useful for debugging:
  tptp_unexceptional_reconstruction |
  unexceptional_reconstruction      |-- when these are true, a low-level exception
                                        is allowed to float to the top (instead of
                                        triggering a higher-level exception, or
                                        simply indicating that the reconstruction failed).
  tptp_max_term_size                --- fail of a term exceeds this size. "0" is taken
                                        to mean infinity.
  tptp_informative_failure          |
  informative_failure               |-- produce more output during reconstruction.
  tptp_trace_reconstruction         |

There are also two attributes, independent of the code here, that
influence the success of reconstruction: blast_depth_limit and
unify_search_bound. These are documented in their respective modules,
but in summary, if unify_search_bound is increased then we can
handle larger terms (at the cost of performance), since the unification
engine takes longer to give up the search; blast_depth_limit is
a limit on proof search performed by Blast. Blast is used for
the limited proof search that needs to be done to interpret
instances of LEO-II's inference rules.

TODO:
  use RemoveRedundantQuantifications instead of the ad hoc use of
   remove_redundant_quantification_in_lit and remove_redundant_quantification
*)

theory TPTP_Proof_Reconstruction
imports TPTP_Parser TPTP_Interpret
(* keywords "import_leo2_proof" :: thy_decl *) (*FIXME currently unused*)
begin


section "Setup"

ML \<open>
  val tptp_unexceptional_reconstruction = Attrib.setup_config_bool \<^binding>\<open>tptp_unexceptional_reconstruction\<close> (K false)
  fun unexceptional_reconstruction ctxt = Config.get ctxt tptp_unexceptional_reconstruction
  val tptp_informative_failure = Attrib.setup_config_bool \<^binding>\<open>tptp_informative_failure\<close> (K false)
  fun informative_failure ctxt = Config.get ctxt tptp_informative_failure
  val tptp_trace_reconstruction = Attrib.setup_config_bool \<^binding>\<open>tptp_trace_reconstruction\<close> (K false)
  val tptp_max_term_size = Attrib.setup_config_int \<^binding>\<open>tptp_max_term_size\<close> (K 0) (*0=infinity*)

  fun exceeds_tptp_max_term_size ctxt size =
    let
      val max = Config.get ctxt tptp_max_term_size
    in
      if max = 0 then false
      else size > max
    end
\<close>

(*FIXME move to TPTP_Proof_Reconstruction_Test_Units*)
declare [[
  tptp_unexceptional_reconstruction = false, (*NOTE should be "false" while testing*)
  tptp_informative_failure = true
]]

ML \<open>
exception UNSUPPORTED_ROLE
exception INTERPRET_INFERENCE
\<close>

ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
ML "open TPTP_Reconstruct_Library"
ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>

(*FIXME fudge*)
declare [[
  blast_depth_limit = 10,
  unify_search_bound = 5
]]


section "Proof reconstruction"
text \<open>There are two parts to proof reconstruction:
\begin{itemize}
  \item interpreting the inferences
  \item building the skeleton, which indicates how to compose
    individual inferences into subproofs, and then compose the
    subproofs to give the proof).
\end{itemize}

One step detects unsound inferences, and the other step detects
unsound composition of inferences.  The two parts can be weakly
coupled. They rely on a "proof index" which maps nodes to the
inference information. This information consists of the (usually
prover-specific) name of the inference step, and the Isabelle
formalisation of the inference as a term. The inference interpretation
then maps these terms into meta-theorems, and the skeleton is used to
compose the inference-level steps into a proof.

Leo2 operates on conjunctions of clauses. Each Leo2 inference has the
following form, where Cx are clauses:

           C1 && ... && Cn
          -----------------
          C'1 && ... && C'n

Clauses consist of disjunctions of literals (shown as Px below), and might
have a prefix of !-bound variables, as shown below.

  ! X... { P1 || ... || Pn}

Literals are usually assigned a polarity, but this isn't always the
case; you can come across inferences looking like this (where A is an
object-level formula):

             F
          --------
          F = true

The symbol "||" represents literal-level disjunction and "&&" is
clause-level conjunction. Rules will typically lift formula-level
conjunctions; for instance the following rule lifts object-level
disjunction:

          {    (A | B) = true    || ... } && ...
          --------------------------------------
          { A = true || B = true || ... } && ...


Using this setup, efficiency might be gained by only interpreting
inferences once, merging identical inference steps, and merging
identical subproofs into single inferences thus avoiding some effort.
We can also attempt to minimising proof search when interpreting
inferences.

It is hoped that this setup can target other provers by modifying the
clause representation to fit them, and adapting the inference
interpretation to handle the rules used by the prover. It should also
facilitate composing together proofs found by different provers.
\<close>


subsection "Instantiation"

lemma polar_allE [rule_format]:
  "\<lbrakk>(\<forall>x. P x) = True; (P x) = True \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>(\<exists>x. P x) = False; (P x) = False \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by auto

lemma polar_exE [rule_format]:
  "\<lbrakk>(\<exists>x. P x) = True; \<And>x. (P x) = True \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  "\<lbrakk>(\<forall>x. P x) = False; \<And>x. (P x) = False \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by auto

ML \<open>
(*This carries out an allE-like rule but on (polarised) literals.
 Instead of yielding a free variable (which is a hell for the
 matcher) it seeks to use one of the subgoals' parameters.
 This ought to be sufficient for emulating extcnf_combined,
 but note that the complexity of the problem can be enormous.*)
fun inst_parametermatch_tac ctxt thms i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val parameters =
      if null gls then []
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> strip_top_all_vars []
        |> fst
        |> map fst (*just get the parameter names*)
  in
    if null parameters then no_tac st
    else
      let
        fun instantiate param =
          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] []) thms
                   |> FIRST')
        val attempts = map instantiate parameters
      in
        (fold (curry (op APPEND')) attempts (K no_tac)) i st
      end
  end

(*Attempts to use the polar_allE theorems on a specific subgoal.*)
fun forall_pos_tac ctxt = inst_parametermatch_tac ctxt @{thms polar_allE}
\<close>

ML \<open>
(*This is similar to inst_parametermatch_tac, but prefers to
  match variables having identical names. Logically, this is
  a hack. But it reduces the complexity of the problem.*)
fun nominal_inst_parametermatch_tac ctxt thm i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val parameters =
      if null gls then []
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> strip_top_all_vars []
        |> fst
        |> map fst (*just get the parameter names*)
  in
    if null parameters then no_tac st
    else
      let
        fun instantiates param =
          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] [] thm

        val quantified_var = head_quantified_variable ctxt i st
      in
        if is_none quantified_var then no_tac st
        else
          if member (op =) parameters (the quantified_var |> fst) then
            instantiates (the quantified_var |> fst) i st
          else
            K no_tac i st
      end
  end
\<close>


subsection "Prefix massaging"

ML \<open>
exception NO_GOALS

(*Get quantifier prefix of the hypothesis and conclusion, reorder
  the hypothesis' quantifiers to have the ones appearing in the
  conclusion first.*)
fun canonicalise_qtfr_order ctxt i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst
  in
    if null gls then raise NO_GOALS
    else
      let
        val (params, (hyp_clause, conc_clause)) =
          rpair (i - 1) gls
          |> uncurry nth
          |> strip_top_all_vars []
          |> apsnd Logic.dest_implies

        val (hyp_quants, hyp_body) =
          HOLogic.dest_Trueprop hyp_clause
          |> strip_top_All_vars
          |> apfst rev

        val conc_quants =
          HOLogic.dest_Trueprop conc_clause
          |> strip_top_All_vars
          |> fst

        val new_hyp =
          (* fold absfree new_hyp_prefix hyp_body *)
          (*HOLogic.list_all*)
          fold_rev (fn (v, ty) => fn t => HOLogic.mk_all (v, ty, t))
           (prefix_intersection_list
             hyp_quants conc_quants)
           hyp_body
          |> HOLogic.mk_Trueprop

         val thm = Goal.prove ctxt [] []
           (Logic.mk_implies (hyp_clause, new_hyp))
           (fn _ =>
              (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
              THEN (REPEAT_DETERM
                    (HEADGOAL
                     (nominal_inst_parametermatch_tac ctxt @{thm allE})))
              THEN HEADGOAL (assume_tac ctxt))
      in
        dresolve_tac ctxt [thm] i st
      end
    end
\<close>


subsection "Some general rules and congruences"

(*this isn't an actual rule used in Leo2, but it seems to be
  applied implicitly during some Leo2 inferences.*)
lemma polarise: "P ==> P = True" by auto

ML \<open>
fun is_polarised t =
  (TPTP_Reconstruct.remove_polarity true t; true)
  handle TPTP_Reconstruct.UNPOLARISED _ => false

fun polarise_subgoal_hyps ctxt =
  COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dresolve_tac ctxt @{thms polarise})
\<close>

lemma simp_meta [rule_format]:
  "(A --> B) == (~A | B)"
  "(A | B) | C == A | B | C"
  "(A & B) & C == A & B & C"
  "(~ (~ A)) == A"
  (* "(A & B) == (~ (~A | ~B))" *)
  "~ (A & B) == (~A | ~B)"
  "~(A | B) == (~A) & (~B)"
by auto


subsection "Emulation of Leo2's inference rules"

(*this is not included in simp_meta since it would make a mess of the polarities*)
lemma expand_iff [rule_format]:
 "((A :: bool) = B) \<equiv> (~ A | B) & (~ B | A)"
by (rule eq_reflection, auto)

lemma polarity_switch [rule_format]:
  "(\<not> P) = True \<Longrightarrow> P = False"
  "(\<not> P) = False \<Longrightarrow> P = True"
  "P = False \<Longrightarrow> (\<not> P) = True"
  "P = True \<Longrightarrow> (\<not> P) = False"
by auto

lemma solved_all_splits: "False = True \<Longrightarrow> False" by simp
ML \<open>
fun solved_all_splits_tac ctxt =
  TRY (eresolve_tac ctxt @{thms conjE} 1)
  THEN resolve_tac ctxt @{thms solved_all_splits} 1
  THEN assume_tac ctxt 1
\<close>

lemma lots_of_logic_expansions_meta [rule_format]:
  "(((A :: bool) = B) = True) == (((A \<longrightarrow> B) = True) & ((B \<longrightarrow> A) = True))"
  "((A :: bool) = B) = False == (((~A) | B) = False) | (((~B) | A) = False)"

  "((F = G) = True) == (\<forall>x. (F x = G x)) = True"
  "((F = G) = False) == (\<forall>x. (F x = G x)) = False"

  "(A | B) = True == (A = True) | (B = True)"
  "(A & B) = False == (A = False) | (B = False)"
  "(A | B) = False == (A = False) & (B = False)"
  "(A & B) = True == (A = True) & (B = True)"
  "(~ A) = True == A = False"
  "(~ A) = False == A = True"
  "~ (A = True) == A = False"
  "~ (A = False) == A = True"
by (rule eq_reflection, auto)+

(*this is used in extcnf_combined handler*)
lemma eq_neg_bool: "((A :: bool) = B) = False ==> ((~ (A | B)) | ~ ((~ A) | (~ B))) = False"
by auto

lemma eq_pos_bool:
  "((A :: bool) = B) = True ==> ((~ (A | B)) | ~ (~ A | ~ B)) = True"
  "(A = B) = True \<Longrightarrow> A = True \<or> B = False"
  "(A = B) = True \<Longrightarrow> A = False \<or> B = True"
by auto

(*next formula is more versatile than
    "(F = G) = True \<Longrightarrow> \<forall>x. ((F x = G x) = True)"
  since it doesn't assume that clause is singleton. After splitqtfr,
  and after applying allI exhaustively to the conclusion, we can
  use the existing functions to find the "(F x = G x) = True"
  disjunct in the conclusion*)
lemma eq_pos_func: "\<And> x. (F = G) = True \<Longrightarrow> (F x = G x) = True"
by auto

(*make sure the conclusion consists of just "False"*)
lemma flip:
  "((A = True) ==> False) ==> A = False"
  "((A = False) ==> False) ==> A = True"
by auto

(*FIXME try to use Drule.equal_elim_rule1 directly for this*)
lemma equal_elim_rule1: "(A \<equiv> B) \<Longrightarrow> A \<Longrightarrow> B" by auto
lemmas leo2_rules =
 lots_of_logic_expansions_meta[THEN equal_elim_rule1]

(*FIXME is there any overlap with lots_of_logic_expansions_meta or leo2_rules?*)
lemma extuni_bool2 [rule_format]: "(A = B) = False \<Longrightarrow> (A = True) | (B = True)" by auto
lemma extuni_bool1 [rule_format]: "(A = B) = False \<Longrightarrow> (A = False) | (B = False)" by auto
lemma extuni_triv [rule_format]: "(A = A) = False \<Longrightarrow> R" by auto

(*Order (of A, B, C, D) matters*)
lemma dec_commut_eq [rule_format]:
  "((A = B) = (C = D)) = False \<Longrightarrow> (B = C) = False | (A = D) = False"
  "((A = B) = (C = D)) = False \<Longrightarrow> (B = D) = False | (A = C) = False"
by auto
lemma dec_commut_disj [rule_format]:
  "((A \<or> B) = (C \<or> D)) = False \<Longrightarrow> (B = C) = False \<or> (A = D) = False"
by auto

lemma extuni_func [rule_format]: "(F = G) = False \<Longrightarrow> (\<forall>X. (F X = G X)) = False" by auto


subsection "Emulation: tactics"

ML \<open>
(*Instantiate a variable according to the info given in the
  proof annotation. Through this we avoid having to come up
  with instantiations during reconstruction.*)
fun bind_tac ctxt prob_name ordered_binds =
  let
    val thy = Proof_Context.theory_of ctxt
    fun term_to_string t =
      Pretty.pure_string_of (Syntax.pretty_term ctxt t)
    val ordered_instances =
      TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds []
      |> map (snd #> term_to_string)
      |> permute

    (*instantiate a list of variables, order matters*)
    fun instantiate_vars ctxt vars : tactic =
      map (fn var =>
            Rule_Insts.eres_inst_tac ctxt
             [((("x", 0), Position.none), var)] [] @{thm allE} 1)
          vars
      |> EVERY

    fun instantiate_tac vars =
      instantiate_vars ctxt vars
      THEN (HEADGOAL (assume_tac ctxt))
  in
    HEADGOAL (canonicalise_qtfr_order ctxt)
    THEN (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})))
    THEN REPEAT_DETERM (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE}))
    (*now only the variable to instantiate should be left*)
    THEN FIRST (map instantiate_tac ordered_instances)
  end
\<close>

ML \<open>
(*Simplification tactics*)
local
  fun rew_goal_tac thms ctxt i =
    rewrite_goal_tac ctxt thms i
    |> CHANGED
in
  val expander_animal =
    rew_goal_tac (@{thms simp_meta} @ @{thms lots_of_logic_expansions_meta})

  val simper_animal =
    rew_goal_tac @{thms simp_meta}
end
\<close>

lemma prop_normalise [rule_format]:
  "(A | B) | C == A | B | C"
  "(A & B) & C == A & B & C"
  "A | B == ~(~A & ~B)"
  "~~ A == A"
by auto
ML \<open>
(*i.e., break_conclusion*)
fun flip_conclusion_tac ctxt =
  let
    val default_tac =
      (TRY o CHANGED o (rewrite_goal_tac ctxt @{thms prop_normalise}))
      THEN' resolve_tac ctxt @{thms notI}
      THEN' (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
      THEN' (TRY o (expander_animal ctxt))
  in
    default_tac ORELSE' resolve_tac ctxt @{thms flip}
  end
\<close>


subsection "Skolemisation"

lemma skolemise [rule_format]:
  "\<forall> P. (\<not> (\<forall>x. P x)) \<longrightarrow> \<not> (P (SOME x. ~ P x))"
proof -
  have "\<And> P. (\<not> (\<forall>x. P x)) \<Longrightarrow> \<not> (P (SOME x. ~ P x))"
  proof -
    fix P
    assume ption: "\<not> (\<forall>x. P x)"
    hence a: "\<exists>x. \<not> P x" by force

    have hilbert : "\<And>P. (\<exists>x. P x) \<Longrightarrow> (P (SOME x. P x))"
    proof -
      fix P
      assume "(\<exists>x. P x)"
      thus "(P (SOME x. P x))"
        apply auto
        apply (rule someI)
        apply auto
        done
    qed

    from a show "\<not> P (SOME x. \<not> P x)"
    proof -
      assume "\<exists>x. \<not> P x"
      hence "\<not> P (SOME x. \<not> P x)" by (rule hilbert)
      thus ?thesis .
    qed
  qed
  thus ?thesis by blast
qed

lemma polar_skolemise [rule_format]:
  "\<forall>P. (\<forall>x. P x) = False \<longrightarrow> (P (SOME x. \<not> P x)) = False"
proof -
  have "\<And>P. (\<forall>x. P x) = False \<Longrightarrow> (P (SOME x. \<not> P x)) = False"
  proof -
    fix P
    assume ption: "(\<forall>x. P x) = False"
    hence "\<not> (\<forall>x. P x)" by force
    hence "\<not> All P" by force
    hence "\<not> (P (SOME x. \<not> P x))" by (rule skolemise)
    thus "(P (SOME x. \<not> P x)) = False" by force
  qed
  thus ?thesis by blast
qed

lemma leo2_skolemise [rule_format]:
  "\<forall>P sk. (\<forall>x. P x) = False \<longrightarrow> (sk = (SOME x. \<not> P x)) \<longrightarrow> (P sk) = False"
by (clarify, rule polar_skolemise)

lemma lift_forall [rule_format]:
  "\<And>x. (\<forall>x. A x) = True \<Longrightarrow> (A x) = True"
  "\<And>x. (\<exists>x. A x) = False \<Longrightarrow> (A x) = False"
by auto
lemma lift_exists [rule_format]:
  "\<lbrakk>(All P) = False; sk = (SOME x. \<not> P x)\<rbrakk> \<Longrightarrow> P sk = False"
  "\<lbrakk>(Ex P) = True; sk = (SOME x. P x)\<rbrakk> \<Longrightarrow> P sk = True"
apply (drule polar_skolemise, simp)
apply (simp, drule someI_ex, simp)
done

ML \<open>
(*FIXME LHS should be constant. Currently allow variables for testing. Probably should still allow Vars (but not Frees) since they'll act as intermediate values*)
fun conc_is_skolem_def t =
  case t of
      Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) =>
      let
        val (h, args) =
          strip_comb t'
          |> apfst (strip_abs #> snd #> strip_comb #> fst)
        val h_property =
          is_Free h orelse
          is_Var h orelse
          (is_Const h
           andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.Ex\<close>)
           andalso (dest_Const_name h <> dest_Const_name \<^term>\<open>HOL.All\<close>)
           andalso (h <> \<^term>\<open>Hilbert_Choice.Eps\<close>)
           andalso (h <> \<^term>\<open>HOL.conj\<close>)
           andalso (h <> \<^term>\<open>HOL.disj\<close>)
           andalso (h <> \<^term>\<open>HOL.eq\<close>)
           andalso (h <> \<^term>\<open>HOL.implies\<close>)
           andalso (h <> \<^term>\<open>HOL.The\<close>)
           andalso (h <> \<^term>\<open>HOL.Ex1\<close>)
           andalso (h <> \<^term>\<open>HOL.Not\<close>)
           andalso (h <> \<^term>\<open>HOL.iff\<close>)
           andalso (h <> \<^term>\<open>HOL.not_equal\<close>))
        val args_property =
          fold (fn t => fn b =>
           b andalso is_Free t) args true
      in
        h_property andalso args_property
      end
    | _ => false
\<close>

ML \<open>
(*Hack used to detect if a Skolem definition, with an LHS Var, has had the LHS instantiated into an unacceptable term.*)
fun conc_is_bad_skolem_def t =
  case t of
      Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) =>
      let
        val (h, args) = strip_comb t'
        val const_h_test =
          if is_Const h then
            (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.Ex\<close>)
             orelse (dest_Const_name h = dest_Const_name \<^term>\<open>HOL.All\<close>)
             orelse (h = \<^term>\<open>Hilbert_Choice.Eps\<close>)
             orelse (h = \<^term>\<open>HOL.conj\<close>)
             orelse (h = \<^term>\<open>HOL.disj\<close>)
             orelse (h = \<^term>\<open>HOL.eq\<close>)
             orelse (h = \<^term>\<open>HOL.implies\<close>)
             orelse (h = \<^term>\<open>HOL.The\<close>)
             orelse (h = \<^term>\<open>HOL.Ex1\<close>)
             orelse (h = \<^term>\<open>HOL.Not\<close>)
             orelse (h = \<^term>\<open>HOL.iff\<close>)
             orelse (h = \<^term>\<open>HOL.not_equal\<close>)
          else true
        val h_property =
          not (is_Free h) andalso
          not (is_Var h) andalso
          const_h_test
        val args_property =
          fold (fn t => fn b =>
           b andalso is_Free t) args true
      in
        h_property andalso args_property
      end
    | _ => false
\<close>

ML \<open>
fun get_skolem_conc t =
  let
    val t' =
      strip_top_all_vars [] t
      |> snd
      |> try_dest_Trueprop
  in
    case t' of
        Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) => SOME t'
      | _ => NONE
  end

fun get_skolem_conc_const t =
  lift_option
   (fn t' =>
     head_of t'
     |> strip_abs_body
     |> head_of
     |> dest_Const)
   (get_skolem_conc t)
\<close>

(*
Technique for handling quantifiers:
  Principles:
  * allE should always match with a !!
  * exE should match with a constant,
     or bind a fresh !! -- currently not doing the latter since it never seems to arised in normal Leo2 proofs.
*)

ML \<open>
fun forall_neg_tac candidate_consts ctxt i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val parameters =
      if null gls then ""
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> strip_top_all_vars []
        |> fst
        |> map fst (*just get the parameter names*)
        |> (fn l =>
              if null l then ""
              else
                implode_space l
                |> pair " "
                |> (op ^))

  in
    if null gls orelse null candidate_consts then no_tac st
    else
      let
        fun instantiate const_name =
          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] []
            @{thm leo2_skolemise}
        val attempts = map instantiate candidate_consts
      in
        (fold (curry (op APPEND')) attempts (K no_tac)) i st
      end
  end
\<close>

ML \<open>
exception SKOLEM_DEF of term (*The tactic wasn't pointed at a skolem definition*)
exception NO_SKOLEM_DEF of (*skolem const name*)string * Binding.binding * term (*The tactic could not find a skolem definition in the theory*)
fun absorb_skolem_def ctxt prob_name_opt i = fn st =>
  let
    val thy = Proof_Context.theory_of ctxt

    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val conclusion =
      if null gls then
        (*this should never be thrown*)
        raise NO_GOALS
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> strip_top_all_vars []
        |> snd
        |> Logic.strip_horn
        |> snd

    fun skolem_const_info_of t =
      case t of
          Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _)) =>
          head_of t'
          |> strip_abs_body (*since in general might have a skolem term, so we want to rip out the prefixing lambdas to get to the constant (which should be at head position)*)
          |> head_of
          |> dest_Const
        | _ => raise SKOLEM_DEF t

    val const_name =
      skolem_const_info_of conclusion
      |> fst

    val def_name = const_name ^ "_def"

    val bnd_def = (*FIXME consts*)
      const_name
      |> Long_Name.implode o tl o Long_Name.explode (*FIXME hack to drop theory-name prefix*)
      |> Binding.qualified_name
      |> Binding.suffix_name "_def"

    val bnd_name =
      case prob_name_opt of
          NONE => bnd_def
        | SOME prob_name =>
(*            Binding.qualify false
             (TPTP_Problem_Name.mangle_problem_name prob_name)
*)
             bnd_def

    val thm =
      (case try (Thm.axiom thy) def_name of
        SOME thm => thm
      | NONE =>
          if is_none prob_name_opt then
            (*This mode is for testing, so we can be a bit
              looser with theories*)
            (* FIXME bad theory context!? *)
            Thm.add_axiom_global (bnd_name, conclusion) thy
            |> fst |> snd
          else
            raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
  in
    resolve_tac ctxt [Drule.export_without_context thm] i st
  end
  handle SKOLEM_DEF _ => no_tac st
\<close>

ML \<open>
(*
In current system, there should only be 2 subgoals: the one where
the skolem definition is being built (with a Var in the LHS), and the other subgoal using Var.
*)
(*arity must be greater than 0. if arity=0 then
  there's no need to use this expensive matching.*)
fun find_skolem_term ctxt consts_candidate arity = fn st =>
  let
    val _ = \<^assert> (arity > 0)

    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    (*extract the conclusion of each subgoal*)
    val conclusions =
      if null gls then
        raise NO_GOALS
      else
        map (strip_top_all_vars [] #> snd #> Logic.strip_horn #> snd) gls
        (*Remove skolem-definition conclusion, to avoid wasting time analysing it*)
        |> filter (try_dest_Trueprop #> conc_is_skolem_def #> not)
        (*There should only be a single goal*) (*FIXME this might not always be the case, in practice*)
        (* |> tap (fn x => @{assert} (is_some (try the_single x))) *)

    (*look for subterms headed by a skolem constant, and whose
      arguments are all parameter Vars*)
    fun get_skolem_terms args (acc : term list) t =
      case t of
          (c as Const _) $ (v as Free _) =>
            if c = consts_candidate andalso
             arity = length args + 1 then
              (list_comb (c, v :: args)) :: acc
            else acc
        | t1 $ (v as Free _) =>
            get_skolem_terms (v :: args) acc t1 @
             get_skolem_terms [] acc t1
        | t1 $ t2 =>
            get_skolem_terms [] acc t1 @
             get_skolem_terms [] acc t2
        | Abs (_, _, t') => get_skolem_terms [] acc t'
        | _ => acc
  in
    map (strip_top_All_vars #> snd) conclusions
    |> maps (get_skolem_terms [] [])
    |> distinct (op =)
  end
\<close>

ML \<open>
fun instantiate_skols ctxt consts_candidates i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val (params, conclusion) =
      if null gls then
        raise NO_GOALS
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> strip_top_all_vars []
        |> apsnd (Logic.strip_horn #> snd)

    fun skolem_const_info_of t =
      case t of
          Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ rhs)) =>
          let
            (*the parameters we will concern ourselves with*)
            val params' =
              Term.add_frees lhs []
              |> distinct (op =)
            (*check to make sure that params' <= params*)
            val _ = \<^assert> (forall (member (op =) params) params')
            val skolem_const_ty =
              let
                val (skolem_const_prety, no_params) =
                  Term.strip_comb lhs
                  |> apfst (dest_Var #> snd) (*head of lhs consists of a logical variable. we just want its type.*)
                  |> apsnd length

                val _ = \<^assert> (length params = no_params)

                (*get value type of a function type after n arguments have been supplied*)
                fun get_val_ty n ty =
                  if n = 0 then ty
                  else get_val_ty (n - 1) (dest_funT ty |> snd)
              in
                get_val_ty no_params skolem_const_prety
              end

          in
            (skolem_const_ty, params')
          end
        | _ => raise (SKOLEM_DEF t)

(*
find skolem const candidates which, after applying distinct members of params' we end up with, give us something of type skolem_const_ty.

given a candidate's type, skolem_const_ty, and params', we get some pemutations of params' (i.e. the order in which they can be given to the candidate in order to get skolem_const_ty). If the list of permutations is empty, then we cannot use that candidate.
*)
(*
only returns a single matching -- since terms are linear, and variable arguments are Vars, order shouldn't matter, so we can ignore permutations.
doesn't work with polymorphism (for which we'd need to use type unification) -- this is OK since no terms should be polymorphic, since Leo2 proofs aren't.
*)
    fun use_candidate target_ty params acc cur_ty =
      if null params then
        if cur_ty = target_ty then
          SOME (rev acc)
        else NONE
      else
        \<^try>\<open>
          let
            val (arg_ty, val_ty) = Term.dest_funT cur_ty
            (*now find a param of type arg_ty*)
            val (candidate_param, params') =
              find_and_remove (snd #> pair arg_ty #> (op =)) params
          in
            use_candidate target_ty params' (candidate_param :: acc) val_ty
          end
          catch TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
             | _ => NONE  (* FIXME avoid catch-all handler *)
        \<close>

    val (skolem_const_ty, params') = skolem_const_info_of conclusion

(*
For each candidate, build a term and pass it to Thm.instantiate, whic in turn is chained with PRIMITIVE to give us this_tactic.

Big picture:
  we run the following:
    drule leo2_skolemise THEN' this_tactic

NOTE: remember to APPEND' instead of ORELSE' the two tactics relating to skolemisation
*)

    val filtered_candidates =
      map (dest_Const_type #> use_candidate skolem_const_ty params' [])
       consts_candidates (* prefiltered_candidates *)
      |> pair consts_candidates (* prefiltered_candidates *)
      |> ListPair.zip
      |> filter (snd #> is_none #> not)
      |> map (apsnd the)

    val skolem_terms =
      let
        fun make_result_t (t, args) =
          (* list_comb (t, map Free args) *)
          if length args > 0 then
            hd (find_skolem_term ctxt t (length args) st)
          else t
      in
        map make_result_t filtered_candidates
      end

    (*prefix a skolem term with bindings for the parameters*)
    (* val contextualise = fold absdummy (map snd params) *)
    val contextualise = fold absfree params

    val skolem_cts = map (contextualise #> Thm.cterm_of ctxt) skolem_terms


(*now the instantiation code*)

    (*there should only be one Var -- that is from the previous application of drule leo2_skolemise. We look for it at the head position in some equation at a conclusion of a subgoal.*)
    val var_opt =
      let
        val pre_var =
          gls
          |> map
              (strip_top_all_vars [] #> snd #>
               Logic.strip_horn #> snd #>
               get_skolem_conc)
          |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
          |> maps (switch Term.add_vars [])

        fun make_var pre_var =
          the_single pre_var
          |> Var
          |> Thm.cterm_of ctxt
          |> SOME
      in
        if null pre_var then NONE
        else make_var pre_var
     end

    fun instantiate_tac from to =
      PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (from, to)))

    val tactic =
      if is_none var_opt then no_tac
      else
        fold (curry (op APPEND))
          (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
  in
    tactic st
  end
\<close>

ML \<open>
fun new_skolem_tac ctxt consts_candidates =
  let
    fun tac thm =
      dresolve_tac ctxt [thm]
      THEN' instantiate_skols ctxt consts_candidates
  in
    if null consts_candidates then K no_tac
    else FIRST' (map tac @{thms lift_exists})
  end
\<close>

(*
need a tactic to expand "? x . P" to "~ ! x. ~ P"
*)
ML \<open>
fun ex_expander_tac ctxt i =
   let
     val simpset =
       empty_simpset ctxt (*NOTE for some reason, Bind exception gets raised if ctxt's simpset isn't emptied*)
       |> Simplifier.add_simp @{lemma "Ex P == (\<not> (\<forall>x. \<not> P x))" by auto}
   in
     CHANGED (asm_full_simp_tac simpset i)
   end
\<close>


subsubsection "extuni_dec"

ML \<open>
(*n-ary decomposition. Code is based on the n-ary arg_cong generator*)
fun extuni_dec_n ctxt arity =
  let
    val _ = \<^assert> (arity > 0)
    val is =
      1 upto arity
      |> map Int.toString
    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", \<^sort>\<open>type\<close>)) is
    val res_ty = TFree ("res" ^ "_ty", \<^sort>\<open>type\<close>)
    val f_ty = arg_tys ---> res_ty
    val f = Free ("f", f_ty)
    val xs = map (fn i =>
      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", \<^sort>\<open>type\<close>))) is
    (*FIXME DRY principle*)
    val ys = map (fn i =>
      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", \<^sort>\<open>type\<close>))) is

    val hyp_lhs = list_comb (f, xs)
    val hyp_rhs = list_comb (f, ys)
    val hyp_eq =
      HOLogic.eq_const res_ty $ hyp_lhs $ hyp_rhs
    val hyp =
      HOLogic.eq_const HOLogic.boolT $ hyp_eq $ \<^term>\<open>False\<close>
      |> HOLogic.mk_Trueprop
    fun conc_eq i =
      let
        val ty = TFree ("arg" ^ i ^ "_ty", \<^sort>\<open>type\<close>)
        val x = Free ("x" ^ i, ty)
        val y = Free ("y" ^ i, ty)
        val eq = HOLogic.eq_const ty $ x $ y
      in
        HOLogic.eq_const HOLogic.boolT $ eq $ \<^term>\<open>False\<close>
      end

    val conc_disjs = map conc_eq is

    val conc =
      if length conc_disjs = 1 then
        the_single conc_disjs
      else
        fold
         (fn t => fn t_conc => HOLogic.mk_disj (t_conc, t))
         (tl conc_disjs) (hd conc_disjs)

    val t =
      Logic.mk_implies (hyp, HOLogic.mk_Trueprop conc)
  in
    Goal.prove ctxt [] [] t (fn _ => auto_tac ctxt)
    |> Drule.export_without_context
  end
\<close>

ML \<open>
(*Determine the arity of a function which the "dec"
  unification rule is about to be applied.
  NOTE:
    * Assumes that there is a single hypothesis
*)
fun find_dec_arity i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst
  in
    if null gls then raise NO_GOALS
    else
      let
        val (params, (literal, conc_clause)) =
          rpair (i - 1) gls
          |> uncurry nth
          |> strip_top_all_vars []
          |> apsnd Logic.strip_horn
          |> apsnd (apfst the_single)

        val get_ty =
          HOLogic.dest_Trueprop
          #> strip_top_All_vars
          #> snd
          #> HOLogic.dest_eq (*polarity's "="*)
          #> fst
          #> HOLogic.dest_eq (*the unification constraint's "="*)
          #> fst
          #> head_of
          #> dest_Const_type

       fun arity_of ty =
         let
           val (_, res_ty) = dest_funT ty

         in
           1 + arity_of res_ty
         end
         handle (TYPE ("dest_funT", _, _)) => 0

      in
        arity_of (get_ty literal)
      end
  end

(*given an inference, it returns the parameters (i.e., we've already matched the leading & shared quantification in the hypothesis & conclusion clauses), and the "raw" inference*)
fun breakdown_inference i = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst
  in
    if null gls then raise NO_GOALS
    else
      rpair (i - 1) gls
      |> uncurry nth
      |> strip_top_all_vars []
  end

(*build a custom elimination rule for extuni_dec, and instantiate it to match a specific subgoal*)
fun extuni_dec_elim_rule ctxt arity i = fn st =>
  let
    val rule = extuni_dec_n ctxt arity

    val rule_hyp =
      Thm.prop_of rule
      |> Logic.dest_implies
      |> fst (*assuming that rule has single hypothesis*)

    (*having run break_hypothesis earlier, we know that the hypothesis
      now consists of a single literal. We can (and should)
      disregard the conclusion, since it hasn't been "broken",
      and it might include some unwanted literals -- the latter
      could cause "diff" to fail (since they won't agree with the
      rule we have generated.*)

    val inference_hyp =
      snd (breakdown_inference i st)
      |> Logic.dest_implies
      |> fst (*assuming that inference has single hypothesis,
               as explained above.*)
  in
    TPTP_Reconstruct_Library.diff_and_instantiate ctxt rule rule_hyp inference_hyp
  end

fun extuni_dec_tac ctxt i = fn st =>
  let
    val arity = find_dec_arity i st

    fun elim_tac i st =
      let
        val rule =
          extuni_dec_elim_rule ctxt arity i st
          (*in case we itroduced free variables during
            instantiation, we generalise the rule to make
            those free variables into logical variables.*)
          |> Thm.forall_intr_frees
          |> Drule.export_without_context
      in dresolve_tac ctxt [rule] i st end
      handle NO_GOALS => no_tac st

    fun closure tac =
     (*batter fails if there's no toplevel disjunction in the
       hypothesis, so we also try atac*)
      SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt))
    val search_tac =
      ASAP
        (resolve_tac ctxt @{thms disjI1} APPEND' resolve_tac ctxt @{thms disjI2})
        (FIRST' (map closure
                  [dresolve_tac ctxt @{thms dec_commut_eq},
                   dresolve_tac ctxt @{thms dec_commut_disj},
                   elim_tac]))
  in
    (CHANGED o search_tac) i st
  end
\<close>


subsubsection "standard_cnf"
(*Given a standard_cnf inference, normalise it
     e.g. ((A & B) & C \<longrightarrow> D & E \<longrightarrow> F \<longrightarrow> G) = False
     is changed to
          (A & B & C & D & E & F \<longrightarrow> G) = False
 then custom-build a metatheorem which validates this:
          (A & B & C & D & E & F \<longrightarrow> G) = False
       -------------------------------------------
          (A = True) & (B = True) & (C = True) &
          (D = True) & (E = True) & (F = True) & (G = False)
 and apply this metatheorem.

There aren't any "positive" standard_cnfs in Leo2's calculus:
  e.g.,  "(A \<longrightarrow> B) = True \<Longrightarrow> A = False | (A = True & B = True)"
since "standard_cnf" seems to be applied at the preprocessing
stage, together with splitting.
*)

ML \<open>
(*Conjunctive counterparts to Term.disjuncts_aux and Term.disjuncts*)
fun conjuncts_aux (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ t $ t') conjs =
     conjuncts_aux t (conjuncts_aux t' conjs)
  | conjuncts_aux t conjs = t :: conjs

fun conjuncts t = conjuncts_aux t []

(*HOL equivalent of Logic.strip_horn*)
local
  fun imp_strip_horn' acc (Const (\<^const_name>\<open>HOL.implies\<close>, _) $ A $ B) =
        imp_strip_horn' (A :: acc) B
    | imp_strip_horn' acc t = (acc, t)
in
  fun imp_strip_horn t =
    imp_strip_horn' [] t
    |> apfst rev
end
\<close>

ML \<open>
(*Returns whether the antecedents are separated by conjunctions
  or implications; the number of antecedents; and the polarity
  of the original clause -- I think this will always be "false".*)
fun standard_cnf_type ctxt i : thm -> (TPTP_Reconstruct.formula_kind * int * bool) option = fn st =>
  let
    val gls =
      Thm.prop_of st
      |> Logic.strip_horn
      |> fst

    val hypos =
      if null gls then raise NO_GOALS
      else
        rpair (i - 1) gls
        |> uncurry nth
        |> TPTP_Reconstruct.strip_top_all_vars []
        |> snd
        |> Logic.strip_horn
        |> fst

    (*hypothesis clause should be singleton*)
    val _ = \<^assert> (length hypos = 1)

    val (t, pol) = the_single hypos
      |> try_dest_Trueprop
      |> TPTP_Reconstruct.strip_top_All_vars
      |> snd
      |> TPTP_Reconstruct.remove_polarity true

    (*literal is negative*)
    val _ = \<^assert> (not pol)

    val (antes, conc) = imp_strip_horn t

    val (ante_type, antes') =
      if length antes = 1 then
        let
          val conjunctive_antes =
            the_single antes
            |> conjuncts
        in
          if length conjunctive_antes > 1 then
            (TPTP_Reconstruct.Conjunctive NONE,
             conjunctive_antes)
          else
            (TPTP_Reconstruct.Implicational NONE,
             antes)
        end
      else
        (TPTP_Reconstruct.Implicational NONE,
         antes)
  in
    if null antes then NONE
    else SOME (ante_type, length antes', pol)
  end
\<close>

ML \<open>
(*Given a certain standard_cnf type, build a metatheorem that would
  validate it*)
fun mk_standard_cnf ctxt kind arity =
  let
    val _ = \<^assert> (arity > 0)
    val vars =
      1 upto (arity + 1)
      |> map (fn i => Free ("x" ^ Int.toString i, HOLogic.boolT))

    val consequent = hd vars
    val antecedents = tl vars

    val conc =
      fold
       (curry HOLogic.mk_conj)
       (map (fn var => HOLogic.mk_eq (var, \<^term>\<open>True\<close>)) antecedents)
       (HOLogic.mk_eq (consequent, \<^term>\<open>False\<close>))

    val pre_hyp =
      case kind of
          TPTP_Reconstruct.Conjunctive NONE =>
            curry HOLogic.mk_imp
             (if length antecedents = 1 then the_single antecedents
              else
                fold (curry HOLogic.mk_conj) (tl antecedents) (hd antecedents))
             (hd vars)
        | TPTP_Reconstruct.Implicational NONE =>
            fold (curry HOLogic.mk_imp) antecedents consequent

    val hyp = HOLogic.mk_eq (pre_hyp, \<^term>\<open>False\<close>)

    val t =
      Logic.mk_implies (HOLogic.mk_Trueprop  hyp, HOLogic.mk_Trueprop conc)
  in
    Goal.prove ctxt [] [] t (fn _ => HEADGOAL (blast_tac ctxt))
    |> Drule.export_without_context
  end
\<close>

ML \<open>
(*Applies a d-tactic, then breaks it up conjunctively.
  This can be used to transform subgoals as follows:
     (A \<longrightarrow> B) = False  \<Longrightarrow> R
              |
              v
  \<lbrakk>A = True; B = False\<rbrakk> \<Longrightarrow> R
*)
fun weak_conj_tac ctxt drule =
  dresolve_tac ctxt [drule] THEN'
  (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
\<close>

ML \<open>
fun uncurry_lit_neg_tac ctxt =
  REPEAT_DETERM o
    dresolve_tac ctxt [@{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}]
\<close>

ML \<open>
fun standard_cnf_tac ctxt i = fn st =>
  let
    fun core_tactic i = fn st =>
      case standard_cnf_type ctxt i st of
          NONE => no_tac st
        | SOME (kind, arity, _) =>
            let
              val rule = mk_standard_cnf ctxt kind arity;
            in
              (weak_conj_tac ctxt rule THEN' assume_tac ctxt) i st
            end
  in
    (uncurry_lit_neg_tac ctxt
     THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt
     THEN' core_tactic) i st
  end
\<close>


subsubsection "Emulator prep"

ML \<open>
datatype cleanup_feature =
    RemoveHypothesesFromSkolemDefs
  | RemoveDuplicates

datatype loop_feature =
    Close_Branch
  | ConjI
  | King_Cong
  | Break_Hypotheses
  | Donkey_Cong (*simper_animal + ex_expander_tac*)
  | RemoveRedundantQuantifications
  | Assumption

  (*Closely based on Leo2 calculus*)
  | Existential_Free
  | Existential_Var
  | Universal
  | Not_pos
  | Not_neg
  | Or_pos
  | Or_neg
  | Equal_pos
  | Equal_neg
  | Extuni_Bool2
  | Extuni_Bool1
  | Extuni_Dec
  | Extuni_Bind
  | Extuni_Triv
  | Extuni_FlexRigid
  | Extuni_Func
  | Polarity_switch
  | Forall_special_pos

datatype feature =
    ConstsDiff
  | StripQuantifiers
  | Flip_Conclusion
  | Loop of loop_feature list
  | LoopOnce of loop_feature list
  | InnerLoopOnce of loop_feature list
  | CleanUp of cleanup_feature list
  | AbsorbSkolemDefs
\<close>

ML \<open>
fun can_feature x l =
  let
    fun sublist_of_clean_up el =
      case el of
          CleanUp l'' => SOME l''
        | _ => NONE
    fun sublist_of_loop el =
      case el of
          Loop l'' => SOME l''
        | _ => NONE
    fun sublist_of_loop_once el =
      case el of
          LoopOnce l'' => SOME l''
        | _ => NONE
    fun sublist_of_inner_loop_once el =
      case el of
          InnerLoopOnce l'' => SOME l''
        | _ => NONE

    fun check_sublist sought_sublist opt_list =
      if forall is_none opt_list then false
      else
        fold_options opt_list
        |> flat
        |> pair sought_sublist
        |> subset (op =)
  in
    case x of
        CleanUp l' =>
          map sublist_of_clean_up l
          |> check_sublist l'
      | Loop l' =>
          map sublist_of_loop l
          |> check_sublist l'
      | LoopOnce l' =>
          map sublist_of_loop_once l
          |> check_sublist l'
      | InnerLoopOnce l' =>
          map sublist_of_inner_loop_once l
          |> check_sublist l'
      | _ => exists (curry (op =) x) l
  end;

fun loop_can_feature loop_feats l =
  can_feature (Loop loop_feats) l orelse
  can_feature (LoopOnce loop_feats) l orelse
  can_feature (InnerLoopOnce loop_feats) l;

\<^assert> (can_feature ConstsDiff [StripQuantifiers, ConstsDiff]);

\<^assert>
  (can_feature (CleanUp [RemoveHypothesesFromSkolemDefs])
    [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]);

\<^assert>
  (can_feature (Loop []) [Loop [Existential_Var]]);

\<^assert>
  (not (can_feature (Loop []) [InnerLoopOnce [Existential_Var]]));
\<close>

ML \<open>
exception NO_LOOP_FEATS
fun get_loop_feats (feats : feature list) =
  let
    val loop_find =
      fold (fn x => fn loop_feats_acc =>
        if is_some loop_feats_acc then loop_feats_acc
        else
          case x of
              Loop loop_feats => SOME loop_feats
            | LoopOnce loop_feats => SOME loop_feats
            | InnerLoopOnce loop_feats => SOME loop_feats
            | _ => NONE)
       feats
       NONE
  in
    if is_some loop_find then the loop_find
    else raise NO_LOOP_FEATS
  end;

\<^assert>
  (get_loop_feats [Loop [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal]] =
   [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal])
\<close>

(*use as elim rule to remove premises*)
lemma insa_prems: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> P" by auto
ML \<open>
fun cleanup_skolem_defs ctxt feats =
  let
    (*remove hypotheses from skolem defs,
     after testing that they look like skolem defs*)
    val dehypothesise_skolem_defs =
      COND' (SOME #> TERMPRED (fn _ => true) conc_is_skolem_def)
        (REPEAT_DETERM o eresolve_tac ctxt @{thms insa_prems})
        (K no_tac)
  in
    if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then
      ALLGOALS (TRY o dehypothesise_skolem_defs)
    else all_tac
  end
\<close>

ML \<open>
fun remove_duplicates_tac feats =
  (if can_feature (CleanUp [RemoveDuplicates]) feats then
     distinct_subgoals_tac
   else all_tac)
\<close>

ML \<open>
(*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*)
fun which_skolem_concs_used ctxt = fn st =>
  let
    val feats = [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]]
    val scrubup_tac =
      cleanup_skolem_defs ctxt feats
      THEN remove_duplicates_tac feats