move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
authorblanchet
Mon Aug 09 12:05:48 2010 +0200 (2010-08-09)
changeset 38282319c59682c51
parent 38281 601b7972eef2
child 38283 1dac99cc8dbd
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
src/HOL/IsaMakefile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Sledgehammer.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Aug 09 11:05:45 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 09 12:05:48 2010 +0200
     1.3 @@ -321,9 +321,10 @@
     1.4    Tools/Sledgehammer/metis_tactics.ML \
     1.5    Tools/Sledgehammer/sledgehammer.ML \
     1.6    Tools/Sledgehammer/sledgehammer_fact_filter.ML \
     1.7 -  Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
     1.8 +  Tools/Sledgehammer/sledgehammer_fact_minimize.ML \
     1.9    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.10    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
    1.11 +  Tools/Sledgehammer/sledgehammer_translate.ML \
    1.12    Tools/Sledgehammer/sledgehammer_util.ML \
    1.13    Tools/SMT/cvc3_solver.ML \
    1.14    Tools/SMT/smtlib_interface.ML \
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 09 11:05:45 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 09 12:05:48 2010 +0200
     2.3 @@ -391,7 +391,7 @@
     2.4      val params = Sledgehammer_Isar.default_params thy
     2.5        [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
     2.6      val minimize =
     2.7 -      Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     2.8 +      Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
     2.9      val _ = log separator
    2.10    in
    2.11      case minimize st (these (!named_thms)) of
     3.1 --- a/src/HOL/Sledgehammer.thy	Mon Aug 09 11:05:45 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Mon Aug 09 12:05:48 2010 +0200
     3.3 @@ -20,9 +20,10 @@
     3.4    ("Tools/Sledgehammer/metis_tactics.ML")
     3.5    ("Tools/Sledgehammer/sledgehammer_util.ML")
     3.6    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     3.7 +  ("Tools/Sledgehammer/sledgehammer_translate.ML")
     3.8    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
     3.9    ("Tools/Sledgehammer/sledgehammer.ML")
    3.10 -  ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
    3.11 +  ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
    3.12    ("Tools/Sledgehammer/sledgehammer_isar.ML")
    3.13  begin
    3.14  
    3.15 @@ -100,10 +101,11 @@
    3.16  
    3.17  use "Tools/Sledgehammer/sledgehammer_util.ML"
    3.18  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    3.19 +use "Tools/Sledgehammer/sledgehammer_translate.ML"
    3.20  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    3.21  use "Tools/Sledgehammer/sledgehammer.ML"
    3.22  setup Sledgehammer.setup
    3.23 -use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
    3.24 +use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
    3.25  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.26  setup Metis_Tactics.setup
    3.27  
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 09 11:05:45 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 09 12:05:48 2010 +0200
     4.3 @@ -149,6 +149,8 @@
     4.4      string -> (string * string) list -> theory -> theory
     4.5    val unregister_frac_type : string -> Proof.context -> Proof.context
     4.6    val unregister_frac_type_global : string -> theory -> theory
     4.7 +  val register_codatatype_generic :
     4.8 +    typ -> string -> styp list -> Context.generic -> Context.generic
     4.9    val register_codatatype :
    4.10      typ -> string -> styp list -> Proof.context -> Proof.context
    4.11    val register_codatatype_global :
     5.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 11:05:45 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 12:05:48 2010 +0200
     5.3 @@ -100,7 +100,7 @@
     5.4  val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
     5.5  val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
     5.6  
     5.7 -(*FIXME: requires more use of cterm constructors*)
     5.8 +(* FIXME: Requires more use of cterm constructors. *)
     5.9  fun abstract ct =
    5.10    let
    5.11        val thy = theory_of_cterm ct
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 11:05:45 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 09 12:05:48 2010 +0200
     6.3 @@ -39,7 +39,7 @@
     6.4       atp_run_time_in_msecs: int,
     6.5       output: string,
     6.6       proof: string,
     6.7 -     internal_thm_names: string Vector.vector,
     6.8 +     axiom_names: string Vector.vector,
     6.9       conjecture_shape: int list list}
    6.10    type prover = params -> minimize_command -> problem -> prover_result
    6.11  
    6.12 @@ -64,6 +64,7 @@
    6.13  open Metis_Clauses
    6.14  open Sledgehammer_Util
    6.15  open Sledgehammer_Fact_Filter
    6.16 +open Sledgehammer_Translate
    6.17  open Sledgehammer_Proof_Reconstruct
    6.18  
    6.19  
    6.20 @@ -73,9 +74,6 @@
    6.21     "Async_Manager". *)
    6.22  val das_Tool = "Sledgehammer"
    6.23  
    6.24 -(* Freshness almost guaranteed! *)
    6.25 -val sledgehammer_weak_prefix = "Sledgehammer:"
    6.26 -
    6.27  fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
    6.28  fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
    6.29  val messages = Async_Manager.thread_messages das_Tool "ATP"
    6.30 @@ -112,7 +110,7 @@
    6.31     atp_run_time_in_msecs: int,
    6.32     output: string,
    6.33     proof: string,
    6.34 -   internal_thm_names: string Vector.vector,
    6.35 +   axiom_names: string Vector.vector,
    6.36     conjecture_shape: int list list}
    6.37  
    6.38  type prover = params -> minimize_command -> problem -> prover_result
    6.39 @@ -158,471 +156,6 @@
    6.40                 else
    6.41                   failure))
    6.42  
    6.43 -
    6.44 -(* Clause preparation *)
    6.45 -
    6.46 -datatype fol_formula =
    6.47 -  FOLFormula of {name: string,
    6.48 -                 kind: kind,
    6.49 -                 combformula: (name, combterm) formula,
    6.50 -                 ctypes_sorts: typ list}
    6.51 -
    6.52 -fun mk_anot phi = AConn (ANot, [phi])
    6.53 -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    6.54 -fun mk_ahorn [] phi = phi
    6.55 -  | mk_ahorn (phi :: phis) psi =
    6.56 -    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    6.57 -
    6.58 -fun combformula_for_prop thy =
    6.59 -  let
    6.60 -    val do_term = combterm_from_term thy
    6.61 -    fun do_quant bs q s T t' =
    6.62 -      do_formula ((s, T) :: bs) t'
    6.63 -      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    6.64 -    and do_conn bs c t1 t2 =
    6.65 -      do_formula bs t1 ##>> do_formula bs t2
    6.66 -      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    6.67 -    and do_formula bs t =
    6.68 -      case t of
    6.69 -        @{const Not} $ t1 =>
    6.70 -        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    6.71 -      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    6.72 -        do_quant bs AForall s T t'
    6.73 -      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    6.74 -        do_quant bs AExists s T t'
    6.75 -      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
    6.76 -      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
    6.77 -      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
    6.78 -      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    6.79 -        do_conn bs AIff t1 t2
    6.80 -      | _ => (fn ts => do_term bs (Envir.eta_contract t)
    6.81 -                       |>> AAtom ||> union (op =) ts)
    6.82 -  in do_formula [] end
    6.83 -
    6.84 -(* Converts an elim-rule into an equivalent theorem that does not have the
    6.85 -   predicate variable. Leaves other theorems unchanged. We simply instantiate
    6.86 -   the conclusion variable to False. (Cf. "transform_elim_term" in
    6.87 -   "ATP_Systems".) *)
    6.88 -fun transform_elim_term t =
    6.89 -  case Logic.strip_imp_concl t of
    6.90 -    @{const Trueprop} $ Var (z, @{typ bool}) =>
    6.91 -    subst_Vars [(z, @{const False})] t
    6.92 -  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
    6.93 -  | _ => t
    6.94 -
    6.95 -fun presimplify_term thy =
    6.96 -  Skip_Proof.make_thm thy
    6.97 -  #> Meson.presimplify
    6.98 -  #> prop_of
    6.99 -
   6.100 -fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
   6.101 -fun conceal_bounds Ts t =
   6.102 -  subst_bounds (map (Free o apfst concealed_bound_name)
   6.103 -                    (0 upto length Ts - 1 ~~ Ts), t)
   6.104 -fun reveal_bounds Ts =
   6.105 -  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   6.106 -                    (0 upto length Ts - 1 ~~ Ts))
   6.107 -
   6.108 -fun introduce_combinators_in_term ctxt kind t =
   6.109 -  let
   6.110 -    val thy = ProofContext.theory_of ctxt
   6.111 -    fun aux Ts t =
   6.112 -      case t of
   6.113 -        @{const Not} $ t1 => @{const Not} $ aux Ts t1
   6.114 -      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   6.115 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   6.116 -      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   6.117 -        t0 $ Abs (s, T, aux (T :: Ts) t')
   6.118 -      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.119 -      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.120 -      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.121 -      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   6.122 -          $ t1 $ t2 =>
   6.123 -        t0 $ aux Ts t1 $ aux Ts t2
   6.124 -      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   6.125 -               t
   6.126 -             else
   6.127 -               let
   6.128 -                 val t = t |> conceal_bounds Ts
   6.129 -                           |> Envir.eta_contract
   6.130 -                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
   6.131 -               in
   6.132 -                 t |> cterm_of thy
   6.133 -                   |> Clausifier.introduce_combinators_in_cterm
   6.134 -                   |> singleton (Variable.export ctxt' ctxt)
   6.135 -                   |> prop_of |> Logic.dest_equals |> snd
   6.136 -                   |> reveal_bounds Ts
   6.137 -               end
   6.138 -  in t |> not (Meson.is_fol_term thy t) ? aux [] end
   6.139 -  handle THM _ =>
   6.140 -         (* A type variable of sort "{}" will make abstraction fail. *)
   6.141 -         case kind of
   6.142 -           Axiom => HOLogic.true_const
   6.143 -         | Conjecture => HOLogic.false_const
   6.144 -
   6.145 -(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   6.146 -   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   6.147 -fun freeze_term t =
   6.148 -  let
   6.149 -    fun aux (t $ u) = aux t $ aux u
   6.150 -      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   6.151 -      | aux (Var ((s, i), T)) =
   6.152 -        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   6.153 -      | aux t = t
   6.154 -  in t |> exists_subterm is_Var t ? aux end
   6.155 -
   6.156 -(* making axiom and conjecture formulas *)
   6.157 -fun make_formula ctxt presimp (name, kind, t) =
   6.158 -  let
   6.159 -    val thy = ProofContext.theory_of ctxt
   6.160 -    val t = t |> transform_elim_term
   6.161 -              |> Object_Logic.atomize_term thy
   6.162 -    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
   6.163 -              |> extensionalize_term
   6.164 -              |> presimp ? presimplify_term thy
   6.165 -              |> perhaps (try (HOLogic.dest_Trueprop))
   6.166 -              |> introduce_combinators_in_term ctxt kind
   6.167 -              |> kind = Conjecture ? freeze_term
   6.168 -    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   6.169 -  in
   6.170 -    FOLFormula {name = name, combformula = combformula, kind = kind,
   6.171 -                ctypes_sorts = ctypes_sorts}
   6.172 -  end
   6.173 -
   6.174 -fun make_axiom ctxt presimp (name, th) =
   6.175 -  (name, make_formula ctxt presimp (name, Axiom, prop_of th))
   6.176 -fun make_conjectures ctxt ts =
   6.177 -  map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
   6.178 -       (0 upto length ts - 1) ts
   6.179 -
   6.180 -(** Helper facts **)
   6.181 -
   6.182 -fun count_combterm (CombConst ((s, _), _, _)) =
   6.183 -    Symtab.map_entry s (Integer.add 1)
   6.184 -  | count_combterm (CombVar _) = I
   6.185 -  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   6.186 -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   6.187 -  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   6.188 -  | count_combformula (AAtom tm) = count_combterm tm
   6.189 -fun count_fol_formula (FOLFormula {combformula, ...}) =
   6.190 -  count_combformula combformula
   6.191 -
   6.192 -val optional_helpers =
   6.193 -  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   6.194 -   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   6.195 -   (["c_COMBS"], @{thms COMBS_def})]
   6.196 -val optional_typed_helpers =
   6.197 -  [(["c_True", "c_False"], @{thms True_or_False}),
   6.198 -   (["c_If"], @{thms if_True if_False True_or_False})]
   6.199 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   6.200 -
   6.201 -val init_counters =
   6.202 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   6.203 -                    [optional_helpers, optional_typed_helpers])
   6.204 -
   6.205 -fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   6.206 -  let
   6.207 -    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
   6.208 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   6.209 -  in
   6.210 -    (optional_helpers
   6.211 -     |> full_types ? append optional_typed_helpers
   6.212 -     |> maps (fn (ss, ths) =>
   6.213 -                 if exists is_needed ss then map (`Thm.get_name_hint) ths
   6.214 -                 else [])) @
   6.215 -    (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
   6.216 -    |> map (snd o make_axiom ctxt false)
   6.217 -  end
   6.218 -
   6.219 -fun meta_not t = @{const "==>"} $ t $ @{prop False}
   6.220 -
   6.221 -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   6.222 -  let
   6.223 -    val thy = ProofContext.theory_of ctxt
   6.224 -    (* Remove existing axioms from the conjecture, as this can dramatically
   6.225 -       boost an ATP's performance (for some reason). *)
   6.226 -    val axiom_ts = map (prop_of o snd) axioms
   6.227 -    val hyp_ts =
   6.228 -      if null hyp_ts then
   6.229 -        []
   6.230 -      else
   6.231 -        let
   6.232 -          val axiom_table = fold (Termtab.update o rpair ()) axiom_ts
   6.233 -                                 Termtab.empty
   6.234 -        in hyp_ts |> filter_out (Termtab.defined axiom_table) end
   6.235 -    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   6.236 -    val is_FO = Meson.is_fol_term thy goal_t
   6.237 -    val subs = tfree_classes_of_terms [goal_t]
   6.238 -    val supers = tvar_classes_of_terms axiom_ts
   6.239 -    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   6.240 -    (* TFrees in the conjecture; TVars in the axioms *)
   6.241 -    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
   6.242 -    val (axiom_names, axioms) =
   6.243 -      ListPair.unzip (map (make_axiom ctxt true) axioms)
   6.244 -    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   6.245 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   6.246 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   6.247 -  in
   6.248 -    (Vector.fromList axiom_names,
   6.249 -     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   6.250 -  end
   6.251 -
   6.252 -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   6.253 -
   6.254 -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   6.255 -  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   6.256 -  | fo_term_for_combtyp (CombType (name, tys)) =
   6.257 -    ATerm (name, map fo_term_for_combtyp tys)
   6.258 -
   6.259 -fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   6.260 -    (true, ATerm (class, [ATerm (name, [])]))
   6.261 -  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   6.262 -    (true, ATerm (class, [ATerm (name, [])]))
   6.263 -
   6.264 -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   6.265 -
   6.266 -fun fo_term_for_combterm full_types =
   6.267 -  let
   6.268 -    fun aux top_level u =
   6.269 -      let
   6.270 -        val (head, args) = strip_combterm_comb u
   6.271 -        val (x, ty_args) =
   6.272 -          case head of
   6.273 -            CombConst (name as (s, s'), _, ty_args) =>
   6.274 -            if s = "equal" then
   6.275 -              (if top_level andalso length args = 2 then name
   6.276 -               else ("c_fequal", @{const_name fequal}), [])
   6.277 -            else if top_level then
   6.278 -              case s of
   6.279 -                "c_False" => (("$false", s'), [])
   6.280 -              | "c_True" => (("$true", s'), [])
   6.281 -              | _ => (name, if full_types then [] else ty_args)
   6.282 -            else
   6.283 -              (name, if full_types then [] else ty_args)
   6.284 -          | CombVar (name, _) => (name, [])
   6.285 -          | CombApp _ => raise Fail "impossible \"CombApp\""
   6.286 -        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   6.287 -                          map (aux false) args)
   6.288 -    in
   6.289 -      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   6.290 -    end
   6.291 -  in aux true end
   6.292 -
   6.293 -fun formula_for_combformula full_types =
   6.294 -  let
   6.295 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   6.296 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   6.297 -      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   6.298 -  in aux end
   6.299 -
   6.300 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
   6.301 -  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   6.302 -                (type_literals_for_types ctypes_sorts))
   6.303 -           (formula_for_combformula full_types combformula)
   6.304 -
   6.305 -fun problem_line_for_fact prefix full_types
   6.306 -                          (formula as FOLFormula {name, kind, ...}) =
   6.307 -  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   6.308 -
   6.309 -fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   6.310 -                                                       superclass, ...}) =
   6.311 -  let val ty_arg = ATerm (("T", "T"), []) in
   6.312 -    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   6.313 -         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   6.314 -                           AAtom (ATerm (superclass, [ty_arg]))]))
   6.315 -  end
   6.316 -
   6.317 -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   6.318 -    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   6.319 -  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   6.320 -    (false, ATerm (c, [ATerm (sort, [])]))
   6.321 -
   6.322 -fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   6.323 -                                                ...}) =
   6.324 -  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   6.325 -       mk_ahorn (map (formula_for_fo_literal o apfst not
   6.326 -                      o fo_literal_for_arity_literal) premLits)
   6.327 -                (formula_for_fo_literal
   6.328 -                     (fo_literal_for_arity_literal conclLit)))
   6.329 -
   6.330 -fun problem_line_for_conjecture full_types
   6.331 -                                (FOLFormula {name, kind, combformula, ...}) =
   6.332 -  Fof (conjecture_prefix ^ name, kind,
   6.333 -       formula_for_combformula full_types combformula)
   6.334 -
   6.335 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
   6.336 -  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   6.337 -
   6.338 -fun problem_line_for_free_type lit =
   6.339 -  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
   6.340 -fun problem_lines_for_free_types conjectures =
   6.341 -  let
   6.342 -    val litss = map free_type_literals_for_conjecture conjectures
   6.343 -    val lits = fold (union (op =)) litss []
   6.344 -  in map problem_line_for_free_type lits end
   6.345 -
   6.346 -(** "hBOOL" and "hAPP" **)
   6.347 -
   6.348 -type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   6.349 -
   6.350 -fun consider_term top_level (ATerm ((s, _), ts)) =
   6.351 -  (if is_tptp_variable s then
   6.352 -     I
   6.353 -   else
   6.354 -     let val n = length ts in
   6.355 -       Symtab.map_default
   6.356 -           (s, {min_arity = n, max_arity = 0, sub_level = false})
   6.357 -           (fn {min_arity, max_arity, sub_level} =>
   6.358 -               {min_arity = Int.min (n, min_arity),
   6.359 -                max_arity = Int.max (n, max_arity),
   6.360 -                sub_level = sub_level orelse not top_level})
   6.361 -     end)
   6.362 -  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   6.363 -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   6.364 -  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   6.365 -  | consider_formula (AAtom tm) = consider_term true tm
   6.366 -
   6.367 -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   6.368 -fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   6.369 -
   6.370 -fun const_table_for_problem explicit_apply problem =
   6.371 -  if explicit_apply then NONE
   6.372 -  else SOME (Symtab.empty |> consider_problem problem)
   6.373 -
   6.374 -val tc_fun = make_fixed_type_const @{type_name fun}
   6.375 -
   6.376 -fun min_arity_of thy full_types NONE s =
   6.377 -    (if s = "equal" orelse s = type_wrapper_name orelse
   6.378 -        String.isPrefix type_const_prefix s orelse
   6.379 -        String.isPrefix class_prefix s then
   6.380 -       16383 (* large number *)
   6.381 -     else if full_types then
   6.382 -       0
   6.383 -     else case strip_prefix_and_undo_ascii const_prefix s of
   6.384 -       SOME s' => num_type_args thy (invert_const s')
   6.385 -     | NONE => 0)
   6.386 -  | min_arity_of _ _ (SOME the_const_tab) s =
   6.387 -    case Symtab.lookup the_const_tab s of
   6.388 -      SOME ({min_arity, ...} : const_info) => min_arity
   6.389 -    | NONE => 0
   6.390 -
   6.391 -fun full_type_of (ATerm ((s, _), [ty, _])) =
   6.392 -    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   6.393 -  | full_type_of _ = raise Fail "expected type wrapper"
   6.394 -
   6.395 -fun list_hAPP_rev _ t1 [] = t1
   6.396 -  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   6.397 -    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   6.398 -  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   6.399 -    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   6.400 -                         [full_type_of t2, ty]) in
   6.401 -      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   6.402 -    end
   6.403 -
   6.404 -fun repair_applications_in_term thy full_types const_tab =
   6.405 -  let
   6.406 -    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   6.407 -      if s = type_wrapper_name then
   6.408 -        case ts of
   6.409 -          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   6.410 -        | _ => raise Fail "malformed type wrapper"
   6.411 -      else
   6.412 -        let
   6.413 -          val ts = map (aux NONE) ts
   6.414 -          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   6.415 -        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   6.416 -  in aux NONE end
   6.417 -
   6.418 -fun boolify t = ATerm (`I "hBOOL", [t])
   6.419 -
   6.420 -(* True if the constant ever appears outside of the top-level position in
   6.421 -   literals, or if it appears with different arities (e.g., because of different
   6.422 -   type instantiations). If false, the constant always receives all of its
   6.423 -   arguments and is used as a predicate. *)
   6.424 -fun is_predicate NONE s =
   6.425 -    s = "equal" orelse String.isPrefix type_const_prefix s orelse
   6.426 -    String.isPrefix class_prefix s
   6.427 -  | is_predicate (SOME the_const_tab) s =
   6.428 -    case Symtab.lookup the_const_tab s of
   6.429 -      SOME {min_arity, max_arity, sub_level} =>
   6.430 -      not sub_level andalso min_arity = max_arity
   6.431 -    | NONE => false
   6.432 -
   6.433 -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   6.434 -  if s = type_wrapper_name then
   6.435 -    case ts of
   6.436 -      [_, t' as ATerm ((s', _), _)] =>
   6.437 -      if is_predicate const_tab s' then t' else boolify t
   6.438 -    | _ => raise Fail "malformed type wrapper"
   6.439 -  else
   6.440 -    t |> not (is_predicate const_tab s) ? boolify
   6.441 -
   6.442 -fun close_universally phi =
   6.443 -  let
   6.444 -    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   6.445 -        (is_tptp_variable s andalso not (member (op =) bounds name))
   6.446 -          ? insert (op =) name
   6.447 -        #> fold (term_vars bounds) tms
   6.448 -    fun formula_vars bounds (AQuant (q, xs, phi)) =
   6.449 -        formula_vars (xs @ bounds) phi
   6.450 -      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   6.451 -      | formula_vars bounds (AAtom tm) = term_vars bounds tm
   6.452 -  in
   6.453 -    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   6.454 -  end
   6.455 -
   6.456 -fun repair_formula thy explicit_forall full_types const_tab =
   6.457 -  let
   6.458 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   6.459 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   6.460 -      | aux (AAtom tm) =
   6.461 -        AAtom (tm |> repair_applications_in_term thy full_types const_tab
   6.462 -                  |> repair_predicates_in_term const_tab)
   6.463 -  in aux #> explicit_forall ? close_universally end
   6.464 -
   6.465 -fun repair_problem_line thy explicit_forall full_types const_tab
   6.466 -                        (Fof (ident, kind, phi)) =
   6.467 -  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   6.468 -fun repair_problem_with_const_table thy =
   6.469 -  map o apsnd o map ooo repair_problem_line thy
   6.470 -
   6.471 -fun repair_problem thy explicit_forall full_types explicit_apply problem =
   6.472 -  repair_problem_with_const_table thy explicit_forall full_types
   6.473 -      (const_table_for_problem explicit_apply problem) problem
   6.474 -
   6.475 -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
   6.476 -                    file (conjectures, axioms, helper_facts, class_rel_clauses,
   6.477 -                          arity_clauses) =
   6.478 -  let
   6.479 -    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   6.480 -    val helper_lines =
   6.481 -      map (problem_line_for_fact helper_prefix full_types) helper_facts
   6.482 -    val conjecture_lines =
   6.483 -      map (problem_line_for_conjecture full_types) conjectures
   6.484 -    val tfree_lines = problem_lines_for_free_types conjectures
   6.485 -    val class_rel_lines =
   6.486 -      map problem_line_for_class_rel_clause class_rel_clauses
   6.487 -    val arity_lines = map problem_line_for_arity_clause arity_clauses
   6.488 -    (* Reordering these might or might not confuse the proof reconstruction
   6.489 -       code or the SPASS Flotter hack. *)
   6.490 -    val problem =
   6.491 -      [("Relevant facts", axiom_lines),
   6.492 -       ("Class relationships", class_rel_lines),
   6.493 -       ("Arity declarations", arity_lines),
   6.494 -       ("Helper facts", helper_lines),
   6.495 -       ("Conjectures", conjecture_lines),
   6.496 -       ("Type variables", tfree_lines)]
   6.497 -      |> repair_problem thy explicit_forall full_types explicit_apply
   6.498 -    val (problem, pool) = nice_tptp_problem readable_names problem
   6.499 -    val conjecture_offset =
   6.500 -      length axiom_lines + length class_rel_lines + length arity_lines
   6.501 -      + length helper_lines
   6.502 -    val _ = File.write_list file (strings_for_tptp_problem problem)
   6.503 -  in
   6.504 -    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   6.505 -     conjecture_offset)
   6.506 -  end
   6.507 -
   6.508  fun extract_clause_sequence output =
   6.509    let
   6.510      val tokens_of = String.tokens (not o Char.isAlphaNum)
   6.511 @@ -694,8 +227,6 @@
   6.512                      max_new_relevant_facts_per_iter
   6.513                      (the_default prefers_theory_relevant theory_relevant)
   6.514                      relevance_override goal hyp_ts concl_t
   6.515 -    val (internal_thm_names, formulas) =
   6.516 -      prepare_formulas ctxt full_types hyp_ts concl_t the_axioms
   6.517  
   6.518      (* path to unique problem file *)
   6.519      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   6.520 @@ -760,9 +291,10 @@
   6.521                                              known_failures output
   6.522                in (output, msecs, proof, outcome) end
   6.523              val readable_names = debug andalso overlord
   6.524 -            val (pool, conjecture_offset) =
   6.525 -              write_tptp_file thy readable_names explicit_forall full_types
   6.526 -                              explicit_apply probfile formulas
   6.527 +            val (problem, pool, conjecture_offset, axiom_names) =
   6.528 +              prepare_problem ctxt readable_names explicit_forall full_types
   6.529 +                              explicit_apply hyp_ts concl_t the_axioms
   6.530 +            val _ = File.write_list probfile (strings_for_tptp_problem problem)
   6.531              val conjecture_shape =
   6.532                conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   6.533                |> map single
   6.534 @@ -773,7 +305,7 @@
   6.535                       |> (fn (output, msecs, proof, outcome) =>
   6.536                              (output, msecs0 + msecs, proof, outcome))
   6.537                     | result => result)
   6.538 -          in ((pool, conjecture_shape), result) end
   6.539 +          in ((pool, conjecture_shape, axiom_names), result) end
   6.540          else
   6.541            error ("Bad executable: " ^ Path.implode command ^ ".")
   6.542  
   6.543 @@ -787,24 +319,24 @@
   6.544        else
   6.545          File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   6.546  
   6.547 -    val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
   6.548 +    val ((pool, conjecture_shape, axiom_names),
   6.549 +         (output, msecs, proof, outcome)) =
   6.550        with_path cleanup export run_on (prob_pathname subgoal)
   6.551 -    val (conjecture_shape, internal_thm_names) =
   6.552 +    val (conjecture_shape, axiom_names) =
   6.553        repair_conjecture_shape_and_theorem_names output conjecture_shape
   6.554 -                                                internal_thm_names
   6.555 +                                                axiom_names
   6.556  
   6.557      val (message, used_thm_names) =
   6.558        case outcome of
   6.559          NONE =>
   6.560          proof_text isar_proof
   6.561              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   6.562 -            (full_types, minimize_command, proof, internal_thm_names, th,
   6.563 -             subgoal)
   6.564 +            (full_types, minimize_command, proof, axiom_names, th, subgoal)
   6.565        | SOME failure => (string_for_failure failure ^ "\n", [])
   6.566    in
   6.567      {outcome = outcome, message = message, pool = pool,
   6.568       used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   6.569 -     output = output, proof = proof, internal_thm_names = internal_thm_names,
   6.570 +     output = output, proof = proof, axiom_names = axiom_names,
   6.571       conjecture_shape = conjecture_shape}
   6.572    end
   6.573  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Mon Aug 09 12:05:48 2010 +0200
     7.3 @@ -0,0 +1,174 @@
     7.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
     7.5 +    Author:     Philipp Meyer, TU Muenchen
     7.6 +    Author:     Jasmin Blanchette, TU Muenchen
     7.7 +
     7.8 +Minimization of theorem list for Metis using automatic theorem provers.
     7.9 +*)
    7.10 +
    7.11 +signature SLEDGEHAMMER_FACT_MINIMIZE =
    7.12 +sig
    7.13 +  type params = Sledgehammer.params
    7.14 +
    7.15 +  val minimize_theorems :
    7.16 +    params -> int -> int -> Proof.state -> (string * thm list) list
    7.17 +    -> (string * thm list) list option * string
    7.18 +  val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
    7.19 +end;
    7.20 +
    7.21 +structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
    7.22 +struct
    7.23 +
    7.24 +open ATP_Systems
    7.25 +open Sledgehammer_Util
    7.26 +open Sledgehammer_Fact_Filter
    7.27 +open Sledgehammer_Proof_Reconstruct
    7.28 +open Sledgehammer
    7.29 +
    7.30 +(* wrapper for calling external prover *)
    7.31 +
    7.32 +fun string_for_failure Unprovable = "Unprovable."
    7.33 +  | string_for_failure TimedOut = "Timed out."
    7.34 +  | string_for_failure _ = "Unknown error."
    7.35 +
    7.36 +fun n_theorems name_thms_pairs =
    7.37 +  let val n = length name_thms_pairs in
    7.38 +    string_of_int n ^ " theorem" ^ plural_s n ^
    7.39 +    (if n > 0 then
    7.40 +       ": " ^ space_implode " "
    7.41 +                  (name_thms_pairs
    7.42 +                   |> map (perhaps (try (unprefix chained_prefix)))
    7.43 +                   |> sort_distinct string_ord)
    7.44 +     else
    7.45 +       "")
    7.46 +  end
    7.47 +
    7.48 +fun test_theorems ({debug, verbose, overlord, atps, full_types,
    7.49 +                    relevance_threshold, relevance_convergence, theory_relevant,
    7.50 +                    defs_relevant, isar_proof, isar_shrink_factor,
    7.51 +                    ...} : params)
    7.52 +                  (prover : prover) explicit_apply timeout subgoal state
    7.53 +                  name_thms_pairs =
    7.54 +  let
    7.55 +    val _ =
    7.56 +      priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
    7.57 +    val params =
    7.58 +      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    7.59 +       full_types = full_types, explicit_apply = explicit_apply,
    7.60 +       relevance_threshold = relevance_threshold,
    7.61 +       relevance_convergence = relevance_convergence,
    7.62 +       theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    7.63 +       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    7.64 +       timeout = timeout, minimize_timeout = timeout}
    7.65 +    val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    7.66 +    val {context = ctxt, facts, goal} = Proof.goal state
    7.67 +    val problem =
    7.68 +     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    7.69 +      relevance_override = {add = [], del = [], only = false},
    7.70 +      axioms = SOME axioms}
    7.71 +    val result as {outcome, used_thm_names, ...} =
    7.72 +      prover params (K "") problem
    7.73 +  in
    7.74 +    priority (case outcome of
    7.75 +                NONE =>
    7.76 +                if length used_thm_names = length name_thms_pairs then
    7.77 +                  "Found proof."
    7.78 +                else
    7.79 +                  "Found proof with " ^ n_theorems used_thm_names ^ "."
    7.80 +              | SOME failure => string_for_failure failure);
    7.81 +    result
    7.82 +  end
    7.83 +
    7.84 +(* minimalization of thms *)
    7.85 +
    7.86 +fun filter_used_facts used =
    7.87 +  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
    7.88 +
    7.89 +fun sublinear_minimize _ [] p = p
    7.90 +  | sublinear_minimize test (x :: xs) (seen, result) =
    7.91 +    case test (xs @ seen) of
    7.92 +      result as {outcome = NONE, proof, used_thm_names, ...}
    7.93 +      : prover_result =>
    7.94 +      sublinear_minimize test (filter_used_facts used_thm_names xs)
    7.95 +                         (filter_used_facts used_thm_names seen, result)
    7.96 +    | _ => sublinear_minimize test xs (x :: seen, result)
    7.97 +
    7.98 +(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
    7.99 +   preprocessing time is included in the estimate below but isn't part of the
   7.100 +   timeout. *)
   7.101 +val fudge_msecs = 250
   7.102 +
   7.103 +fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
   7.104 +  | minimize_theorems
   7.105 +        (params as {debug, verbose, overlord, atps as atp :: _, full_types,
   7.106 +                    relevance_threshold, relevance_convergence, theory_relevant,
   7.107 +                    defs_relevant, isar_proof, isar_shrink_factor,
   7.108 +                    minimize_timeout, ...})
   7.109 +        i n state name_thms_pairs =
   7.110 +  let
   7.111 +    val thy = Proof.theory_of state
   7.112 +    val prover = get_prover_fun thy atp
   7.113 +    val msecs = Time.toMilliseconds minimize_timeout
   7.114 +    val _ =
   7.115 +      priority ("Sledgehammer minimize: ATP " ^ quote atp ^
   7.116 +                " with a time limit of " ^ string_of_int msecs ^ " ms.")
   7.117 +    val {context = ctxt, goal, ...} = Proof.goal state
   7.118 +    val (_, hyp_ts, concl_t) = strip_subgoal goal i
   7.119 +    val explicit_apply =
   7.120 +      not (forall (Meson.is_fol_term thy)
   7.121 +                  (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
   7.122 +    fun do_test timeout =
   7.123 +      test_theorems params prover explicit_apply timeout i state
   7.124 +    val timer = Timer.startRealTimer ()
   7.125 +  in
   7.126 +    (case do_test minimize_timeout name_thms_pairs of
   7.127 +       result as {outcome = NONE, pool, used_thm_names,
   7.128 +                  conjecture_shape, ...} =>
   7.129 +       let
   7.130 +         val time = Timer.checkRealTimer timer
   7.131 +         val new_timeout =
   7.132 +           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
   7.133 +           |> Time.fromMilliseconds
   7.134 +         val (min_thms, {proof, axiom_names, ...}) =
   7.135 +           sublinear_minimize (do_test new_timeout)
   7.136 +               (filter_used_facts used_thm_names name_thms_pairs) ([], result)
   7.137 +         val n = length min_thms
   7.138 +         val _ = priority (cat_lines
   7.139 +           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
   7.140 +            (case filter (String.isPrefix chained_prefix o fst) min_thms of
   7.141 +               [] => ""
   7.142 +             | chained => " (including " ^ Int.toString (length chained) ^
   7.143 +                          " chained)") ^ ".")
   7.144 +       in
   7.145 +         (SOME min_thms,
   7.146 +          proof_text isar_proof
   7.147 +              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   7.148 +              (full_types, K "", proof, axiom_names, goal, i) |> fst)
   7.149 +       end
   7.150 +     | {outcome = SOME TimedOut, ...} =>
   7.151 +       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   7.152 +              \option (e.g., \"timeout = " ^
   7.153 +              string_of_int (10 + msecs div 1000) ^ " s\").")
   7.154 +     | {outcome = SOME UnknownError, ...} =>
   7.155 +       (* Failure sometimes mean timeout, unfortunately. *)
   7.156 +       (NONE, "Failure: No proof was found with the current time limit. You \
   7.157 +              \can increase the time limit using the \"timeout\" \
   7.158 +              \option (e.g., \"timeout = " ^
   7.159 +              string_of_int (10 + msecs div 1000) ^ " s\").")
   7.160 +     | {message, ...} => (NONE, "ATP error: " ^ message))
   7.161 +    handle ERROR msg => (NONE, "Error: " ^ msg)
   7.162 +  end
   7.163 +
   7.164 +fun run_minimize params i refs state =
   7.165 +  let
   7.166 +    val ctxt = Proof.context_of state
   7.167 +    val chained_ths = #facts (Proof.goal state)
   7.168 +    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
   7.169 +  in
   7.170 +    case subgoal_count state of
   7.171 +      0 => priority "No subgoal!"
   7.172 +    | n =>
   7.173 +      (kill_atps ();
   7.174 +       priority (#2 (minimize_theorems params i n state name_thms_pairs)))
   7.175 +  end
   7.176 +
   7.177 +end;
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Aug 09 11:05:45 2010 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,174 +0,0 @@
     8.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
     8.5 -    Author:     Philipp Meyer, TU Muenchen
     8.6 -    Author:     Jasmin Blanchette, TU Muenchen
     8.7 -
     8.8 -Minimization of theorem list for Metis using automatic theorem provers.
     8.9 -*)
    8.10 -
    8.11 -signature SLEDGEHAMMER_FACT_MINIMIZER =
    8.12 -sig
    8.13 -  type params = Sledgehammer.params
    8.14 -
    8.15 -  val minimize_theorems :
    8.16 -    params -> int -> int -> Proof.state -> (string * thm list) list
    8.17 -    -> (string * thm list) list option * string
    8.18 -  val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
    8.19 -end;
    8.20 -
    8.21 -structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
    8.22 -struct
    8.23 -
    8.24 -open ATP_Systems
    8.25 -open Sledgehammer_Util
    8.26 -open Sledgehammer_Fact_Filter
    8.27 -open Sledgehammer_Proof_Reconstruct
    8.28 -open Sledgehammer
    8.29 -
    8.30 -(* wrapper for calling external prover *)
    8.31 -
    8.32 -fun string_for_failure Unprovable = "Unprovable."
    8.33 -  | string_for_failure TimedOut = "Timed out."
    8.34 -  | string_for_failure _ = "Unknown error."
    8.35 -
    8.36 -fun n_theorems name_thms_pairs =
    8.37 -  let val n = length name_thms_pairs in
    8.38 -    string_of_int n ^ " theorem" ^ plural_s n ^
    8.39 -    (if n > 0 then
    8.40 -       ": " ^ space_implode " "
    8.41 -                  (name_thms_pairs
    8.42 -                   |> map (perhaps (try (unprefix chained_prefix)))
    8.43 -                   |> sort_distinct string_ord)
    8.44 -     else
    8.45 -       "")
    8.46 -  end
    8.47 -
    8.48 -fun test_theorems ({debug, verbose, overlord, atps, full_types,
    8.49 -                    relevance_threshold, relevance_convergence, theory_relevant,
    8.50 -                    defs_relevant, isar_proof, isar_shrink_factor,
    8.51 -                    ...} : params)
    8.52 -                  (prover : prover) explicit_apply timeout subgoal state
    8.53 -                  name_thms_pairs =
    8.54 -  let
    8.55 -    val _ =
    8.56 -      priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
    8.57 -    val params =
    8.58 -      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    8.59 -       full_types = full_types, explicit_apply = explicit_apply,
    8.60 -       relevance_threshold = relevance_threshold,
    8.61 -       relevance_convergence = relevance_convergence,
    8.62 -       theory_relevant = theory_relevant, defs_relevant = defs_relevant,
    8.63 -       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    8.64 -       timeout = timeout, minimize_timeout = timeout}
    8.65 -    val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    8.66 -    val {context = ctxt, facts, goal} = Proof.goal state
    8.67 -    val problem =
    8.68 -     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    8.69 -      relevance_override = {add = [], del = [], only = false},
    8.70 -      axioms = SOME axioms}
    8.71 -    val result as {outcome, used_thm_names, ...} =
    8.72 -      prover params (K "") problem
    8.73 -  in
    8.74 -    priority (case outcome of
    8.75 -                NONE =>
    8.76 -                if length used_thm_names = length name_thms_pairs then
    8.77 -                  "Found proof."
    8.78 -                else
    8.79 -                  "Found proof with " ^ n_theorems used_thm_names ^ "."
    8.80 -              | SOME failure => string_for_failure failure);
    8.81 -    result
    8.82 -  end
    8.83 -
    8.84 -(* minimalization of thms *)
    8.85 -
    8.86 -fun filter_used_facts used =
    8.87 -  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
    8.88 -
    8.89 -fun sublinear_minimize _ [] p = p
    8.90 -  | sublinear_minimize test (x :: xs) (seen, result) =
    8.91 -    case test (xs @ seen) of
    8.92 -      result as {outcome = NONE, proof, used_thm_names, ...}
    8.93 -      : prover_result =>
    8.94 -      sublinear_minimize test (filter_used_facts used_thm_names xs)
    8.95 -                         (filter_used_facts used_thm_names seen, result)
    8.96 -    | _ => sublinear_minimize test xs (x :: seen, result)
    8.97 -
    8.98 -(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
    8.99 -   preprocessing time is included in the estimate below but isn't part of the
   8.100 -   timeout. *)
   8.101 -val fudge_msecs = 250
   8.102 -
   8.103 -fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
   8.104 -  | minimize_theorems
   8.105 -        (params as {debug, verbose, overlord, atps as atp :: _, full_types,
   8.106 -                    relevance_threshold, relevance_convergence, theory_relevant,
   8.107 -                    defs_relevant, isar_proof, isar_shrink_factor,
   8.108 -                    minimize_timeout, ...})
   8.109 -        i n state name_thms_pairs =
   8.110 -  let
   8.111 -    val thy = Proof.theory_of state
   8.112 -    val prover = get_prover_fun thy atp
   8.113 -    val msecs = Time.toMilliseconds minimize_timeout
   8.114 -    val _ =
   8.115 -      priority ("Sledgehammer minimizer: ATP " ^ quote atp ^
   8.116 -                " with a time limit of " ^ string_of_int msecs ^ " ms.")
   8.117 -    val {context = ctxt, goal, ...} = Proof.goal state
   8.118 -    val (_, hyp_ts, concl_t) = strip_subgoal goal i
   8.119 -    val explicit_apply =
   8.120 -      not (forall (Meson.is_fol_term thy)
   8.121 -                  (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
   8.122 -    fun do_test timeout =
   8.123 -      test_theorems params prover explicit_apply timeout i state
   8.124 -    val timer = Timer.startRealTimer ()
   8.125 -  in
   8.126 -    (case do_test minimize_timeout name_thms_pairs of
   8.127 -       result as {outcome = NONE, pool, used_thm_names,
   8.128 -                  conjecture_shape, ...} =>
   8.129 -       let
   8.130 -         val time = Timer.checkRealTimer timer
   8.131 -         val new_timeout =
   8.132 -           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
   8.133 -           |> Time.fromMilliseconds
   8.134 -         val (min_thms, {proof, internal_thm_names, ...}) =
   8.135 -           sublinear_minimize (do_test new_timeout)
   8.136 -               (filter_used_facts used_thm_names name_thms_pairs) ([], result)
   8.137 -         val n = length min_thms
   8.138 -         val _ = priority (cat_lines
   8.139 -           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
   8.140 -            (case filter (String.isPrefix chained_prefix o fst) min_thms of
   8.141 -               [] => ""
   8.142 -             | chained => " (including " ^ Int.toString (length chained) ^
   8.143 -                          " chained)") ^ ".")
   8.144 -       in
   8.145 -         (SOME min_thms,
   8.146 -          proof_text isar_proof
   8.147 -              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   8.148 -              (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
   8.149 -       end
   8.150 -     | {outcome = SOME TimedOut, ...} =>
   8.151 -       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
   8.152 -              \option (e.g., \"timeout = " ^
   8.153 -              string_of_int (10 + msecs div 1000) ^ " s\").")
   8.154 -     | {outcome = SOME UnknownError, ...} =>
   8.155 -       (* Failure sometimes mean timeout, unfortunately. *)
   8.156 -       (NONE, "Failure: No proof was found with the current time limit. You \
   8.157 -              \can increase the time limit using the \"timeout\" \
   8.158 -              \option (e.g., \"timeout = " ^
   8.159 -              string_of_int (10 + msecs div 1000) ^ " s\").")
   8.160 -     | {message, ...} => (NONE, "ATP error: " ^ message))
   8.161 -    handle ERROR msg => (NONE, "Error: " ^ msg)
   8.162 -  end
   8.163 -
   8.164 -fun run_minimizer params i refs state =
   8.165 -  let
   8.166 -    val ctxt = Proof.context_of state
   8.167 -    val chained_ths = #facts (Proof.goal state)
   8.168 -    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
   8.169 -  in
   8.170 -    case subgoal_count state of
   8.171 -      0 => priority "No subgoal!"
   8.172 -    | n =>
   8.173 -      (kill_atps ();
   8.174 -       priority (#2 (minimize_theorems params i n state name_thms_pairs)))
   8.175 -  end
   8.176 -
   8.177 -end;
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 09 11:05:45 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 09 12:05:48 2010 +0200
     9.3 @@ -20,7 +20,7 @@
     9.4  open ATP_Systems
     9.5  open Sledgehammer_Util
     9.6  open Sledgehammer
     9.7 -open Sledgehammer_Fact_Minimizer
     9.8 +open Sledgehammer_Fact_Minimize
     9.9  
    9.10  (** Sledgehammer commands **)
    9.11  
    9.12 @@ -226,9 +226,9 @@
    9.13                           (minimize_command override_params i) state
    9.14        end
    9.15      else if subcommand = minimizeN then
    9.16 -      run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
    9.17 -                                override_params))
    9.18 -                    (the_default 1 opt_i) (#add relevance_override) state
    9.19 +      run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
    9.20 +                               override_params))
    9.21 +                   (the_default 1 opt_i) (#add relevance_override) state
    9.22      else if subcommand = messagesN then
    9.23        messages opt_i
    9.24      else if subcommand = available_atpsN then
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Aug 09 11:05:45 2010 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Aug 09 12:05:48 2010 +0200
    10.3 @@ -10,12 +10,6 @@
    10.4  sig
    10.5    type minimize_command = string list -> string
    10.6  
    10.7 -  val axiom_prefix : string
    10.8 -  val conjecture_prefix : string
    10.9 -  val helper_prefix : string
   10.10 -  val class_rel_clause_prefix : string
   10.11 -  val arity_clause_prefix : string
   10.12 -  val tfrees_name : string
   10.13    val metis_line: bool -> int -> int -> string list -> string
   10.14    val metis_proof_text:
   10.15      bool * minimize_command * string * string vector * thm * int
   10.16 @@ -37,16 +31,10 @@
   10.17  open Metis_Clauses
   10.18  open Sledgehammer_Util
   10.19  open Sledgehammer_Fact_Filter
   10.20 +open Sledgehammer_Translate
   10.21  
   10.22  type minimize_command = string list -> string
   10.23  
   10.24 -val axiom_prefix = "ax_"
   10.25 -val conjecture_prefix = "conj_"
   10.26 -val helper_prefix = "help_"
   10.27 -val class_rel_clause_prefix = "clrel_";
   10.28 -val arity_clause_prefix = "arity_"
   10.29 -val tfrees_name = "tfrees"
   10.30 -
   10.31  (* Simple simplifications to ensure that sort annotations don't leave a trail of
   10.32     spurious "True"s. *)
   10.33  fun s_not @{const False} = @{const True}
   10.34 @@ -71,9 +59,9 @@
   10.35  fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
   10.36  
   10.37  fun index_in_shape x = find_index (exists (curry (op =) x))
   10.38 -fun is_axiom_number thm_names num =
   10.39 -  num > 0 andalso num <= Vector.length thm_names andalso
   10.40 -  Vector.sub (thm_names, num - 1) <> ""
   10.41 +fun is_axiom_number axiom_names num =
   10.42 +  num > 0 andalso num <= Vector.length axiom_names andalso
   10.43 +  Vector.sub (axiom_names, num - 1) <> ""
   10.44  fun is_conjecture_number conjecture_shape num =
   10.45    index_in_shape num conjecture_shape >= 0
   10.46  
   10.47 @@ -491,10 +479,10 @@
   10.48  (* Discard axioms; consolidate adjacent lines that prove the same formula, since
   10.49     they differ only in type information.*)
   10.50  fun add_line _ _ (line as Definition _) lines = line :: lines
   10.51 -  | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
   10.52 +  | add_line conjecture_shape axiom_names (Inference (num, t, [])) lines =
   10.53      (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   10.54         definitions. *)
   10.55 -    if is_axiom_number thm_names num then
   10.56 +    if is_axiom_number axiom_names num then
   10.57        (* Axioms are not proof lines. *)
   10.58        if is_only_type_information t then
   10.59          map (replace_deps_in_line (num, [])) lines
   10.60 @@ -540,10 +528,10 @@
   10.61  
   10.62  fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
   10.63      (j, line :: map (replace_deps_in_line (num, [])) lines)
   10.64 -  | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
   10.65 +  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   10.66                       (Inference (num, t, deps)) (j, lines) =
   10.67      (j + 1,
   10.68 -     if is_axiom_number thm_names num orelse
   10.69 +     if is_axiom_number axiom_names num orelse
   10.70          is_conjecture_number conjecture_shape num orelse
   10.71          (not (is_only_type_information t) andalso
   10.72           null (Term.add_tvars t []) andalso
   10.73 @@ -562,16 +550,18 @@
   10.74     (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
   10.75     the first number (108) is extracted. For Vampire, we look for
   10.76     "108. ... [input]". *)
   10.77 -fun used_facts_in_atp_proof thm_names atp_proof =
   10.78 +fun used_facts_in_atp_proof axiom_names atp_proof =
   10.79    let
   10.80      fun axiom_name num =
   10.81        let val j = Int.fromString num |> the_default ~1 in
   10.82 -        if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1))
   10.83 -        else NONE
   10.84 +        if is_axiom_number axiom_names j then
   10.85 +          SOME (Vector.sub (axiom_names, j - 1))
   10.86 +        else
   10.87 +          NONE
   10.88        end
   10.89      val tokens_of =
   10.90        String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
   10.91 -    val thm_name_list = Vector.foldr (op ::) [] thm_names
   10.92 +    val thm_name_list = Vector.foldr (op ::) [] axiom_names
   10.93      fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
   10.94          (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
   10.95             SOME name =>
   10.96 @@ -617,16 +607,16 @@
   10.97  
   10.98  val unprefix_chained = perhaps (try (unprefix chained_prefix))
   10.99  
  10.100 -fun used_facts thm_names =
  10.101 -  used_facts_in_atp_proof thm_names
  10.102 +fun used_facts axiom_names =
  10.103 +  used_facts_in_atp_proof axiom_names
  10.104    #> List.partition (String.isPrefix chained_prefix)
  10.105    #>> map (unprefix chained_prefix)
  10.106    #> pairself (sort_distinct string_ord)
  10.107  
  10.108 -fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
  10.109 -                      i) =
  10.110 +fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
  10.111 +                      goal, i) =
  10.112    let
  10.113 -    val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof
  10.114 +    val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
  10.115      val lemmas = other_lemmas @ chained_lemmas
  10.116      val n = Logic.count_prems (prop_of goal)
  10.117    in
  10.118 @@ -656,9 +646,9 @@
  10.119  fun smart_case_split [] facts = ByMetis facts
  10.120    | smart_case_split proofs facts = CaseSplit (proofs, facts)
  10.121  
  10.122 -fun add_fact_from_dep thm_names num =
  10.123 -  if is_axiom_number thm_names num then
  10.124 -    apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
  10.125 +fun add_fact_from_dep axiom_names num =
  10.126 +  if is_axiom_number axiom_names num then
  10.127 +    apsnd (insert (op =) (Vector.sub (axiom_names, num - 1)))
  10.128    else
  10.129      apfst (insert (op =) (raw_prefix, num))
  10.130  
  10.131 @@ -667,27 +657,27 @@
  10.132  
  10.133  fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
  10.134    | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
  10.135 -  | step_for_line thm_names j (Inference (num, t, deps)) =
  10.136 +  | step_for_line axiom_names j (Inference (num, t, deps)) =
  10.137      Have (if j = 1 then [Show] else [], (raw_prefix, num),
  10.138            forall_vars t,
  10.139 -          ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
  10.140 +          ByMetis (fold (add_fact_from_dep axiom_names) deps ([], [])))
  10.141  
  10.142  fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
  10.143 -                         atp_proof conjecture_shape thm_names params frees =
  10.144 +                         atp_proof conjecture_shape axiom_names params frees =
  10.145    let
  10.146      val lines =
  10.147        atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
  10.148        |> parse_proof pool
  10.149        |> sort (int_ord o pairself raw_step_number)
  10.150        |> decode_lines ctxt full_types tfrees
  10.151 -      |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
  10.152 +      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
  10.153        |> rpair [] |-> fold_rev add_nontrivial_line
  10.154        |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
  10.155 -                                               conjecture_shape thm_names frees)
  10.156 +                                             conjecture_shape axiom_names frees)
  10.157        |> snd
  10.158    in
  10.159      (if null params then [] else [Fix params]) @
  10.160 -    map2 (step_for_line thm_names) (length lines downto 1) lines
  10.161 +    map2 (step_for_line axiom_names) (length lines downto 1) lines
  10.162    end
  10.163  
  10.164  (* When redirecting proofs, we keep information about the labels seen so far in
  10.165 @@ -995,8 +985,8 @@
  10.166    in do_proof end
  10.167  
  10.168  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
  10.169 -                    (other_params as (full_types, _, atp_proof, thm_names, goal,
  10.170 -                                      i)) =
  10.171 +                    (other_params as (full_types, _, atp_proof, axiom_names,
  10.172 +                                      goal, i)) =
  10.173    let
  10.174      val (params, hyp_ts, concl_t) = strip_subgoal goal i
  10.175      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
  10.176 @@ -1005,7 +995,7 @@
  10.177      val (one_line_proof, lemma_names) = metis_proof_text other_params
  10.178      fun isar_proof_for () =
  10.179        case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
  10.180 -                                atp_proof conjecture_shape thm_names params
  10.181 +                                atp_proof conjecture_shape axiom_names params
  10.182                                  frees
  10.183             |> redirect_proof conjecture_shape hyp_ts concl_t
  10.184             |> kill_duplicate_assumptions_in_proof
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 09 12:05:48 2010 +0200
    11.3 @@ -0,0 +1,505 @@
    11.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
    11.5 +    Author:     Fabian Immler, TU Muenchen
    11.6 +    Author:     Makarius
    11.7 +    Author:     Jasmin Blanchette, TU Muenchen
    11.8 +
    11.9 +Translation of HOL to FOL.
   11.10 +*)
   11.11 +
   11.12 +signature SLEDGEHAMMER_TRANSLATE =
   11.13 +sig
   11.14 +  type 'a problem = 'a ATP_Problem.problem
   11.15 +
   11.16 +  val axiom_prefix : string
   11.17 +  val conjecture_prefix : string
   11.18 +  val helper_prefix : string
   11.19 +  val class_rel_clause_prefix : string
   11.20 +  val arity_clause_prefix : string
   11.21 +  val tfrees_name : string
   11.22 +  val prepare_problem :
   11.23 +    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
   11.24 +    -> (string * thm) list
   11.25 +    -> string problem * string Symtab.table * int * string Vector.vector
   11.26 +end;
   11.27 +
   11.28 +structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
   11.29 +struct
   11.30 +
   11.31 +open ATP_Problem
   11.32 +open Metis_Clauses
   11.33 +open Sledgehammer_Util
   11.34 +
   11.35 +val axiom_prefix = "ax_"
   11.36 +val conjecture_prefix = "conj_"
   11.37 +val helper_prefix = "help_"
   11.38 +val class_rel_clause_prefix = "clrel_";
   11.39 +val arity_clause_prefix = "arity_"
   11.40 +val tfrees_name = "tfrees"
   11.41 +
   11.42 +(* Freshness almost guaranteed! *)
   11.43 +val sledgehammer_weak_prefix = "Sledgehammer:"
   11.44 +
   11.45 +datatype fol_formula =
   11.46 +  FOLFormula of {name: string,
   11.47 +                 kind: kind,
   11.48 +                 combformula: (name, combterm) formula,
   11.49 +                 ctypes_sorts: typ list}
   11.50 +
   11.51 +fun mk_anot phi = AConn (ANot, [phi])
   11.52 +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
   11.53 +fun mk_ahorn [] phi = phi
   11.54 +  | mk_ahorn (phi :: phis) psi =
   11.55 +    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
   11.56 +
   11.57 +fun combformula_for_prop thy =
   11.58 +  let
   11.59 +    val do_term = combterm_from_term thy
   11.60 +    fun do_quant bs q s T t' =
   11.61 +      do_formula ((s, T) :: bs) t'
   11.62 +      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
   11.63 +    and do_conn bs c t1 t2 =
   11.64 +      do_formula bs t1 ##>> do_formula bs t2
   11.65 +      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
   11.66 +    and do_formula bs t =
   11.67 +      case t of
   11.68 +        @{const Not} $ t1 =>
   11.69 +        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
   11.70 +      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   11.71 +        do_quant bs AForall s T t'
   11.72 +      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   11.73 +        do_quant bs AExists s T t'
   11.74 +      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
   11.75 +      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
   11.76 +      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
   11.77 +      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   11.78 +        do_conn bs AIff t1 t2
   11.79 +      | _ => (fn ts => do_term bs (Envir.eta_contract t)
   11.80 +                       |>> AAtom ||> union (op =) ts)
   11.81 +  in do_formula [] end
   11.82 +
   11.83 +(* Converts an elim-rule into an equivalent theorem that does not have the
   11.84 +   predicate variable. Leaves other theorems unchanged. We simply instantiate
   11.85 +   the conclusion variable to False. (Cf. "transform_elim_term" in
   11.86 +   "ATP_Systems".) *)
   11.87 +fun transform_elim_term t =
   11.88 +  case Logic.strip_imp_concl t of
   11.89 +    @{const Trueprop} $ Var (z, @{typ bool}) =>
   11.90 +    subst_Vars [(z, @{const False})] t
   11.91 +  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
   11.92 +  | _ => t
   11.93 +
   11.94 +fun presimplify_term thy =
   11.95 +  Skip_Proof.make_thm thy
   11.96 +  #> Meson.presimplify
   11.97 +  #> prop_of
   11.98 +
   11.99 +fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
  11.100 +fun conceal_bounds Ts t =
  11.101 +  subst_bounds (map (Free o apfst concealed_bound_name)
  11.102 +                    (0 upto length Ts - 1 ~~ Ts), t)
  11.103 +fun reveal_bounds Ts =
  11.104 +  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
  11.105 +                    (0 upto length Ts - 1 ~~ Ts))
  11.106 +
  11.107 +fun introduce_combinators_in_term ctxt kind t =
  11.108 +  let
  11.109 +    val thy = ProofContext.theory_of ctxt
  11.110 +    fun aux Ts t =
  11.111 +      case t of
  11.112 +        @{const Not} $ t1 => @{const Not} $ aux Ts t1
  11.113 +      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
  11.114 +        t0 $ Abs (s, T, aux (T :: Ts) t')
  11.115 +      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
  11.116 +        t0 $ Abs (s, T, aux (T :: Ts) t')
  11.117 +      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  11.118 +      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  11.119 +      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  11.120 +      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
  11.121 +          $ t1 $ t2 =>
  11.122 +        t0 $ aux Ts t1 $ aux Ts t2
  11.123 +      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
  11.124 +               t
  11.125 +             else
  11.126 +               let
  11.127 +                 val t = t |> conceal_bounds Ts
  11.128 +                           |> Envir.eta_contract
  11.129 +                 val ([t], ctxt') = Variable.import_terms true [t] ctxt
  11.130 +               in
  11.131 +                 t |> cterm_of thy
  11.132 +                   |> Clausifier.introduce_combinators_in_cterm
  11.133 +                   |> singleton (Variable.export ctxt' ctxt)
  11.134 +                   |> prop_of |> Logic.dest_equals |> snd
  11.135 +                   |> reveal_bounds Ts
  11.136 +               end
  11.137 +  in t |> not (Meson.is_fol_term thy t) ? aux [] end
  11.138 +  handle THM _ =>
  11.139 +         (* A type variable of sort "{}" will make abstraction fail. *)
  11.140 +         case kind of
  11.141 +           Axiom => HOLogic.true_const
  11.142 +         | Conjecture => HOLogic.false_const
  11.143 +
  11.144 +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
  11.145 +   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
  11.146 +fun freeze_term t =
  11.147 +  let
  11.148 +    fun aux (t $ u) = aux t $ aux u
  11.149 +      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
  11.150 +      | aux (Var ((s, i), T)) =
  11.151 +        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  11.152 +      | aux t = t
  11.153 +  in t |> exists_subterm is_Var t ? aux end
  11.154 +
  11.155 +(* making axiom and conjecture formulas *)
  11.156 +fun make_formula ctxt presimp (name, kind, t) =
  11.157 +  let
  11.158 +    val thy = ProofContext.theory_of ctxt
  11.159 +    val t = t |> transform_elim_term
  11.160 +              |> Object_Logic.atomize_term thy
  11.161 +    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
  11.162 +              |> extensionalize_term
  11.163 +              |> presimp ? presimplify_term thy
  11.164 +              |> perhaps (try (HOLogic.dest_Trueprop))
  11.165 +              |> introduce_combinators_in_term ctxt kind
  11.166 +              |> kind = Conjecture ? freeze_term
  11.167 +    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
  11.168 +  in
  11.169 +    FOLFormula {name = name, combformula = combformula, kind = kind,
  11.170 +                ctypes_sorts = ctypes_sorts}
  11.171 +  end
  11.172 +
  11.173 +fun make_axiom ctxt presimp (name, th) =
  11.174 +  (name, make_formula ctxt presimp (name, Axiom, prop_of th))
  11.175 +fun make_conjectures ctxt ts =
  11.176 +  map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
  11.177 +       (0 upto length ts - 1) ts
  11.178 +
  11.179 +(** Helper facts **)
  11.180 +
  11.181 +fun count_combterm (CombConst ((s, _), _, _)) =
  11.182 +    Symtab.map_entry s (Integer.add 1)
  11.183 +  | count_combterm (CombVar _) = I
  11.184 +  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
  11.185 +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
  11.186 +  | count_combformula (AConn (_, phis)) = fold count_combformula phis
  11.187 +  | count_combformula (AAtom tm) = count_combterm tm
  11.188 +fun count_fol_formula (FOLFormula {combformula, ...}) =
  11.189 +  count_combformula combformula
  11.190 +
  11.191 +val optional_helpers =
  11.192 +  [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
  11.193 +   (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
  11.194 +   (["c_COMBS"], @{thms COMBS_def})]
  11.195 +val optional_typed_helpers =
  11.196 +  [(["c_True", "c_False"], @{thms True_or_False}),
  11.197 +   (["c_If"], @{thms if_True if_False True_or_False})]
  11.198 +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
  11.199 +
  11.200 +val init_counters =
  11.201 +  Symtab.make (maps (maps (map (rpair 0) o fst))
  11.202 +                    [optional_helpers, optional_typed_helpers])
  11.203 +
  11.204 +fun get_helper_facts ctxt is_FO full_types conjectures axioms =
  11.205 +  let
  11.206 +    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
  11.207 +    fun is_needed c = the (Symtab.lookup ct c) > 0
  11.208 +  in
  11.209 +    (optional_helpers
  11.210 +     |> full_types ? append optional_typed_helpers
  11.211 +     |> maps (fn (ss, ths) =>
  11.212 +                 if exists is_needed ss then map (`Thm.get_name_hint) ths
  11.213 +                 else [])) @
  11.214 +    (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
  11.215 +    |> map (snd o make_axiom ctxt false)
  11.216 +  end
  11.217 +
  11.218 +fun meta_not t = @{const "==>"} $ t $ @{prop False}
  11.219 +
  11.220 +fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
  11.221 +  let
  11.222 +    val thy = ProofContext.theory_of ctxt
  11.223 +    val axiom_ts = map (prop_of o snd) axioms
  11.224 +    val hyp_ts =
  11.225 +      if null hyp_ts then
  11.226 +        []
  11.227 +      else
  11.228 +        (* Remove existing axioms from the conjecture, as this can dramatically
  11.229 +           boost an ATP's performance (for some reason). *)
  11.230 +        let
  11.231 +          val axiom_table = fold (Termtab.update o rpair ()) axiom_ts
  11.232 +                                 Termtab.empty
  11.233 +        in hyp_ts |> filter_out (Termtab.defined axiom_table) end
  11.234 +    val goal_t = Logic.list_implies (hyp_ts, concl_t)
  11.235 +    val is_FO = Meson.is_fol_term thy goal_t
  11.236 +    val subs = tfree_classes_of_terms [goal_t]
  11.237 +    val supers = tvar_classes_of_terms axiom_ts
  11.238 +    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
  11.239 +    (* TFrees in the conjecture; TVars in the axioms *)
  11.240 +    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
  11.241 +    val (axiom_names, axioms) =
  11.242 +      ListPair.unzip (map (make_axiom ctxt true) axioms)
  11.243 +    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
  11.244 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
  11.245 +    val class_rel_clauses = make_class_rel_clauses thy subs supers'
  11.246 +  in
  11.247 +    (Vector.fromList axiom_names,
  11.248 +     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
  11.249 +  end
  11.250 +
  11.251 +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
  11.252 +
  11.253 +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
  11.254 +  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
  11.255 +  | fo_term_for_combtyp (CombType (name, tys)) =
  11.256 +    ATerm (name, map fo_term_for_combtyp tys)
  11.257 +
  11.258 +fun fo_literal_for_type_literal (TyLitVar (class, name)) =
  11.259 +    (true, ATerm (class, [ATerm (name, [])]))
  11.260 +  | fo_literal_for_type_literal (TyLitFree (class, name)) =
  11.261 +    (true, ATerm (class, [ATerm (name, [])]))
  11.262 +
  11.263 +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
  11.264 +
  11.265 +fun fo_term_for_combterm full_types =
  11.266 +  let
  11.267 +    fun aux top_level u =
  11.268 +      let
  11.269 +        val (head, args) = strip_combterm_comb u
  11.270 +        val (x, ty_args) =
  11.271 +          case head of
  11.272 +            CombConst (name as (s, s'), _, ty_args) =>
  11.273 +            if s = "equal" then
  11.274 +              (if top_level andalso length args = 2 then name
  11.275 +               else ("c_fequal", @{const_name fequal}), [])
  11.276 +            else if top_level then
  11.277 +              case s of
  11.278 +                "c_False" => (("$false", s'), [])
  11.279 +              | "c_True" => (("$true", s'), [])
  11.280 +              | _ => (name, if full_types then [] else ty_args)
  11.281 +            else
  11.282 +              (name, if full_types then [] else ty_args)
  11.283 +          | CombVar (name, _) => (name, [])
  11.284 +          | CombApp _ => raise Fail "impossible \"CombApp\""
  11.285 +        val t = ATerm (x, map fo_term_for_combtyp ty_args @
  11.286 +                          map (aux false) args)
  11.287 +    in
  11.288 +      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
  11.289 +    end
  11.290 +  in aux true end
  11.291 +
  11.292 +fun formula_for_combformula full_types =
  11.293 +  let
  11.294 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
  11.295 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
  11.296 +      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
  11.297 +  in aux end
  11.298 +
  11.299 +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
  11.300 +  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
  11.301 +                (type_literals_for_types ctypes_sorts))
  11.302 +           (formula_for_combformula full_types combformula)
  11.303 +
  11.304 +fun problem_line_for_fact prefix full_types
  11.305 +                          (formula as FOLFormula {name, kind, ...}) =
  11.306 +  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
  11.307 +
  11.308 +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
  11.309 +                                                       superclass, ...}) =
  11.310 +  let val ty_arg = ATerm (("T", "T"), []) in
  11.311 +    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
  11.312 +         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
  11.313 +                           AAtom (ATerm (superclass, [ty_arg]))]))
  11.314 +  end
  11.315 +
  11.316 +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
  11.317 +    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
  11.318 +  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
  11.319 +    (false, ATerm (c, [ATerm (sort, [])]))
  11.320 +
  11.321 +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
  11.322 +                                                ...}) =
  11.323 +  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
  11.324 +       mk_ahorn (map (formula_for_fo_literal o apfst not
  11.325 +                      o fo_literal_for_arity_literal) premLits)
  11.326 +                (formula_for_fo_literal
  11.327 +                     (fo_literal_for_arity_literal conclLit)))
  11.328 +
  11.329 +fun problem_line_for_conjecture full_types
  11.330 +                                (FOLFormula {name, kind, combformula, ...}) =
  11.331 +  Fof (conjecture_prefix ^ name, kind,
  11.332 +       formula_for_combformula full_types combformula)
  11.333 +
  11.334 +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
  11.335 +  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
  11.336 +
  11.337 +fun problem_line_for_free_type lit =
  11.338 +  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
  11.339 +fun problem_lines_for_free_types conjectures =
  11.340 +  let
  11.341 +    val litss = map free_type_literals_for_conjecture conjectures
  11.342 +    val lits = fold (union (op =)) litss []
  11.343 +  in map problem_line_for_free_type lits end
  11.344 +
  11.345 +(** "hBOOL" and "hAPP" **)
  11.346 +
  11.347 +type const_info = {min_arity: int, max_arity: int, sub_level: bool}
  11.348 +
  11.349 +fun consider_term top_level (ATerm ((s, _), ts)) =
  11.350 +  (if is_tptp_variable s then
  11.351 +     I
  11.352 +   else
  11.353 +     let val n = length ts in
  11.354 +       Symtab.map_default
  11.355 +           (s, {min_arity = n, max_arity = 0, sub_level = false})
  11.356 +           (fn {min_arity, max_arity, sub_level} =>
  11.357 +               {min_arity = Int.min (n, min_arity),
  11.358 +                max_arity = Int.max (n, max_arity),
  11.359 +                sub_level = sub_level orelse not top_level})
  11.360 +     end)
  11.361 +  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
  11.362 +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
  11.363 +  | consider_formula (AConn (_, phis)) = fold consider_formula phis
  11.364 +  | consider_formula (AAtom tm) = consider_term true tm
  11.365 +
  11.366 +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
  11.367 +fun consider_problem problem = fold (fold consider_problem_line o snd) problem
  11.368 +
  11.369 +fun const_table_for_problem explicit_apply problem =
  11.370 +  if explicit_apply then NONE
  11.371 +  else SOME (Symtab.empty |> consider_problem problem)
  11.372 +
  11.373 +fun min_arity_of thy full_types NONE s =
  11.374 +    (if s = "equal" orelse s = type_wrapper_name orelse
  11.375 +        String.isPrefix type_const_prefix s orelse
  11.376 +        String.isPrefix class_prefix s then
  11.377 +       16383 (* large number *)
  11.378 +     else if full_types then
  11.379 +       0
  11.380 +     else case strip_prefix_and_undo_ascii const_prefix s of
  11.381 +       SOME s' => num_type_args thy (invert_const s')
  11.382 +     | NONE => 0)
  11.383 +  | min_arity_of _ _ (SOME the_const_tab) s =
  11.384 +    case Symtab.lookup the_const_tab s of
  11.385 +      SOME ({min_arity, ...} : const_info) => min_arity
  11.386 +    | NONE => 0
  11.387 +
  11.388 +fun full_type_of (ATerm ((s, _), [ty, _])) =
  11.389 +    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
  11.390 +  | full_type_of _ = raise Fail "expected type wrapper"
  11.391 +
  11.392 +fun list_hAPP_rev _ t1 [] = t1
  11.393 +  | list_hAPP_rev NONE t1 (t2 :: ts2) =
  11.394 +    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
  11.395 +  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
  11.396 +    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
  11.397 +                         [full_type_of t2, ty]) in
  11.398 +      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
  11.399 +    end
  11.400 +
  11.401 +fun repair_applications_in_term thy full_types const_tab =
  11.402 +  let
  11.403 +    fun aux opt_ty (ATerm (name as (s, _), ts)) =
  11.404 +      if s = type_wrapper_name then
  11.405 +        case ts of
  11.406 +          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
  11.407 +        | _ => raise Fail "malformed type wrapper"
  11.408 +      else
  11.409 +        let
  11.410 +          val ts = map (aux NONE) ts
  11.411 +          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
  11.412 +        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
  11.413 +  in aux NONE end
  11.414 +
  11.415 +fun boolify t = ATerm (`I "hBOOL", [t])
  11.416 +
  11.417 +(* True if the constant ever appears outside of the top-level position in
  11.418 +   literals, or if it appears with different arities (e.g., because of different
  11.419 +   type instantiations). If false, the constant always receives all of its
  11.420 +   arguments and is used as a predicate. *)
  11.421 +fun is_predicate NONE s =
  11.422 +    s = "equal" orelse String.isPrefix type_const_prefix s orelse
  11.423 +    String.isPrefix class_prefix s
  11.424 +  | is_predicate (SOME the_const_tab) s =
  11.425 +    case Symtab.lookup the_const_tab s of
  11.426 +      SOME {min_arity, max_arity, sub_level} =>
  11.427 +      not sub_level andalso min_arity = max_arity
  11.428 +    | NONE => false
  11.429 +
  11.430 +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
  11.431 +  if s = type_wrapper_name then
  11.432 +    case ts of
  11.433 +      [_, t' as ATerm ((s', _), _)] =>
  11.434 +      if is_predicate const_tab s' then t' else boolify t
  11.435 +    | _ => raise Fail "malformed type wrapper"
  11.436 +  else
  11.437 +    t |> not (is_predicate const_tab s) ? boolify
  11.438 +
  11.439 +fun close_universally phi =
  11.440 +  let
  11.441 +    fun term_vars bounds (ATerm (name as (s, _), tms)) =
  11.442 +        (is_tptp_variable s andalso not (member (op =) bounds name))
  11.443 +          ? insert (op =) name
  11.444 +        #> fold (term_vars bounds) tms
  11.445 +    fun formula_vars bounds (AQuant (q, xs, phi)) =
  11.446 +        formula_vars (xs @ bounds) phi
  11.447 +      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
  11.448 +      | formula_vars bounds (AAtom tm) = term_vars bounds tm
  11.449 +  in
  11.450 +    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
  11.451 +  end
  11.452 +
  11.453 +fun repair_formula thy explicit_forall full_types const_tab =
  11.454 +  let
  11.455 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
  11.456 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
  11.457 +      | aux (AAtom tm) =
  11.458 +        AAtom (tm |> repair_applications_in_term thy full_types const_tab
  11.459 +                  |> repair_predicates_in_term const_tab)
  11.460 +  in aux #> explicit_forall ? close_universally end
  11.461 +
  11.462 +fun repair_problem_line thy explicit_forall full_types const_tab
  11.463 +                        (Fof (ident, kind, phi)) =
  11.464 +  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
  11.465 +fun repair_problem_with_const_table thy =
  11.466 +  map o apsnd o map ooo repair_problem_line thy
  11.467 +
  11.468 +fun repair_problem thy explicit_forall full_types explicit_apply problem =
  11.469 +  repair_problem_with_const_table thy explicit_forall full_types
  11.470 +      (const_table_for_problem explicit_apply problem) problem
  11.471 +
  11.472 +fun prepare_problem ctxt readable_names explicit_forall full_types
  11.473 +                    explicit_apply hyp_ts concl_t axiom_ts =
  11.474 +  let
  11.475 +    val thy = ProofContext.theory_of ctxt
  11.476 +    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
  11.477 +                       arity_clauses)) =
  11.478 +      prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts
  11.479 +    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
  11.480 +    val helper_lines =
  11.481 +      map (problem_line_for_fact helper_prefix full_types) helper_facts
  11.482 +    val conjecture_lines =
  11.483 +      map (problem_line_for_conjecture full_types) conjectures
  11.484 +    val tfree_lines = problem_lines_for_free_types conjectures
  11.485 +    val class_rel_lines =
  11.486 +      map problem_line_for_class_rel_clause class_rel_clauses
  11.487 +    val arity_lines = map problem_line_for_arity_clause arity_clauses
  11.488 +    (* Reordering these might or might not confuse the proof reconstruction
  11.489 +       code or the SPASS Flotter hack. *)
  11.490 +    val problem =
  11.491 +      [("Relevant facts", axiom_lines),
  11.492 +       ("Class relationships", class_rel_lines),
  11.493 +       ("Arity declarations", arity_lines),
  11.494 +       ("Helper facts", helper_lines),
  11.495 +       ("Conjectures", conjecture_lines),
  11.496 +       ("Type variables", tfree_lines)]
  11.497 +      |> repair_problem thy explicit_forall full_types explicit_apply
  11.498 +    val (problem, pool) = nice_tptp_problem readable_names problem
  11.499 +    val conjecture_offset =
  11.500 +      length axiom_lines + length class_rel_lines + length arity_lines
  11.501 +      + length helper_lines
  11.502 +  in
  11.503 +    (problem,
  11.504 +     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  11.505 +     conjecture_offset, axiom_names)
  11.506 +  end
  11.507 +
  11.508 +end;