src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 63167 0909deb8059b
parent 62243 dd22d2423047
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  section "Setup"
     1.6  
     1.7 -ML {*
     1.8 +ML \<open>
     1.9    val tptp_unexceptional_reconstruction = Attrib.setup_config_bool @{binding tptp_unexceptional_reconstruction} (K false)
    1.10    fun unexceptional_reconstruction ctxt = Config.get ctxt tptp_unexceptional_reconstruction
    1.11    val tptp_informative_failure = Attrib.setup_config_bool @{binding tptp_informative_failure} (K false)
    1.12 @@ -67,7 +67,7 @@
    1.13        if max = 0 then false
    1.14        else size > max
    1.15      end
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  (*FIXME move to TPTP_Proof_Reconstruction_Test_Units*)
    1.20  declare [[
    1.21 @@ -87,7 +87,7 @@
    1.22  
    1.23  
    1.24  section "Proof reconstruction"
    1.25 -text {*There are two parts to proof reconstruction:
    1.26 +text \<open>There are two parts to proof reconstruction:
    1.27  \begin{itemize}
    1.28    \item interpreting the inferences
    1.29    \item building the skeleton, which indicates how to compose
    1.30 @@ -144,7 +144,7 @@
    1.31  clause representation to fit them, and adapting the inference
    1.32  interpretation to handle the rules used by the prover. It should also
    1.33  facilitate composing together proofs found by different provers.
    1.34 -*}
    1.35 +\<close>
    1.36  
    1.37  
    1.38  subsection "Instantiation"
    1.39 @@ -159,7 +159,7 @@
    1.40    "\<lbrakk>(\<forall>x. P x) = False; \<And>x. (P x) = False \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    1.41  by auto
    1.42  
    1.43 -ML {*
    1.44 +ML \<open>
    1.45  (*This carries out an allE-like rule but on (polarised) literals.
    1.46   Instead of yielding a free variable (which is a hell for the
    1.47   matcher) it seeks to use one of the subgoals' parameters.
    1.48 @@ -195,9 +195,9 @@
    1.49  
    1.50  (*Attempts to use the polar_allE theorems on a specific subgoal.*)
    1.51  fun forall_pos_tac ctxt = inst_parametermatch_tac ctxt @{thms polar_allE}
    1.52 -*}
    1.53 +\<close>
    1.54  
    1.55 -ML {*
    1.56 +ML \<open>
    1.57  (*This is similar to inst_parametermatch_tac, but prefers to
    1.58    match variables having identical names. Logically, this is
    1.59    a hack. But it reduces the complexity of the problem.*)
    1.60 @@ -233,12 +233,12 @@
    1.61              K no_tac i st
    1.62        end
    1.63    end
    1.64 -*}
    1.65 +\<close>
    1.66  
    1.67  
    1.68  subsection "Prefix massaging"
    1.69  
    1.70 -ML {*
    1.71 +ML \<open>
    1.72  exception NO_GOALS
    1.73  
    1.74  (*Get quantifier prefix of the hypothesis and conclusion, reorder
    1.75 @@ -291,7 +291,7 @@
    1.76          dresolve_tac ctxt [thm] i st
    1.77        end
    1.78      end
    1.79 -*}
    1.80 +\<close>
    1.81  
    1.82  
    1.83  subsection "Some general rules and congruences"
    1.84 @@ -300,14 +300,14 @@
    1.85    applied implicitly during some Leo2 inferences.*)
    1.86  lemma polarise: "P ==> P = True" by auto
    1.87  
    1.88 -ML {*
    1.89 +ML \<open>
    1.90  fun is_polarised t =
    1.91    (TPTP_Reconstruct.remove_polarity true t; true)
    1.92    handle TPTP_Reconstruct.UNPOLARISED _ => false
    1.93  
    1.94  fun polarise_subgoal_hyps ctxt =
    1.95    COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dresolve_tac ctxt @{thms polarise})
    1.96 -*}
    1.97 +\<close>
    1.98  
    1.99  lemma simp_meta [rule_format]:
   1.100    "(A --> B) == (~A | B)"
   1.101 @@ -335,12 +335,12 @@
   1.102  by auto
   1.103  
   1.104  lemma solved_all_splits: "False = True \<Longrightarrow> False" by simp
   1.105 -ML {*
   1.106 +ML \<open>
   1.107  fun solved_all_splits_tac ctxt =
   1.108    TRY (eresolve_tac ctxt @{thms conjE} 1)
   1.109    THEN resolve_tac ctxt @{thms solved_all_splits} 1
   1.110    THEN assume_tac ctxt 1
   1.111 -*}
   1.112 +\<close>
   1.113  
   1.114  lemma lots_of_logic_expansions_meta [rule_format]:
   1.115    "(((A :: bool) = B) = True) == (((A \<longrightarrow> B) = True) & ((B \<longrightarrow> A) = True))"
   1.116 @@ -408,7 +408,7 @@
   1.117  
   1.118  subsection "Emulation: tactics"
   1.119  
   1.120 -ML {*
   1.121 +ML \<open>
   1.122  (*Instantiate a variable according to the info given in the
   1.123    proof annotation. Through this we avoid having to come up
   1.124    with instantiations during reconstruction.*)
   1.125 @@ -441,9 +441,9 @@
   1.126      (*now only the variable to instantiate should be left*)
   1.127      THEN FIRST (map instantiate_tac ordered_instances)
   1.128    end
   1.129 -*}
   1.130 +\<close>
   1.131  
   1.132 -ML {*
   1.133 +ML \<open>
   1.134  (*Simplification tactics*)
   1.135  local
   1.136    fun rew_goal_tac thms ctxt i =
   1.137 @@ -456,7 +456,7 @@
   1.138    val simper_animal =
   1.139      rew_goal_tac @{thms simp_meta}
   1.140  end
   1.141 -*}
   1.142 +\<close>
   1.143  
   1.144  lemma prop_normalise [rule_format]:
   1.145    "(A | B) | C == A | B | C"
   1.146 @@ -464,7 +464,7 @@
   1.147    "A | B == ~(~A & ~B)"
   1.148    "~~ A == A"
   1.149  by auto
   1.150 -ML {*
   1.151 +ML \<open>
   1.152  (*i.e., break_conclusion*)
   1.153  fun flip_conclusion_tac ctxt =
   1.154    let
   1.155 @@ -476,7 +476,7 @@
   1.156    in
   1.157      default_tac ORELSE' resolve_tac ctxt @{thms flip}
   1.158    end
   1.159 -*}
   1.160 +\<close>
   1.161  
   1.162  
   1.163  subsection "Skolemisation"
   1.164 @@ -541,7 +541,7 @@
   1.165  apply (simp, drule someI_ex, simp)
   1.166  done
   1.167  
   1.168 -ML {*
   1.169 +ML \<open>
   1.170  (*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*)
   1.171  fun conc_is_skolem_def t =
   1.172    case t of
   1.173 @@ -574,9 +574,9 @@
   1.174          h_property andalso args_property
   1.175        end
   1.176      | _ => false
   1.177 -*}
   1.178 +\<close>
   1.179  
   1.180 -ML {*
   1.181 +ML \<open>
   1.182  (*Hack used to detect if a Skolem definition, with an LHS Var, has had the LHS instantiated into an unacceptable term.*)
   1.183  fun conc_is_bad_skolem_def t =
   1.184    case t of
   1.185 @@ -610,9 +610,9 @@
   1.186          h_property andalso args_property
   1.187        end
   1.188      | _ => false
   1.189 -*}
   1.190 +\<close>
   1.191  
   1.192 -ML {*
   1.193 +ML \<open>
   1.194  fun get_skolem_conc t =
   1.195    let
   1.196      val t' =
   1.197 @@ -633,7 +633,7 @@
   1.198       |> head_of
   1.199       |> dest_Const)
   1.200     (get_skolem_conc t)
   1.201 -*}
   1.202 +\<close>
   1.203  
   1.204  (*
   1.205  Technique for handling quantifiers:
   1.206 @@ -643,7 +643,7 @@
   1.207       or bind a fresh !! -- currently not doing the latter since it never seems to arised in normal Leo2 proofs.
   1.208  *)
   1.209  
   1.210 -ML {*
   1.211 +ML \<open>
   1.212  fun forall_neg_tac candidate_consts ctxt i = fn st =>
   1.213    let
   1.214      val gls =
   1.215 @@ -678,9 +678,9 @@
   1.216          (fold (curry (op APPEND')) attempts (K no_tac)) i st
   1.217        end
   1.218    end
   1.219 -*}
   1.220 +\<close>
   1.221  
   1.222 -ML {*
   1.223 +ML \<open>
   1.224  exception SKOLEM_DEF of term (*The tactic wasn't pointed at a skolem definition*)
   1.225  exception NO_SKOLEM_DEF of (*skolem const name*)string * Binding.binding * term (*The tactic could not find a skolem definition in the theory*)
   1.226  fun absorb_skolem_def ctxt prob_name_opt i = fn st =>
   1.227 @@ -750,9 +750,9 @@
   1.228      resolve_tac ctxt [Drule.export_without_context thm] i st
   1.229    end
   1.230    handle SKOLEM_DEF _ => no_tac st
   1.231 -*}
   1.232 +\<close>
   1.233  
   1.234 -ML {*
   1.235 +ML \<open>
   1.236  (*
   1.237  In current system, there should only be 2 subgoals: the one where
   1.238  the skolem definition is being built (with a Var in the LHS), and the other subgoal using Var.
   1.239 @@ -801,9 +801,9 @@
   1.240      |> maps (get_skolem_terms [] [])
   1.241      |> distinct (op =)
   1.242    end
   1.243 -*}
   1.244 +\<close>
   1.245  
   1.246 -ML {*
   1.247 +ML \<open>
   1.248  fun instantiate_skols ctxt consts_candidates i = fn st =>
   1.249    let
   1.250      val gls =
   1.251 @@ -953,9 +953,9 @@
   1.252    in
   1.253      tactic st
   1.254    end
   1.255 -*}
   1.256 +\<close>
   1.257  
   1.258 -ML {*
   1.259 +ML \<open>
   1.260  fun new_skolem_tac ctxt consts_candidates =
   1.261    let
   1.262      fun tac thm =
   1.263 @@ -965,12 +965,12 @@
   1.264      if null consts_candidates then K no_tac
   1.265      else FIRST' (map tac @{thms lift_exists})
   1.266    end
   1.267 -*}
   1.268 +\<close>
   1.269  
   1.270  (*
   1.271  need a tactic to expand "? x . P" to "~ ! x. ~ P"
   1.272  *)
   1.273 -ML {*
   1.274 +ML \<open>
   1.275  fun ex_expander_tac ctxt i =
   1.276     let
   1.277       val simpset =
   1.278 @@ -979,12 +979,12 @@
   1.279     in
   1.280       CHANGED (asm_full_simp_tac simpset i)
   1.281     end
   1.282 -*}
   1.283 +\<close>
   1.284  
   1.285  
   1.286  subsubsection "extuni_dec"
   1.287  
   1.288 -ML {*
   1.289 +ML \<open>
   1.290  (*n-ary decomposition. Code is based on the n-ary arg_cong generator*)
   1.291  fun extuni_dec_n ctxt arity =
   1.292    let
   1.293 @@ -1035,9 +1035,9 @@
   1.294      Goal.prove ctxt [] [] t (fn _ => auto_tac ctxt)
   1.295      |> Drule.export_without_context
   1.296    end
   1.297 -*}
   1.298 +\<close>
   1.299  
   1.300 -ML {*
   1.301 +ML \<open>
   1.302  (*Determine the arity of a function which the "dec"
   1.303    unification rule is about to be applied.
   1.304    NOTE:
   1.305 @@ -1157,7 +1157,7 @@
   1.306    in
   1.307      (CHANGED o search_tac) i st
   1.308    end
   1.309 -*}
   1.310 +\<close>
   1.311  
   1.312  
   1.313  subsubsection "standard_cnf"
   1.314 @@ -1178,7 +1178,7 @@
   1.315  stage, together with splitting.
   1.316  *)
   1.317  
   1.318 -ML {*
   1.319 +ML \<open>
   1.320  (*Conjunctive counterparts to Term.disjuncts_aux and Term.disjuncts*)
   1.321  fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs =
   1.322       conjuncts_aux t (conjuncts_aux t' conjs)
   1.323 @@ -1196,9 +1196,9 @@
   1.324      imp_strip_horn' [] t
   1.325      |> apfst rev
   1.326  end
   1.327 -*}
   1.328 +\<close>
   1.329  
   1.330 -ML {*
   1.331 +ML \<open>
   1.332  (*Returns whether the antecedents are separated by conjunctions
   1.333    or implications; the number of antecedents; and the polarity
   1.334    of the original clause -- I think this will always be "false".*)
   1.335 @@ -1254,9 +1254,9 @@
   1.336      if null antes then NONE
   1.337      else SOME (ante_type, length antes', pol)
   1.338    end
   1.339 -*}
   1.340 +\<close>
   1.341  
   1.342 -ML {*
   1.343 +ML \<open>
   1.344  (*Given a certain standard_cnf type, build a metatheorem that would
   1.345    validate it*)
   1.346  fun mk_standard_cnf ctxt kind arity =
   1.347 @@ -1294,9 +1294,9 @@
   1.348      Goal.prove ctxt [] [] t (fn _ => HEADGOAL (blast_tac ctxt))
   1.349      |> Drule.export_without_context
   1.350    end
   1.351 -*}
   1.352 +\<close>
   1.353  
   1.354 -ML {*
   1.355 +ML \<open>
   1.356  (*Applies a d-tactic, then breaks it up conjunctively.
   1.357    This can be used to transform subgoals as follows:
   1.358       (A \<longrightarrow> B) = False  \<Longrightarrow> R
   1.359 @@ -1307,15 +1307,15 @@
   1.360  fun weak_conj_tac ctxt drule =
   1.361    dresolve_tac ctxt [drule] THEN'
   1.362    (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE})
   1.363 -*}
   1.364 +\<close>
   1.365  
   1.366 -ML {*
   1.367 +ML \<open>
   1.368  fun uncurry_lit_neg_tac ctxt =
   1.369    REPEAT_DETERM o
   1.370      dresolve_tac ctxt [@{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}]
   1.371 -*}
   1.372 +\<close>
   1.373  
   1.374 -ML {*
   1.375 +ML \<open>
   1.376  fun standard_cnf_tac ctxt i = fn st =>
   1.377    let
   1.378      fun core_tactic i = fn st =>
   1.379 @@ -1332,12 +1332,12 @@
   1.380       THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt
   1.381       THEN' core_tactic) i st
   1.382    end
   1.383 -*}
   1.384 +\<close>
   1.385  
   1.386  
   1.387  subsubsection "Emulator prep"
   1.388  
   1.389 -ML {*
   1.390 +ML \<open>
   1.391  datatype cleanup_feature =
   1.392      RemoveHypothesesFromSkolemDefs
   1.393    | RemoveDuplicates
   1.394 @@ -1380,9 +1380,9 @@
   1.395    | InnerLoopOnce of loop_feature list
   1.396    | CleanUp of cleanup_feature list
   1.397    | AbsorbSkolemDefs
   1.398 -*}
   1.399 +\<close>
   1.400  
   1.401 -ML {*
   1.402 +ML \<open>
   1.403  fun can_feature x l =
   1.404    let
   1.405      fun sublist_of_clean_up el =
   1.406 @@ -1442,9 +1442,9 @@
   1.407  
   1.408  @{assert}
   1.409    (not (can_feature (Loop []) [InnerLoopOnce [Existential_Var]]));
   1.410 -*}
   1.411 +\<close>
   1.412  
   1.413 -ML {*
   1.414 +ML \<open>
   1.415  exception NO_LOOP_FEATS
   1.416  fun get_loop_feats (feats : feature list) =
   1.417    let
   1.418 @@ -1467,11 +1467,11 @@
   1.419  @{assert}
   1.420    (get_loop_feats [Loop [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal]] =
   1.421     [King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal])
   1.422 -*}
   1.423 +\<close>
   1.424  
   1.425  (*use as elim rule to remove premises*)
   1.426  lemma insa_prems: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> P" by auto
   1.427 -ML {*
   1.428 +ML \<open>
   1.429  fun cleanup_skolem_defs ctxt feats =
   1.430    let
   1.431      (*remove hypotheses from skolem defs,
   1.432 @@ -1485,16 +1485,16 @@
   1.433        ALLGOALS (TRY o dehypothesise_skolem_defs)
   1.434      else all_tac
   1.435    end
   1.436 -*}
   1.437 +\<close>
   1.438  
   1.439 -ML {*
   1.440 +ML \<open>
   1.441  fun remove_duplicates_tac feats =
   1.442    (if can_feature (CleanUp [RemoveDuplicates]) feats then
   1.443       ALLGOALS distinct_subgoal_tac
   1.444     else all_tac)
   1.445 -*}
   1.446 +\<close>
   1.447  
   1.448 -ML {*
   1.449 +ML \<open>
   1.450  (*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*)
   1.451  fun which_skolem_concs_used ctxt = fn st =>
   1.452    let
   1.453 @@ -1512,9 +1512,9 @@
   1.454      |> switch (fold (fn x => fn l => if is_some x then the x :: l else l)) []
   1.455      |> map Const
   1.456    end
   1.457 -*}
   1.458 +\<close>
   1.459  
   1.460 -ML {*
   1.461 +ML \<open>
   1.462  fun exists_tac ctxt feats consts_diff =
   1.463    let
   1.464      val ex_var =
   1.465 @@ -1535,7 +1535,7 @@
   1.466    if loop_can_feature [Universal] feats then
   1.467      forall_pos_tac ctxt
   1.468    else K no_tac
   1.469 -*}
   1.470 +\<close>
   1.471  
   1.472  
   1.473  subsubsection "Finite types"
   1.474 @@ -1545,7 +1545,7 @@
   1.475  
   1.476  (*predicate over the type of the leading quantified variable*)
   1.477  
   1.478 -ML {*
   1.479 +ML \<open>
   1.480  fun extcnf_forall_special_pos_tac ctxt =
   1.481    let
   1.482      val bool =
   1.483 @@ -1565,19 +1565,19 @@
   1.484              (*FIXME could check the type of the leading quantified variable, instead of trying everything*)
   1.485              (tacs (bool @ bool_to_bool)))
   1.486    end
   1.487 -*}
   1.488 +\<close>
   1.489  
   1.490  
   1.491  subsubsection "Emulator"
   1.492  
   1.493  lemma efq: "[|A = True; A = False|] ==> R" by auto
   1.494 -ML {*
   1.495 +ML \<open>
   1.496  fun efq_tac ctxt =
   1.497    (eresolve_tac ctxt @{thms efq} THEN' assume_tac ctxt)
   1.498    ORELSE' assume_tac ctxt
   1.499 -*}
   1.500 +\<close>
   1.501  
   1.502 -ML {*
   1.503 +ML \<open>
   1.504  (*This is applied to all subgoals, repeatedly*)
   1.505  fun extcnf_combined_main ctxt feats consts_diff =
   1.506    let
   1.507 @@ -1697,9 +1697,9 @@
   1.508      if head_of t = Logic.implies then do_diff t
   1.509      else []
   1.510    end
   1.511 -*}
   1.512 +\<close>
   1.513  
   1.514 -ML {*
   1.515 +ML \<open>
   1.516  (*remove quantification in hypothesis clause (! X. t), if
   1.517    X not free in t*)
   1.518  fun remove_redundant_quantification ctxt i = fn st =>
   1.519 @@ -1740,14 +1740,14 @@
   1.520            end
   1.521       end
   1.522    end
   1.523 -*}
   1.524 +\<close>
   1.525  
   1.526 -ML {*
   1.527 +ML \<open>
   1.528  fun remove_redundant_quantification_ignore_skolems ctxt i =
   1.529    COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
   1.530      no_tac
   1.531      (remove_redundant_quantification ctxt i)
   1.532 -*}
   1.533 +\<close>
   1.534  
   1.535  lemma drop_redundant_literal_qtfr:
   1.536    "(! X. P) = True \<Longrightarrow> P = True"
   1.537 @@ -1756,7 +1756,7 @@
   1.538    "(? X. P) = False \<Longrightarrow> P = False"
   1.539  by auto
   1.540  
   1.541 -ML {*
   1.542 +ML \<open>
   1.543  (*remove quantification in the literal "(! X. t) = True/False"
   1.544    in the singleton hypothesis clause, if X not free in t*)
   1.545  fun remove_redundant_quantification_in_lit ctxt i = fn st =>
   1.546 @@ -1808,16 +1808,16 @@
   1.547            end
   1.548       end
   1.549    end
   1.550 -*}
   1.551 +\<close>
   1.552  
   1.553 -ML {*
   1.554 +ML \<open>
   1.555  fun remove_redundant_quantification_in_lit_ignore_skolems ctxt i =
   1.556    COND (TERMPRED (fn _ => true) conc_is_skolem_def (SOME i))
   1.557      no_tac
   1.558      (remove_redundant_quantification_in_lit ctxt i)
   1.559 -*}
   1.560 +\<close>
   1.561  
   1.562 -ML {*
   1.563 +ML \<open>
   1.564  fun extcnf_combined_tac ctxt prob_name_opt feats skolem_consts = fn st =>
   1.565    let
   1.566      val thy = Proof_Context.theory_of ctxt
   1.567 @@ -1889,7 +1889,7 @@
   1.568    in
   1.569      DEPTH_SOLVE (CHANGED tec) st
   1.570    end
   1.571 -*}
   1.572 +\<close>
   1.573  
   1.574  
   1.575  subsubsection "unfold_def"
   1.576 @@ -1904,7 +1904,7 @@
   1.577  lemma un_meta_polarise: "(X \<equiv> True) \<Longrightarrow> X" by auto
   1.578  lemma meta_polarise: "X \<Longrightarrow> X \<equiv> True" by auto
   1.579  
   1.580 -ML {*
   1.581 +ML \<open>
   1.582  fun unfold_def_tac ctxt depends_on_defs = fn st =>
   1.583    let
   1.584      (*This is used when we end up with something like
   1.585 @@ -1946,7 +1946,7 @@
   1.586    in
   1.587      tactic st
   1.588    end
   1.589 -*}
   1.590 +\<close>
   1.591  
   1.592  
   1.593  subsection "Handling split 'preprocessing'"
   1.594 @@ -1960,7 +1960,7 @@
   1.595  by (rule eq_reflection, auto)+
   1.596  
   1.597  (*Same idiom as ex_expander_tac*)
   1.598 -ML {*
   1.599 +ML \<open>
   1.600  fun split_simp_tac (ctxt : Proof.context) i =
   1.601     let
   1.602       val simpset =
   1.603 @@ -1968,11 +1968,11 @@
   1.604     in
   1.605       CHANGED (asm_full_simp_tac simpset i)
   1.606     end
   1.607 -*}
   1.608 +\<close>
   1.609  
   1.610  
   1.611  subsection "Alternative reconstruction tactics"
   1.612 -ML {*
   1.613 +ML \<open>
   1.614  (*An "auto"-based proof reconstruction, where we attempt to reconstruct each inference
   1.615    using auto_tac. A realistic tactic would inspect the inference name and act
   1.616    accordingly.*)
   1.617 @@ -1989,11 +1989,11 @@
   1.618            Goal.prove ctxt [] [] inference_fmla
   1.619             (fn pdata => auto_tac (#context pdata)))
   1.620    end
   1.621 -*}
   1.622 +\<close>
   1.623  
   1.624  (*An oracle-based reconstruction, which is only used to test the shunting part of the system*)
   1.625  oracle oracle_iinterp = "fn t => t"
   1.626 -ML {*
   1.627 +ML \<open>
   1.628  fun oracle_based_reconstruction_tac ctxt prob_name n =
   1.629    let
   1.630      val thy = Proof_Context.theory_of ctxt
   1.631 @@ -2006,12 +2006,12 @@
   1.632        |> (fn {inference_fmla, ...} => Thm.cterm_of ctxt inference_fmla)
   1.633        |> oracle_iinterp
   1.634    end
   1.635 -*}
   1.636 +\<close>
   1.637  
   1.638  
   1.639  subsection "Leo2 reconstruction tactic"
   1.640  
   1.641 -ML {*
   1.642 +ML \<open>
   1.643  exception UNSUPPORTED_ROLE
   1.644  exception INTERPRET_INFERENCE
   1.645  
   1.646 @@ -2171,9 +2171,9 @@
   1.647      | "flexflex" => default_tac
   1.648      | other => fail ctxt ("Unknown inference rule: " ^ other)
   1.649    end
   1.650 -*}
   1.651 +\<close>
   1.652  
   1.653 -ML {*
   1.654 +ML \<open>
   1.655  fun interpret_leo2_inference ctxt prob_name node =
   1.656    let
   1.657      val thy = Proof_Context.theory_of ctxt
   1.658 @@ -2204,9 +2204,9 @@
   1.659             Syntax.pretty_term ctxt inference_fmla]))
   1.660      | SOME thm => thm
   1.661    end
   1.662 -*}
   1.663 +\<close>
   1.664  
   1.665 -ML {*
   1.666 +ML \<open>
   1.667  (*filter a set of nodes based on which inference rule was used to
   1.668    derive a node*)
   1.669  fun nodes_by_inference (fms : TPTP_Reconstruct.formula_meaning list) inference_rule =
   1.670 @@ -2221,12 +2221,12 @@
   1.671    in
   1.672      fold fold_fun (map fst fms) []
   1.673    end
   1.674 -*}
   1.675 +\<close>
   1.676  
   1.677  
   1.678  section "Importing proofs and reconstructing theorems"
   1.679  
   1.680 -ML {*
   1.681 +ML \<open>
   1.682  (*Preprocessing carried out on a LEO-II proof.*)
   1.683  fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
   1.684    let
   1.685 @@ -2256,9 +2256,9 @@
   1.686        meta = #meta pannot},
   1.687       thy')
   1.688    end
   1.689 -*}
   1.690 +\<close>
   1.691  
   1.692 -ML {*
   1.693 +ML \<open>
   1.694  (*Imports and reconstructs a LEO-II proof.*)
   1.695  fun reconstruct_leo2 path thy =
   1.696    let
   1.697 @@ -2280,6 +2280,6 @@
   1.698         users could get the thy value from the thm value.*)
   1.699      (thy', theorem)
   1.700    end
   1.701 -*}
   1.702 +\<close>
   1.703  
   1.704  end