src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

 begin
 
 
 section "Setup"
 
-ML {*
+ML \<open>
   val tptp_unexceptional_reconstruction = Attrib.setup_config_bool @{binding tptp_unexceptional_reconstruction} (K false)
   fun unexceptional_reconstruction ctxt = Config.get ctxt tptp_unexceptional_reconstruction
   val tptp_informative_failure = Attrib.setup_config_bool @{binding tptp_informative_failure} (K false)
   fun informative_failure ctxt = Config.get ctxt tptp_informative_failure
   val tptp_trace_reconstruction = Attrib.setup_config_bool @{binding tptp_trace_reconstruction} (K false)

       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

   unify_search_bound = 5
 ]]
 
 
 section "Proof reconstruction"
-text {*There are two parts to 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).

 
 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]:

 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 {*
+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.*)

       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}
-*}
-
-ML {*
+\<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

             instantiates (the quantified_var |> fst) i st
           else
             K no_tac i st
       end
   end
-*}
+\<close>
 
 
 subsection "Prefix massaging"
 
-ML {*
+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.*)

               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 {*
+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"

   "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 {*
+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)"
 

 lemma extuni_func [rule_format]: "(F = G) = False \<Longrightarrow> (! X. (F X = G X)) = False" by auto
 
 
 subsection "Emulation: tactics"
 
-ML {*
+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

     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
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 (*Simplification tactics*)
 local
   fun rew_goal_tac thms ctxt i =
     rewrite_goal_tac ctxt thms i
     |> CHANGED

     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 {*
+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' (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]:

   "\<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 {*
+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 HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _) =>
       let

            b andalso is_Free t) args true
       in
         h_property andalso args_property
       end
     | _ => false
