# HG changeset patch
# User blanchet
# Date 1287748491 -7200
# Node ID 0783415ed7f067520531367c2e927e593890e672
# Parent  80d4ea0e536a2ef7dba7e962c274bbe0a731c67e
renamed files

diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 22 13:49:44 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 22 13:54:51 2010 +0200
@@ -327,8 +327,8 @@
   Tools/Sledgehammer/sledgehammer_filter.ML \
   Tools/Sledgehammer/sledgehammer_minimize.ML \
   Tools/Sledgehammer/sledgehammer_isar.ML \
-  Tools/Sledgehammer/sledgehammer_reconstruct.ML \
-  Tools/Sledgehammer/sledgehammer_translate.ML \
+  Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
+  Tools/Sledgehammer/sledgehammer_atp_translate.ML \
   Tools/Sledgehammer/sledgehammer_util.ML \
   Tools/SMT/cvc3_solver.ML \
   Tools/SMT/smtlib_interface.ML \
diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Oct 22 13:49:44 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Oct 22 13:54:51 2010 +0200
@@ -10,8 +10,8 @@
 imports ATP
 uses "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
-     "Tools/Sledgehammer/sledgehammer_translate.ML"
-     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
+     "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
+     "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
      "Tools/Sledgehammer/sledgehammer.ML"
      "Tools/Sledgehammer/sledgehammer_minimize.ML"
      "Tools/Sledgehammer/sledgehammer_isar.ML"
diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:54:51 2010 +0200
@@ -0,0 +1,946 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
+    Author:     Claire Quigley, Cambridge University Computer Laboratory
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Proof reconstruction for Sledgehammer.
+*)
+
+signature SLEDGEHAMMER_RECONSTRUCT =
+sig
+  type locality = Sledgehammer_Filter.locality
+  type minimize_command = string list -> string
+  type metis_params =
+    string * bool * minimize_command * string * (string * locality) list vector
+    * thm * int
+  type isar_params =
+    string Symtab.table * bool * int * Proof.context * int list list
+  type text_result = string * (string * locality) list
+
+  val repair_conjecture_shape_and_axiom_names :
+    string -> int list list -> (string * locality) list vector
+    -> int list list * (string * locality) list vector
+  val apply_on_subgoal : int -> int -> string
+  val command_call : string -> string list -> string
+  val try_command_line : string -> string -> string
+  val minimize_line : ('a list -> string) -> 'a list -> string
+  val metis_proof_text : metis_params -> text_result
+  val isar_proof_text : isar_params -> metis_params -> text_result
+  val proof_text : bool -> isar_params -> metis_params -> text_result
+end;
+
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
+struct
+
+open ATP_Problem
+open ATP_Proof
+open Metis_Translate
+open Sledgehammer_Util
+open Sledgehammer_Filter
+open Sledgehammer_Translate
+
+type minimize_command = string list -> string
+type metis_params =
+  string * bool * minimize_command * string * (string * locality) list vector
+  * thm * int
+type isar_params =
+  string Symtab.table * bool * int * Proof.context * int list list
+type text_result = string * (string * locality) list
+
+fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+
+fun find_first_in_list_vector vec key =
+  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+                 | (_, value) => value) NONE vec
+
+
+(** SPASS's Flotter hack **)
+
+(* This is a hack required for keeping track of axioms after they have been
+   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
+   part of this hack. *)
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+fun extract_clause_sequence output =
+  let
+    val tokens_of = String.tokens (not o Char.isAlphaNum)
+    fun extract_num ("clause" :: (ss as _ :: _)) =
+    Int.fromString (List.last ss)
+      | extract_num _ = NONE
+  in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val parse_clause_formula_pair =
+  $$ "(" |-- scan_integer --| $$ ","
+  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
+  --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+  |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+  Substring.full #> Substring.position set_ClauseFormulaRelationN
+  #> snd #> Substring.position "." #> fst #> Substring.string
+  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
+  #> fst
+
+fun repair_conjecture_shape_and_axiom_names output conjecture_shape
+                                            axiom_names =
+  if String.isSubstring set_ClauseFormulaRelationN output then
+    let
+      val j0 = hd (hd conjecture_shape)
+      val seq = extract_clause_sequence output
+      val name_map = extract_clause_formula_relation output
+      fun renumber_conjecture j =
+        conjecture_prefix ^ string_of_int (j - j0)
+        |> AList.find (fn (s, ss) => member (op =) ss s) name_map
+        |> map (fn s => find_index (curry (op =) s) seq + 1)
+      fun names_for_number j =
+        j |> AList.lookup (op =) name_map |> these
+          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
+          |> map (fn name =>
+                     (name, name |> find_first_in_list_vector axiom_names
+                                 |> the)
+                     handle Option.Option =>
+                            error ("No such fact: " ^ quote name ^ "."))
+    in
+      (conjecture_shape |> map (maps renumber_conjecture),
+       seq |> map names_for_number |> Vector.fromList)
+    end
+  else
+    (conjecture_shape, axiom_names)
+
+
+(** Soft-core proof reconstruction: Metis one-liner **)
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun apply_on_subgoal _ 1 = "by "
+  | apply_on_subgoal 1 _ = "apply "
+  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
+fun command_call name [] = name
+  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun try_command_line banner command =
+  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
+fun using_labels [] = ""
+  | using_labels ls =
+    "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun metis_name full_types = if full_types then "metisFT" else "metis"
+fun metis_call full_types ss = command_call (metis_name full_types) ss
+fun metis_command full_types i n (ls, ss) =
+  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
+fun metis_line banner full_types i n ss =
+  try_command_line banner (metis_command full_types i n ([], ss))
+fun minimize_line _ [] = ""
+  | minimize_line minimize_command ss =
+    case minimize_command ss of
+      "" => ""
+    | command =>
+      "\nTo minimize the number of lemmas, try this: " ^
+      Markup.markup Markup.sendback command ^ "."
+
+fun resolve_axiom axiom_names ((_, SOME s)) =
+    (case strip_prefix_and_unascii axiom_prefix s of
+       SOME s' => (case find_first_in_list_vector axiom_names s' of
+                     SOME x => [(s', x)]
+                   | NONE => [])
+     | NONE => [])
+  | resolve_axiom axiom_names (num, NONE) =
+    case Int.fromString num of
+      SOME j =>
+      if j > 0 andalso j <= Vector.length axiom_names then
+        Vector.sub (axiom_names, j - 1)
+      else
+        []
+    | NONE => []
+
+fun add_fact axiom_names (Inference (name, _, [])) =
+    append (resolve_axiom axiom_names name)
+  | add_fact _ _ = I
+
+fun used_facts_in_tstplike_proof axiom_names =
+  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
+
+fun used_facts axiom_names =
+  used_facts_in_tstplike_proof axiom_names
+  #> List.partition (curry (op =) Chained o snd)
+  #> pairself (sort_distinct (string_ord o pairself fst))
+
+fun metis_proof_text (banner, full_types, minimize_command,
+                      tstplike_proof, axiom_names, goal, i) =
+  let
+    val (chained_lemmas, other_lemmas) =
+      used_facts axiom_names tstplike_proof
+    val n = Logic.count_prems (prop_of goal)
+  in
+    (metis_line banner full_types i n (map fst other_lemmas) ^
+     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
+     other_lemmas @ chained_lemmas)
+  end
+
+
+(** Hard-core proof reconstruction: structured Isar proofs **)
+
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+   spurious "True"s. *)
+fun s_not @{const False} = @{const True}
+  | s_not @{const True} = @{const False}
+  | s_not (@{const Not} $ t) = t
+  | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+  | s_conj (t1, @{const True}) = t1
+  | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+  | s_disj (t1, @{const False}) = t1
+  | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+  | s_imp (t1, @{const False}) = s_not t1
+  | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+  | s_iff (t1, @{const True}) = t1
+  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+
+fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
+  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
+  | negate_term (@{const HOL.implies} $ t1 $ t2) =
+    @{const HOL.conj} $ t1 $ negate_term t2
+  | negate_term (@{const HOL.conj} $ t1 $ t2) =
+    @{const HOL.disj} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const HOL.disj} $ t1 $ t2) =
+    @{const HOL.conj} $ negate_term t1 $ negate_term t2
+  | negate_term (@{const Not} $ t) = t
+  | negate_term t = @{const Not} $ t
+
+val indent_size = 2
+val no_label = ("", ~1)
+
+val raw_prefix = "X"
+val assum_prefix = "A"
+val fact_prefix = "F"
+
+fun resolve_conjecture conjecture_shape (num, s_opt) =
+  let
+    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
+              SOME s => Int.fromString s |> the_default ~1
+            | NONE => case Int.fromString num of
+                        SOME j => find_index (exists (curry (op =) j))
+                                             conjecture_shape
+                      | NONE => ~1
+  in if k >= 0 then [k] else [] end
+
+fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
+fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
+
+fun raw_label_for_name conjecture_shape name =
+  case resolve_conjecture conjecture_shape name of
+    [j] => (conjecture_prefix, j)
+  | _ => case Int.fromString (fst name) of
+           SOME j => (raw_prefix, j)
+         | NONE => (raw_prefix ^ fst name, 0)
+
+(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
+
+exception FO_TERM of string fo_term list
+exception FORMULA of (string, string fo_term) formula list
+exception SAME of unit
+
+(* Type variables are given the basic sort "HOL.type". Some will later be
+   constrained by information from type literals, or by type inference. *)
+fun type_from_fo_term tfrees (u as ATerm (a, us)) =
+  let val Ts = map (type_from_fo_term tfrees) us in
+    case strip_prefix_and_unascii type_const_prefix a of
+      SOME b => Type (invert_const b, Ts)
+    | NONE =>
+      if not (null us) then
+        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
+      else case strip_prefix_and_unascii tfree_prefix a of
+        SOME b =>
+        let val s = "'" ^ b in
+          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+        end
+      | NONE =>
+        case strip_prefix_and_unascii tvar_prefix a of
+          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
+        | NONE =>
+          (* Variable from the ATP, say "X1" *)
+          Type_Infer.param 0 (a, HOLogic.typeS)
+  end
+
+(* Type class literal applied to a type. Returns triple of polarity, class,
+   type. *)
+fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
+  case (strip_prefix_and_unascii class_prefix a,
+        map (type_from_fo_term tfrees) us) of
+    (SOME b, [T]) => (pos, b, T)
+  | _ => raise FO_TERM [u]
+
+(** Accumulate type constraints in a formula: negative type literals **)
+fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
+fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
+  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
+  | add_type_constraint _ = I
+
+fun repair_atp_variable_name f s =
+  let
+    fun subscript_name s n = s ^ nat_subscript n
+    val s = String.map f s
+  in
+    case space_explode "_" s of
+      [_] => (case take_suffix Char.isDigit (String.explode s) of
+                (cs1 as _ :: _, cs2 as _ :: _) =>
+                subscript_name (String.implode cs1)
+                               (the (Int.fromString (String.implode cs2)))
+              | (_, _) => s)
+    | [s1, s2] => (case Int.fromString s2 of
+                     SOME n => subscript_name s1 n
+                   | NONE => s)
+    | _ => s
+  end
+
+(* First-order translation. No types are known for variables. "HOLogic.typeT"
+   should allow them to be inferred. *)
+fun raw_term_from_pred thy full_types tfrees =
+  let
+    fun aux opt_T extra_us u =
+      case u of
+        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
+      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
+      | ATerm (a, us) =>
+        if a = type_wrapper_name then
+          case us of
+            [typ_u, term_u] =>
+            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
+          | _ => raise FO_TERM us
+        else case strip_prefix_and_unascii const_prefix a of
+          SOME "equal" =>
+          let val ts = map (aux NONE []) us in
+            if length ts = 2 andalso hd ts aconv List.last ts then
+              (* Vampire is keen on producing these. *)
+              @{const True}
+            else
+              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+          end
+        | SOME b =>
+          let
+            val c = invert_const b
+            val num_type_args = num_type_args thy c
+            val (type_us, term_us) =
+              chop (if full_types then 0 else num_type_args) us
+            (* Extra args from "hAPP" come after any arguments given directly to
+               the constant. *)
+            val term_ts = map (aux NONE []) term_us
+            val extra_ts = map (aux NONE []) extra_us
+            val t =
+              Const (c, if full_types then
+                          case opt_T of
+                            SOME T => map fastype_of term_ts ---> T
+                          | NONE =>
+                            if num_type_args = 0 then
+                              Sign.const_instance thy (c, [])
+                            else
+                              raise Fail ("no type information for " ^ quote c)
+                        else
+                          Sign.const_instance thy (c,
+                              map (type_from_fo_term tfrees) type_us))
+          in list_comb (t, term_ts @ extra_ts) end
+        | NONE => (* a free or schematic variable *)
+          let
+            val ts = map (aux NONE []) (us @ extra_us)
+            val T = map fastype_of ts ---> HOLogic.typeT
+            val t =
+              case strip_prefix_and_unascii fixed_var_prefix a of
+                SOME b => Free (b, T)
+              | NONE =>
+                case strip_prefix_and_unascii schematic_var_prefix a of
+                  SOME b => Var ((b, 0), T)
+                | NONE =>
+                  if is_atp_variable a then
+                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
+                  else
+                    (* Skolem constants? *)
+                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
+          in list_comb (t, ts) end
+  in aux (SOME HOLogic.boolT) [] end
+
+fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
+  if String.isPrefix class_prefix s then
+    add_type_constraint (type_constraint_from_term pos tfrees u)
+    #> pair @{const True}
+  else
+    pair (raw_term_from_pred thy full_types tfrees u)
+
+val combinator_table =
+  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
+   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
+   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
+   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
+   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+
+fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
+  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
+  | uncombine_term (t as Const (x as (s, _))) =
+    (case AList.lookup (op =) combinator_table s of
+       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+     | NONE => t)
+  | uncombine_term t = t
+
+(* Update schematic type variables with detected sort constraints. It's not
+   totally clear when this code is necessary. *)
+fun repair_tvar_sorts (t, tvar_tab) =
+  let
+    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+      | do_type (TVar (xi, s)) =
+        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
+      | do_type (TFree z) = TFree z
+    fun do_term (Const (a, T)) = Const (a, do_type T)
+      | do_term (Free (a, T)) = Free (a, do_type T)
+      | do_term (Var (xi, T)) = Var (xi, do_type T)
+      | do_term (t as Bound _) = t
+      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+      | do_term (t1 $ t2) = do_term t1 $ do_term t2
+  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
+
+fun quantify_over_var quant_of var_s t =
+  let
+    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
+                  |> map Var
+  in fold_rev quant_of vars t end
+
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
+   appear in the formula. *)
+fun prop_from_formula thy full_types tfrees phi =
+  let
+    fun do_formula pos phi =
+      case phi of
+        AQuant (_, [], phi) => do_formula pos phi
+      | AQuant (q, x :: xs, phi') =>
+        do_formula pos (AQuant (q, xs, phi'))
+        #>> quantify_over_var (case q of
+                                 AForall => forall_of
+                               | AExists => exists_of)
+                              (repair_atp_variable_name Char.toLower x)
+      | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
+      | AConn (c, [phi1, phi2]) =>
+        do_formula (pos |> c = AImplies ? not) phi1
+        ##>> do_formula pos phi2
+        #>> (case c of
+               AAnd => s_conj
+             | AOr => s_disj
+             | AImplies => s_imp
+             | AIf => s_imp o swap
+             | AIff => s_iff
+             | ANotIff => s_not o s_iff)
+      | AAtom tm => term_from_pred thy full_types tfrees pos tm
+      | _ => raise FORMULA [phi]
+  in repair_tvar_sorts (do_formula true phi Vartab.empty) end
+
+fun check_formula ctxt =
+  Type.constraint HOLogic.boolT
+  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
+
+
+(**** Translation of TSTP files to Isar Proofs ****)
+
+fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
+  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
+
+fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
+    let
+      val thy = ProofContext.theory_of ctxt
+      val t1 = prop_from_formula thy full_types tfrees phi1
+      val vars = snd (strip_comb t1)
+      val frees = map unvarify_term vars
+      val unvarify_args = subst_atomic (vars ~~ frees)
+      val t2 = prop_from_formula thy full_types tfrees phi2
+      val (t1, t2) =
+        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
+        |> unvarify_args |> uncombine_term |> check_formula ctxt
+        |> HOLogic.dest_eq
+    in
+      (Definition (name, t1, t2),
+       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
+    end
+  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
+    let
+      val thy = ProofContext.theory_of ctxt
+      val t = u |> prop_from_formula thy full_types tfrees
+                |> uncombine_term |> check_formula ctxt
+    in
+      (Inference (name, t, deps),
+       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
+    end
+fun decode_lines ctxt full_types tfrees lines =
+  fst (fold_map (decode_line full_types tfrees) lines ctxt)
+
+fun is_same_inference _ (Definition _) = false
+  | is_same_inference t (Inference (_, t', _)) = t aconv t'
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or
+   clsarity). *)
+val is_only_type_information = curry (op aconv) HOLogic.true_const
+
+fun replace_one_dependency (old, new) dep =
+  if is_same_step (dep, old) then new else [dep]
+fun replace_dependencies_in_line _ (line as Definition _) = line
+  | replace_dependencies_in_line p (Inference (name, t, deps)) =
+    Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
+
+(* Discard axioms; consolidate adjacent lines that prove the same formula, since
+   they differ only in type information.*)
+fun add_line _ _ (line as Definition _) lines = line :: lines
+  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
+    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
+       definitions. *)
+    if is_axiom axiom_names name then
+      (* Axioms are not proof lines. *)
+      if is_only_type_information t then
+        map (replace_dependencies_in_line (name, [])) lines
+      (* Is there a repetition? If so, replace later line by earlier one. *)
+      else case take_prefix (not o is_same_inference t) lines of
+        (_, []) => lines (* no repetition of proof line *)
+      | (pre, Inference (name', _, _) :: post) =>
+        pre @ map (replace_dependencies_in_line (name', [name])) post
+    else if is_conjecture conjecture_shape name then
+      Inference (name, negate_term t, []) :: lines
+    else
+      map (replace_dependencies_in_line (name, [])) lines
+  | add_line _ _ (Inference (name, t, deps)) lines =
+    (* Type information will be deleted later; skip repetition test. *)
+    if is_only_type_information t then
+      Inference (name, t, deps) :: lines
+    (* Is there a repetition? If so, replace later line by earlier one. *)
+    else case take_prefix (not o is_same_inference t) lines of
+      (* FIXME: Doesn't this code risk conflating proofs involving different
+         types? *)
+       (_, []) => Inference (name, t, deps) :: lines
+     | (pre, Inference (name', t', _) :: post) =>
+       Inference (name, t', deps) ::
+       pre @ map (replace_dependencies_in_line (name', [name])) post
+
+(* Recursively delete empty lines (type information) from the proof. *)
+fun add_nontrivial_line (Inference (name, t, [])) lines =
+    if is_only_type_information t then delete_dependency name lines
+    else Inference (name, t, []) :: lines
+  | add_nontrivial_line line lines = line :: lines
+and delete_dependency name lines =
+  fold_rev add_nontrivial_line
+           (map (replace_dependencies_in_line (name, [])) lines) []
+
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+   offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+  | is_bad_free _ _ = false
+
+fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+    (j, line :: map (replace_dependencies_in_line (name, [])) lines)
+  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
+                     (Inference (name, t, deps)) (j, lines) =
+    (j + 1,
+     if is_axiom axiom_names name orelse
+        is_conjecture conjecture_shape name orelse
+        (* the last line must be kept *)
+        j = 0 orelse
+        (not (is_only_type_information t) andalso
+         null (Term.add_tvars t []) andalso
+         not (exists_subterm (is_bad_free frees) t) andalso
+         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
+         (* kill next to last line, which usually results in a trivial step *)
+         j <> 1) then
+       Inference (name, t, deps) :: lines  (* keep line *)
+     else
+       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
+
+(** Isar proof construction and manipulation **)
+
+fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
+  (union (op =) ls1 ls2, union (op =) ss1 ss2)
+
+type label = string * int
+type facts = label list * string list
+
+datatype isar_qualifier = Show | Then | Moreover | Ultimately
+
+datatype isar_step =
+  Fix of (string * typ) list |
+  Let of term * term |
+  Assume of label * term |
+  Have of isar_qualifier list * label * term * byline
+and byline =
+  ByMetis of facts |
+  CaseSplit of isar_step list list * facts
+
+fun smart_case_split [] facts = ByMetis facts
+  | smart_case_split proofs facts = CaseSplit (proofs, facts)
+
+fun add_fact_from_dependency conjecture_shape axiom_names name =
+  if is_axiom axiom_names name then
+    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
+  else
+    apfst (insert (op =) (raw_label_for_name conjecture_shape name))
+
+fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
+  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
+    Assume (raw_label_for_name conjecture_shape name, t)
+  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
+    Have (if j = 1 then [Show] else [],
+          raw_label_for_name conjecture_shape name,
+          fold_rev forall_of (map Var (Term.add_vars t [])) t,
+          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
+                        deps ([], [])))
+
+fun repair_name "$true" = "c_True"
+  | repair_name "$false" = "c_False"
+  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
+  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
+  | repair_name s =
+    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
+      "c_equal" (* seen in Vampire proofs *)
+    else
+      s
+
+fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
+        tstplike_proof conjecture_shape axiom_names params frees =
+  let
+    val lines =
+      tstplike_proof
+      |> atp_proof_from_tstplike_string
+      |> nasty_atp_proof pool
+      |> map_term_names_in_atp_proof repair_name
+      |> decode_lines ctxt full_types tfrees
+      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
+      |> rpair [] |-> fold_rev add_nontrivial_line
+      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
+                                             conjecture_shape axiom_names frees)
+      |> snd
+  in
+    (if null params then [] else [Fix params]) @
+    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
+         lines
+  end
+
+(* When redirecting proofs, we keep information about the labels seen so far in
+   the "backpatches" data structure. The first component indicates which facts
+   should be associated with forthcoming proof steps. The second component is a
+   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+   become assumptions and "drop_ls" are the labels that should be dropped in a
+   case split. *)
+type backpatches = (label * facts) list * (label list * label list)
+
+fun used_labels_of_step (Have (_, _, _, by)) =
+    (case by of
+       ByMetis (ls, _) => ls
+     | CaseSplit (proofs, (ls, _)) =>
+       fold (union (op =) o used_labels_of) proofs ls)
+  | used_labels_of_step _ = []
+and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
+
+fun new_labels_of_step (Fix _) = []
+  | new_labels_of_step (Let _) = []
+  | new_labels_of_step (Assume (l, _)) = [l]
+  | new_labels_of_step (Have (_, l, _, _)) = [l]
+val new_labels_of = maps new_labels_of_step
+
+val join_proofs =
+  let
+    fun aux _ [] = NONE
+      | aux proof_tail (proofs as (proof1 :: _)) =
+        if exists null proofs then
+          NONE
+        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
+          aux (hd proof1 :: proof_tail) (map tl proofs)
+        else case hd proof1 of
+          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
+          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
+                      | _ => false) (tl proofs) andalso
+             not (exists (member (op =) (maps new_labels_of proofs))
+                         (used_labels_of proof_tail)) then
+            SOME (l, t, map rev proofs, proof_tail)
+          else
+            NONE
+        | _ => NONE
+  in aux [] o map rev end
+
+fun case_split_qualifiers proofs =
+  case length proofs of
+    0 => []
+  | 1 => [Then]
+  | _ => [Ultimately]
+
+fun redirect_proof hyp_ts concl_t proof =
+  let
+    (* The first pass outputs those steps that are independent of the negated
+       conjecture. The second pass flips the proof by contradiction to obtain a
+       direct proof, introducing case splits when an inference depends on
+       several facts that depend on the negated conjecture. *)
+     val concl_l = (conjecture_prefix, length hyp_ts)
+     fun first_pass ([], contra) = ([], contra)
+       | first_pass ((step as Fix _) :: proof, contra) =
+         first_pass (proof, contra) |>> cons step
+       | first_pass ((step as Let _) :: proof, contra) =
+         first_pass (proof, contra) |>> cons step
+       | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
+         if l = concl_l then first_pass (proof, contra ||> cons step)
+         else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
+       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
+           if exists (member (op =) (fst contra)) ls then
+             first_pass (proof, contra |>> cons l ||> cons step)
+           else
+             first_pass (proof, contra) |>> cons step
+         end
+       | first_pass _ = raise Fail "malformed proof"
+    val (proof_top, (contra_ls, contra_proof)) =
+      first_pass (proof, ([concl_l], []))
+    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
+    fun backpatch_labels patches ls =
+      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
+    fun second_pass end_qs ([], assums, patches) =
+        ([Have (end_qs, no_label, concl_t,
+                ByMetis (backpatch_labels patches (map snd assums)))], patches)
+      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
+        second_pass end_qs (proof, (t, l) :: assums, patches)
+      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
+                            patches) =
+        (if member (op =) (snd (snd patches)) l andalso
+            not (member (op =) (fst (snd patches)) l) andalso
+            not (AList.defined (op =) (fst patches) l) then
+           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
+         else case List.partition (member (op =) contra_ls) ls of
+           ([contra_l], co_ls) =>
+           if member (op =) qs Show then
+             second_pass end_qs (proof, assums,
+                                 patches |>> cons (contra_l, (co_ls, ss)))
+           else
+             second_pass end_qs
+                         (proof, assums,
+                          patches |>> cons (contra_l, (l :: co_ls, ss)))
+             |>> cons (if member (op =) (fst (snd patches)) l then
+                         Assume (l, negate_term t)
+                       else
+                         Have (qs, l, negate_term t,
+                               ByMetis (backpatch_label patches l)))
+         | (contra_ls as _ :: _, co_ls) =>
+           let
+             val proofs =
+               map_filter
+                   (fn l =>
+                       if l = concl_l then
+                         NONE
+                       else
+                         let
+                           val drop_ls = filter (curry (op <>) l) contra_ls
+                         in
+                           second_pass []
+                               (proof, assums,
+                                patches ||> apfst (insert (op =) l)
+                                        ||> apsnd (union (op =) drop_ls))
+                           |> fst |> SOME
+                         end) contra_ls
+             val (assumes, facts) =
+               if member (op =) (fst (snd patches)) l then
+                 ([Assume (l, negate_term t)], (l :: co_ls, ss))
+               else
+                 ([], (co_ls, ss))
+           in
+             (case join_proofs proofs of
+                SOME (l, t, proofs, proof_tail) =>
+                Have (case_split_qualifiers proofs @
+                      (if null proof_tail then end_qs else []), l, t,
+                      smart_case_split proofs facts) :: proof_tail
+              | NONE =>
+                [Have (case_split_qualifiers proofs @ end_qs, no_label,
+                       concl_t, smart_case_split proofs facts)],
+              patches)
+             |>> append assumes
+           end
+         | _ => raise Fail "malformed proof")
+       | second_pass _ _ = raise Fail "malformed proof"
+    val proof_bottom =
+      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
+  in proof_top @ proof_bottom end
+
+(* FIXME: Still needed? Probably not. *)
+val kill_duplicate_assumptions_in_proof =
+  let
+    fun relabel_facts subst =
+      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
+    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
+        (case AList.lookup (op aconv) assums t of
+           SOME l' => (proof, (l, l') :: subst, assums)
+         | NONE => (step :: proof, subst, (t, l) :: assums))
+      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
+        (Have (qs, l, t,
+               case by of
+                 ByMetis facts => ByMetis (relabel_facts subst facts)
+               | CaseSplit (proofs, facts) =>
+                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
+         proof, subst, assums)
+      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
+    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
+  in do_proof end
+
+val then_chain_proof =
+  let
+    fun aux _ [] = []
+      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
+      | aux l' (Have (qs, l, t, by) :: proof) =
+        (case by of
+           ByMetis (ls, ss) =>
+           Have (if member (op =) ls l' then
+                   (Then :: qs, l, t,
+                    ByMetis (filter_out (curry (op =) l') ls, ss))
+                 else
+                   (qs, l, t, ByMetis (ls, ss)))
+         | CaseSplit (proofs, facts) =>
+           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
+        aux l proof
+      | aux _ (step :: proof) = step :: aux no_label proof
+  in aux no_label end
+
+fun kill_useless_labels_in_proof proof =
+  let
+    val used_ls = used_labels_of proof
+    fun do_label l = if member (op =) used_ls l then l else no_label
+    fun do_step (Assume (l, t)) = Assume (do_label l, t)
+      | do_step (Have (qs, l, t, by)) =
+        Have (qs, do_label l, t,
+              case by of
+                CaseSplit (proofs, facts) =>
+                CaseSplit (map (map do_step) proofs, facts)
+              | _ => by)
+      | do_step step = step
+  in map do_step proof end
+
+fun prefix_for_depth n = replicate_string (n + 1)
+
+val relabel_proof =
+  let
+    fun aux _ _ _ [] = []
+      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
+        if l = no_label then
+          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
+        else
+          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
+            Assume (l', t) ::
+            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
+          end
+      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
+        let
+          val (l', subst, next_fact) =
+            if l = no_label then
+              (l, subst, next_fact)
+            else
+              let
+                val l' = (prefix_for_depth depth fact_prefix, next_fact)
+              in (l', (l, l') :: subst, next_fact + 1) end
+          val relabel_facts =
+            apfst (maps (the_list o AList.lookup (op =) subst))
+          val by =
+            case by of
+              ByMetis facts => ByMetis (relabel_facts facts)
+            | CaseSplit (proofs, facts) =>
+              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
+                         relabel_facts facts)
+        in
+          Have (qs, l', t, by) ::
+          aux subst depth (next_assum, next_fact) proof
+        end
+      | aux subst depth nextp (step :: proof) =
+        step :: aux subst depth nextp proof
+  in aux [] 0 (1, 1) end
+
+fun string_for_proof ctxt0 full_types i n =
+  let
+    val ctxt = ctxt0
+      |> Config.put show_free_types false
+      |> Config.put show_types true
+    fun fix_print_mode f x =
+      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                               (print_mode_value ())) f x
+    fun do_indent ind = replicate_string (ind * indent_size) " "
+    fun do_free (s, T) =
+      maybe_quote s ^ " :: " ^
+      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
+    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
+    fun do_have qs =
+      (if member (op =) qs Moreover then "moreover " else "") ^
+      (if member (op =) qs Ultimately then "ultimately " else "") ^
+      (if member (op =) qs Then then
+         if member (op =) qs Show then "thus" else "hence"
+       else
+         if member (op =) qs Show then "show" else "have")
+    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+    fun do_facts (ls, ss) =
+      metis_command full_types 1 1
+                    (ls |> sort_distinct (prod_ord string_ord int_ord),
+                     ss |> sort_distinct string_ord)
+    and do_step ind (Fix xs) =
+        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+      | do_step ind (Let (t1, t2)) =
+        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
+      | do_step ind (Assume (l, t)) =
+        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
+      | do_step ind (Have (qs, l, t, ByMetis facts)) =
+        do_indent ind ^ do_have qs ^ " " ^
+        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
+      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
+        space_implode (do_indent ind ^ "moreover\n")
+                      (map (do_block ind) proofs) ^
+        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
+        do_facts facts ^ "\n"
+    and do_steps prefix suffix ind steps =
+      let val s = implode (map (do_step ind) steps) in
+        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+        String.extract (s, ind * indent_size,
+                        SOME (size s - ind * indent_size - 1)) ^
+        suffix ^ "\n"
+      end
+    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
+    (* One-step proofs are pointless; better use the Metis one-liner
+       directly. *)
+    and do_proof [Have (_, _, _, ByMetis _)] = ""
+      | do_proof proof =
+        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
+        (if n <> 1 then "next" else "qed")
+  in do_proof end
+
+fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+                    (other_params as (_, full_types, _, tstplike_proof,
+                                      axiom_names, goal, i)) =
+  let
+    val (params, hyp_ts, concl_t) = strip_subgoal goal i
+    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+    val n = Logic.count_prems (prop_of goal)
+    val (one_line_proof, lemma_names) = metis_proof_text other_params
+    fun isar_proof_for () =
+      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
+               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
+               params frees
+           |> redirect_proof hyp_ts concl_t
+           |> kill_duplicate_assumptions_in_proof
+           |> then_chain_proof
+           |> kill_useless_labels_in_proof
+           |> relabel_proof
+           |> string_for_proof ctxt full_types i n of
+        "" => "\nNo structured proof available."
+      | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
+    val isar_proof =
+      if debug then
+        isar_proof_for ()
+      else
+        try isar_proof_for ()
+        |> the_default "\nWarning: The Isar proof construction failed."
+  in (one_line_proof ^ isar_proof, lemma_names) end
+
+fun proof_text isar_proof isar_params other_params =
+  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
+      other_params
+
+end;
diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:54:51 2010 +0200
@@ -0,0 +1,533 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
+    Author:     Fabian Immler, TU Muenchen
+    Author:     Makarius
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Translation of HOL to FOL for Sledgehammer.
+*)
+
+signature SLEDGEHAMMER_TRANSLATE =
+sig
+  type 'a problem = 'a ATP_Problem.problem
+  type fol_formula
+
+  val axiom_prefix : string
+  val conjecture_prefix : string
+  val prepare_axiom :
+    Proof.context -> (string * 'a) * thm
+    -> term * ((string * 'a) * fol_formula) option
+  val prepare_atp_problem :
+    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
+    -> (term * ((string * 'a) * fol_formula) option) list
+    -> string problem * string Symtab.table * int * (string * 'a) list vector
+end;
+
+structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
+struct
+
+open ATP_Problem
+open Metis_Translate
+open Sledgehammer_Util
+
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
+val tfree_prefix = "tfree_"
+
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
+type fol_formula =
+  {name: string,
+   kind: kind,
+   combformula: (name, combterm) formula,
+   ctypes_sorts: typ list}
+
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+  | mk_ahorn (phi :: phis) psi =
+    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
+
+fun combformula_for_prop thy =
+  let
+    val do_term = combterm_from_term thy ~1
+    fun do_quant bs q s T t' =
+      let val s = Name.variant (map fst bs) s in
+        do_formula ((s, T) :: bs) t'
+        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+      end
+    and do_conn bs c t1 t2 =
+      do_formula bs t1 ##>> do_formula bs t2
+      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+    and do_formula bs t =
+      case t of
+        @{const Not} $ t1 =>
+        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+        do_quant bs AForall s T t'
+      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+        do_quant bs AExists s T t'
+      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
+      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
+      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+        do_conn bs AIff t1 t2
+      | _ => (fn ts => do_term bs (Envir.eta_contract t)
+                       |>> AAtom ||> union (op =) ts)
+  in do_formula [] end
+
+val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
+fun conceal_bounds Ts t =
+  subst_bounds (map (Free o apfst concealed_bound_name)
+                    (0 upto length Ts - 1 ~~ Ts), t)
+fun reveal_bounds Ts =
+  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+                    (0 upto length Ts - 1 ~~ Ts))
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
+fun extensionalize_term t =
+  let
+    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
+      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
+                                        Type (_, [_, res_T])]))
+                    $ t2 $ Abs (var_s, var_T, t')) =
+        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
+          let val var_t = Var ((var_s, j), var_T) in
+            Const (s, T' --> T' --> res_T)
+              $ betapply (t2, var_t) $ subst_bound (var_t, t')
+            |> aux (j + 1)
+          end
+        else
+          t
+      | aux _ t = t
+  in aux (maxidx_of_term t + 1) t end
+
+fun introduce_combinators_in_term ctxt kind t =
+  let val thy = ProofContext.theory_of ctxt in
+    if Meson.is_fol_term thy t then
+      t
+    else
+      let
+        fun aux Ts t =
+          case t of
+            @{const Not} $ t1 => @{const Not} $ aux Ts t1
+          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+            t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name All}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
+          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+            t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
+          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
+              $ t1 $ t2 =>
+            t0 $ aux Ts t1 $ aux Ts t2
+          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+                   t
+                 else
+                   t |> conceal_bounds Ts
+                     |> Envir.eta_contract
+                     |> cterm_of thy
+                     |> Meson_Clausify.introduce_combinators_in_cterm
+                     |> prop_of |> Logic.dest_equals |> snd
+                     |> reveal_bounds Ts
+        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+      handle THM _ =>
+             (* A type variable of sort "{}" will make abstraction fail. *)
+             if kind = Conjecture then HOLogic.false_const
+             else HOLogic.true_const
+  end
+
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+  let
+    fun aux (t $ u) = aux t $ aux u
+      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+      | aux (Var ((s, i), T)) =
+        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+      | aux t = t
+  in t |> exists_subterm is_Var t ? aux end
+
+(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
+    it leaves metaequalities over "prop"s alone. *)
+val atomize_term =
+  let
+    fun aux (@{const Trueprop} $ t1) = t1
+      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
+        HOLogic.all_const T $ Abs (s, T, aux t')
+      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
+      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
+        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
+      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
+        HOLogic.eq_const T $ t1 $ t2
+      | aux _ = raise Fail "aux"
+  in perhaps (try aux) end
+
+(* making axiom and conjecture formulas *)
+fun make_formula ctxt presimp name kind t =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val t = t |> Envir.beta_eta_contract
+              |> transform_elim_term
+              |> atomize_term
+    val need_trueprop = (fastype_of t = HOLogic.boolT)
+    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
+              |> extensionalize_term
+              |> presimp ? presimplify_term thy
+              |> perhaps (try (HOLogic.dest_Trueprop))
+              |> introduce_combinators_in_term ctxt kind
+              |> kind <> Axiom ? freeze_term
+    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
+  in
+    {name = name, combformula = combformula, kind = kind,
+     ctypes_sorts = ctypes_sorts}
+  end
+
+fun make_axiom ctxt presimp ((name, loc), th) =
+  case make_formula ctxt presimp name Axiom (prop_of th) of
+    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
+  | formula => SOME ((name, loc), formula)
+fun make_conjecture ctxt ts =
+  let val last = length ts - 1 in
+    map2 (fn j => make_formula ctxt true (Int.toString j)
+                               (if j = last then Conjecture else Hypothesis))
+         (0 upto last) ts
+  end
+
+(** Helper facts **)
+
+fun count_combterm (CombConst ((s, _), _, _)) =
+    Symtab.map_entry s (Integer.add 1)
+  | count_combterm (CombVar _) = I
+  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+  | count_combformula (AConn (_, phis)) = fold count_combformula phis
+  | count_combformula (AAtom tm) = count_combterm tm
+fun count_fol_formula ({combformula, ...} : fol_formula) =
+  count_combformula combformula
+
+val optional_helpers =
+  [(["c_COMBI"], @{thms Meson.COMBI_def}),
+   (["c_COMBK"], @{thms Meson.COMBK_def}),
+   (["c_COMBB"], @{thms Meson.COMBB_def}),
+   (["c_COMBC"], @{thms Meson.COMBC_def}),
+   (["c_COMBS"], @{thms Meson.COMBS_def})]
+val optional_typed_helpers =
+  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
+   (["c_If"], @{thms if_True if_False})]
+val mandatory_helpers = @{thms Metis.fequal_def}
+
+val init_counters =
+  [optional_helpers, optional_typed_helpers] |> maps (maps fst)
+  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
+
+fun get_helper_facts ctxt is_FO full_types conjectures axioms =
+  let
+    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
+    fun is_needed c = the (Symtab.lookup ct c) > 0
+    fun baptize th = ((Thm.get_name_hint th, false), th)
+  in
+    (optional_helpers
+     |> full_types ? append optional_typed_helpers
+     |> maps (fn (ss, ths) =>
+                 if exists is_needed ss then map baptize ths else [])) @
+    (if is_FO then [] else map baptize mandatory_helpers)
+    |> map_filter (Option.map snd o make_axiom ctxt false)
+  end
+
+fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
+
+fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
+    (* Remove existing axioms from the conjecture, as this can dramatically
+       boost an ATP's performance (for some reason). *)
+    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
+    val goal_t = Logic.list_implies (hyp_ts, concl_t)
+    val is_FO = Meson.is_fol_term thy goal_t
+    val subs = tfree_classes_of_terms [goal_t]
+    val supers = tvar_classes_of_terms axiom_ts
+    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
+    (* TFrees in the conjecture; TVars in the axioms *)
+    val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
+    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
+    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
+    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+    val class_rel_clauses = make_class_rel_clauses thy subs supers'
+  in
+    (axiom_names |> map single |> Vector.fromList,
+     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
+  end
+
+fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
+
+fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
+  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
+  | fo_term_for_combtyp (CombType (name, tys)) =
+    ATerm (name, map fo_term_for_combtyp tys)
+
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+    (true, ATerm (class, [ATerm (name, [])]))
+  | fo_literal_for_type_literal (TyLitFree (class, name)) =
+    (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+
+fun fo_term_for_combterm full_types =
+  let
+    fun aux top_level u =
+      let
+        val (head, args) = strip_combterm_comb u
+        val (x, ty_args) =
+          case head of
+            CombConst (name as (s, s'), _, ty_args) =>
+            let val ty_args = if full_types then [] else ty_args in
+              if s = "equal" then
+                if top_level andalso length args = 2 then (name, [])
+                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
+              else if top_level then
+                case s of
+                  "c_False" => (("$false", s'), [])
+                | "c_True" => (("$true", s'), [])
+                | _ => (name, ty_args)
+              else
+                (name, ty_args)
+            end
+          | CombVar (name, _) => (name, [])
+          | CombApp _ => raise Fail "impossible \"CombApp\""
+        val t = ATerm (x, map fo_term_for_combtyp ty_args @
+                          map (aux false) args)
+    in
+      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+    end
+  in aux true end
+
+fun formula_for_combformula full_types =
+  let
+    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+      | aux (AConn (c, phis)) = AConn (c, map aux phis)
+      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
+  in aux end
+
+fun formula_for_axiom full_types
+                      ({combformula, ctypes_sorts, ...} : fol_formula) =
+  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+                (type_literals_for_types ctypes_sorts))
+           (formula_for_combformula full_types combformula)
+
+fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
+  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
+
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+                                                       superclass, ...}) =
+  let val ty_arg = ATerm (("T", "T"), []) in
+    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
+         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+                           AAtom (ATerm (superclass, [ty_arg]))]))
+  end
+
+fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
+    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
+    (false, ATerm (c, [ATerm (sort, [])]))
+
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+                                                ...}) =
+  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
+       mk_ahorn (map (formula_for_fo_literal o apfst not
+                      o fo_literal_for_arity_literal) premLits)
+                (formula_for_fo_literal
+                     (fo_literal_for_arity_literal conclLit)))
+
+fun problem_line_for_conjecture full_types
+                                ({name, kind, combformula, ...} : fol_formula) =
+  Fof (conjecture_prefix ^ name, kind,
+       formula_for_combformula full_types combformula)
+
+fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
+  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
+
+fun problem_line_for_free_type j lit =
+  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
+fun problem_lines_for_free_types conjectures =
+  let
+    val litss = map free_type_literals_for_conjecture conjectures
+    val lits = fold (union (op =)) litss []
+  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
+
+(** "hBOOL" and "hAPP" **)
+
+type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+
+fun consider_term top_level (ATerm ((s, _), ts)) =
+  (if is_atp_variable s then
+     I
+   else
+     let val n = length ts in
+       Symtab.map_default
+           (s, {min_arity = n, max_arity = 0, sub_level = false})
+           (fn {min_arity, max_arity, sub_level} =>
+               {min_arity = Int.min (n, min_arity),
+                max_arity = Int.max (n, max_arity),
+                sub_level = sub_level orelse not top_level})
+     end)
+  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
+fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
+  | consider_formula (AConn (_, phis)) = fold consider_formula phis
+  | consider_formula (AAtom tm) = consider_term true tm
+
+fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
+
+fun const_table_for_problem explicit_apply problem =
+  if explicit_apply then NONE
+  else SOME (Symtab.empty |> consider_problem problem)
+
+fun min_arity_of thy full_types NONE s =
+    (if s = "equal" orelse s = type_wrapper_name orelse
+        String.isPrefix type_const_prefix s orelse
+        String.isPrefix class_prefix s then
+       16383 (* large number *)
+     else if full_types then
+       0
+     else case strip_prefix_and_unascii const_prefix s of
+       SOME s' => num_type_args thy (invert_const s')
+     | NONE => 0)
+  | min_arity_of _ _ (SOME the_const_tab) s =
+    case Symtab.lookup the_const_tab s of
+      SOME ({min_arity, ...} : const_info) => min_arity
+    | NONE => 0
+
+fun full_type_of (ATerm ((s, _), [ty, _])) =
+    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
+  | full_type_of _ = raise Fail "expected type wrapper"
+
+fun list_hAPP_rev _ t1 [] = t1
+  | list_hAPP_rev NONE t1 (t2 :: ts2) =
+    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
+    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
+                         [full_type_of t2, ty]) in
+      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
+    end
+
+fun repair_applications_in_term thy full_types const_tab =
+  let
+    fun aux opt_ty (ATerm (name as (s, _), ts)) =
+      if s = type_wrapper_name then
+        case ts of
+          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
+        | _ => raise Fail "malformed type wrapper"
+      else
+        let
+          val ts = map (aux NONE) ts
+          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
+        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
+  in aux NONE end
+
+fun boolify t = ATerm (`I "hBOOL", [t])
+
+(* True if the constant ever appears outside of the top-level position in
+   literals, or if it appears with different arities (e.g., because of different
+   type instantiations). If false, the constant always receives all of its
+   arguments and is used as a predicate. *)
+fun is_predicate NONE s =
+    s = "equal" orelse s = "$false" orelse s = "$true" orelse
+    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
+  | is_predicate (SOME the_const_tab) s =
+    case Symtab.lookup the_const_tab s of
+      SOME {min_arity, max_arity, sub_level} =>
+      not sub_level andalso min_arity = max_arity
+    | NONE => false
+
+fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+  if s = type_wrapper_name then
+    case ts of
+      [_, t' as ATerm ((s', _), _)] =>
+      if is_predicate const_tab s' then t' else boolify t
+    | _ => raise Fail "malformed type wrapper"
+  else
+    t |> not (is_predicate const_tab s) ? boolify
+
+fun close_universally phi =
+  let
+    fun term_vars bounds (ATerm (name as (s, _), tms)) =
+        (is_atp_variable s andalso not (member (op =) bounds name))
+          ? insert (op =) name
+        #> fold (term_vars bounds) tms
+    fun formula_vars bounds (AQuant (_, xs, phi)) =
+        formula_vars (xs @ bounds) phi
+      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
+      | formula_vars bounds (AAtom tm) = term_vars bounds tm
+  in
+    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
+  end
+
+fun repair_formula thy explicit_forall full_types const_tab =
+  let
+    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+      | aux (AConn (c, phis)) = AConn (c, map aux phis)
+      | aux (AAtom tm) =
+        AAtom (tm |> repair_applications_in_term thy full_types const_tab
+                  |> repair_predicates_in_term const_tab)
+  in aux #> explicit_forall ? close_universally end
+
+fun repair_problem_line thy explicit_forall full_types const_tab
+                        (Fof (ident, kind, phi)) =
+  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
+fun repair_problem_with_const_table thy =
+  map o apsnd o map ooo repair_problem_line thy
+
+fun repair_problem thy explicit_forall full_types explicit_apply problem =
+  repair_problem_with_const_table thy explicit_forall full_types
+      (const_table_for_problem explicit_apply problem) problem
+
+fun prepare_atp_problem ctxt readable_names explicit_forall full_types
+                        explicit_apply hyp_ts concl_t axioms =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
+                       arity_clauses)) =
+      prepare_formulas ctxt full_types hyp_ts concl_t axioms
+    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+    val helper_lines =
+      map (problem_line_for_fact helper_prefix full_types) helper_facts
+    val conjecture_lines =
+      map (problem_line_for_conjecture full_types) conjectures
+    val tfree_lines = problem_lines_for_free_types conjectures
+    val class_rel_lines =
+      map problem_line_for_class_rel_clause class_rel_clauses
+    val arity_lines = map problem_line_for_arity_clause arity_clauses
+    (* Reordering these might or might not confuse the proof reconstruction
+       code or the SPASS Flotter hack. *)
+    val problem =
+      [("Relevant facts", axiom_lines),
+       ("Class relationships", class_rel_lines),
+       ("Arity declarations", arity_lines),
+       ("Helper facts", helper_lines),
+       ("Conjectures", conjecture_lines),
+       ("Type variables", tfree_lines)]
+      |> repair_problem thy explicit_forall full_types explicit_apply
+    val (problem, pool) = nice_atp_problem readable_names problem
+    val conjecture_offset =
+      length axiom_lines + length class_rel_lines + length arity_lines
+      + length helper_lines
+  in
+    (problem,
+     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+     conjecture_offset, axiom_names)
+  end
+
+end;
diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Oct 22 13:49:44 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,946 +0,0 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
-    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
-    Author:     Claire Quigley, Cambridge University Computer Laboratory
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Proof reconstruction for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_RECONSTRUCT =
-sig
-  type locality = Sledgehammer_Filter.locality
-  type minimize_command = string list -> string
-  type metis_params =
-    string * bool * minimize_command * string * (string * locality) list vector
-    * thm * int
-  type isar_params =
-    string Symtab.table * bool * int * Proof.context * int list list
-  type text_result = string * (string * locality) list
-
-  val repair_conjecture_shape_and_axiom_names :
-    string -> int list list -> (string * locality) list vector
-    -> int list list * (string * locality) list vector
-  val apply_on_subgoal : int -> int -> string
-  val command_call : string -> string list -> string
-  val try_command_line : string -> string -> string
-  val minimize_line : ('a list -> string) -> 'a list -> string
-  val metis_proof_text : metis_params -> text_result
-  val isar_proof_text : isar_params -> metis_params -> text_result
-  val proof_text : bool -> isar_params -> metis_params -> text_result
-end;
-
-structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
-struct
-
-open ATP_Problem
-open ATP_Proof
-open Metis_Translate
-open Sledgehammer_Util
-open Sledgehammer_Filter
-open Sledgehammer_Translate
-
-type minimize_command = string list -> string
-type metis_params =
-  string * bool * minimize_command * string * (string * locality) list vector
-  * thm * int
-type isar_params =
-  string Symtab.table * bool * int * Proof.context * int list list
-type text_result = string * (string * locality) list
-
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
-fun find_first_in_list_vector vec key =
-  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
-                 | (_, value) => value) NONE vec
-
-
-(** SPASS's Flotter hack **)
-
-(* This is a hack required for keeping track of axioms after they have been
-   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
-   part of this hack. *)
-
-val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
-
-fun extract_clause_sequence output =
-  let
-    val tokens_of = String.tokens (not o Char.isAlphaNum)
-    fun extract_num ("clause" :: (ss as _ :: _)) =
-    Int.fromString (List.last ss)
-      | extract_num _ = NONE
-  in output |> split_lines |> map_filter (extract_num o tokens_of) end
-
-val parse_clause_formula_pair =
-  $$ "(" |-- scan_integer --| $$ ","
-  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
-  --| Scan.option ($$ ",")
-val parse_clause_formula_relation =
-  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
-  |-- Scan.repeat parse_clause_formula_pair
-val extract_clause_formula_relation =
-  Substring.full #> Substring.position set_ClauseFormulaRelationN
-  #> snd #> Substring.position "." #> fst #> Substring.string
-  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
-  #> fst
-
-fun repair_conjecture_shape_and_axiom_names output conjecture_shape
-                                            axiom_names =
-  if String.isSubstring set_ClauseFormulaRelationN output then
-    let
-      val j0 = hd (hd conjecture_shape)
-      val seq = extract_clause_sequence output
-      val name_map = extract_clause_formula_relation output
-      fun renumber_conjecture j =
-        conjecture_prefix ^ string_of_int (j - j0)
-        |> AList.find (fn (s, ss) => member (op =) ss s) name_map
-        |> map (fn s => find_index (curry (op =) s) seq + 1)
-      fun names_for_number j =
-        j |> AList.lookup (op =) name_map |> these
-          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
-          |> map (fn name =>
-                     (name, name |> find_first_in_list_vector axiom_names
-                                 |> the)
-                     handle Option.Option =>
-                            error ("No such fact: " ^ quote name ^ "."))
-    in
-      (conjecture_shape |> map (maps renumber_conjecture),
-       seq |> map names_for_number |> Vector.fromList)
-    end
-  else
-    (conjecture_shape, axiom_names)
-
-
-(** Soft-core proof reconstruction: Metis one-liner **)
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
-fun apply_on_subgoal _ 1 = "by "
-  | apply_on_subgoal 1 _ = "apply "
-  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
-fun command_call name [] = name
-  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-fun try_command_line banner command =
-  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
-fun using_labels [] = ""
-  | using_labels ls =
-    "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types ss = command_call (metis_name full_types) ss
-fun metis_command full_types i n (ls, ss) =
-  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
-fun metis_line banner full_types i n ss =
-  try_command_line banner (metis_command full_types i n ([], ss))
-fun minimize_line _ [] = ""
-  | minimize_line minimize_command ss =
-    case minimize_command ss of
-      "" => ""
-    | command =>
-      "\nTo minimize the number of lemmas, try this: " ^
-      Markup.markup Markup.sendback command ^ "."
-
-fun resolve_axiom axiom_names ((_, SOME s)) =
-    (case strip_prefix_and_unascii axiom_prefix s of
-       SOME s' => (case find_first_in_list_vector axiom_names s' of
-                     SOME x => [(s', x)]
-                   | NONE => [])
-     | NONE => [])
-  | resolve_axiom axiom_names (num, NONE) =
-    case Int.fromString num of
-      SOME j =>
-      if j > 0 andalso j <= Vector.length axiom_names then
-        Vector.sub (axiom_names, j - 1)
-      else
-        []
-    | NONE => []
-
-fun add_fact axiom_names (Inference (name, _, [])) =
-    append (resolve_axiom axiom_names name)
-  | add_fact _ _ = I
-
-fun used_facts_in_tstplike_proof axiom_names =
-  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
-
-fun used_facts axiom_names =
-  used_facts_in_tstplike_proof axiom_names
-  #> List.partition (curry (op =) Chained o snd)
-  #> pairself (sort_distinct (string_ord o pairself fst))
-
-fun metis_proof_text (banner, full_types, minimize_command,
-                      tstplike_proof, axiom_names, goal, i) =
-  let
-    val (chained_lemmas, other_lemmas) =
-      used_facts axiom_names tstplike_proof
-    val n = Logic.count_prems (prop_of goal)
-  in
-    (metis_line banner full_types i n (map fst other_lemmas) ^
-     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
-     other_lemmas @ chained_lemmas)
-  end
-
-
-(** Hard-core proof reconstruction: structured Isar proofs **)
-
-(* Simple simplifications to ensure that sort annotations don't leave a trail of
-   spurious "True"s. *)
-fun s_not @{const False} = @{const True}
-  | s_not @{const True} = @{const False}
-  | s_not (@{const Not} $ t) = t
-  | s_not t = @{const Not} $ t
-fun s_conj (@{const True}, t2) = t2
-  | s_conj (t1, @{const True}) = t1
-  | s_conj p = HOLogic.mk_conj p
-fun s_disj (@{const False}, t2) = t2
-  | s_disj (t1, @{const False}) = t1
-  | s_disj p = HOLogic.mk_disj p
-fun s_imp (@{const True}, t2) = t2
-  | s_imp (t1, @{const False}) = s_not t1
-  | s_imp p = HOLogic.mk_imp p
-fun s_iff (@{const True}, t2) = t2
-  | s_iff (t1, @{const True}) = t1
-  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
-
-fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
-    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
-  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
-    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
-  | negate_term (@{const HOL.implies} $ t1 $ t2) =
-    @{const HOL.conj} $ t1 $ negate_term t2
-  | negate_term (@{const HOL.conj} $ t1 $ t2) =
-    @{const HOL.disj} $ negate_term t1 $ negate_term t2
-  | negate_term (@{const HOL.disj} $ t1 $ t2) =
-    @{const HOL.conj} $ negate_term t1 $ negate_term t2
-  | negate_term (@{const Not} $ t) = t
-  | negate_term t = @{const Not} $ t
-
-val indent_size = 2
-val no_label = ("", ~1)
-
-val raw_prefix = "X"
-val assum_prefix = "A"
-val fact_prefix = "F"
-
-fun resolve_conjecture conjecture_shape (num, s_opt) =
-  let
-    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
-              SOME s => Int.fromString s |> the_default ~1
-            | NONE => case Int.fromString num of
-                        SOME j => find_index (exists (curry (op =) j))
-                                             conjecture_shape
-                      | NONE => ~1
-  in if k >= 0 then [k] else [] end
-
-fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
-fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
-
-fun raw_label_for_name conjecture_shape name =
-  case resolve_conjecture conjecture_shape name of
-    [j] => (conjecture_prefix, j)
-  | _ => case Int.fromString (fst name) of
-           SOME j => (raw_prefix, j)
-         | NONE => (raw_prefix ^ fst name, 0)
-
-(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-
-exception FO_TERM of string fo_term list
-exception FORMULA of (string, string fo_term) formula list
-exception SAME of unit
-
-(* Type variables are given the basic sort "HOL.type". Some will later be
-   constrained by information from type literals, or by type inference. *)
-fun type_from_fo_term tfrees (u as ATerm (a, us)) =
-  let val Ts = map (type_from_fo_term tfrees) us in
-    case strip_prefix_and_unascii type_const_prefix a of
-      SOME b => Type (invert_const b, Ts)
-    | NONE =>
-      if not (null us) then
-        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
-      else case strip_prefix_and_unascii tfree_prefix a of
-        SOME b =>
-        let val s = "'" ^ b in
-          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
-        end
-      | NONE =>
-        case strip_prefix_and_unascii tvar_prefix a of
-          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
-        | NONE =>
-          (* Variable from the ATP, say "X1" *)
-          Type_Infer.param 0 (a, HOLogic.typeS)
-  end
-
-(* Type class literal applied to a type. Returns triple of polarity, class,
-   type. *)
-fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
-  case (strip_prefix_and_unascii class_prefix a,
-        map (type_from_fo_term tfrees) us) of
-    (SOME b, [T]) => (pos, b, T)
-  | _ => raise FO_TERM [u]
-
-(** Accumulate type constraints in a formula: negative type literals **)
-fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
-fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
-  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
-  | add_type_constraint _ = I
-
-fun repair_atp_variable_name f s =
-  let
-    fun subscript_name s n = s ^ nat_subscript n
-    val s = String.map f s
-  in
-    case space_explode "_" s of
-      [_] => (case take_suffix Char.isDigit (String.explode s) of
-                (cs1 as _ :: _, cs2 as _ :: _) =>
-                subscript_name (String.implode cs1)
-                               (the (Int.fromString (String.implode cs2)))
-              | (_, _) => s)
-    | [s1, s2] => (case Int.fromString s2 of
-                     SOME n => subscript_name s1 n
-                   | NONE => s)
-    | _ => s
-  end
-
-(* First-order translation. No types are known for variables. "HOLogic.typeT"
-   should allow them to be inferred. *)
-fun raw_term_from_pred thy full_types tfrees =
-  let
-    fun aux opt_T extra_us u =
-      case u of
-        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
-      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
-      | ATerm (a, us) =>
-        if a = type_wrapper_name then
-          case us of
-            [typ_u, term_u] =>
-            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
-          | _ => raise FO_TERM us
-        else case strip_prefix_and_unascii const_prefix a of
-          SOME "equal" =>
-          let val ts = map (aux NONE []) us in
-            if length ts = 2 andalso hd ts aconv List.last ts then
-              (* Vampire is keen on producing these. *)
-              @{const True}
-            else
-              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
-          end
-        | SOME b =>
-          let
-            val c = invert_const b
-            val num_type_args = num_type_args thy c
-            val (type_us, term_us) =
-              chop (if full_types then 0 else num_type_args) us
-            (* Extra args from "hAPP" come after any arguments given directly to
-               the constant. *)
-            val term_ts = map (aux NONE []) term_us
-            val extra_ts = map (aux NONE []) extra_us
-            val t =
-              Const (c, if full_types then
-                          case opt_T of
-                            SOME T => map fastype_of term_ts ---> T
-                          | NONE =>
-                            if num_type_args = 0 then
-                              Sign.const_instance thy (c, [])
-                            else
-                              raise Fail ("no type information for " ^ quote c)
-                        else
-                          Sign.const_instance thy (c,
-                              map (type_from_fo_term tfrees) type_us))
-          in list_comb (t, term_ts @ extra_ts) end
-        | NONE => (* a free or schematic variable *)
-          let
-            val ts = map (aux NONE []) (us @ extra_us)
-            val T = map fastype_of ts ---> HOLogic.typeT
-            val t =
-              case strip_prefix_and_unascii fixed_var_prefix a of
-                SOME b => Free (b, T)
-              | NONE =>
-                case strip_prefix_and_unascii schematic_var_prefix a of
-                  SOME b => Var ((b, 0), T)
-                | NONE =>
-                  if is_atp_variable a then
-                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
-                  else
-                    (* Skolem constants? *)
-                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
-          in list_comb (t, ts) end
-  in aux (SOME HOLogic.boolT) [] end
-
-fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
-  if String.isPrefix class_prefix s then
-    add_type_constraint (type_constraint_from_term pos tfrees u)
-    #> pair @{const True}
-  else
-    pair (raw_term_from_pred thy full_types tfrees u)
-
-val combinator_table =
-  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
-   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
-   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
-   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
-   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
-
-fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
-  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
-  | uncombine_term (t as Const (x as (s, _))) =
-    (case AList.lookup (op =) combinator_table s of
-       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
-     | NONE => t)
-  | uncombine_term t = t
-
-(* Update schematic type variables with detected sort constraints. It's not
-   totally clear when this code is necessary. *)
-fun repair_tvar_sorts (t, tvar_tab) =
-  let
-    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
-      | do_type (TVar (xi, s)) =
-        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
-      | do_type (TFree z) = TFree z
-    fun do_term (Const (a, T)) = Const (a, do_type T)
-      | do_term (Free (a, T)) = Free (a, do_type T)
-      | do_term (Var (xi, T)) = Var (xi, do_type T)
-      | do_term (t as Bound _) = t
-      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
-      | do_term (t1 $ t2) = do_term t1 $ do_term t2
-  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
-
-fun quantify_over_var quant_of var_s t =
-  let
-    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
-                  |> map Var
-  in fold_rev quant_of vars t end
-
-(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
-   appear in the formula. *)
-fun prop_from_formula thy full_types tfrees phi =
-  let
-    fun do_formula pos phi =
-      case phi of
-        AQuant (_, [], phi) => do_formula pos phi
-      | AQuant (q, x :: xs, phi') =>
-        do_formula pos (AQuant (q, xs, phi'))
-        #>> quantify_over_var (case q of
-                                 AForall => forall_of
-                               | AExists => exists_of)
-                              (repair_atp_variable_name Char.toLower x)
-      | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
-      | AConn (c, [phi1, phi2]) =>
-        do_formula (pos |> c = AImplies ? not) phi1
-        ##>> do_formula pos phi2
-        #>> (case c of
-               AAnd => s_conj
-             | AOr => s_disj
-             | AImplies => s_imp
-             | AIf => s_imp o swap
-             | AIff => s_iff
-             | ANotIff => s_not o s_iff)
-      | AAtom tm => term_from_pred thy full_types tfrees pos tm
-      | _ => raise FORMULA [phi]
-  in repair_tvar_sorts (do_formula true phi Vartab.empty) end
-
-fun check_formula ctxt =
-  Type.constraint HOLogic.boolT
-  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-
-
-(**** Translation of TSTP files to Isar Proofs ****)
-
-fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
-  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-
-fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val t1 = prop_from_formula thy full_types tfrees phi1
-      val vars = snd (strip_comb t1)
-      val frees = map unvarify_term vars
-      val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = prop_from_formula thy full_types tfrees phi2
-      val (t1, t2) =
-        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
-        |> unvarify_args |> uncombine_term |> check_formula ctxt
-        |> HOLogic.dest_eq
-    in
-      (Definition (name, t1, t2),
-       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
-    end
-  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
-    let
-      val thy = ProofContext.theory_of ctxt
-      val t = u |> prop_from_formula thy full_types tfrees
-                |> uncombine_term |> check_formula ctxt
-    in
-      (Inference (name, t, deps),
-       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
-    end
-fun decode_lines ctxt full_types tfrees lines =
-  fst (fold_map (decode_line full_types tfrees) lines ctxt)
-
-fun is_same_inference _ (Definition _) = false
-  | is_same_inference t (Inference (_, t', _)) = t aconv t'
-
-(* No "real" literals means only type information (tfree_tcs, clsrel, or
-   clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
-
-fun replace_one_dependency (old, new) dep =
-  if is_same_step (dep, old) then new else [dep]
-fun replace_dependencies_in_line _ (line as Definition _) = line
-  | replace_dependencies_in_line p (Inference (name, t, deps)) =
-    Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
-
-(* Discard axioms; consolidate adjacent lines that prove the same formula, since
-   they differ only in type information.*)
-fun add_line _ _ (line as Definition _) lines = line :: lines
-  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
-    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
-       definitions. *)
-    if is_axiom axiom_names name then
-      (* Axioms are not proof lines. *)
-      if is_only_type_information t then
-        map (replace_dependencies_in_line (name, [])) lines
-      (* Is there a repetition? If so, replace later line by earlier one. *)
-      else case take_prefix (not o is_same_inference t) lines of
-        (_, []) => lines (* no repetition of proof line *)
-      | (pre, Inference (name', _, _) :: post) =>
-        pre @ map (replace_dependencies_in_line (name', [name])) post
-    else if is_conjecture conjecture_shape name then
-      Inference (name, negate_term t, []) :: lines
-    else
-      map (replace_dependencies_in_line (name, [])) lines
-  | add_line _ _ (Inference (name, t, deps)) lines =
-    (* Type information will be deleted later; skip repetition test. *)
-    if is_only_type_information t then
-      Inference (name, t, deps) :: lines
-    (* Is there a repetition? If so, replace later line by earlier one. *)
-    else case take_prefix (not o is_same_inference t) lines of
-      (* FIXME: Doesn't this code risk conflating proofs involving different
-         types? *)
-       (_, []) => Inference (name, t, deps) :: lines
-     | (pre, Inference (name', t', _) :: post) =>
-       Inference (name, t', deps) ::
-       pre @ map (replace_dependencies_in_line (name', [name])) post
-
-(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (Inference (name, t, [])) lines =
-    if is_only_type_information t then delete_dependency name lines
-    else Inference (name, t, []) :: lines
-  | add_nontrivial_line line lines = line :: lines
-and delete_dependency name lines =
-  fold_rev add_nontrivial_line
-           (map (replace_dependencies_in_line (name, [])) lines) []
-
-(* ATPs sometimes reuse free variable names in the strangest ways. Removing
-   offending lines often does the trick. *)
-fun is_bad_free frees (Free x) = not (member (op =) frees x)
-  | is_bad_free _ _ = false
-
-fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
-    (j, line :: map (replace_dependencies_in_line (name, [])) lines)
-  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
-                     (Inference (name, t, deps)) (j, lines) =
-    (j + 1,
-     if is_axiom axiom_names name orelse
-        is_conjecture conjecture_shape name orelse
-        (* the last line must be kept *)
-        j = 0 orelse
-        (not (is_only_type_information t) andalso
-         null (Term.add_tvars t []) andalso
-         not (exists_subterm (is_bad_free frees) t) andalso
-         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
-         (* kill next to last line, which usually results in a trivial step *)
-         j <> 1) then
-       Inference (name, t, deps) :: lines  (* keep line *)
-     else
-       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
-
-(** Isar proof construction and manipulation **)
-
-fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
-  (union (op =) ls1 ls2, union (op =) ss1 ss2)
-
-type label = string * int
-type facts = label list * string list
-
-datatype isar_qualifier = Show | Then | Moreover | Ultimately
-
-datatype isar_step =
-  Fix of (string * typ) list |
-  Let of term * term |
-  Assume of label * term |
-  Have of isar_qualifier list * label * term * byline
-and byline =
-  ByMetis of facts |
-  CaseSplit of isar_step list list * facts
-
-fun smart_case_split [] facts = ByMetis facts
-  | smart_case_split proofs facts = CaseSplit (proofs, facts)
-
-fun add_fact_from_dependency conjecture_shape axiom_names name =
-  if is_axiom axiom_names name then
-    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
-  else
-    apfst (insert (op =) (raw_label_for_name conjecture_shape name))
-
-fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
-  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
-    Assume (raw_label_for_name conjecture_shape name, t)
-  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
-    Have (if j = 1 then [Show] else [],
-          raw_label_for_name conjecture_shape name,
-          fold_rev forall_of (map Var (Term.add_vars t [])) t,
-          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
-                        deps ([], [])))
-
-fun repair_name "$true" = "c_True"
-  | repair_name "$false" = "c_False"
-  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
-  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
-  | repair_name s =
-    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
-      "c_equal" (* seen in Vampire proofs *)
-    else
-      s
-
-fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
-        tstplike_proof conjecture_shape axiom_names params frees =
-  let
-    val lines =
-      tstplike_proof
-      |> atp_proof_from_tstplike_string
-      |> nasty_atp_proof pool
-      |> map_term_names_in_atp_proof repair_name
-      |> decode_lines ctxt full_types tfrees
-      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
-      |> rpair [] |-> fold_rev add_nontrivial_line
-      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
-                                             conjecture_shape axiom_names frees)
-      |> snd
-  in
-    (if null params then [] else [Fix params]) @
-    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
-         lines
-  end
-
-(* When redirecting proofs, we keep information about the labels seen so far in
-   the "backpatches" data structure. The first component indicates which facts
-   should be associated with forthcoming proof steps. The second component is a
-   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
-   become assumptions and "drop_ls" are the labels that should be dropped in a
-   case split. *)
-type backpatches = (label * facts) list * (label list * label list)
-
-fun used_labels_of_step (Have (_, _, _, by)) =
-    (case by of
-       ByMetis (ls, _) => ls
-     | CaseSplit (proofs, (ls, _)) =>
-       fold (union (op =) o used_labels_of) proofs ls)
-  | used_labels_of_step _ = []
-and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
-
-fun new_labels_of_step (Fix _) = []
-  | new_labels_of_step (Let _) = []
-  | new_labels_of_step (Assume (l, _)) = [l]
-  | new_labels_of_step (Have (_, l, _, _)) = [l]
-val new_labels_of = maps new_labels_of_step
-
-val join_proofs =
-  let
-    fun aux _ [] = NONE
-      | aux proof_tail (proofs as (proof1 :: _)) =
-        if exists null proofs then
-          NONE
-        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
-          aux (hd proof1 :: proof_tail) (map tl proofs)
-        else case hd proof1 of
-          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
-          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
-                      | _ => false) (tl proofs) andalso
-             not (exists (member (op =) (maps new_labels_of proofs))
-                         (used_labels_of proof_tail)) then
-            SOME (l, t, map rev proofs, proof_tail)
-          else
-            NONE
-        | _ => NONE
-  in aux [] o map rev end
-
-fun case_split_qualifiers proofs =
-  case length proofs of
-    0 => []
-  | 1 => [Then]
-  | _ => [Ultimately]
-
-fun redirect_proof hyp_ts concl_t proof =
-  let
-    (* The first pass outputs those steps that are independent of the negated
-       conjecture. The second pass flips the proof by contradiction to obtain a
-       direct proof, introducing case splits when an inference depends on
-       several facts that depend on the negated conjecture. *)
-     val concl_l = (conjecture_prefix, length hyp_ts)
-     fun first_pass ([], contra) = ([], contra)
-       | first_pass ((step as Fix _) :: proof, contra) =
-         first_pass (proof, contra) |>> cons step
-       | first_pass ((step as Let _) :: proof, contra) =
-         first_pass (proof, contra) |>> cons step
-       | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
-         if l = concl_l then first_pass (proof, contra ||> cons step)
-         else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
-       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
-         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
-           if exists (member (op =) (fst contra)) ls then
-             first_pass (proof, contra |>> cons l ||> cons step)
-           else
-             first_pass (proof, contra) |>> cons step
-         end
-       | first_pass _ = raise Fail "malformed proof"
-    val (proof_top, (contra_ls, contra_proof)) =
-      first_pass (proof, ([concl_l], []))
-    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
-    fun backpatch_labels patches ls =
-      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
-    fun second_pass end_qs ([], assums, patches) =
-        ([Have (end_qs, no_label, concl_t,
-                ByMetis (backpatch_labels patches (map snd assums)))], patches)
-      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
-        second_pass end_qs (proof, (t, l) :: assums, patches)
-      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
-                            patches) =
-        (if member (op =) (snd (snd patches)) l andalso
-            not (member (op =) (fst (snd patches)) l) andalso
-            not (AList.defined (op =) (fst patches) l) then
-           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
-         else case List.partition (member (op =) contra_ls) ls of
-           ([contra_l], co_ls) =>
-           if member (op =) qs Show then
-             second_pass end_qs (proof, assums,
-                                 patches |>> cons (contra_l, (co_ls, ss)))
-           else
-             second_pass end_qs
-                         (proof, assums,
-                          patches |>> cons (contra_l, (l :: co_ls, ss)))
-             |>> cons (if member (op =) (fst (snd patches)) l then
-                         Assume (l, negate_term t)
-                       else
-                         Have (qs, l, negate_term t,
-                               ByMetis (backpatch_label patches l)))
-         | (contra_ls as _ :: _, co_ls) =>
-           let
-             val proofs =
-               map_filter
-                   (fn l =>
-                       if l = concl_l then
-                         NONE
-                       else
-                         let
-                           val drop_ls = filter (curry (op <>) l) contra_ls
-                         in
-                           second_pass []
-                               (proof, assums,
-                                patches ||> apfst (insert (op =) l)
-                                        ||> apsnd (union (op =) drop_ls))
-                           |> fst |> SOME
-                         end) contra_ls
-             val (assumes, facts) =
-               if member (op =) (fst (snd patches)) l then
-                 ([Assume (l, negate_term t)], (l :: co_ls, ss))
-               else
-                 ([], (co_ls, ss))
-           in
-             (case join_proofs proofs of
-                SOME (l, t, proofs, proof_tail) =>
-                Have (case_split_qualifiers proofs @
-                      (if null proof_tail then end_qs else []), l, t,
-                      smart_case_split proofs facts) :: proof_tail
-              | NONE =>
-                [Have (case_split_qualifiers proofs @ end_qs, no_label,
-                       concl_t, smart_case_split proofs facts)],
-              patches)
-             |>> append assumes
-           end
-         | _ => raise Fail "malformed proof")
-       | second_pass _ _ = raise Fail "malformed proof"
-    val proof_bottom =
-      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
-  in proof_top @ proof_bottom end
-
-(* FIXME: Still needed? Probably not. *)
-val kill_duplicate_assumptions_in_proof =
-  let
-    fun relabel_facts subst =
-      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
-    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
-        (case AList.lookup (op aconv) assums t of
-           SOME l' => (proof, (l, l') :: subst, assums)
-         | NONE => (step :: proof, subst, (t, l) :: assums))
-      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
-        (Have (qs, l, t,
-               case by of
-                 ByMetis facts => ByMetis (relabel_facts subst facts)
-               | CaseSplit (proofs, facts) =>
-                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
-         proof, subst, assums)
-      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
-    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
-  in do_proof end
-
-val then_chain_proof =
-  let
-    fun aux _ [] = []
-      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
-      | aux l' (Have (qs, l, t, by) :: proof) =
-        (case by of
-           ByMetis (ls, ss) =>
-           Have (if member (op =) ls l' then
-                   (Then :: qs, l, t,
-                    ByMetis (filter_out (curry (op =) l') ls, ss))
-                 else
-                   (qs, l, t, ByMetis (ls, ss)))
-         | CaseSplit (proofs, facts) =>
-           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
-        aux l proof
-      | aux _ (step :: proof) = step :: aux no_label proof
-  in aux no_label end
-
-fun kill_useless_labels_in_proof proof =
-  let
-    val used_ls = used_labels_of proof
-    fun do_label l = if member (op =) used_ls l then l else no_label
-    fun do_step (Assume (l, t)) = Assume (do_label l, t)
-      | do_step (Have (qs, l, t, by)) =
-        Have (qs, do_label l, t,
-              case by of
-                CaseSplit (proofs, facts) =>
-                CaseSplit (map (map do_step) proofs, facts)
-              | _ => by)
-      | do_step step = step
-  in map do_step proof end
-
-fun prefix_for_depth n = replicate_string (n + 1)
-
-val relabel_proof =
-  let
-    fun aux _ _ _ [] = []
-      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
-        if l = no_label then
-          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
-        else
-          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
-            Assume (l', t) ::
-            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
-          end
-      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
-        let
-          val (l', subst, next_fact) =
-            if l = no_label then
-              (l, subst, next_fact)
-            else
-              let
-                val l' = (prefix_for_depth depth fact_prefix, next_fact)
-              in (l', (l, l') :: subst, next_fact + 1) end
-          val relabel_facts =
-            apfst (maps (the_list o AList.lookup (op =) subst))
-          val by =
-            case by of
-              ByMetis facts => ByMetis (relabel_facts facts)
-            | CaseSplit (proofs, facts) =>
-              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
-                         relabel_facts facts)
-        in
-          Have (qs, l', t, by) ::
-          aux subst depth (next_assum, next_fact) proof
-        end
-      | aux subst depth nextp (step :: proof) =
-        step :: aux subst depth nextp proof
-  in aux [] 0 (1, 1) end
-
-fun string_for_proof ctxt0 full_types i n =
-  let
-    val ctxt = ctxt0
-      |> Config.put show_free_types false
-      |> Config.put show_types true
-    fun fix_print_mode f x =
-      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                               (print_mode_value ())) f x
-    fun do_indent ind = replicate_string (ind * indent_size) " "
-    fun do_free (s, T) =
-      maybe_quote s ^ " :: " ^
-      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
-    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
-    fun do_have qs =
-      (if member (op =) qs Moreover then "moreover " else "") ^
-      (if member (op =) qs Ultimately then "ultimately " else "") ^
-      (if member (op =) qs Then then
-         if member (op =) qs Show then "thus" else "hence"
-       else
-         if member (op =) qs Show then "show" else "have")
-    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    fun do_facts (ls, ss) =
-      metis_command full_types 1 1
-                    (ls |> sort_distinct (prod_ord string_ord int_ord),
-                     ss |> sort_distinct string_ord)
-    and do_step ind (Fix xs) =
-        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
-      | do_step ind (Let (t1, t2)) =
-        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
-      | do_step ind (Assume (l, t)) =
-        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
-      | do_step ind (Have (qs, l, t, ByMetis facts)) =
-        do_indent ind ^ do_have qs ^ " " ^
-        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
-      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
-        space_implode (do_indent ind ^ "moreover\n")
-                      (map (do_block ind) proofs) ^
-        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
-        do_facts facts ^ "\n"
-    and do_steps prefix suffix ind steps =
-      let val s = implode (map (do_step ind) steps) in
-        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
-        String.extract (s, ind * indent_size,
-                        SOME (size s - ind * indent_size - 1)) ^
-        suffix ^ "\n"
-      end
-    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
-    (* One-step proofs are pointless; better use the Metis one-liner
-       directly. *)
-    and do_proof [Have (_, _, _, ByMetis _)] = ""
-      | do_proof proof =
-        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
-        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
-        (if n <> 1 then "next" else "qed")
-  in do_proof end
-
-fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-                    (other_params as (_, full_types, _, tstplike_proof,
-                                      axiom_names, goal, i)) =
-  let
-    val (params, hyp_ts, concl_t) = strip_subgoal goal i
-    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
-    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
-    val n = Logic.count_prems (prop_of goal)
-    val (one_line_proof, lemma_names) = metis_proof_text other_params
-    fun isar_proof_for () =
-      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
-               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
-               params frees
-           |> redirect_proof hyp_ts concl_t
-           |> kill_duplicate_assumptions_in_proof
-           |> then_chain_proof
-           |> kill_useless_labels_in_proof
-           |> relabel_proof
-           |> string_for_proof ctxt full_types i n of
-        "" => "\nNo structured proof available."
-      | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
-    val isar_proof =
-      if debug then
-        isar_proof_for ()
-      else
-        try isar_proof_for ()
-        |> the_default "\nWarning: The Isar proof construction failed."
-  in (one_line_proof ^ isar_proof, lemma_names) end
-
-fun proof_text isar_proof isar_params other_params =
-  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
-      other_params
-
-end;
diff -r 80d4ea0e536a -r 0783415ed7f0 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Oct 22 13:49:44 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,533 +0,0 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
-    Author:     Fabian Immler, TU Muenchen
-    Author:     Makarius
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Translation of HOL to FOL for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_TRANSLATE =
-sig
-  type 'a problem = 'a ATP_Problem.problem
-  type fol_formula
-
-  val axiom_prefix : string
-  val conjecture_prefix : string
-  val prepare_axiom :
-    Proof.context -> (string * 'a) * thm
-    -> term * ((string * 'a) * fol_formula) option
-  val prepare_atp_problem :
-    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> (term * ((string * 'a) * fol_formula) option) list
-    -> string problem * string Symtab.table * int * (string * 'a) list vector
-end;
-
-structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
-struct
-
-open ATP_Problem
-open Metis_Translate
-open Sledgehammer_Util
-
-val axiom_prefix = "ax_"
-val conjecture_prefix = "conj_"
-val helper_prefix = "help_"
-val class_rel_clause_prefix = "clrel_";
-val arity_clause_prefix = "arity_"
-val tfree_prefix = "tfree_"
-
-(* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
-
-type fol_formula =
-  {name: string,
-   kind: kind,
-   combformula: (name, combterm) formula,
-   ctypes_sorts: typ list}
-
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
-fun mk_ahorn [] phi = phi
-  | mk_ahorn (phi :: phis) psi =
-    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
-
-fun combformula_for_prop thy =
-  let
-    val do_term = combterm_from_term thy ~1
-    fun do_quant bs q s T t' =
-      let val s = Name.variant (map fst bs) s in
-        do_formula ((s, T) :: bs) t'
-        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
-      end
-    and do_conn bs c t1 t2 =
-      do_formula bs t1 ##>> do_formula bs t2
-      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
-    and do_formula bs t =
-      case t of
-        @{const Not} $ t1 =>
-        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
-      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
-        do_quant bs AForall s T t'
-      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
-        do_quant bs AExists s T t'
-      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
-      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
-      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
-      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
-        do_conn bs AIff t1 t2
-      | _ => (fn ts => do_term bs (Envir.eta_contract t)
-                       |>> AAtom ||> union (op =) ts)
-  in do_formula [] end
-
-val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
-
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
-fun conceal_bounds Ts t =
-  subst_bounds (map (Free o apfst concealed_bound_name)
-                    (0 upto length Ts - 1 ~~ Ts), t)
-fun reveal_bounds Ts =
-  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
-                    (0 upto length Ts - 1 ~~ Ts))
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
-   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
-fun extensionalize_term t =
-  let
-    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
-      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
-                                        Type (_, [_, res_T])]))
-                    $ t2 $ Abs (var_s, var_T, t')) =
-        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
-          let val var_t = Var ((var_s, j), var_T) in
-            Const (s, T' --> T' --> res_T)
-              $ betapply (t2, var_t) $ subst_bound (var_t, t')
-            |> aux (j + 1)
-          end
-        else
-          t
-      | aux _ t = t
-  in aux (maxidx_of_term t + 1) t end
-
-fun introduce_combinators_in_term ctxt kind t =
-  let val thy = ProofContext.theory_of ctxt in
-    if Meson.is_fol_term thy t then
-      t
-    else
-      let
-        fun aux Ts t =
-          case t of
-            @{const Not} $ t1 => @{const Not} $ aux Ts t1
-          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
-            t0 $ Abs (s, T, aux (T :: Ts) t')
-          | (t0 as Const (@{const_name All}, _)) $ t1 =>
-            aux Ts (t0 $ eta_expand Ts t1 1)
-          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
-            t0 $ Abs (s, T, aux (T :: Ts) t')
-          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
-            aux Ts (t0 $ eta_expand Ts t1 1)
-          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
-              $ t1 $ t2 =>
-            t0 $ aux Ts t1 $ aux Ts t2
-          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
-                   t
-                 else
-                   t |> conceal_bounds Ts
-                     |> Envir.eta_contract
-                     |> cterm_of thy
-                     |> Meson_Clausify.introduce_combinators_in_cterm
-                     |> prop_of |> Logic.dest_equals |> snd
-                     |> reveal_bounds Ts
-        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
-      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
-      handle THM _ =>
-             (* A type variable of sort "{}" will make abstraction fail. *)
-             if kind = Conjecture then HOLogic.false_const
-             else HOLogic.true_const
-  end
-
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
-   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
-fun freeze_term t =
-  let
-    fun aux (t $ u) = aux t $ aux u
-      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
-      | aux (Var ((s, i), T)) =
-        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
-      | aux t = t
-  in t |> exists_subterm is_Var t ? aux end
-
-(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
-    it leaves metaequalities over "prop"s alone. *)
-val atomize_term =
-  let
-    fun aux (@{const Trueprop} $ t1) = t1
-      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
-        HOLogic.all_const T $ Abs (s, T, aux t')
-      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
-      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
-        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
-      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
-        HOLogic.eq_const T $ t1 $ t2
-      | aux _ = raise Fail "aux"
-  in perhaps (try aux) end
-
-(* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp name kind t =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val t = t |> Envir.beta_eta_contract
-              |> transform_elim_term
-              |> atomize_term
-    val need_trueprop = (fastype_of t = HOLogic.boolT)
-    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
-              |> extensionalize_term
-              |> presimp ? presimplify_term thy
-              |> perhaps (try (HOLogic.dest_Trueprop))
-              |> introduce_combinators_in_term ctxt kind
-              |> kind <> Axiom ? freeze_term
-    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
-  in
-    {name = name, combformula = combformula, kind = kind,
-     ctypes_sorts = ctypes_sorts}
-  end
-
-fun make_axiom ctxt presimp ((name, loc), th) =
-  case make_formula ctxt presimp name Axiom (prop_of th) of
-    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
-  | formula => SOME ((name, loc), formula)
-fun make_conjecture ctxt ts =
-  let val last = length ts - 1 in
-    map2 (fn j => make_formula ctxt true (Int.toString j)
-                               (if j = last then Conjecture else Hypothesis))
-         (0 upto last) ts
-  end
-
-(** Helper facts **)
-
-fun count_combterm (CombConst ((s, _), _, _)) =
-    Symtab.map_entry s (Integer.add 1)
-  | count_combterm (CombVar _) = I
-  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
-fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
-  | count_combformula (AConn (_, phis)) = fold count_combformula phis
-  | count_combformula (AAtom tm) = count_combterm tm
-fun count_fol_formula ({combformula, ...} : fol_formula) =
-  count_combformula combformula
-
-val optional_helpers =
-  [(["c_COMBI"], @{thms Meson.COMBI_def}),
-   (["c_COMBK"], @{thms Meson.COMBK_def}),
-   (["c_COMBB"], @{thms Meson.COMBB_def}),
-   (["c_COMBC"], @{thms Meson.COMBC_def}),
-   (["c_COMBS"], @{thms Meson.COMBS_def})]
-val optional_typed_helpers =
-  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
-   (["c_If"], @{thms if_True if_False})]
-val mandatory_helpers = @{thms Metis.fequal_def}
-
-val init_counters =
-  [optional_helpers, optional_typed_helpers] |> maps (maps fst)
-  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
-
-fun get_helper_facts ctxt is_FO full_types conjectures axioms =
-  let
-    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
-    fun is_needed c = the (Symtab.lookup ct c) > 0
-    fun baptize th = ((Thm.get_name_hint th, false), th)
-  in
-    (optional_helpers
-     |> full_types ? append optional_typed_helpers
-     |> maps (fn (ss, ths) =>
-                 if exists is_needed ss then map baptize ths else [])) @
-    (if is_FO then [] else map baptize mandatory_helpers)
-    |> map_filter (Option.map snd o make_axiom ctxt false)
-  end
-
-fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
-
-fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
-    (* Remove existing axioms from the conjecture, as this can dramatically
-       boost an ATP's performance (for some reason). *)
-    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
-    val goal_t = Logic.list_implies (hyp_ts, concl_t)
-    val is_FO = Meson.is_fol_term thy goal_t
-    val subs = tfree_classes_of_terms [goal_t]
-    val supers = tvar_classes_of_terms axiom_ts
-    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
-    (* TFrees in the conjecture; TVars in the axioms *)
-    val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
-    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
-    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
-    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
-    val class_rel_clauses = make_class_rel_clauses thy subs supers'
-  in
-    (axiom_names |> map single |> Vector.fromList,
-     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
-  end
-
-fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-
-fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
-  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
-  | fo_term_for_combtyp (CombType (name, tys)) =
-    ATerm (name, map fo_term_for_combtyp tys)
-
-fun fo_literal_for_type_literal (TyLitVar (class, name)) =
-    (true, ATerm (class, [ATerm (name, [])]))
-  | fo_literal_for_type_literal (TyLitFree (class, name)) =
-    (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun fo_term_for_combterm full_types =
-  let
-    fun aux top_level u =
-      let
-        val (head, args) = strip_combterm_comb u
-        val (x, ty_args) =
-          case head of
-            CombConst (name as (s, s'), _, ty_args) =>
-            let val ty_args = if full_types then [] else ty_args in
-              if s = "equal" then
-                if top_level andalso length args = 2 then (name, [])
-                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
-              else if top_level then
-                case s of
-                  "c_False" => (("$false", s'), [])
-                | "c_True" => (("$true", s'), [])
-                | _ => (name, ty_args)
-              else
-                (name, ty_args)
-            end
-          | CombVar (name, _) => (name, [])
-          | CombApp _ => raise Fail "impossible \"CombApp\""
-        val t = ATerm (x, map fo_term_for_combtyp ty_args @
-                          map (aux false) args)
-    in
-      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
-    end
-  in aux true end
-
-fun formula_for_combformula full_types =
-  let
-    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
-      | aux (AConn (c, phis)) = AConn (c, map aux phis)
-      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
-  in aux end
-
-fun formula_for_axiom full_types
-                      ({combformula, ctypes_sorts, ...} : fol_formula) =
-  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
-                (type_literals_for_types ctypes_sorts))
-           (formula_for_combformula full_types combformula)
-
-fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
-  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
-
-fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
-                                                       superclass, ...}) =
-  let val ty_arg = ATerm (("T", "T"), []) in
-    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
-         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
-                           AAtom (ATerm (superclass, [ty_arg]))]))
-  end
-
-fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
-    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
-  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
-    (false, ATerm (c, [ATerm (sort, [])]))
-
-fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
-                                                ...}) =
-  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
-       mk_ahorn (map (formula_for_fo_literal o apfst not
-                      o fo_literal_for_arity_literal) premLits)
-                (formula_for_fo_literal
-                     (fo_literal_for_arity_literal conclLit)))
-
-fun problem_line_for_conjecture full_types
-                                ({name, kind, combformula, ...} : fol_formula) =
-  Fof (conjecture_prefix ^ name, kind,
-       formula_for_combformula full_types combformula)
-
-fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
-  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
-
-fun problem_line_for_free_type j lit =
-  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
-fun problem_lines_for_free_types conjectures =
-  let
-    val litss = map free_type_literals_for_conjecture conjectures
-    val lits = fold (union (op =)) litss []
-  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
-
-(** "hBOOL" and "hAPP" **)
-
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
-
-fun consider_term top_level (ATerm ((s, _), ts)) =
-  (if is_atp_variable s then
-     I
-   else
-     let val n = length ts in
-       Symtab.map_default
-           (s, {min_arity = n, max_arity = 0, sub_level = false})
-           (fn {min_arity, max_arity, sub_level} =>
-               {min_arity = Int.min (n, min_arity),
-                max_arity = Int.max (n, max_arity),
-                sub_level = sub_level orelse not top_level})
-     end)
-  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
-fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
-  | consider_formula (AConn (_, phis)) = fold consider_formula phis
-  | consider_formula (AAtom tm) = consider_term true tm
-
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
-fun consider_problem problem = fold (fold consider_problem_line o snd) problem
-
-fun const_table_for_problem explicit_apply problem =
-  if explicit_apply then NONE
-  else SOME (Symtab.empty |> consider_problem problem)
-
-fun min_arity_of thy full_types NONE s =
-    (if s = "equal" orelse s = type_wrapper_name orelse
-        String.isPrefix type_const_prefix s orelse
-        String.isPrefix class_prefix s then
-       16383 (* large number *)
-     else if full_types then
-       0
-     else case strip_prefix_and_unascii const_prefix s of
-       SOME s' => num_type_args thy (invert_const s')
-     | NONE => 0)
-  | min_arity_of _ _ (SOME the_const_tab) s =
-    case Symtab.lookup the_const_tab s of
-      SOME ({min_arity, ...} : const_info) => min_arity
-    | NONE => 0
-
-fun full_type_of (ATerm ((s, _), [ty, _])) =
-    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
-  | full_type_of _ = raise Fail "expected type wrapper"
-
-fun list_hAPP_rev _ t1 [] = t1
-  | list_hAPP_rev NONE t1 (t2 :: ts2) =
-    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
-  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
-    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
-                         [full_type_of t2, ty]) in
-      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
-    end
-
-fun repair_applications_in_term thy full_types const_tab =
-  let
-    fun aux opt_ty (ATerm (name as (s, _), ts)) =
-      if s = type_wrapper_name then
-        case ts of
-          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
-        | _ => raise Fail "malformed type wrapper"
-      else
-        let
-          val ts = map (aux NONE) ts
-          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
-        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
-  in aux NONE end
-
-fun boolify t = ATerm (`I "hBOOL", [t])
-
-(* True if the constant ever appears outside of the top-level position in
-   literals, or if it appears with different arities (e.g., because of different
-   type instantiations). If false, the constant always receives all of its
-   arguments and is used as a predicate. *)
-fun is_predicate NONE s =
-    s = "equal" orelse s = "$false" orelse s = "$true" orelse
-    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
-  | is_predicate (SOME the_const_tab) s =
-    case Symtab.lookup the_const_tab s of
-      SOME {min_arity, max_arity, sub_level} =>
-      not sub_level andalso min_arity = max_arity
-    | NONE => false
-
-fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
-  if s = type_wrapper_name then
-    case ts of
-      [_, t' as ATerm ((s', _), _)] =>
-      if is_predicate const_tab s' then t' else boolify t
-    | _ => raise Fail "malformed type wrapper"
-  else
-    t |> not (is_predicate const_tab s) ? boolify
-
-fun close_universally phi =
-  let
-    fun term_vars bounds (ATerm (name as (s, _), tms)) =
-        (is_atp_variable s andalso not (member (op =) bounds name))
-          ? insert (op =) name
-        #> fold (term_vars bounds) tms
-    fun formula_vars bounds (AQuant (_, xs, phi)) =
-        formula_vars (xs @ bounds) phi
-      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
-      | formula_vars bounds (AAtom tm) = term_vars bounds tm
-  in
-    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
-  end
-
-fun repair_formula thy explicit_forall full_types const_tab =
-  let
-    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
-      | aux (AConn (c, phis)) = AConn (c, map aux phis)
-      | aux (AAtom tm) =
-        AAtom (tm |> repair_applications_in_term thy full_types const_tab
-                  |> repair_predicates_in_term const_tab)
-  in aux #> explicit_forall ? close_universally end
-
-fun repair_problem_line thy explicit_forall full_types const_tab
-                        (Fof (ident, kind, phi)) =
-  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
-fun repair_problem_with_const_table thy =
-  map o apsnd o map ooo repair_problem_line thy
-
-fun repair_problem thy explicit_forall full_types explicit_apply problem =
-  repair_problem_with_const_table thy explicit_forall full_types
-      (const_table_for_problem explicit_apply problem) problem
-
-fun prepare_atp_problem ctxt readable_names explicit_forall full_types
-                        explicit_apply hyp_ts concl_t axioms =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
-                       arity_clauses)) =
-      prepare_formulas ctxt full_types hyp_ts concl_t axioms
-    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
-    val helper_lines =
-      map (problem_line_for_fact helper_prefix full_types) helper_facts
-    val conjecture_lines =
-      map (problem_line_for_conjecture full_types) conjectures
-    val tfree_lines = problem_lines_for_free_types conjectures
-    val class_rel_lines =
-      map problem_line_for_class_rel_clause class_rel_clauses
-    val arity_lines = map problem_line_for_arity_clause arity_clauses
-    (* Reordering these might or might not confuse the proof reconstruction
-       code or the SPASS Flotter hack. *)
-    val problem =
-      [("Relevant facts", axiom_lines),
-       ("Class relationships", class_rel_lines),
-       ("Arity declarations", arity_lines),
-       ("Helper facts", helper_lines),
-       ("Conjectures", conjecture_lines),
-       ("Type variables", tfree_lines)]
-      |> repair_problem thy explicit_forall full_types explicit_apply
-    val (problem, pool) = nice_atp_problem readable_names problem
-    val conjecture_offset =
-      length axiom_lines + length class_rel_lines + length arity_lines
-      + length helper_lines
-  in
-    (problem,
-     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
-     conjecture_offset, axiom_names)
-  end
-
-end;