src/HOL/TPTP/atp_problem_import.ML

 *)
 
 signature ATP_PROBLEM_IMPORT =
 sig
   val read_tptp_file : theory -> (string * term -> 'a) -> string ->
-    'a list * ('a list * 'a list) * Proof.context
+    'a list * ('a list * 'a list) * local_theory
   val nitpick_tptp_file : theory -> int -> string -> unit
   val refute_tptp_file : theory -> int -> string -> unit
   val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
   val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
-  val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
+  val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string ->
     int -> tactic
-  val smt_solver_tac : string -> Proof.context -> int -> tactic
-  val freeze_problem_consts : theory -> term -> term
+  val smt_solver_tac : string -> local_theory -> int -> tactic
   val make_conj : term list * term list -> term list -> term
   val sledgehammer_tptp_file : theory -> int -> string -> unit
   val isabelle_tptp_file : theory -> int -> string -> unit
   val isabelle_hot_tptp_file : theory -> int -> string -> unit
   val translate_tptp_file : theory -> string -> string -> unit

     (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u)
   | is_legitimate_tptp_def _ = false
 
 fun nitpick_tptp_file thy timeout file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
-    val thy = Proof_Context.theory_of ctxt
+    val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name
+    val thy = Proof_Context.theory_of lthy
     val (defs, pseudo_defs) = defs
-      |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
+      |> map (ATP_Util.abs_extensionalize_term lthy #> aptrueprop (hol_open_form I))
       |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
         o ATP_Util.unextensionalize_def)
     val nondefs = pseudo_defs @ nondefs
-    val state = Proof.init ctxt
+    val state = Proof.init lthy
     val params =
       [("card", "1-100"),
        ("box", "false"),
        ("max_threads", "1"),
        ("batch_size", "5"),

       (if s = "genuine" then
          if falsify then "CounterSatisfiable" else "Satisfiable"
        else
          "GaveUp")
       |> writeln
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
+    val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name
     val params =
       [("maxtime", string_of_int timeout),
        ("maxvars", "100000")]
   in
-    Refute.refute_term ctxt params (defs @ nondefs)
+    Refute.refute_term lthy params (defs @ nondefs)
       (case conjs of conj :: _ => conj | [] => \<^prop>\<open>True\<close>)
     |> print_szs_of_outcome (not (null conjs))
   end
 
 

     (case result of
       NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
     | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
   end
 
-fun nitpick_finite_oracle_tac ctxt timeout i th =
+fun nitpick_finite_oracle_tac lthy timeout i th =
   let
     fun is_safe (Type (\<^type_name>\<open>fun\<close>, Ts)) = forall is_safe Ts
       | is_safe \<^typ>\<open>prop\<close> = true
       | is_safe \<^typ>\<open>bool\<close> = true
       | is_safe _ = false

   in
     if exists_type (not o is_safe) conj then
       Seq.empty
     else
       let
-        val thy = Proof_Context.theory_of ctxt
-        val state = Proof.init ctxt
+        val thy = Proof_Context.theory_of lthy
+        val state = Proof.init lthy
         val params =
           [("box", "false"),
            ("max_threads", "1"),
            ("verbose", "true"),
            ("debug", if debug then "true" else "false"),

         val step = 0
         val subst = []
         val (outcome, _) =
           Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
       in
-        if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
+        if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac lthy) th else Seq.empty
       end
   end
 
-fun atp_tac ctxt completeness override_params timeout assms prover =
-  let
-    val thy = Proof_Context.theory_of ctxt
+fun atp_tac lthy completeness override_params timeout assms prover =
+  let
+    val thy = Proof_Context.theory_of lthy
     val assm_ths0 = map (Skip_Proof.make_thm thy) assms
-    val ((assm_name, _), ctxt) = ctxt
+    val ((assm_name, _), lthy) = lthy
       |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
       |> Local_Theory.note ((\<^binding>\<open>thms\<close>, []), assm_ths0)
 
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
     val ref_of_assms = (Facts.named assm_name, [])
   in
-    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+    Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy
       ([("debug", if debug then "true" else "false"),
         ("overlord", if overlord then "true" else "false"),
         ("provers", prover),
         ("timeout", string_of_int timeout)] @
        (if completeness > 0 then

           []) @
        override_params)
       {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
   end
 
-fun sledgehammer_tac demo ctxt timeout assms i =
+fun sledgehammer_tac demo lthy timeout assms i =
   let
     val frac = if demo then 16 else 12
     fun slice mult completeness prover =
       SOLVE_TIMEOUT (mult * timeout div frac)
         (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
-        (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
+        (atp_tac lthy completeness [] (mult * timeout div frac) assms prover i)
   in
     slice 2 0 ATP_Proof.spassN
     ORELSE slice 2 0 ATP_Proof.vampireN
     ORELSE slice 2 0 ATP_Proof.eN
     ORELSE slice 2 0 ATP_Proof.z3_tptpN

          ORELSE slice 2 0 ATP_Proof.leo2N
        else
          no_tac)
   end
 
-fun smt_solver_tac solver ctxt =
-  let
-    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
-  in SMT_Solver.smt_tac ctxt [] end
-
-fun auto_etc_tac ctxt timeout assms i =
-  SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
+fun smt_solver_tac solver lthy =
+  let
+    val lthy = lthy |> Context.proof_map (SMT_Config.select_solver solver)
+  in SMT_Solver.smt_tac lthy [] end
+
+fun auto_etc_tac lthy timeout assms i =
+  SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac lthy (timeout div 20) i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac lthy i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
-    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
+    (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN))
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i)
 
 fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
-
-(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
-   unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
-fun freeze_problem_consts thy =
-  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
-    map_aterms
-      (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
-        | t => t)
-  end
 
 fun make_conj (defs, nondefs) conjs =
   Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\<open>False\<close>)
 
 fun print_szs_of_success conjs success =

      else
        "GaveUp"))
 
 fun sledgehammer_tptp_file thy timeout file_name =
   let
-    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
+    val (conjs, assms, lthy) = read_tptp_file thy snd file_name
     val conj = make_conj ([], []) conjs
     val assms = op @ assms
   in
-    can_tac ctxt (fn ctxt => sledgehammer_tac true ctxt timeout assms 1) conj
+    can_tac lthy (fn lthy => sledgehammer_tac true lthy timeout assms 1) conj
     |> print_szs_of_success conjs
   end
 
 fun generic_isabelle_tptp_file demo thy timeout file_name =
   let
-    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
+    val (conjs, assms, lthy) = read_tptp_file thy snd file_name
     val conj = make_conj ([], []) conjs
     val full_conj = make_conj assms conjs
     val assms = op @ assms
     val (last_hope_atp, last_hope_completeness) =
       if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
   in
-    (can_tac ctxt (fn ctxt => auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
-     can_tac ctxt (fn ctxt => sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
-     can_tac ctxt (fn ctxt => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
-       (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
+    (can_tac lthy (fn lthy => auto_etc_tac lthy (timeout div 2) assms 1) full_conj orelse
+     can_tac lthy (fn lthy => sledgehammer_tac demo lthy (timeout div 2) assms 1) conj orelse
+     can_tac lthy (fn lthy => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+       (atp_tac lthy last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
     |> print_szs_of_success conjs
   end
 
 val isabelle_tptp_file = generic_isabelle_tptp_file false
 val isabelle_hot_tptp_file = generic_isabelle_tptp_file true

 
 (** Translator between TPTP(-like) file formats **)
 
 fun translate_tptp_file thy format_str file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
+    val (conjs, (defs, nondefs), lthy) = read_tptp_file thy I file_name
     val conj = make_conj ([], []) (map snd conjs)
 
     val (format, type_enc, lam_trans) =
       (case format_str of
         "FOF" => (FOF, "mono_guards??", liftingN)

     val presimp = true
     val facts =
       map (apfst (rpair (Global, Non_Rec_Def))) defs @
       map (apfst (rpair (Global, General))) nondefs
     val (atp_problem, _, _, _) =
-      generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
+      generate_atp_problem lthy generate_info format Hypothesis (type_enc_of_string Strict type_enc)
         Translator
         lam_trans uncurried_aliases readable_names presimp [] conj facts
 
-    val ord = effective_term_order ctxt spassN
+    val ord = effective_term_order lthy spassN
     val ord_info = K []
     val lines = lines_of_atp_problem format ord ord_info atp_problem
   in
     List.app Output.physical_stdout lines
   end