-*}
-
-ML {*
+\<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 HOL.eq}, _) $ t' $ (Const (@{const_name Hilbert_Choice.Eps}, _) $ _) =>
       let

            b andalso is_Free t) args true
       in
         h_property andalso args_property
       end
     | _ => false
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun get_skolem_conc t =
   let
     val t' =
       strip_top_all_vars [] t
       |> snd

      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 {*
+ML \<open>
 fun forall_neg_tac candidate_consts ctxt i = fn st =>
   let
     val gls =
       Thm.prop_of st
       |> Logic.strip_horn

         val attempts = map instantiate candidate_consts
       in
         (fold (curry (op APPEND')) attempts (K no_tac)) i st
       end
   end
-*}
-
-ML {*
+\<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

             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
-*}
-
-ML {*
+\<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

   in
     map (strip_top_All_vars #> snd) conclusions
     |> maps (get_skolem_terms [] [])
     |> distinct (op =)
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun instantiate_skols ctxt consts_candidates i = fn st =>
   let
     val gls =
       Thm.prop_of st
       |> Logic.strip_horn

         fold (curry (op APPEND))
           (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
   in
     tactic st
   end
-*}
-
-ML {*
+\<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 {*
+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 == (~ (! x. ~ P x))" by auto}
    in
      CHANGED (asm_full_simp_tac simpset i)
    end
-*}
+\<close>
 
 
 subsubsection "extuni_dec"
 
-ML {*
+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 =

       Logic.mk_implies (hyp, HOLogic.mk_Trueprop conc)
   in
     Goal.prove ctxt [] [] t (fn _ => auto_tac ctxt)
     |> Drule.export_without_context
   end
-*}
-
-ML {*
+\<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
 *)

                    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

   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 {*
+ML \<open>
 (*Conjunctive counterparts to Term.disjuncts_aux and Term.disjuncts*)
 fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs =
      conjuncts_aux t (conjuncts_aux t' conjs)
   | conjuncts_aux t conjs = t :: conjs
 

 in
   fun imp_strip_horn t =
     imp_strip_horn' [] t
     |> apfst rev
 end
-*}
-
-ML {*
+\<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

          antes)
   in
     if null antes then NONE
     else SOME (ante_type, length antes', pol)
   end
-*}
-
-ML {*
+\<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)

       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
-*}
-
-ML {*
+\<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})
-*}
-
-ML {*
+\<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}]
-*}
-
-ML {*
+\<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

   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 {*
+ML \<open>
 datatype cleanup_feature =
     RemoveHypothesesFromSkolemDefs
   | RemoveDuplicates
 
 datatype loop_feature =

   | Loop of loop_feature list
   | LoopOnce of loop_feature list
   | InnerLoopOnce of loop_feature list
   | CleanUp of cleanup_feature list
   | AbsorbSkolemDefs
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun can_feature x l =
   let
     fun sublist_of_clean_up el =
       case el of
           CleanUp l'' => SOME l''

 @{assert}
   (can_feature (Loop []) [Loop [Existential_Var]]);
 
 @{assert}
   (not (can_feature (Loop []) [InnerLoopOnce [Existential_Var]]));
-*}
-
-ML {*
+\<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 =>

   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 {*
+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 =

   in
     if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then
       ALLGOALS (TRY o dehypothesise_skolem_defs)
     else all_tac
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun remove_duplicates_tac feats =
   (if can_feature (CleanUp [RemoveDuplicates]) feats then
      ALLGOALS distinct_subgoal_tac
    else all_tac)
-*}
-
-ML {*
+\<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 =

     |> TERMFUN (snd (*discard hypotheses*)
                  #> get_skolem_conc_const) NONE
     |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
     |> map Const
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun exists_tac ctxt feats consts_diff =
   let
     val ex_var =
       if loop_can_feature [Existential_Var] feats andalso consts_diff <> [] then
         new_skolem_tac ctxt consts_diff

 
 fun forall_tac ctxt feats =
   if loop_can_feature [Universal] feats then
     forall_pos_tac ctxt
   else K no_tac
-*}
+\<close>
 
 
 subsubsection "Finite types"
 (*lift quantification from a singleton literal to a singleton clause*)
 lemma forall_pos_lift:
 "\<lbrakk>(! X. P X) = True; ! X. (P X = True) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto
 
 (*predicate over the type of the leading quantified variable*)
 
-ML {*
+ML \<open>
 fun extcnf_forall_special_pos_tac ctxt =
   let
     val bool =
       ["True", "False"]
 

     THEN' (assume_tac ctxt
            ORELSE' FIRST'
             (*FIXME could check the type of the leading quantified variable, instead of trying everything*)
             (tacs (bool @ bool_to_bool)))
   end
-*}
+\<close>
 
 
 subsubsection "Emulator"
 
 lemma efq: "[|A = True; A = False|] ==> R" by auto
-ML {*
+ML \<open>
 fun efq_tac ctxt =
   (eresolve_tac ctxt @{thms efq} THEN' assume_tac ctxt)
   ORELSE' assume_tac ctxt
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 (*This is applied to all subgoals, repeatedly*)
 fun extcnf_combined_main ctxt feats consts_diff =
   let
     (*This is applied to subgoals which don't have a conclusion
       consisting of a Skolem definition*)

              not (member (op =) interpreted_consts n))
   in
     if head_of t = Logic.implies then do_diff t
     else []
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 (*remove quantification in hypothesis clause (! X. t), if
   X not free in t*)
 fun remove_redundant_quantification ctxt i = fn st =>
   let
     val gls =

               Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] []
                 @{thm allE} i st
           end
      end
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun remove_redundant_quantification_ignore_skolems ctxt i =
   COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
     no_tac
     (remove_redundant_quantification ctxt i)
-*}
+\<close>
 
 lemma drop_redundant_literal_qtfr:
   "(! X. P) = True \<Longrightarrow> P = True"
   "(? X. P) = True \<Longrightarrow> P = True"
   "(! X. P) = False \<Longrightarrow> P = False"
   "(? X. P) = False \<Longrightarrow> P = False"
 by auto
 
-ML {*
+ML \<open>
 (*remove quantification in the literal "(! X. t) = True/False"
   in the singleton hypothesis clause, if X not free in t*)
 fun remove_redundant_quantification_in_lit ctxt i = fn st =>
   let
     val gls =

                   dresolve_tac ctxt @{thms drop_redundant_literal_qtfr} i st
               end
           end
      end
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun remove_redundant_quantification_in_lit_ignore_skolems ctxt i =
   COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
     no_tac
     (remove_redundant_quantification_in_lit ctxt i)
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun extcnf_combined_tac ctxt prob_name_opt feats skolem_consts = fn st =>
   let
     val thy = Proof_Context.theory_of ctxt
 
     (*Initially, st consists of a single goal, showing the

       THEN IF_UNSOLVED cleanup
 
   in
     DEPTH_SOLVE (CHANGED tec) st
   end
-*}
+\<close>
 
 
 subsubsection "unfold_def"
 
 (*this is used when handling unfold_tac, because the skeleton includes the definitions conjoined with the goal. it turns out that, for my tactic, the definitions are harmful. instead of modifying the skeleton (which may be nontrivial) i'm just dropping the information using this lemma. obviously, and from the name, order matters here.*)

   or reflexive, or else turned back into an object equation
   and broken down further.*)
 lemma un_meta_polarise: "(X \<equiv> True) \<Longrightarrow> X" by auto
 lemma meta_polarise: "X \<Longrightarrow> X \<equiv> True" by auto
 
-ML {*
+ML \<open>
 fun unfold_def_tac ctxt depends_on_defs = fn st =>
   let
     (*This is used when we end up with something like
         (A & B) \<equiv> True \<Longrightarrow> (B & A) \<equiv> True.
       It breaks down this subgoal until it can be trivially

             (unfold_tac ctxt depends_on_defs
              THEN IF_UNSOLVED continue_reducing_tac)))
   in
     tactic st
   end
-*}
+\<close>
 
 
 subsection "Handling split 'preprocessing'"
 
 lemma split_tranfs:

   "(A & B) & C \<equiv> A & B & C"
   "A = B \<equiv> (A --> B) & (B --> A)"
 by (rule eq_reflection, auto)+
 
 (*Same idiom as ex_expander_tac*)
-ML {*
+ML \<open>
 fun split_simp_tac (ctxt : Proof.context) i =
    let
      val simpset =
        fold Simplifier.add_simp @{thms split_tranfs} (empty_simpset ctxt)
    in
      CHANGED (asm_full_simp_tac simpset i)
    end
-*}
+\<close>
 
 
 subsection "Alternative reconstruction tactics"
-ML {*
+ML \<open>
 (*An "auto"-based proof reconstruction, where we attempt to reconstruct each inference
   using auto_tac. A realistic tactic would inspect the inference name and act
   accordingly.*)
 fun auto_based_reconstruction_tac ctxt prob_name n =
   let

       |> the
       |> (fn {inference_fmla, ...} =>
           Goal.prove ctxt [] [] inference_fmla
            (fn pdata => auto_tac (#context pdata)))
   end
-*}
+\<close>
 
 (*An oracle-based reconstruction, which is only used to test the shunting part of the system*)
 oracle oracle_iinterp = "fn t => t"
-ML {*
+ML \<open>
 fun oracle_based_reconstruction_tac ctxt prob_name n =
   let
     val thy = Proof_Context.theory_of ctxt
     val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
   in

      prob_name (#meta pannot) n
       |> the
       |> (fn {inference_fmla, ...} => Thm.cterm_of ctxt inference_fmla)
       |> oracle_iinterp
   end
-*}
+\<close>
 
 
 subsection "Leo2 reconstruction tactic"
 
-ML {*
+ML \<open>
 exception UNSUPPORTED_ROLE
 exception INTERPRET_INFERENCE
 
 (*Failure reports can be adjusted to avoid interrupting
   an overall reconstruction process*)

     | "res" => default_tac
     | "rename" => default_tac
     | "flexflex" => default_tac
     | other => fail ctxt ("Unknown inference rule: " ^ other)
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 fun interpret_leo2_inference ctxt prob_name node =
   let
     val thy = Proof_Context.theory_of ctxt
     val pannot = TPTP_Reconstruct.get_pannot_of_prob thy prob_name
 

           [Pretty.str ("Failed inference reconstruction for '" ^
             inference_name ^ "' at node " ^ node ^ ":\n"),
            Syntax.pretty_term ctxt inference_fmla]))
     | SOME thm => thm
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 (*filter a set of nodes based on which inference rule was used to
   derive a node*)
 fun nodes_by_inference (fms : TPTP_Reconstruct.formula_meaning list) inference_rule =
   let
     fun fold_fun n l =

             if rule_name = inference_rule then n :: l
             else l
   in
     fold fold_fun (map fst fms) []
   end
-*}
+\<close>
 
 
 section "Importing proofs and reconstructing theorems"
 
-ML {*
+ML \<open>
 (*Preprocessing carried out on a LEO-II proof.*)
 fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val dud = ("", Binding.empty, @{term False})

       defs = #defs pannot,
       axs = #axs pannot,
       meta = #meta pannot},
      thy')
   end
-*}
-
-ML {*
+\<close>
+
+ML \<open>
 (*Imports and reconstructs a LEO-II proof.*)
 fun reconstruct_leo2 path thy =
   let
     val prob_file = Path.base path
     val dir = Path.dir path

   in
     (*NOTE we could return the theorem value alone, since
        users could get the thy value from the thm value.*)
     (thy', theorem)
   end
-*}
+\<close>
 
 end