renamed files
authorblanchet
Fri Oct 22 13:54:51 2010 +0200 (2010-10-22)
changeset 400670783415ed7f0
parent 40066 80d4ea0e536a
child 40068 ed2869dd9bfa
renamed files
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 22 13:49:44 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 22 13:54:51 2010 +0200
     1.3 @@ -327,8 +327,8 @@
     1.4    Tools/Sledgehammer/sledgehammer_filter.ML \
     1.5    Tools/Sledgehammer/sledgehammer_minimize.ML \
     1.6    Tools/Sledgehammer/sledgehammer_isar.ML \
     1.7 -  Tools/Sledgehammer/sledgehammer_reconstruct.ML \
     1.8 -  Tools/Sledgehammer/sledgehammer_translate.ML \
     1.9 +  Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
    1.10 +  Tools/Sledgehammer/sledgehammer_atp_translate.ML \
    1.11    Tools/Sledgehammer/sledgehammer_util.ML \
    1.12    Tools/SMT/cvc3_solver.ML \
    1.13    Tools/SMT/smtlib_interface.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Fri Oct 22 13:49:44 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Fri Oct 22 13:54:51 2010 +0200
     2.3 @@ -10,8 +10,8 @@
     2.4  imports ATP
     2.5  uses "Tools/Sledgehammer/sledgehammer_util.ML"
     2.6       "Tools/Sledgehammer/sledgehammer_filter.ML"
     2.7 -     "Tools/Sledgehammer/sledgehammer_translate.ML"
     2.8 -     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
     2.9 +     "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
    2.10 +     "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
    2.11       "Tools/Sledgehammer/sledgehammer.ML"
    2.12       "Tools/Sledgehammer/sledgehammer_minimize.ML"
    2.13       "Tools/Sledgehammer/sledgehammer_isar.ML"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:54:51 2010 +0200
     3.3 @@ -0,0 +1,946 @@
     3.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     3.5 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3.6 +    Author:     Claire Quigley, Cambridge University Computer Laboratory
     3.7 +    Author:     Jasmin Blanchette, TU Muenchen
     3.8 +
     3.9 +Proof reconstruction for Sledgehammer.
    3.10 +*)
    3.11 +
    3.12 +signature SLEDGEHAMMER_RECONSTRUCT =
    3.13 +sig
    3.14 +  type locality = Sledgehammer_Filter.locality
    3.15 +  type minimize_command = string list -> string
    3.16 +  type metis_params =
    3.17 +    string * bool * minimize_command * string * (string * locality) list vector
    3.18 +    * thm * int
    3.19 +  type isar_params =
    3.20 +    string Symtab.table * bool * int * Proof.context * int list list
    3.21 +  type text_result = string * (string * locality) list
    3.22 +
    3.23 +  val repair_conjecture_shape_and_axiom_names :
    3.24 +    string -> int list list -> (string * locality) list vector
    3.25 +    -> int list list * (string * locality) list vector
    3.26 +  val apply_on_subgoal : int -> int -> string
    3.27 +  val command_call : string -> string list -> string
    3.28 +  val try_command_line : string -> string -> string
    3.29 +  val minimize_line : ('a list -> string) -> 'a list -> string
    3.30 +  val metis_proof_text : metis_params -> text_result
    3.31 +  val isar_proof_text : isar_params -> metis_params -> text_result
    3.32 +  val proof_text : bool -> isar_params -> metis_params -> text_result
    3.33 +end;
    3.34 +
    3.35 +structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    3.36 +struct
    3.37 +
    3.38 +open ATP_Problem
    3.39 +open ATP_Proof
    3.40 +open Metis_Translate
    3.41 +open Sledgehammer_Util
    3.42 +open Sledgehammer_Filter
    3.43 +open Sledgehammer_Translate
    3.44 +
    3.45 +type minimize_command = string list -> string
    3.46 +type metis_params =
    3.47 +  string * bool * minimize_command * string * (string * locality) list vector
    3.48 +  * thm * int
    3.49 +type isar_params =
    3.50 +  string Symtab.table * bool * int * Proof.context * int list list
    3.51 +type text_result = string * (string * locality) list
    3.52 +
    3.53 +fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    3.54 +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    3.55 +
    3.56 +fun find_first_in_list_vector vec key =
    3.57 +  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    3.58 +                 | (_, value) => value) NONE vec
    3.59 +
    3.60 +
    3.61 +(** SPASS's Flotter hack **)
    3.62 +
    3.63 +(* This is a hack required for keeping track of axioms after they have been
    3.64 +   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    3.65 +   part of this hack. *)
    3.66 +
    3.67 +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    3.68 +
    3.69 +fun extract_clause_sequence output =
    3.70 +  let
    3.71 +    val tokens_of = String.tokens (not o Char.isAlphaNum)
    3.72 +    fun extract_num ("clause" :: (ss as _ :: _)) =
    3.73 +    Int.fromString (List.last ss)
    3.74 +      | extract_num _ = NONE
    3.75 +  in output |> split_lines |> map_filter (extract_num o tokens_of) end
    3.76 +
    3.77 +val parse_clause_formula_pair =
    3.78 +  $$ "(" |-- scan_integer --| $$ ","
    3.79 +  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
    3.80 +  --| Scan.option ($$ ",")
    3.81 +val parse_clause_formula_relation =
    3.82 +  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    3.83 +  |-- Scan.repeat parse_clause_formula_pair
    3.84 +val extract_clause_formula_relation =
    3.85 +  Substring.full #> Substring.position set_ClauseFormulaRelationN
    3.86 +  #> snd #> Substring.position "." #> fst #> Substring.string
    3.87 +  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    3.88 +  #> fst
    3.89 +
    3.90 +fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    3.91 +                                            axiom_names =
    3.92 +  if String.isSubstring set_ClauseFormulaRelationN output then
    3.93 +    let
    3.94 +      val j0 = hd (hd conjecture_shape)
    3.95 +      val seq = extract_clause_sequence output
    3.96 +      val name_map = extract_clause_formula_relation output
    3.97 +      fun renumber_conjecture j =
    3.98 +        conjecture_prefix ^ string_of_int (j - j0)
    3.99 +        |> AList.find (fn (s, ss) => member (op =) ss s) name_map
   3.100 +        |> map (fn s => find_index (curry (op =) s) seq + 1)
   3.101 +      fun names_for_number j =
   3.102 +        j |> AList.lookup (op =) name_map |> these
   3.103 +          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   3.104 +          |> map (fn name =>
   3.105 +                     (name, name |> find_first_in_list_vector axiom_names
   3.106 +                                 |> the)
   3.107 +                     handle Option.Option =>
   3.108 +                            error ("No such fact: " ^ quote name ^ "."))
   3.109 +    in
   3.110 +      (conjecture_shape |> map (maps renumber_conjecture),
   3.111 +       seq |> map names_for_number |> Vector.fromList)
   3.112 +    end
   3.113 +  else
   3.114 +    (conjecture_shape, axiom_names)
   3.115 +
   3.116 +
   3.117 +(** Soft-core proof reconstruction: Metis one-liner **)
   3.118 +
   3.119 +fun string_for_label (s, num) = s ^ string_of_int num
   3.120 +
   3.121 +fun apply_on_subgoal _ 1 = "by "
   3.122 +  | apply_on_subgoal 1 _ = "apply "
   3.123 +  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
   3.124 +fun command_call name [] = name
   3.125 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   3.126 +fun try_command_line banner command =
   3.127 +  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   3.128 +fun using_labels [] = ""
   3.129 +  | using_labels ls =
   3.130 +    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   3.131 +fun metis_name full_types = if full_types then "metisFT" else "metis"
   3.132 +fun metis_call full_types ss = command_call (metis_name full_types) ss
   3.133 +fun metis_command full_types i n (ls, ss) =
   3.134 +  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
   3.135 +fun metis_line banner full_types i n ss =
   3.136 +  try_command_line banner (metis_command full_types i n ([], ss))
   3.137 +fun minimize_line _ [] = ""
   3.138 +  | minimize_line minimize_command ss =
   3.139 +    case minimize_command ss of
   3.140 +      "" => ""
   3.141 +    | command =>
   3.142 +      "\nTo minimize the number of lemmas, try this: " ^
   3.143 +      Markup.markup Markup.sendback command ^ "."
   3.144 +
   3.145 +fun resolve_axiom axiom_names ((_, SOME s)) =
   3.146 +    (case strip_prefix_and_unascii axiom_prefix s of
   3.147 +       SOME s' => (case find_first_in_list_vector axiom_names s' of
   3.148 +                     SOME x => [(s', x)]
   3.149 +                   | NONE => [])
   3.150 +     | NONE => [])
   3.151 +  | resolve_axiom axiom_names (num, NONE) =
   3.152 +    case Int.fromString num of
   3.153 +      SOME j =>
   3.154 +      if j > 0 andalso j <= Vector.length axiom_names then
   3.155 +        Vector.sub (axiom_names, j - 1)
   3.156 +      else
   3.157 +        []
   3.158 +    | NONE => []
   3.159 +
   3.160 +fun add_fact axiom_names (Inference (name, _, [])) =
   3.161 +    append (resolve_axiom axiom_names name)
   3.162 +  | add_fact _ _ = I
   3.163 +
   3.164 +fun used_facts_in_tstplike_proof axiom_names =
   3.165 +  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
   3.166 +
   3.167 +fun used_facts axiom_names =
   3.168 +  used_facts_in_tstplike_proof axiom_names
   3.169 +  #> List.partition (curry (op =) Chained o snd)
   3.170 +  #> pairself (sort_distinct (string_ord o pairself fst))
   3.171 +
   3.172 +fun metis_proof_text (banner, full_types, minimize_command,
   3.173 +                      tstplike_proof, axiom_names, goal, i) =
   3.174 +  let
   3.175 +    val (chained_lemmas, other_lemmas) =
   3.176 +      used_facts axiom_names tstplike_proof
   3.177 +    val n = Logic.count_prems (prop_of goal)
   3.178 +  in
   3.179 +    (metis_line banner full_types i n (map fst other_lemmas) ^
   3.180 +     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   3.181 +     other_lemmas @ chained_lemmas)
   3.182 +  end
   3.183 +
   3.184 +
   3.185 +(** Hard-core proof reconstruction: structured Isar proofs **)
   3.186 +
   3.187 +(* Simple simplifications to ensure that sort annotations don't leave a trail of
   3.188 +   spurious "True"s. *)
   3.189 +fun s_not @{const False} = @{const True}
   3.190 +  | s_not @{const True} = @{const False}
   3.191 +  | s_not (@{const Not} $ t) = t
   3.192 +  | s_not t = @{const Not} $ t
   3.193 +fun s_conj (@{const True}, t2) = t2
   3.194 +  | s_conj (t1, @{const True}) = t1
   3.195 +  | s_conj p = HOLogic.mk_conj p
   3.196 +fun s_disj (@{const False}, t2) = t2
   3.197 +  | s_disj (t1, @{const False}) = t1
   3.198 +  | s_disj p = HOLogic.mk_disj p
   3.199 +fun s_imp (@{const True}, t2) = t2
   3.200 +  | s_imp (t1, @{const False}) = s_not t1
   3.201 +  | s_imp p = HOLogic.mk_imp p
   3.202 +fun s_iff (@{const True}, t2) = t2
   3.203 +  | s_iff (t1, @{const True}) = t1
   3.204 +  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   3.205 +
   3.206 +fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   3.207 +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   3.208 +
   3.209 +fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   3.210 +    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   3.211 +  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   3.212 +    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   3.213 +  | negate_term (@{const HOL.implies} $ t1 $ t2) =
   3.214 +    @{const HOL.conj} $ t1 $ negate_term t2
   3.215 +  | negate_term (@{const HOL.conj} $ t1 $ t2) =
   3.216 +    @{const HOL.disj} $ negate_term t1 $ negate_term t2
   3.217 +  | negate_term (@{const HOL.disj} $ t1 $ t2) =
   3.218 +    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   3.219 +  | negate_term (@{const Not} $ t) = t
   3.220 +  | negate_term t = @{const Not} $ t
   3.221 +
   3.222 +val indent_size = 2
   3.223 +val no_label = ("", ~1)
   3.224 +
   3.225 +val raw_prefix = "X"
   3.226 +val assum_prefix = "A"
   3.227 +val fact_prefix = "F"
   3.228 +
   3.229 +fun resolve_conjecture conjecture_shape (num, s_opt) =
   3.230 +  let
   3.231 +    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   3.232 +              SOME s => Int.fromString s |> the_default ~1
   3.233 +            | NONE => case Int.fromString num of
   3.234 +                        SOME j => find_index (exists (curry (op =) j))
   3.235 +                                             conjecture_shape
   3.236 +                      | NONE => ~1
   3.237 +  in if k >= 0 then [k] else [] end
   3.238 +
   3.239 +fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   3.240 +fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   3.241 +
   3.242 +fun raw_label_for_name conjecture_shape name =
   3.243 +  case resolve_conjecture conjecture_shape name of
   3.244 +    [j] => (conjecture_prefix, j)
   3.245 +  | _ => case Int.fromString (fst name) of
   3.246 +           SOME j => (raw_prefix, j)
   3.247 +         | NONE => (raw_prefix ^ fst name, 0)
   3.248 +
   3.249 +(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   3.250 +
   3.251 +exception FO_TERM of string fo_term list
   3.252 +exception FORMULA of (string, string fo_term) formula list
   3.253 +exception SAME of unit
   3.254 +
   3.255 +(* Type variables are given the basic sort "HOL.type". Some will later be
   3.256 +   constrained by information from type literals, or by type inference. *)
   3.257 +fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   3.258 +  let val Ts = map (type_from_fo_term tfrees) us in
   3.259 +    case strip_prefix_and_unascii type_const_prefix a of
   3.260 +      SOME b => Type (invert_const b, Ts)
   3.261 +    | NONE =>
   3.262 +      if not (null us) then
   3.263 +        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   3.264 +      else case strip_prefix_and_unascii tfree_prefix a of
   3.265 +        SOME b =>
   3.266 +        let val s = "'" ^ b in
   3.267 +          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   3.268 +        end
   3.269 +      | NONE =>
   3.270 +        case strip_prefix_and_unascii tvar_prefix a of
   3.271 +          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   3.272 +        | NONE =>
   3.273 +          (* Variable from the ATP, say "X1" *)
   3.274 +          Type_Infer.param 0 (a, HOLogic.typeS)
   3.275 +  end
   3.276 +
   3.277 +(* Type class literal applied to a type. Returns triple of polarity, class,
   3.278 +   type. *)
   3.279 +fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   3.280 +  case (strip_prefix_and_unascii class_prefix a,
   3.281 +        map (type_from_fo_term tfrees) us) of
   3.282 +    (SOME b, [T]) => (pos, b, T)
   3.283 +  | _ => raise FO_TERM [u]
   3.284 +
   3.285 +(** Accumulate type constraints in a formula: negative type literals **)
   3.286 +fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   3.287 +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   3.288 +  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   3.289 +  | add_type_constraint _ = I
   3.290 +
   3.291 +fun repair_atp_variable_name f s =
   3.292 +  let
   3.293 +    fun subscript_name s n = s ^ nat_subscript n
   3.294 +    val s = String.map f s
   3.295 +  in
   3.296 +    case space_explode "_" s of
   3.297 +      [_] => (case take_suffix Char.isDigit (String.explode s) of
   3.298 +                (cs1 as _ :: _, cs2 as _ :: _) =>
   3.299 +                subscript_name (String.implode cs1)
   3.300 +                               (the (Int.fromString (String.implode cs2)))
   3.301 +              | (_, _) => s)
   3.302 +    | [s1, s2] => (case Int.fromString s2 of
   3.303 +                     SOME n => subscript_name s1 n
   3.304 +                   | NONE => s)
   3.305 +    | _ => s
   3.306 +  end
   3.307 +
   3.308 +(* First-order translation. No types are known for variables. "HOLogic.typeT"
   3.309 +   should allow them to be inferred. *)
   3.310 +fun raw_term_from_pred thy full_types tfrees =
   3.311 +  let
   3.312 +    fun aux opt_T extra_us u =
   3.313 +      case u of
   3.314 +        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   3.315 +      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   3.316 +      | ATerm (a, us) =>
   3.317 +        if a = type_wrapper_name then
   3.318 +          case us of
   3.319 +            [typ_u, term_u] =>
   3.320 +            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   3.321 +          | _ => raise FO_TERM us
   3.322 +        else case strip_prefix_and_unascii const_prefix a of
   3.323 +          SOME "equal" =>
   3.324 +          let val ts = map (aux NONE []) us in
   3.325 +            if length ts = 2 andalso hd ts aconv List.last ts then
   3.326 +              (* Vampire is keen on producing these. *)
   3.327 +              @{const True}
   3.328 +            else
   3.329 +              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   3.330 +          end
   3.331 +        | SOME b =>
   3.332 +          let
   3.333 +            val c = invert_const b
   3.334 +            val num_type_args = num_type_args thy c
   3.335 +            val (type_us, term_us) =
   3.336 +              chop (if full_types then 0 else num_type_args) us
   3.337 +            (* Extra args from "hAPP" come after any arguments given directly to
   3.338 +               the constant. *)
   3.339 +            val term_ts = map (aux NONE []) term_us
   3.340 +            val extra_ts = map (aux NONE []) extra_us
   3.341 +            val t =
   3.342 +              Const (c, if full_types then
   3.343 +                          case opt_T of
   3.344 +                            SOME T => map fastype_of term_ts ---> T
   3.345 +                          | NONE =>
   3.346 +                            if num_type_args = 0 then
   3.347 +                              Sign.const_instance thy (c, [])
   3.348 +                            else
   3.349 +                              raise Fail ("no type information for " ^ quote c)
   3.350 +                        else
   3.351 +                          Sign.const_instance thy (c,
   3.352 +                              map (type_from_fo_term tfrees) type_us))
   3.353 +          in list_comb (t, term_ts @ extra_ts) end
   3.354 +        | NONE => (* a free or schematic variable *)
   3.355 +          let
   3.356 +            val ts = map (aux NONE []) (us @ extra_us)
   3.357 +            val T = map fastype_of ts ---> HOLogic.typeT
   3.358 +            val t =
   3.359 +              case strip_prefix_and_unascii fixed_var_prefix a of
   3.360 +                SOME b => Free (b, T)
   3.361 +              | NONE =>
   3.362 +                case strip_prefix_and_unascii schematic_var_prefix a of
   3.363 +                  SOME b => Var ((b, 0), T)
   3.364 +                | NONE =>
   3.365 +                  if is_atp_variable a then
   3.366 +                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
   3.367 +                  else
   3.368 +                    (* Skolem constants? *)
   3.369 +                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   3.370 +          in list_comb (t, ts) end
   3.371 +  in aux (SOME HOLogic.boolT) [] end
   3.372 +
   3.373 +fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   3.374 +  if String.isPrefix class_prefix s then
   3.375 +    add_type_constraint (type_constraint_from_term pos tfrees u)
   3.376 +    #> pair @{const True}
   3.377 +  else
   3.378 +    pair (raw_term_from_pred thy full_types tfrees u)
   3.379 +
   3.380 +val combinator_table =
   3.381 +  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   3.382 +   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   3.383 +   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   3.384 +   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   3.385 +   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   3.386 +
   3.387 +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   3.388 +  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   3.389 +  | uncombine_term (t as Const (x as (s, _))) =
   3.390 +    (case AList.lookup (op =) combinator_table s of
   3.391 +       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   3.392 +     | NONE => t)
   3.393 +  | uncombine_term t = t
   3.394 +
   3.395 +(* Update schematic type variables with detected sort constraints. It's not
   3.396 +   totally clear when this code is necessary. *)
   3.397 +fun repair_tvar_sorts (t, tvar_tab) =
   3.398 +  let
   3.399 +    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   3.400 +      | do_type (TVar (xi, s)) =
   3.401 +        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   3.402 +      | do_type (TFree z) = TFree z
   3.403 +    fun do_term (Const (a, T)) = Const (a, do_type T)
   3.404 +      | do_term (Free (a, T)) = Free (a, do_type T)
   3.405 +      | do_term (Var (xi, T)) = Var (xi, do_type T)
   3.406 +      | do_term (t as Bound _) = t
   3.407 +      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   3.408 +      | do_term (t1 $ t2) = do_term t1 $ do_term t2
   3.409 +  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   3.410 +
   3.411 +fun quantify_over_var quant_of var_s t =
   3.412 +  let
   3.413 +    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   3.414 +                  |> map Var
   3.415 +  in fold_rev quant_of vars t end
   3.416 +
   3.417 +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   3.418 +   appear in the formula. *)
   3.419 +fun prop_from_formula thy full_types tfrees phi =
   3.420 +  let
   3.421 +    fun do_formula pos phi =
   3.422 +      case phi of
   3.423 +        AQuant (_, [], phi) => do_formula pos phi
   3.424 +      | AQuant (q, x :: xs, phi') =>
   3.425 +        do_formula pos (AQuant (q, xs, phi'))
   3.426 +        #>> quantify_over_var (case q of
   3.427 +                                 AForall => forall_of
   3.428 +                               | AExists => exists_of)
   3.429 +                              (repair_atp_variable_name Char.toLower x)
   3.430 +      | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   3.431 +      | AConn (c, [phi1, phi2]) =>
   3.432 +        do_formula (pos |> c = AImplies ? not) phi1
   3.433 +        ##>> do_formula pos phi2
   3.434 +        #>> (case c of
   3.435 +               AAnd => s_conj
   3.436 +             | AOr => s_disj
   3.437 +             | AImplies => s_imp
   3.438 +             | AIf => s_imp o swap
   3.439 +             | AIff => s_iff
   3.440 +             | ANotIff => s_not o s_iff)
   3.441 +      | AAtom tm => term_from_pred thy full_types tfrees pos tm
   3.442 +      | _ => raise FORMULA [phi]
   3.443 +  in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   3.444 +
   3.445 +fun check_formula ctxt =
   3.446 +  Type.constraint HOLogic.boolT
   3.447 +  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   3.448 +
   3.449 +
   3.450 +(**** Translation of TSTP files to Isar Proofs ****)
   3.451 +
   3.452 +fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   3.453 +  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   3.454 +
   3.455 +fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   3.456 +    let
   3.457 +      val thy = ProofContext.theory_of ctxt
   3.458 +      val t1 = prop_from_formula thy full_types tfrees phi1
   3.459 +      val vars = snd (strip_comb t1)
   3.460 +      val frees = map unvarify_term vars
   3.461 +      val unvarify_args = subst_atomic (vars ~~ frees)
   3.462 +      val t2 = prop_from_formula thy full_types tfrees phi2
   3.463 +      val (t1, t2) =
   3.464 +        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   3.465 +        |> unvarify_args |> uncombine_term |> check_formula ctxt
   3.466 +        |> HOLogic.dest_eq
   3.467 +    in
   3.468 +      (Definition (name, t1, t2),
   3.469 +       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   3.470 +    end
   3.471 +  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   3.472 +    let
   3.473 +      val thy = ProofContext.theory_of ctxt
   3.474 +      val t = u |> prop_from_formula thy full_types tfrees
   3.475 +                |> uncombine_term |> check_formula ctxt
   3.476 +    in
   3.477 +      (Inference (name, t, deps),
   3.478 +       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   3.479 +    end
   3.480 +fun decode_lines ctxt full_types tfrees lines =
   3.481 +  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   3.482 +
   3.483 +fun is_same_inference _ (Definition _) = false
   3.484 +  | is_same_inference t (Inference (_, t', _)) = t aconv t'
   3.485 +
   3.486 +(* No "real" literals means only type information (tfree_tcs, clsrel, or
   3.487 +   clsarity). *)
   3.488 +val is_only_type_information = curry (op aconv) HOLogic.true_const
   3.489 +
   3.490 +fun replace_one_dependency (old, new) dep =
   3.491 +  if is_same_step (dep, old) then new else [dep]
   3.492 +fun replace_dependencies_in_line _ (line as Definition _) = line
   3.493 +  | replace_dependencies_in_line p (Inference (name, t, deps)) =
   3.494 +    Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   3.495 +
   3.496 +(* Discard axioms; consolidate adjacent lines that prove the same formula, since
   3.497 +   they differ only in type information.*)
   3.498 +fun add_line _ _ (line as Definition _) lines = line :: lines
   3.499 +  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   3.500 +    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   3.501 +       definitions. *)
   3.502 +    if is_axiom axiom_names name then
   3.503 +      (* Axioms are not proof lines. *)
   3.504 +      if is_only_type_information t then
   3.505 +        map (replace_dependencies_in_line (name, [])) lines
   3.506 +      (* Is there a repetition? If so, replace later line by earlier one. *)
   3.507 +      else case take_prefix (not o is_same_inference t) lines of
   3.508 +        (_, []) => lines (* no repetition of proof line *)
   3.509 +      | (pre, Inference (name', _, _) :: post) =>
   3.510 +        pre @ map (replace_dependencies_in_line (name', [name])) post
   3.511 +    else if is_conjecture conjecture_shape name then
   3.512 +      Inference (name, negate_term t, []) :: lines
   3.513 +    else
   3.514 +      map (replace_dependencies_in_line (name, [])) lines
   3.515 +  | add_line _ _ (Inference (name, t, deps)) lines =
   3.516 +    (* Type information will be deleted later; skip repetition test. *)
   3.517 +    if is_only_type_information t then
   3.518 +      Inference (name, t, deps) :: lines
   3.519 +    (* Is there a repetition? If so, replace later line by earlier one. *)
   3.520 +    else case take_prefix (not o is_same_inference t) lines of
   3.521 +      (* FIXME: Doesn't this code risk conflating proofs involving different
   3.522 +         types? *)
   3.523 +       (_, []) => Inference (name, t, deps) :: lines
   3.524 +     | (pre, Inference (name', t', _) :: post) =>
   3.525 +       Inference (name, t', deps) ::
   3.526 +       pre @ map (replace_dependencies_in_line (name', [name])) post
   3.527 +
   3.528 +(* Recursively delete empty lines (type information) from the proof. *)
   3.529 +fun add_nontrivial_line (Inference (name, t, [])) lines =
   3.530 +    if is_only_type_information t then delete_dependency name lines
   3.531 +    else Inference (name, t, []) :: lines
   3.532 +  | add_nontrivial_line line lines = line :: lines
   3.533 +and delete_dependency name lines =
   3.534 +  fold_rev add_nontrivial_line
   3.535 +           (map (replace_dependencies_in_line (name, [])) lines) []
   3.536 +
   3.537 +(* ATPs sometimes reuse free variable names in the strangest ways. Removing
   3.538 +   offending lines often does the trick. *)
   3.539 +fun is_bad_free frees (Free x) = not (member (op =) frees x)
   3.540 +  | is_bad_free _ _ = false
   3.541 +
   3.542 +fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   3.543 +    (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   3.544 +  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   3.545 +                     (Inference (name, t, deps)) (j, lines) =
   3.546 +    (j + 1,
   3.547 +     if is_axiom axiom_names name orelse
   3.548 +        is_conjecture conjecture_shape name orelse
   3.549 +        (* the last line must be kept *)
   3.550 +        j = 0 orelse
   3.551 +        (not (is_only_type_information t) andalso
   3.552 +         null (Term.add_tvars t []) andalso
   3.553 +         not (exists_subterm (is_bad_free frees) t) andalso
   3.554 +         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   3.555 +         (* kill next to last line, which usually results in a trivial step *)
   3.556 +         j <> 1) then
   3.557 +       Inference (name, t, deps) :: lines  (* keep line *)
   3.558 +     else
   3.559 +       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   3.560 +
   3.561 +(** Isar proof construction and manipulation **)
   3.562 +
   3.563 +fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   3.564 +  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   3.565 +
   3.566 +type label = string * int
   3.567 +type facts = label list * string list
   3.568 +
   3.569 +datatype isar_qualifier = Show | Then | Moreover | Ultimately
   3.570 +
   3.571 +datatype isar_step =
   3.572 +  Fix of (string * typ) list |
   3.573 +  Let of term * term |
   3.574 +  Assume of label * term |
   3.575 +  Have of isar_qualifier list * label * term * byline
   3.576 +and byline =
   3.577 +  ByMetis of facts |
   3.578 +  CaseSplit of isar_step list list * facts
   3.579 +
   3.580 +fun smart_case_split [] facts = ByMetis facts
   3.581 +  | smart_case_split proofs facts = CaseSplit (proofs, facts)
   3.582 +
   3.583 +fun add_fact_from_dependency conjecture_shape axiom_names name =
   3.584 +  if is_axiom axiom_names name then
   3.585 +    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   3.586 +  else
   3.587 +    apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   3.588 +
   3.589 +fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   3.590 +  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   3.591 +    Assume (raw_label_for_name conjecture_shape name, t)
   3.592 +  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   3.593 +    Have (if j = 1 then [Show] else [],
   3.594 +          raw_label_for_name conjecture_shape name,
   3.595 +          fold_rev forall_of (map Var (Term.add_vars t [])) t,
   3.596 +          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   3.597 +                        deps ([], [])))
   3.598 +
   3.599 +fun repair_name "$true" = "c_True"
   3.600 +  | repair_name "$false" = "c_False"
   3.601 +  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   3.602 +  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   3.603 +  | repair_name s =
   3.604 +    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   3.605 +      "c_equal" (* seen in Vampire proofs *)
   3.606 +    else
   3.607 +      s
   3.608 +
   3.609 +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   3.610 +        tstplike_proof conjecture_shape axiom_names params frees =
   3.611 +  let
   3.612 +    val lines =
   3.613 +      tstplike_proof
   3.614 +      |> atp_proof_from_tstplike_string
   3.615 +      |> nasty_atp_proof pool
   3.616 +      |> map_term_names_in_atp_proof repair_name
   3.617 +      |> decode_lines ctxt full_types tfrees
   3.618 +      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   3.619 +      |> rpair [] |-> fold_rev add_nontrivial_line
   3.620 +      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   3.621 +                                             conjecture_shape axiom_names frees)
   3.622 +      |> snd
   3.623 +  in
   3.624 +    (if null params then [] else [Fix params]) @
   3.625 +    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   3.626 +         lines
   3.627 +  end
   3.628 +
   3.629 +(* When redirecting proofs, we keep information about the labels seen so far in
   3.630 +   the "backpatches" data structure. The first component indicates which facts
   3.631 +   should be associated with forthcoming proof steps. The second component is a
   3.632 +   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   3.633 +   become assumptions and "drop_ls" are the labels that should be dropped in a
   3.634 +   case split. *)
   3.635 +type backpatches = (label * facts) list * (label list * label list)
   3.636 +
   3.637 +fun used_labels_of_step (Have (_, _, _, by)) =
   3.638 +    (case by of
   3.639 +       ByMetis (ls, _) => ls
   3.640 +     | CaseSplit (proofs, (ls, _)) =>
   3.641 +       fold (union (op =) o used_labels_of) proofs ls)
   3.642 +  | used_labels_of_step _ = []
   3.643 +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   3.644 +
   3.645 +fun new_labels_of_step (Fix _) = []
   3.646 +  | new_labels_of_step (Let _) = []
   3.647 +  | new_labels_of_step (Assume (l, _)) = [l]
   3.648 +  | new_labels_of_step (Have (_, l, _, _)) = [l]
   3.649 +val new_labels_of = maps new_labels_of_step
   3.650 +
   3.651 +val join_proofs =
   3.652 +  let
   3.653 +    fun aux _ [] = NONE
   3.654 +      | aux proof_tail (proofs as (proof1 :: _)) =
   3.655 +        if exists null proofs then
   3.656 +          NONE
   3.657 +        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   3.658 +          aux (hd proof1 :: proof_tail) (map tl proofs)
   3.659 +        else case hd proof1 of
   3.660 +          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   3.661 +          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   3.662 +                      | _ => false) (tl proofs) andalso
   3.663 +             not (exists (member (op =) (maps new_labels_of proofs))
   3.664 +                         (used_labels_of proof_tail)) then
   3.665 +            SOME (l, t, map rev proofs, proof_tail)
   3.666 +          else
   3.667 +            NONE
   3.668 +        | _ => NONE
   3.669 +  in aux [] o map rev end
   3.670 +
   3.671 +fun case_split_qualifiers proofs =
   3.672 +  case length proofs of
   3.673 +    0 => []
   3.674 +  | 1 => [Then]
   3.675 +  | _ => [Ultimately]
   3.676 +
   3.677 +fun redirect_proof hyp_ts concl_t proof =
   3.678 +  let
   3.679 +    (* The first pass outputs those steps that are independent of the negated
   3.680 +       conjecture. The second pass flips the proof by contradiction to obtain a
   3.681 +       direct proof, introducing case splits when an inference depends on
   3.682 +       several facts that depend on the negated conjecture. *)
   3.683 +     val concl_l = (conjecture_prefix, length hyp_ts)
   3.684 +     fun first_pass ([], contra) = ([], contra)
   3.685 +       | first_pass ((step as Fix _) :: proof, contra) =
   3.686 +         first_pass (proof, contra) |>> cons step
   3.687 +       | first_pass ((step as Let _) :: proof, contra) =
   3.688 +         first_pass (proof, contra) |>> cons step
   3.689 +       | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   3.690 +         if l = concl_l then first_pass (proof, contra ||> cons step)
   3.691 +         else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   3.692 +       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   3.693 +         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   3.694 +           if exists (member (op =) (fst contra)) ls then
   3.695 +             first_pass (proof, contra |>> cons l ||> cons step)
   3.696 +           else
   3.697 +             first_pass (proof, contra) |>> cons step
   3.698 +         end
   3.699 +       | first_pass _ = raise Fail "malformed proof"
   3.700 +    val (proof_top, (contra_ls, contra_proof)) =
   3.701 +      first_pass (proof, ([concl_l], []))
   3.702 +    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   3.703 +    fun backpatch_labels patches ls =
   3.704 +      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   3.705 +    fun second_pass end_qs ([], assums, patches) =
   3.706 +        ([Have (end_qs, no_label, concl_t,
   3.707 +                ByMetis (backpatch_labels patches (map snd assums)))], patches)
   3.708 +      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   3.709 +        second_pass end_qs (proof, (t, l) :: assums, patches)
   3.710 +      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   3.711 +                            patches) =
   3.712 +        (if member (op =) (snd (snd patches)) l andalso
   3.713 +            not (member (op =) (fst (snd patches)) l) andalso
   3.714 +            not (AList.defined (op =) (fst patches) l) then
   3.715 +           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   3.716 +         else case List.partition (member (op =) contra_ls) ls of
   3.717 +           ([contra_l], co_ls) =>
   3.718 +           if member (op =) qs Show then
   3.719 +             second_pass end_qs (proof, assums,
   3.720 +                                 patches |>> cons (contra_l, (co_ls, ss)))
   3.721 +           else
   3.722 +             second_pass end_qs
   3.723 +                         (proof, assums,
   3.724 +                          patches |>> cons (contra_l, (l :: co_ls, ss)))
   3.725 +             |>> cons (if member (op =) (fst (snd patches)) l then
   3.726 +                         Assume (l, negate_term t)
   3.727 +                       else
   3.728 +                         Have (qs, l, negate_term t,
   3.729 +                               ByMetis (backpatch_label patches l)))
   3.730 +         | (contra_ls as _ :: _, co_ls) =>
   3.731 +           let
   3.732 +             val proofs =
   3.733 +               map_filter
   3.734 +                   (fn l =>
   3.735 +                       if l = concl_l then
   3.736 +                         NONE
   3.737 +                       else
   3.738 +                         let
   3.739 +                           val drop_ls = filter (curry (op <>) l) contra_ls
   3.740 +                         in
   3.741 +                           second_pass []
   3.742 +                               (proof, assums,
   3.743 +                                patches ||> apfst (insert (op =) l)
   3.744 +                                        ||> apsnd (union (op =) drop_ls))
   3.745 +                           |> fst |> SOME
   3.746 +                         end) contra_ls
   3.747 +             val (assumes, facts) =
   3.748 +               if member (op =) (fst (snd patches)) l then
   3.749 +                 ([Assume (l, negate_term t)], (l :: co_ls, ss))
   3.750 +               else
   3.751 +                 ([], (co_ls, ss))
   3.752 +           in
   3.753 +             (case join_proofs proofs of
   3.754 +                SOME (l, t, proofs, proof_tail) =>
   3.755 +                Have (case_split_qualifiers proofs @
   3.756 +                      (if null proof_tail then end_qs else []), l, t,
   3.757 +                      smart_case_split proofs facts) :: proof_tail
   3.758 +              | NONE =>
   3.759 +                [Have (case_split_qualifiers proofs @ end_qs, no_label,
   3.760 +                       concl_t, smart_case_split proofs facts)],
   3.761 +              patches)
   3.762 +             |>> append assumes
   3.763 +           end
   3.764 +         | _ => raise Fail "malformed proof")
   3.765 +       | second_pass _ _ = raise Fail "malformed proof"
   3.766 +    val proof_bottom =
   3.767 +      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   3.768 +  in proof_top @ proof_bottom end
   3.769 +
   3.770 +(* FIXME: Still needed? Probably not. *)
   3.771 +val kill_duplicate_assumptions_in_proof =
   3.772 +  let
   3.773 +    fun relabel_facts subst =
   3.774 +      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   3.775 +    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   3.776 +        (case AList.lookup (op aconv) assums t of
   3.777 +           SOME l' => (proof, (l, l') :: subst, assums)
   3.778 +         | NONE => (step :: proof, subst, (t, l) :: assums))
   3.779 +      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   3.780 +        (Have (qs, l, t,
   3.781 +               case by of
   3.782 +                 ByMetis facts => ByMetis (relabel_facts subst facts)
   3.783 +               | CaseSplit (proofs, facts) =>
   3.784 +                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   3.785 +         proof, subst, assums)
   3.786 +      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   3.787 +    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   3.788 +  in do_proof end
   3.789 +
   3.790 +val then_chain_proof =
   3.791 +  let
   3.792 +    fun aux _ [] = []
   3.793 +      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   3.794 +      | aux l' (Have (qs, l, t, by) :: proof) =
   3.795 +        (case by of
   3.796 +           ByMetis (ls, ss) =>
   3.797 +           Have (if member (op =) ls l' then
   3.798 +                   (Then :: qs, l, t,
   3.799 +                    ByMetis (filter_out (curry (op =) l') ls, ss))
   3.800 +                 else
   3.801 +                   (qs, l, t, ByMetis (ls, ss)))
   3.802 +         | CaseSplit (proofs, facts) =>
   3.803 +           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   3.804 +        aux l proof
   3.805 +      | aux _ (step :: proof) = step :: aux no_label proof
   3.806 +  in aux no_label end
   3.807 +
   3.808 +fun kill_useless_labels_in_proof proof =
   3.809 +  let
   3.810 +    val used_ls = used_labels_of proof
   3.811 +    fun do_label l = if member (op =) used_ls l then l else no_label
   3.812 +    fun do_step (Assume (l, t)) = Assume (do_label l, t)
   3.813 +      | do_step (Have (qs, l, t, by)) =
   3.814 +        Have (qs, do_label l, t,
   3.815 +              case by of
   3.816 +                CaseSplit (proofs, facts) =>
   3.817 +                CaseSplit (map (map do_step) proofs, facts)
   3.818 +              | _ => by)
   3.819 +      | do_step step = step
   3.820 +  in map do_step proof end
   3.821 +
   3.822 +fun prefix_for_depth n = replicate_string (n + 1)
   3.823 +
   3.824 +val relabel_proof =
   3.825 +  let
   3.826 +    fun aux _ _ _ [] = []
   3.827 +      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   3.828 +        if l = no_label then
   3.829 +          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   3.830 +        else
   3.831 +          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   3.832 +            Assume (l', t) ::
   3.833 +            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   3.834 +          end
   3.835 +      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   3.836 +        let
   3.837 +          val (l', subst, next_fact) =
   3.838 +            if l = no_label then
   3.839 +              (l, subst, next_fact)
   3.840 +            else
   3.841 +              let
   3.842 +                val l' = (prefix_for_depth depth fact_prefix, next_fact)
   3.843 +              in (l', (l, l') :: subst, next_fact + 1) end
   3.844 +          val relabel_facts =
   3.845 +            apfst (maps (the_list o AList.lookup (op =) subst))
   3.846 +          val by =
   3.847 +            case by of
   3.848 +              ByMetis facts => ByMetis (relabel_facts facts)
   3.849 +            | CaseSplit (proofs, facts) =>
   3.850 +              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   3.851 +                         relabel_facts facts)
   3.852 +        in
   3.853 +          Have (qs, l', t, by) ::
   3.854 +          aux subst depth (next_assum, next_fact) proof
   3.855 +        end
   3.856 +      | aux subst depth nextp (step :: proof) =
   3.857 +        step :: aux subst depth nextp proof
   3.858 +  in aux [] 0 (1, 1) end
   3.859 +
   3.860 +fun string_for_proof ctxt0 full_types i n =
   3.861 +  let
   3.862 +    val ctxt = ctxt0
   3.863 +      |> Config.put show_free_types false
   3.864 +      |> Config.put show_types true
   3.865 +    fun fix_print_mode f x =
   3.866 +      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   3.867 +                               (print_mode_value ())) f x
   3.868 +    fun do_indent ind = replicate_string (ind * indent_size) " "
   3.869 +    fun do_free (s, T) =
   3.870 +      maybe_quote s ^ " :: " ^
   3.871 +      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   3.872 +    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   3.873 +    fun do_have qs =
   3.874 +      (if member (op =) qs Moreover then "moreover " else "") ^
   3.875 +      (if member (op =) qs Ultimately then "ultimately " else "") ^
   3.876 +      (if member (op =) qs Then then
   3.877 +         if member (op =) qs Show then "thus" else "hence"
   3.878 +       else
   3.879 +         if member (op =) qs Show then "show" else "have")
   3.880 +    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   3.881 +    fun do_facts (ls, ss) =
   3.882 +      metis_command full_types 1 1
   3.883 +                    (ls |> sort_distinct (prod_ord string_ord int_ord),
   3.884 +                     ss |> sort_distinct string_ord)
   3.885 +    and do_step ind (Fix xs) =
   3.886 +        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   3.887 +      | do_step ind (Let (t1, t2)) =
   3.888 +        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   3.889 +      | do_step ind (Assume (l, t)) =
   3.890 +        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   3.891 +      | do_step ind (Have (qs, l, t, ByMetis facts)) =
   3.892 +        do_indent ind ^ do_have qs ^ " " ^
   3.893 +        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   3.894 +      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   3.895 +        space_implode (do_indent ind ^ "moreover\n")
   3.896 +                      (map (do_block ind) proofs) ^
   3.897 +        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   3.898 +        do_facts facts ^ "\n"
   3.899 +    and do_steps prefix suffix ind steps =
   3.900 +      let val s = implode (map (do_step ind) steps) in
   3.901 +        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   3.902 +        String.extract (s, ind * indent_size,
   3.903 +                        SOME (size s - ind * indent_size - 1)) ^
   3.904 +        suffix ^ "\n"
   3.905 +      end
   3.906 +    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   3.907 +    (* One-step proofs are pointless; better use the Metis one-liner
   3.908 +       directly. *)
   3.909 +    and do_proof [Have (_, _, _, ByMetis _)] = ""
   3.910 +      | do_proof proof =
   3.911 +        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   3.912 +        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   3.913 +        (if n <> 1 then "next" else "qed")
   3.914 +  in do_proof end
   3.915 +
   3.916 +fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   3.917 +                    (other_params as (_, full_types, _, tstplike_proof,
   3.918 +                                      axiom_names, goal, i)) =
   3.919 +  let
   3.920 +    val (params, hyp_ts, concl_t) = strip_subgoal goal i
   3.921 +    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   3.922 +    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   3.923 +    val n = Logic.count_prems (prop_of goal)
   3.924 +    val (one_line_proof, lemma_names) = metis_proof_text other_params
   3.925 +    fun isar_proof_for () =
   3.926 +      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   3.927 +               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   3.928 +               params frees
   3.929 +           |> redirect_proof hyp_ts concl_t
   3.930 +           |> kill_duplicate_assumptions_in_proof
   3.931 +           |> then_chain_proof
   3.932 +           |> kill_useless_labels_in_proof
   3.933 +           |> relabel_proof
   3.934 +           |> string_for_proof ctxt full_types i n of
   3.935 +        "" => "\nNo structured proof available."
   3.936 +      | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   3.937 +    val isar_proof =
   3.938 +      if debug then
   3.939 +        isar_proof_for ()
   3.940 +      else
   3.941 +        try isar_proof_for ()
   3.942 +        |> the_default "\nWarning: The Isar proof construction failed."
   3.943 +  in (one_line_proof ^ isar_proof, lemma_names) end
   3.944 +
   3.945 +fun proof_text isar_proof isar_params other_params =
   3.946 +  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   3.947 +      other_params
   3.948 +
   3.949 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:54:51 2010 +0200
     4.3 @@ -0,0 +1,533 @@
     4.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     4.5 +    Author:     Fabian Immler, TU Muenchen
     4.6 +    Author:     Makarius
     4.7 +    Author:     Jasmin Blanchette, TU Muenchen
     4.8 +
     4.9 +Translation of HOL to FOL for Sledgehammer.
    4.10 +*)
    4.11 +
    4.12 +signature SLEDGEHAMMER_TRANSLATE =
    4.13 +sig
    4.14 +  type 'a problem = 'a ATP_Problem.problem
    4.15 +  type fol_formula
    4.16 +
    4.17 +  val axiom_prefix : string
    4.18 +  val conjecture_prefix : string
    4.19 +  val prepare_axiom :
    4.20 +    Proof.context -> (string * 'a) * thm
    4.21 +    -> term * ((string * 'a) * fol_formula) option
    4.22 +  val prepare_atp_problem :
    4.23 +    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    4.24 +    -> (term * ((string * 'a) * fol_formula) option) list
    4.25 +    -> string problem * string Symtab.table * int * (string * 'a) list vector
    4.26 +end;
    4.27 +
    4.28 +structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    4.29 +struct
    4.30 +
    4.31 +open ATP_Problem
    4.32 +open Metis_Translate
    4.33 +open Sledgehammer_Util
    4.34 +
    4.35 +val axiom_prefix = "ax_"
    4.36 +val conjecture_prefix = "conj_"
    4.37 +val helper_prefix = "help_"
    4.38 +val class_rel_clause_prefix = "clrel_";
    4.39 +val arity_clause_prefix = "arity_"
    4.40 +val tfree_prefix = "tfree_"
    4.41 +
    4.42 +(* Freshness almost guaranteed! *)
    4.43 +val sledgehammer_weak_prefix = "Sledgehammer:"
    4.44 +
    4.45 +type fol_formula =
    4.46 +  {name: string,
    4.47 +   kind: kind,
    4.48 +   combformula: (name, combterm) formula,
    4.49 +   ctypes_sorts: typ list}
    4.50 +
    4.51 +fun mk_anot phi = AConn (ANot, [phi])
    4.52 +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    4.53 +fun mk_ahorn [] phi = phi
    4.54 +  | mk_ahorn (phi :: phis) psi =
    4.55 +    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    4.56 +
    4.57 +fun combformula_for_prop thy =
    4.58 +  let
    4.59 +    val do_term = combterm_from_term thy ~1
    4.60 +    fun do_quant bs q s T t' =
    4.61 +      let val s = Name.variant (map fst bs) s in
    4.62 +        do_formula ((s, T) :: bs) t'
    4.63 +        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    4.64 +      end
    4.65 +    and do_conn bs c t1 t2 =
    4.66 +      do_formula bs t1 ##>> do_formula bs t2
    4.67 +      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    4.68 +    and do_formula bs t =
    4.69 +      case t of
    4.70 +        @{const Not} $ t1 =>
    4.71 +        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    4.72 +      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    4.73 +        do_quant bs AForall s T t'
    4.74 +      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    4.75 +        do_quant bs AExists s T t'
    4.76 +      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
    4.77 +      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
    4.78 +      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
    4.79 +      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    4.80 +        do_conn bs AIff t1 t2
    4.81 +      | _ => (fn ts => do_term bs (Envir.eta_contract t)
    4.82 +                       |>> AAtom ||> union (op =) ts)
    4.83 +  in do_formula [] end
    4.84 +
    4.85 +val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
    4.86 +
    4.87 +fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    4.88 +fun conceal_bounds Ts t =
    4.89 +  subst_bounds (map (Free o apfst concealed_bound_name)
    4.90 +                    (0 upto length Ts - 1 ~~ Ts), t)
    4.91 +fun reveal_bounds Ts =
    4.92 +  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
    4.93 +                    (0 upto length Ts - 1 ~~ Ts))
    4.94 +
    4.95 +(* Removes the lambdas from an equation of the form "t = (%x. u)".
    4.96 +   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
    4.97 +fun extensionalize_term t =
    4.98 +  let
    4.99 +    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   4.100 +      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   4.101 +                                        Type (_, [_, res_T])]))
   4.102 +                    $ t2 $ Abs (var_s, var_T, t')) =
   4.103 +        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   4.104 +          let val var_t = Var ((var_s, j), var_T) in
   4.105 +            Const (s, T' --> T' --> res_T)
   4.106 +              $ betapply (t2, var_t) $ subst_bound (var_t, t')
   4.107 +            |> aux (j + 1)
   4.108 +          end
   4.109 +        else
   4.110 +          t
   4.111 +      | aux _ t = t
   4.112 +  in aux (maxidx_of_term t + 1) t end
   4.113 +
   4.114 +fun introduce_combinators_in_term ctxt kind t =
   4.115 +  let val thy = ProofContext.theory_of ctxt in
   4.116 +    if Meson.is_fol_term thy t then
   4.117 +      t
   4.118 +    else
   4.119 +      let
   4.120 +        fun aux Ts t =
   4.121 +          case t of
   4.122 +            @{const Not} $ t1 => @{const Not} $ aux Ts t1
   4.123 +          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   4.124 +            t0 $ Abs (s, T, aux (T :: Ts) t')
   4.125 +          | (t0 as Const (@{const_name All}, _)) $ t1 =>
   4.126 +            aux Ts (t0 $ eta_expand Ts t1 1)
   4.127 +          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   4.128 +            t0 $ Abs (s, T, aux (T :: Ts) t')
   4.129 +          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   4.130 +            aux Ts (t0 $ eta_expand Ts t1 1)
   4.131 +          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   4.132 +          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   4.133 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   4.134 +          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   4.135 +              $ t1 $ t2 =>
   4.136 +            t0 $ aux Ts t1 $ aux Ts t2
   4.137 +          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   4.138 +                   t
   4.139 +                 else
   4.140 +                   t |> conceal_bounds Ts
   4.141 +                     |> Envir.eta_contract
   4.142 +                     |> cterm_of thy
   4.143 +                     |> Meson_Clausify.introduce_combinators_in_cterm
   4.144 +                     |> prop_of |> Logic.dest_equals |> snd
   4.145 +                     |> reveal_bounds Ts
   4.146 +        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   4.147 +      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   4.148 +      handle THM _ =>
   4.149 +             (* A type variable of sort "{}" will make abstraction fail. *)
   4.150 +             if kind = Conjecture then HOLogic.false_const
   4.151 +             else HOLogic.true_const
   4.152 +  end
   4.153 +
   4.154 +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   4.155 +   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   4.156 +fun freeze_term t =
   4.157 +  let
   4.158 +    fun aux (t $ u) = aux t $ aux u
   4.159 +      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   4.160 +      | aux (Var ((s, i), T)) =
   4.161 +        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   4.162 +      | aux t = t
   4.163 +  in t |> exists_subterm is_Var t ? aux end
   4.164 +
   4.165 +(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
   4.166 +    it leaves metaequalities over "prop"s alone. *)
   4.167 +val atomize_term =
   4.168 +  let
   4.169 +    fun aux (@{const Trueprop} $ t1) = t1
   4.170 +      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
   4.171 +        HOLogic.all_const T $ Abs (s, T, aux t')
   4.172 +      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
   4.173 +      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
   4.174 +        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
   4.175 +      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   4.176 +        HOLogic.eq_const T $ t1 $ t2
   4.177 +      | aux _ = raise Fail "aux"
   4.178 +  in perhaps (try aux) end
   4.179 +
   4.180 +(* making axiom and conjecture formulas *)
   4.181 +fun make_formula ctxt presimp name kind t =
   4.182 +  let
   4.183 +    val thy = ProofContext.theory_of ctxt
   4.184 +    val t = t |> Envir.beta_eta_contract
   4.185 +              |> transform_elim_term
   4.186 +              |> atomize_term
   4.187 +    val need_trueprop = (fastype_of t = HOLogic.boolT)
   4.188 +    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   4.189 +              |> extensionalize_term
   4.190 +              |> presimp ? presimplify_term thy
   4.191 +              |> perhaps (try (HOLogic.dest_Trueprop))
   4.192 +              |> introduce_combinators_in_term ctxt kind
   4.193 +              |> kind <> Axiom ? freeze_term
   4.194 +    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   4.195 +  in
   4.196 +    {name = name, combformula = combformula, kind = kind,
   4.197 +     ctypes_sorts = ctypes_sorts}
   4.198 +  end
   4.199 +
   4.200 +fun make_axiom ctxt presimp ((name, loc), th) =
   4.201 +  case make_formula ctxt presimp name Axiom (prop_of th) of
   4.202 +    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   4.203 +  | formula => SOME ((name, loc), formula)
   4.204 +fun make_conjecture ctxt ts =
   4.205 +  let val last = length ts - 1 in
   4.206 +    map2 (fn j => make_formula ctxt true (Int.toString j)
   4.207 +                               (if j = last then Conjecture else Hypothesis))
   4.208 +         (0 upto last) ts
   4.209 +  end
   4.210 +
   4.211 +(** Helper facts **)
   4.212 +
   4.213 +fun count_combterm (CombConst ((s, _), _, _)) =
   4.214 +    Symtab.map_entry s (Integer.add 1)
   4.215 +  | count_combterm (CombVar _) = I
   4.216 +  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   4.217 +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   4.218 +  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   4.219 +  | count_combformula (AAtom tm) = count_combterm tm
   4.220 +fun count_fol_formula ({combformula, ...} : fol_formula) =
   4.221 +  count_combformula combformula
   4.222 +
   4.223 +val optional_helpers =
   4.224 +  [(["c_COMBI"], @{thms Meson.COMBI_def}),
   4.225 +   (["c_COMBK"], @{thms Meson.COMBK_def}),
   4.226 +   (["c_COMBB"], @{thms Meson.COMBB_def}),
   4.227 +   (["c_COMBC"], @{thms Meson.COMBC_def}),
   4.228 +   (["c_COMBS"], @{thms Meson.COMBS_def})]
   4.229 +val optional_typed_helpers =
   4.230 +  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
   4.231 +   (["c_If"], @{thms if_True if_False})]
   4.232 +val mandatory_helpers = @{thms Metis.fequal_def}
   4.233 +
   4.234 +val init_counters =
   4.235 +  [optional_helpers, optional_typed_helpers] |> maps (maps fst)
   4.236 +  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
   4.237 +
   4.238 +fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   4.239 +  let
   4.240 +    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
   4.241 +    fun is_needed c = the (Symtab.lookup ct c) > 0
   4.242 +    fun baptize th = ((Thm.get_name_hint th, false), th)
   4.243 +  in
   4.244 +    (optional_helpers
   4.245 +     |> full_types ? append optional_typed_helpers
   4.246 +     |> maps (fn (ss, ths) =>
   4.247 +                 if exists is_needed ss then map baptize ths else [])) @
   4.248 +    (if is_FO then [] else map baptize mandatory_helpers)
   4.249 +    |> map_filter (Option.map snd o make_axiom ctxt false)
   4.250 +  end
   4.251 +
   4.252 +fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
   4.253 +
   4.254 +fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   4.255 +  let
   4.256 +    val thy = ProofContext.theory_of ctxt
   4.257 +    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
   4.258 +    (* Remove existing axioms from the conjecture, as this can dramatically
   4.259 +       boost an ATP's performance (for some reason). *)
   4.260 +    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
   4.261 +    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   4.262 +    val is_FO = Meson.is_fol_term thy goal_t
   4.263 +    val subs = tfree_classes_of_terms [goal_t]
   4.264 +    val supers = tvar_classes_of_terms axiom_ts
   4.265 +    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   4.266 +    (* TFrees in the conjecture; TVars in the axioms *)
   4.267 +    val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   4.268 +    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
   4.269 +    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   4.270 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   4.271 +    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   4.272 +  in
   4.273 +    (axiom_names |> map single |> Vector.fromList,
   4.274 +     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   4.275 +  end
   4.276 +
   4.277 +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   4.278 +
   4.279 +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   4.280 +  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   4.281 +  | fo_term_for_combtyp (CombType (name, tys)) =
   4.282 +    ATerm (name, map fo_term_for_combtyp tys)
   4.283 +
   4.284 +fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   4.285 +    (true, ATerm (class, [ATerm (name, [])]))
   4.286 +  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   4.287 +    (true, ATerm (class, [ATerm (name, [])]))
   4.288 +
   4.289 +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   4.290 +
   4.291 +fun fo_term_for_combterm full_types =
   4.292 +  let
   4.293 +    fun aux top_level u =
   4.294 +      let
   4.295 +        val (head, args) = strip_combterm_comb u
   4.296 +        val (x, ty_args) =
   4.297 +          case head of
   4.298 +            CombConst (name as (s, s'), _, ty_args) =>
   4.299 +            let val ty_args = if full_types then [] else ty_args in
   4.300 +              if s = "equal" then
   4.301 +                if top_level andalso length args = 2 then (name, [])
   4.302 +                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
   4.303 +              else if top_level then
   4.304 +                case s of
   4.305 +                  "c_False" => (("$false", s'), [])
   4.306 +                | "c_True" => (("$true", s'), [])
   4.307 +                | _ => (name, ty_args)
   4.308 +              else
   4.309 +                (name, ty_args)
   4.310 +            end
   4.311 +          | CombVar (name, _) => (name, [])
   4.312 +          | CombApp _ => raise Fail "impossible \"CombApp\""
   4.313 +        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   4.314 +                          map (aux false) args)
   4.315 +    in
   4.316 +      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   4.317 +    end
   4.318 +  in aux true end
   4.319 +
   4.320 +fun formula_for_combformula full_types =
   4.321 +  let
   4.322 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   4.323 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   4.324 +      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   4.325 +  in aux end
   4.326 +
   4.327 +fun formula_for_axiom full_types
   4.328 +                      ({combformula, ctypes_sorts, ...} : fol_formula) =
   4.329 +  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   4.330 +                (type_literals_for_types ctypes_sorts))
   4.331 +           (formula_for_combformula full_types combformula)
   4.332 +
   4.333 +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   4.334 +  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   4.335 +
   4.336 +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   4.337 +                                                       superclass, ...}) =
   4.338 +  let val ty_arg = ATerm (("T", "T"), []) in
   4.339 +    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   4.340 +         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   4.341 +                           AAtom (ATerm (superclass, [ty_arg]))]))
   4.342 +  end
   4.343 +
   4.344 +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   4.345 +    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   4.346 +  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   4.347 +    (false, ATerm (c, [ATerm (sort, [])]))
   4.348 +
   4.349 +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   4.350 +                                                ...}) =
   4.351 +  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   4.352 +       mk_ahorn (map (formula_for_fo_literal o apfst not
   4.353 +                      o fo_literal_for_arity_literal) premLits)
   4.354 +                (formula_for_fo_literal
   4.355 +                     (fo_literal_for_arity_literal conclLit)))
   4.356 +
   4.357 +fun problem_line_for_conjecture full_types
   4.358 +                                ({name, kind, combformula, ...} : fol_formula) =
   4.359 +  Fof (conjecture_prefix ^ name, kind,
   4.360 +       formula_for_combformula full_types combformula)
   4.361 +
   4.362 +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
   4.363 +  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   4.364 +
   4.365 +fun problem_line_for_free_type j lit =
   4.366 +  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
   4.367 +fun problem_lines_for_free_types conjectures =
   4.368 +  let
   4.369 +    val litss = map free_type_literals_for_conjecture conjectures
   4.370 +    val lits = fold (union (op =)) litss []
   4.371 +  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   4.372 +
   4.373 +(** "hBOOL" and "hAPP" **)
   4.374 +
   4.375 +type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   4.376 +
   4.377 +fun consider_term top_level (ATerm ((s, _), ts)) =
   4.378 +  (if is_atp_variable s then
   4.379 +     I
   4.380 +   else
   4.381 +     let val n = length ts in
   4.382 +       Symtab.map_default
   4.383 +           (s, {min_arity = n, max_arity = 0, sub_level = false})
   4.384 +           (fn {min_arity, max_arity, sub_level} =>
   4.385 +               {min_arity = Int.min (n, min_arity),
   4.386 +                max_arity = Int.max (n, max_arity),
   4.387 +                sub_level = sub_level orelse not top_level})
   4.388 +     end)
   4.389 +  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   4.390 +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   4.391 +  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   4.392 +  | consider_formula (AAtom tm) = consider_term true tm
   4.393 +
   4.394 +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   4.395 +fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   4.396 +
   4.397 +fun const_table_for_problem explicit_apply problem =
   4.398 +  if explicit_apply then NONE
   4.399 +  else SOME (Symtab.empty |> consider_problem problem)
   4.400 +
   4.401 +fun min_arity_of thy full_types NONE s =
   4.402 +    (if s = "equal" orelse s = type_wrapper_name orelse
   4.403 +        String.isPrefix type_const_prefix s orelse
   4.404 +        String.isPrefix class_prefix s then
   4.405 +       16383 (* large number *)
   4.406 +     else if full_types then
   4.407 +       0
   4.408 +     else case strip_prefix_and_unascii const_prefix s of
   4.409 +       SOME s' => num_type_args thy (invert_const s')
   4.410 +     | NONE => 0)
   4.411 +  | min_arity_of _ _ (SOME the_const_tab) s =
   4.412 +    case Symtab.lookup the_const_tab s of
   4.413 +      SOME ({min_arity, ...} : const_info) => min_arity
   4.414 +    | NONE => 0
   4.415 +
   4.416 +fun full_type_of (ATerm ((s, _), [ty, _])) =
   4.417 +    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   4.418 +  | full_type_of _ = raise Fail "expected type wrapper"
   4.419 +
   4.420 +fun list_hAPP_rev _ t1 [] = t1
   4.421 +  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   4.422 +    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   4.423 +  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   4.424 +    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   4.425 +                         [full_type_of t2, ty]) in
   4.426 +      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   4.427 +    end
   4.428 +
   4.429 +fun repair_applications_in_term thy full_types const_tab =
   4.430 +  let
   4.431 +    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   4.432 +      if s = type_wrapper_name then
   4.433 +        case ts of
   4.434 +          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   4.435 +        | _ => raise Fail "malformed type wrapper"
   4.436 +      else
   4.437 +        let
   4.438 +          val ts = map (aux NONE) ts
   4.439 +          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   4.440 +        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   4.441 +  in aux NONE end
   4.442 +
   4.443 +fun boolify t = ATerm (`I "hBOOL", [t])
   4.444 +
   4.445 +(* True if the constant ever appears outside of the top-level position in
   4.446 +   literals, or if it appears with different arities (e.g., because of different
   4.447 +   type instantiations). If false, the constant always receives all of its
   4.448 +   arguments and is used as a predicate. *)
   4.449 +fun is_predicate NONE s =
   4.450 +    s = "equal" orelse s = "$false" orelse s = "$true" orelse
   4.451 +    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   4.452 +  | is_predicate (SOME the_const_tab) s =
   4.453 +    case Symtab.lookup the_const_tab s of
   4.454 +      SOME {min_arity, max_arity, sub_level} =>
   4.455 +      not sub_level andalso min_arity = max_arity
   4.456 +    | NONE => false
   4.457 +
   4.458 +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   4.459 +  if s = type_wrapper_name then
   4.460 +    case ts of
   4.461 +      [_, t' as ATerm ((s', _), _)] =>
   4.462 +      if is_predicate const_tab s' then t' else boolify t
   4.463 +    | _ => raise Fail "malformed type wrapper"
   4.464 +  else
   4.465 +    t |> not (is_predicate const_tab s) ? boolify
   4.466 +
   4.467 +fun close_universally phi =
   4.468 +  let
   4.469 +    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   4.470 +        (is_atp_variable s andalso not (member (op =) bounds name))
   4.471 +          ? insert (op =) name
   4.472 +        #> fold (term_vars bounds) tms
   4.473 +    fun formula_vars bounds (AQuant (_, xs, phi)) =
   4.474 +        formula_vars (xs @ bounds) phi
   4.475 +      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   4.476 +      | formula_vars bounds (AAtom tm) = term_vars bounds tm
   4.477 +  in
   4.478 +    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   4.479 +  end
   4.480 +
   4.481 +fun repair_formula thy explicit_forall full_types const_tab =
   4.482 +  let
   4.483 +    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   4.484 +      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   4.485 +      | aux (AAtom tm) =
   4.486 +        AAtom (tm |> repair_applications_in_term thy full_types const_tab
   4.487 +                  |> repair_predicates_in_term const_tab)
   4.488 +  in aux #> explicit_forall ? close_universally end
   4.489 +
   4.490 +fun repair_problem_line thy explicit_forall full_types const_tab
   4.491 +                        (Fof (ident, kind, phi)) =
   4.492 +  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   4.493 +fun repair_problem_with_const_table thy =
   4.494 +  map o apsnd o map ooo repair_problem_line thy
   4.495 +
   4.496 +fun repair_problem thy explicit_forall full_types explicit_apply problem =
   4.497 +  repair_problem_with_const_table thy explicit_forall full_types
   4.498 +      (const_table_for_problem explicit_apply problem) problem
   4.499 +
   4.500 +fun prepare_atp_problem ctxt readable_names explicit_forall full_types
   4.501 +                        explicit_apply hyp_ts concl_t axioms =
   4.502 +  let
   4.503 +    val thy = ProofContext.theory_of ctxt
   4.504 +    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   4.505 +                       arity_clauses)) =
   4.506 +      prepare_formulas ctxt full_types hyp_ts concl_t axioms
   4.507 +    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   4.508 +    val helper_lines =
   4.509 +      map (problem_line_for_fact helper_prefix full_types) helper_facts
   4.510 +    val conjecture_lines =
   4.511 +      map (problem_line_for_conjecture full_types) conjectures
   4.512 +    val tfree_lines = problem_lines_for_free_types conjectures
   4.513 +    val class_rel_lines =
   4.514 +      map problem_line_for_class_rel_clause class_rel_clauses
   4.515 +    val arity_lines = map problem_line_for_arity_clause arity_clauses
   4.516 +    (* Reordering these might or might not confuse the proof reconstruction
   4.517 +       code or the SPASS Flotter hack. *)
   4.518 +    val problem =
   4.519 +      [("Relevant facts", axiom_lines),
   4.520 +       ("Class relationships", class_rel_lines),
   4.521 +       ("Arity declarations", arity_lines),
   4.522 +       ("Helper facts", helper_lines),
   4.523 +       ("Conjectures", conjecture_lines),
   4.524 +       ("Type variables", tfree_lines)]
   4.525 +      |> repair_problem thy explicit_forall full_types explicit_apply
   4.526 +    val (problem, pool) = nice_atp_problem readable_names problem
   4.527 +    val conjecture_offset =
   4.528 +      length axiom_lines + length class_rel_lines + length arity_lines
   4.529 +      + length helper_lines
   4.530 +  in
   4.531 +    (problem,
   4.532 +     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   4.533 +     conjecture_offset, axiom_names)
   4.534 +  end
   4.535 +
   4.536 +end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Oct 22 13:49:44 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,946 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     5.5 -    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     5.6 -    Author:     Claire Quigley, Cambridge University Computer Laboratory
     5.7 -    Author:     Jasmin Blanchette, TU Muenchen
     5.8 -
     5.9 -Proof reconstruction for Sledgehammer.
    5.10 -*)
    5.11 -
    5.12 -signature SLEDGEHAMMER_RECONSTRUCT =
    5.13 -sig
    5.14 -  type locality = Sledgehammer_Filter.locality
    5.15 -  type minimize_command = string list -> string
    5.16 -  type metis_params =
    5.17 -    string * bool * minimize_command * string * (string * locality) list vector
    5.18 -    * thm * int
    5.19 -  type isar_params =
    5.20 -    string Symtab.table * bool * int * Proof.context * int list list
    5.21 -  type text_result = string * (string * locality) list
    5.22 -
    5.23 -  val repair_conjecture_shape_and_axiom_names :
    5.24 -    string -> int list list -> (string * locality) list vector
    5.25 -    -> int list list * (string * locality) list vector
    5.26 -  val apply_on_subgoal : int -> int -> string
    5.27 -  val command_call : string -> string list -> string
    5.28 -  val try_command_line : string -> string -> string
    5.29 -  val minimize_line : ('a list -> string) -> 'a list -> string
    5.30 -  val metis_proof_text : metis_params -> text_result
    5.31 -  val isar_proof_text : isar_params -> metis_params -> text_result
    5.32 -  val proof_text : bool -> isar_params -> metis_params -> text_result
    5.33 -end;
    5.34 -
    5.35 -structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    5.36 -struct
    5.37 -
    5.38 -open ATP_Problem
    5.39 -open ATP_Proof
    5.40 -open Metis_Translate
    5.41 -open Sledgehammer_Util
    5.42 -open Sledgehammer_Filter
    5.43 -open Sledgehammer_Translate
    5.44 -
    5.45 -type minimize_command = string list -> string
    5.46 -type metis_params =
    5.47 -  string * bool * minimize_command * string * (string * locality) list vector
    5.48 -  * thm * int
    5.49 -type isar_params =
    5.50 -  string Symtab.table * bool * int * Proof.context * int list list
    5.51 -type text_result = string * (string * locality) list
    5.52 -
    5.53 -fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    5.54 -val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    5.55 -
    5.56 -fun find_first_in_list_vector vec key =
    5.57 -  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    5.58 -                 | (_, value) => value) NONE vec
    5.59 -
    5.60 -
    5.61 -(** SPASS's Flotter hack **)
    5.62 -
    5.63 -(* This is a hack required for keeping track of axioms after they have been
    5.64 -   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    5.65 -   part of this hack. *)
    5.66 -
    5.67 -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    5.68 -
    5.69 -fun extract_clause_sequence output =
    5.70 -  let
    5.71 -    val tokens_of = String.tokens (not o Char.isAlphaNum)
    5.72 -    fun extract_num ("clause" :: (ss as _ :: _)) =
    5.73 -    Int.fromString (List.last ss)
    5.74 -      | extract_num _ = NONE
    5.75 -  in output |> split_lines |> map_filter (extract_num o tokens_of) end
    5.76 -
    5.77 -val parse_clause_formula_pair =
    5.78 -  $$ "(" |-- scan_integer --| $$ ","
    5.79 -  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
    5.80 -  --| Scan.option ($$ ",")
    5.81 -val parse_clause_formula_relation =
    5.82 -  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    5.83 -  |-- Scan.repeat parse_clause_formula_pair
    5.84 -val extract_clause_formula_relation =
    5.85 -  Substring.full #> Substring.position set_ClauseFormulaRelationN
    5.86 -  #> snd #> Substring.position "." #> fst #> Substring.string
    5.87 -  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    5.88 -  #> fst
    5.89 -
    5.90 -fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    5.91 -                                            axiom_names =
    5.92 -  if String.isSubstring set_ClauseFormulaRelationN output then
    5.93 -    let
    5.94 -      val j0 = hd (hd conjecture_shape)
    5.95 -      val seq = extract_clause_sequence output
    5.96 -      val name_map = extract_clause_formula_relation output
    5.97 -      fun renumber_conjecture j =
    5.98 -        conjecture_prefix ^ string_of_int (j - j0)
    5.99 -        |> AList.find (fn (s, ss) => member (op =) ss s) name_map
   5.100 -        |> map (fn s => find_index (curry (op =) s) seq + 1)
   5.101 -      fun names_for_number j =
   5.102 -        j |> AList.lookup (op =) name_map |> these
   5.103 -          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   5.104 -          |> map (fn name =>
   5.105 -                     (name, name |> find_first_in_list_vector axiom_names
   5.106 -                                 |> the)
   5.107 -                     handle Option.Option =>
   5.108 -                            error ("No such fact: " ^ quote name ^ "."))
   5.109 -    in
   5.110 -      (conjecture_shape |> map (maps renumber_conjecture),
   5.111 -       seq |> map names_for_number |> Vector.fromList)
   5.112 -    end
   5.113 -  else
   5.114 -    (conjecture_shape, axiom_names)
   5.115 -
   5.116 -
   5.117 -(** Soft-core proof reconstruction: Metis one-liner **)
   5.118 -
   5.119 -fun string_for_label (s, num) = s ^ string_of_int num
   5.120 -
   5.121 -fun apply_on_subgoal _ 1 = "by "
   5.122 -  | apply_on_subgoal 1 _ = "apply "
   5.123 -  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
   5.124 -fun command_call name [] = name
   5.125 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   5.126 -fun try_command_line banner command =
   5.127 -  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   5.128 -fun using_labels [] = ""
   5.129 -  | using_labels ls =
   5.130 -    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   5.131 -fun metis_name full_types = if full_types then "metisFT" else "metis"
   5.132 -fun metis_call full_types ss = command_call (metis_name full_types) ss
   5.133 -fun metis_command full_types i n (ls, ss) =
   5.134 -  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
   5.135 -fun metis_line banner full_types i n ss =
   5.136 -  try_command_line banner (metis_command full_types i n ([], ss))
   5.137 -fun minimize_line _ [] = ""
   5.138 -  | minimize_line minimize_command ss =
   5.139 -    case minimize_command ss of
   5.140 -      "" => ""
   5.141 -    | command =>
   5.142 -      "\nTo minimize the number of lemmas, try this: " ^
   5.143 -      Markup.markup Markup.sendback command ^ "."
   5.144 -
   5.145 -fun resolve_axiom axiom_names ((_, SOME s)) =
   5.146 -    (case strip_prefix_and_unascii axiom_prefix s of
   5.147 -       SOME s' => (case find_first_in_list_vector axiom_names s' of
   5.148 -                     SOME x => [(s', x)]
   5.149 -                   | NONE => [])
   5.150 -     | NONE => [])
   5.151 -  | resolve_axiom axiom_names (num, NONE) =
   5.152 -    case Int.fromString num of
   5.153 -      SOME j =>
   5.154 -      if j > 0 andalso j <= Vector.length axiom_names then
   5.155 -        Vector.sub (axiom_names, j - 1)
   5.156 -      else
   5.157 -        []
   5.158 -    | NONE => []
   5.159 -
   5.160 -fun add_fact axiom_names (Inference (name, _, [])) =
   5.161 -    append (resolve_axiom axiom_names name)
   5.162 -  | add_fact _ _ = I
   5.163 -
   5.164 -fun used_facts_in_tstplike_proof axiom_names =
   5.165 -  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
   5.166 -
   5.167 -fun used_facts axiom_names =
   5.168 -  used_facts_in_tstplike_proof axiom_names
   5.169 -  #> List.partition (curry (op =) Chained o snd)
   5.170 -  #> pairself (sort_distinct (string_ord o pairself fst))
   5.171 -
   5.172 -fun metis_proof_text (banner, full_types, minimize_command,
   5.173 -                      tstplike_proof, axiom_names, goal, i) =
   5.174 -  let
   5.175 -    val (chained_lemmas, other_lemmas) =
   5.176 -      used_facts axiom_names tstplike_proof
   5.177 -    val n = Logic.count_prems (prop_of goal)
   5.178 -  in
   5.179 -    (metis_line banner full_types i n (map fst other_lemmas) ^
   5.180 -     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   5.181 -     other_lemmas @ chained_lemmas)
   5.182 -  end
   5.183 -
   5.184 -
   5.185 -(** Hard-core proof reconstruction: structured Isar proofs **)
   5.186 -
   5.187 -(* Simple simplifications to ensure that sort annotations don't leave a trail of
   5.188 -   spurious "True"s. *)
   5.189 -fun s_not @{const False} = @{const True}
   5.190 -  | s_not @{const True} = @{const False}
   5.191 -  | s_not (@{const Not} $ t) = t
   5.192 -  | s_not t = @{const Not} $ t
   5.193 -fun s_conj (@{const True}, t2) = t2
   5.194 -  | s_conj (t1, @{const True}) = t1
   5.195 -  | s_conj p = HOLogic.mk_conj p
   5.196 -fun s_disj (@{const False}, t2) = t2
   5.197 -  | s_disj (t1, @{const False}) = t1
   5.198 -  | s_disj p = HOLogic.mk_disj p
   5.199 -fun s_imp (@{const True}, t2) = t2
   5.200 -  | s_imp (t1, @{const False}) = s_not t1
   5.201 -  | s_imp p = HOLogic.mk_imp p
   5.202 -fun s_iff (@{const True}, t2) = t2
   5.203 -  | s_iff (t1, @{const True}) = t1
   5.204 -  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   5.205 -
   5.206 -fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   5.207 -fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   5.208 -
   5.209 -fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   5.210 -    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   5.211 -  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   5.212 -    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   5.213 -  | negate_term (@{const HOL.implies} $ t1 $ t2) =
   5.214 -    @{const HOL.conj} $ t1 $ negate_term t2
   5.215 -  | negate_term (@{const HOL.conj} $ t1 $ t2) =
   5.216 -    @{const HOL.disj} $ negate_term t1 $ negate_term t2
   5.217 -  | negate_term (@{const HOL.disj} $ t1 $ t2) =
   5.218 -    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   5.219 -  | negate_term (@{const Not} $ t) = t
   5.220 -  | negate_term t = @{const Not} $ t
   5.221 -
   5.222 -val indent_size = 2
   5.223 -val no_label = ("", ~1)
   5.224 -
   5.225 -val raw_prefix = "X"
   5.226 -val assum_prefix = "A"
   5.227 -val fact_prefix = "F"
   5.228 -
   5.229 -fun resolve_conjecture conjecture_shape (num, s_opt) =
   5.230 -  let
   5.231 -    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   5.232 -              SOME s => Int.fromString s |> the_default ~1
   5.233 -            | NONE => case Int.fromString num of
   5.234 -                        SOME j => find_index (exists (curry (op =) j))
   5.235 -                                             conjecture_shape
   5.236 -                      | NONE => ~1
   5.237 -  in if k >= 0 then [k] else [] end
   5.238 -
   5.239 -fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   5.240 -fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   5.241 -
   5.242 -fun raw_label_for_name conjecture_shape name =
   5.243 -  case resolve_conjecture conjecture_shape name of
   5.244 -    [j] => (conjecture_prefix, j)
   5.245 -  | _ => case Int.fromString (fst name) of
   5.246 -           SOME j => (raw_prefix, j)
   5.247 -         | NONE => (raw_prefix ^ fst name, 0)
   5.248 -
   5.249 -(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   5.250 -
   5.251 -exception FO_TERM of string fo_term list
   5.252 -exception FORMULA of (string, string fo_term) formula list
   5.253 -exception SAME of unit
   5.254 -
   5.255 -(* Type variables are given the basic sort "HOL.type". Some will later be
   5.256 -   constrained by information from type literals, or by type inference. *)
   5.257 -fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   5.258 -  let val Ts = map (type_from_fo_term tfrees) us in
   5.259 -    case strip_prefix_and_unascii type_const_prefix a of
   5.260 -      SOME b => Type (invert_const b, Ts)
   5.261 -    | NONE =>
   5.262 -      if not (null us) then
   5.263 -        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   5.264 -      else case strip_prefix_and_unascii tfree_prefix a of
   5.265 -        SOME b =>
   5.266 -        let val s = "'" ^ b in
   5.267 -          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   5.268 -        end
   5.269 -      | NONE =>
   5.270 -        case strip_prefix_and_unascii tvar_prefix a of
   5.271 -          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   5.272 -        | NONE =>
   5.273 -          (* Variable from the ATP, say "X1" *)
   5.274 -          Type_Infer.param 0 (a, HOLogic.typeS)
   5.275 -  end
   5.276 -
   5.277 -(* Type class literal applied to a type. Returns triple of polarity, class,
   5.278 -   type. *)
   5.279 -fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   5.280 -  case (strip_prefix_and_unascii class_prefix a,
   5.281 -        map (type_from_fo_term tfrees) us) of
   5.282 -    (SOME b, [T]) => (pos, b, T)
   5.283 -  | _ => raise FO_TERM [u]
   5.284 -
   5.285 -(** Accumulate type constraints in a formula: negative type literals **)
   5.286 -fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   5.287 -fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   5.288 -  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   5.289 -  | add_type_constraint _ = I
   5.290 -
   5.291 -fun repair_atp_variable_name f s =
   5.292 -  let
   5.293 -    fun subscript_name s n = s ^ nat_subscript n
   5.294 -    val s = String.map f s
   5.295 -  in
   5.296 -    case space_explode "_" s of
   5.297 -      [_] => (case take_suffix Char.isDigit (String.explode s) of
   5.298 -                (cs1 as _ :: _, cs2 as _ :: _) =>
   5.299 -                subscript_name (String.implode cs1)
   5.300 -                               (the (Int.fromString (String.implode cs2)))
   5.301 -              | (_, _) => s)
   5.302 -    | [s1, s2] => (case Int.fromString s2 of
   5.303 -                     SOME n => subscript_name s1 n
   5.304 -                   | NONE => s)
   5.305 -    | _ => s
   5.306 -  end
   5.307 -
   5.308 -(* First-order translation. No types are known for variables. "HOLogic.typeT"
   5.309 -   should allow them to be inferred. *)
   5.310 -fun raw_term_from_pred thy full_types tfrees =
   5.311 -  let
   5.312 -    fun aux opt_T extra_us u =
   5.313 -      case u of
   5.314 -        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   5.315 -      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   5.316 -      | ATerm (a, us) =>
   5.317 -        if a = type_wrapper_name then
   5.318 -          case us of
   5.319 -            [typ_u, term_u] =>
   5.320 -            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   5.321 -          | _ => raise FO_TERM us
   5.322 -        else case strip_prefix_and_unascii const_prefix a of
   5.323 -          SOME "equal" =>
   5.324 -          let val ts = map (aux NONE []) us in
   5.325 -            if length ts = 2 andalso hd ts aconv List.last ts then
   5.326 -              (* Vampire is keen on producing these. *)
   5.327 -              @{const True}
   5.328 -            else
   5.329 -              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   5.330 -          end
   5.331 -        | SOME b =>
   5.332 -          let
   5.333 -            val c = invert_const b
   5.334 -            val num_type_args = num_type_args thy c
   5.335 -            val (type_us, term_us) =
   5.336 -              chop (if full_types then 0 else num_type_args) us
   5.337 -            (* Extra args from "hAPP" come after any arguments given directly to
   5.338 -               the constant. *)
   5.339 -            val term_ts = map (aux NONE []) term_us
   5.340 -            val extra_ts = map (aux NONE []) extra_us
   5.341 -            val t =
   5.342 -              Const (c, if full_types then
   5.343 -                          case opt_T of
   5.344 -                            SOME T => map fastype_of term_ts ---> T
   5.345 -                          | NONE =>
   5.346 -                            if num_type_args = 0 then
   5.347 -                              Sign.const_instance thy (c, [])
   5.348 -                            else
   5.349 -                              raise Fail ("no type information for " ^ quote c)
   5.350 -                        else
   5.351 -                          Sign.const_instance thy (c,
   5.352 -                              map (type_from_fo_term tfrees) type_us))
   5.353 -          in list_comb (t, term_ts @ extra_ts) end
   5.354 -        | NONE => (* a free or schematic variable *)
   5.355 -          let
   5.356 -            val ts = map (aux NONE []) (us @ extra_us)
   5.357 -            val T = map fastype_of ts ---> HOLogic.typeT
   5.358 -            val t =
   5.359 -              case strip_prefix_and_unascii fixed_var_prefix a of
   5.360 -                SOME b => Free (b, T)
   5.361 -              | NONE =>
   5.362 -                case strip_prefix_and_unascii schematic_var_prefix a of
   5.363 -                  SOME b => Var ((b, 0), T)
   5.364 -                | NONE =>
   5.365 -                  if is_atp_variable a then
   5.366 -                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
   5.367 -                  else
   5.368 -                    (* Skolem constants? *)
   5.369 -                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   5.370 -          in list_comb (t, ts) end
   5.371 -  in aux (SOME HOLogic.boolT) [] end
   5.372 -
   5.373 -fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   5.374 -  if String.isPrefix class_prefix s then
   5.375 -    add_type_constraint (type_constraint_from_term pos tfrees u)
   5.376 -    #> pair @{const True}
   5.377 -  else
   5.378 -    pair (raw_term_from_pred thy full_types tfrees u)
   5.379 -
   5.380 -val combinator_table =
   5.381 -  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   5.382 -   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   5.383 -   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   5.384 -   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   5.385 -   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   5.386 -
   5.387 -fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   5.388 -  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   5.389 -  | uncombine_term (t as Const (x as (s, _))) =
   5.390 -    (case AList.lookup (op =) combinator_table s of
   5.391 -       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   5.392 -     | NONE => t)
   5.393 -  | uncombine_term t = t
   5.394 -
   5.395 -(* Update schematic type variables with detected sort constraints. It's not
   5.396 -   totally clear when this code is necessary. *)
   5.397 -fun repair_tvar_sorts (t, tvar_tab) =
   5.398 -  let
   5.399 -    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   5.400 -      | do_type (TVar (xi, s)) =
   5.401 -        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   5.402 -      | do_type (TFree z) = TFree z
   5.403 -    fun do_term (Const (a, T)) = Const (a, do_type T)
   5.404 -      | do_term (Free (a, T)) = Free (a, do_type T)
   5.405 -      | do_term (Var (xi, T)) = Var (xi, do_type T)
   5.406 -      | do_term (t as Bound _) = t
   5.407 -      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   5.408 -      | do_term (t1 $ t2) = do_term t1 $ do_term t2
   5.409 -  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   5.410 -
   5.411 -fun quantify_over_var quant_of var_s t =
   5.412 -  let
   5.413 -    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   5.414 -                  |> map Var
   5.415 -  in fold_rev quant_of vars t end
   5.416 -
   5.417 -(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   5.418 -   appear in the formula. *)
   5.419 -fun prop_from_formula thy full_types tfrees phi =
   5.420 -  let
   5.421 -    fun do_formula pos phi =
   5.422 -      case phi of
   5.423 -        AQuant (_, [], phi) => do_formula pos phi
   5.424 -      | AQuant (q, x :: xs, phi') =>
   5.425 -        do_formula pos (AQuant (q, xs, phi'))
   5.426 -        #>> quantify_over_var (case q of
   5.427 -                                 AForall => forall_of
   5.428 -                               | AExists => exists_of)
   5.429 -                              (repair_atp_variable_name Char.toLower x)
   5.430 -      | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   5.431 -      | AConn (c, [phi1, phi2]) =>
   5.432 -        do_formula (pos |> c = AImplies ? not) phi1
   5.433 -        ##>> do_formula pos phi2
   5.434 -        #>> (case c of
   5.435 -               AAnd => s_conj
   5.436 -             | AOr => s_disj
   5.437 -             | AImplies => s_imp
   5.438 -             | AIf => s_imp o swap
   5.439 -             | AIff => s_iff
   5.440 -             | ANotIff => s_not o s_iff)
   5.441 -      | AAtom tm => term_from_pred thy full_types tfrees pos tm
   5.442 -      | _ => raise FORMULA [phi]
   5.443 -  in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   5.444 -
   5.445 -fun check_formula ctxt =
   5.446 -  Type.constraint HOLogic.boolT
   5.447 -  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   5.448 -
   5.449 -
   5.450 -(**** Translation of TSTP files to Isar Proofs ****)
   5.451 -
   5.452 -fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   5.453 -  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   5.454 -
   5.455 -fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   5.456 -    let
   5.457 -      val thy = ProofContext.theory_of ctxt
   5.458 -      val t1 = prop_from_formula thy full_types tfrees phi1
   5.459 -      val vars = snd (strip_comb t1)
   5.460 -      val frees = map unvarify_term vars
   5.461 -      val unvarify_args = subst_atomic (vars ~~ frees)
   5.462 -      val t2 = prop_from_formula thy full_types tfrees phi2
   5.463 -      val (t1, t2) =
   5.464 -        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   5.465 -        |> unvarify_args |> uncombine_term |> check_formula ctxt
   5.466 -        |> HOLogic.dest_eq
   5.467 -    in
   5.468 -      (Definition (name, t1, t2),
   5.469 -       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   5.470 -    end
   5.471 -  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   5.472 -    let
   5.473 -      val thy = ProofContext.theory_of ctxt
   5.474 -      val t = u |> prop_from_formula thy full_types tfrees
   5.475 -                |> uncombine_term |> check_formula ctxt
   5.476 -    in
   5.477 -      (Inference (name, t, deps),
   5.478 -       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   5.479 -    end
   5.480 -fun decode_lines ctxt full_types tfrees lines =
   5.481 -  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   5.482 -
   5.483 -fun is_same_inference _ (Definition _) = false
   5.484 -  | is_same_inference t (Inference (_, t', _)) = t aconv t'
   5.485 -
   5.486 -(* No "real" literals means only type information (tfree_tcs, clsrel, or
   5.487 -   clsarity). *)
   5.488 -val is_only_type_information = curry (op aconv) HOLogic.true_const
   5.489 -
   5.490 -fun replace_one_dependency (old, new) dep =
   5.491 -  if is_same_step (dep, old) then new else [dep]
   5.492 -fun replace_dependencies_in_line _ (line as Definition _) = line
   5.493 -  | replace_dependencies_in_line p (Inference (name, t, deps)) =
   5.494 -    Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   5.495 -
   5.496 -(* Discard axioms; consolidate adjacent lines that prove the same formula, since
   5.497 -   they differ only in type information.*)
   5.498 -fun add_line _ _ (line as Definition _) lines = line :: lines
   5.499 -  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   5.500 -    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   5.501 -       definitions. *)
   5.502 -    if is_axiom axiom_names name then
   5.503 -      (* Axioms are not proof lines. *)
   5.504 -      if is_only_type_information t then
   5.505 -        map (replace_dependencies_in_line (name, [])) lines
   5.506 -      (* Is there a repetition? If so, replace later line by earlier one. *)
   5.507 -      else case take_prefix (not o is_same_inference t) lines of
   5.508 -        (_, []) => lines (* no repetition of proof line *)
   5.509 -      | (pre, Inference (name', _, _) :: post) =>
   5.510 -        pre @ map (replace_dependencies_in_line (name', [name])) post
   5.511 -    else if is_conjecture conjecture_shape name then
   5.512 -      Inference (name, negate_term t, []) :: lines
   5.513 -    else
   5.514 -      map (replace_dependencies_in_line (name, [])) lines
   5.515 -  | add_line _ _ (Inference (name, t, deps)) lines =
   5.516 -    (* Type information will be deleted later; skip repetition test. *)
   5.517 -    if is_only_type_information t then
   5.518 -      Inference (name, t, deps) :: lines
   5.519 -    (* Is there a repetition? If so, replace later line by earlier one. *)
   5.520 -    else case take_prefix (not o is_same_inference t) lines of
   5.521 -      (* FIXME: Doesn't this code risk conflating proofs involving different
   5.522 -         types? *)
   5.523 -       (_, []) => Inference (name, t, deps) :: lines
   5.524 -     | (pre, Inference (name', t', _) :: post) =>
   5.525 -       Inference (name, t', deps) ::
   5.526 -       pre @ map (replace_dependencies_in_line (name', [name])) post
   5.527 -
   5.528 -(* Recursively delete empty lines (type information) from the proof. *)
   5.529 -fun add_nontrivial_line (Inference (name, t, [])) lines =
   5.530 -    if is_only_type_information t then delete_dependency name lines
   5.531 -    else Inference (name, t, []) :: lines
   5.532 -  | add_nontrivial_line line lines = line :: lines
   5.533 -and delete_dependency name lines =
   5.534 -  fold_rev add_nontrivial_line
   5.535 -           (map (replace_dependencies_in_line (name, [])) lines) []
   5.536 -
   5.537 -(* ATPs sometimes reuse free variable names in the strangest ways. Removing
   5.538 -   offending lines often does the trick. *)
   5.539 -fun is_bad_free frees (Free x) = not (member (op =) frees x)
   5.540 -  | is_bad_free _ _ = false
   5.541 -
   5.542 -fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   5.543 -    (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   5.544 -  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   5.545 -                     (Inference (name, t, deps)) (j, lines) =
   5.546 -    (j + 1,
   5.547 -     if is_axiom axiom_names name orelse
   5.548 -        is_conjecture conjecture_shape name orelse
   5.549 -        (* the last line must be kept *)
   5.550 -        j = 0 orelse
   5.551 -        (not (is_only_type_information t) andalso
   5.552 -         null (Term.add_tvars t []) andalso
   5.553 -         not (exists_subterm (is_bad_free frees) t) andalso
   5.554 -         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   5.555 -         (* kill next to last line, which usually results in a trivial step *)
   5.556 -         j <> 1) then
   5.557 -       Inference (name, t, deps) :: lines  (* keep line *)
   5.558 -     else
   5.559 -       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   5.560 -
   5.561 -(** Isar proof construction and manipulation **)
   5.562 -
   5.563 -fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   5.564 -  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   5.565 -
   5.566 -type label = string * int
   5.567 -type facts = label list * string list
   5.568 -
   5.569 -datatype isar_qualifier = Show | Then | Moreover | Ultimately
   5.570 -
   5.571 -datatype isar_step =
   5.572 -  Fix of (string * typ) list |
   5.573 -  Let of term * term |
   5.574 -  Assume of label * term |
   5.575 -  Have of isar_qualifier list * label * term * byline
   5.576 -and byline =
   5.577 -  ByMetis of facts |
   5.578 -  CaseSplit of isar_step list list * facts
   5.579 -
   5.580 -fun smart_case_split [] facts = ByMetis facts
   5.581 -  | smart_case_split proofs facts = CaseSplit (proofs, facts)
   5.582 -
   5.583 -fun add_fact_from_dependency conjecture_shape axiom_names name =
   5.584 -  if is_axiom axiom_names name then
   5.585 -    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   5.586 -  else
   5.587 -    apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   5.588 -
   5.589 -fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   5.590 -  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   5.591 -    Assume (raw_label_for_name conjecture_shape name, t)
   5.592 -  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   5.593 -    Have (if j = 1 then [Show] else [],
   5.594 -          raw_label_for_name conjecture_shape name,
   5.595 -          fold_rev forall_of (map Var (Term.add_vars t [])) t,
   5.596 -          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   5.597 -                        deps ([], [])))
   5.598 -
   5.599 -fun repair_name "$true" = "c_True"
   5.600 -  | repair_name "$false" = "c_False"
   5.601 -  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   5.602 -  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   5.603 -  | repair_name s =
   5.604 -    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   5.605 -      "c_equal" (* seen in Vampire proofs *)
   5.606 -    else
   5.607 -      s
   5.608 -
   5.609 -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   5.610 -        tstplike_proof conjecture_shape axiom_names params frees =
   5.611 -  let
   5.612 -    val lines =
   5.613 -      tstplike_proof
   5.614 -      |> atp_proof_from_tstplike_string
   5.615 -      |> nasty_atp_proof pool
   5.616 -      |> map_term_names_in_atp_proof repair_name
   5.617 -      |> decode_lines ctxt full_types tfrees
   5.618 -      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   5.619 -      |> rpair [] |-> fold_rev add_nontrivial_line
   5.620 -      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   5.621 -                                             conjecture_shape axiom_names frees)
   5.622 -      |> snd
   5.623 -  in
   5.624 -    (if null params then [] else [Fix params]) @
   5.625 -    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   5.626 -         lines
   5.627 -  end
   5.628 -
   5.629 -(* When redirecting proofs, we keep information about the labels seen so far in
   5.630 -   the "backpatches" data structure. The first component indicates which facts
   5.631 -   should be associated with forthcoming proof steps. The second component is a
   5.632 -   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   5.633 -   become assumptions and "drop_ls" are the labels that should be dropped in a
   5.634 -   case split. *)
   5.635 -type backpatches = (label * facts) list * (label list * label list)
   5.636 -
   5.637 -fun used_labels_of_step (Have (_, _, _, by)) =
   5.638 -    (case by of
   5.639 -       ByMetis (ls, _) => ls
   5.640 -     | CaseSplit (proofs, (ls, _)) =>
   5.641 -       fold (union (op =) o used_labels_of) proofs ls)
   5.642 -  | used_labels_of_step _ = []
   5.643 -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   5.644 -
   5.645 -fun new_labels_of_step (Fix _) = []
   5.646 -  | new_labels_of_step (Let _) = []
   5.647 -  | new_labels_of_step (Assume (l, _)) = [l]
   5.648 -  | new_labels_of_step (Have (_, l, _, _)) = [l]
   5.649 -val new_labels_of = maps new_labels_of_step
   5.650 -
   5.651 -val join_proofs =
   5.652 -  let
   5.653 -    fun aux _ [] = NONE
   5.654 -      | aux proof_tail (proofs as (proof1 :: _)) =
   5.655 -        if exists null proofs then
   5.656 -          NONE
   5.657 -        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   5.658 -          aux (hd proof1 :: proof_tail) (map tl proofs)
   5.659 -        else case hd proof1 of
   5.660 -          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   5.661 -          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   5.662 -                      | _ => false) (tl proofs) andalso
   5.663 -             not (exists (member (op =) (maps new_labels_of proofs))
   5.664 -                         (used_labels_of proof_tail)) then
   5.665 -            SOME (l, t, map rev proofs, proof_tail)
   5.666 -          else
   5.667 -            NONE
   5.668 -        | _ => NONE
   5.669 -  in aux [] o map rev end
   5.670 -
   5.671 -fun case_split_qualifiers proofs =
   5.672 -  case length proofs of
   5.673 -    0 => []
   5.674 -  | 1 => [Then]
   5.675 -  | _ => [Ultimately]
   5.676 -
   5.677 -fun redirect_proof hyp_ts concl_t proof =
   5.678 -  let
   5.679 -    (* The first pass outputs those steps that are independent of the negated
   5.680 -       conjecture. The second pass flips the proof by contradiction to obtain a
   5.681 -       direct proof, introducing case splits when an inference depends on
   5.682 -       several facts that depend on the negated conjecture. *)
   5.683 -     val concl_l = (conjecture_prefix, length hyp_ts)
   5.684 -     fun first_pass ([], contra) = ([], contra)
   5.685 -       | first_pass ((step as Fix _) :: proof, contra) =
   5.686 -         first_pass (proof, contra) |>> cons step
   5.687 -       | first_pass ((step as Let _) :: proof, contra) =
   5.688 -         first_pass (proof, contra) |>> cons step
   5.689 -       | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   5.690 -         if l = concl_l then first_pass (proof, contra ||> cons step)
   5.691 -         else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   5.692 -       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   5.693 -         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   5.694 -           if exists (member (op =) (fst contra)) ls then
   5.695 -             first_pass (proof, contra |>> cons l ||> cons step)
   5.696 -           else
   5.697 -             first_pass (proof, contra) |>> cons step
   5.698 -         end
   5.699 -       | first_pass _ = raise Fail "malformed proof"
   5.700 -    val (proof_top, (contra_ls, contra_proof)) =
   5.701 -      first_pass (proof, ([concl_l], []))
   5.702 -    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   5.703 -    fun backpatch_labels patches ls =
   5.704 -      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   5.705 -    fun second_pass end_qs ([], assums, patches) =
   5.706 -        ([Have (end_qs, no_label, concl_t,
   5.707 -                ByMetis (backpatch_labels patches (map snd assums)))], patches)
   5.708 -      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   5.709 -        second_pass end_qs (proof, (t, l) :: assums, patches)
   5.710 -      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   5.711 -                            patches) =
   5.712 -        (if member (op =) (snd (snd patches)) l andalso
   5.713 -            not (member (op =) (fst (snd patches)) l) andalso
   5.714 -            not (AList.defined (op =) (fst patches) l) then
   5.715 -           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   5.716 -         else case List.partition (member (op =) contra_ls) ls of
   5.717 -           ([contra_l], co_ls) =>
   5.718 -           if member (op =) qs Show then
   5.719 -             second_pass end_qs (proof, assums,
   5.720 -                                 patches |>> cons (contra_l, (co_ls, ss)))
   5.721 -           else
   5.722 -             second_pass end_qs
   5.723 -                         (proof, assums,
   5.724 -                          patches |>> cons (contra_l, (l :: co_ls, ss)))
   5.725 -             |>> cons (if member (op =) (fst (snd patches)) l then
   5.726 -                         Assume (l, negate_term t)
   5.727 -                       else
   5.728 -                         Have (qs, l, negate_term t,
   5.729 -                               ByMetis (backpatch_label patches l)))
   5.730 -         | (contra_ls as _ :: _, co_ls) =>
   5.731 -           let
   5.732 -             val proofs =
   5.733 -               map_filter
   5.734 -                   (fn l =>
   5.735 -                       if l = concl_l then
   5.736 -                         NONE
   5.737 -                       else
   5.738 -                         let
   5.739 -                           val drop_ls = filter (curry (op <>) l) contra_ls
   5.740 -                         in
   5.741 -                           second_pass []
   5.742 -                               (proof, assums,
   5.743 -                                patches ||> apfst (insert (op =) l)
   5.744 -                                        ||> apsnd (union (op =) drop_ls))
   5.745 -                           |> fst |> SOME
   5.746 -                         end) contra_ls
   5.747 -             val (assumes, facts) =
   5.748 -               if member (op =) (fst (snd patches)) l then
   5.749 -                 ([Assume (l, negate_term t)], (l :: co_ls, ss))
   5.750 -               else
   5.751 -                 ([], (co_ls, ss))
   5.752 -           in
   5.753 -             (case join_proofs proofs of
   5.754 -                SOME (l, t, proofs, proof_tail) =>
   5.755 -                Have (case_split_qualifiers proofs @
   5.756 -                      (if null proof_tail then end_qs else []), l, t,
   5.757 -                      smart_case_split proofs facts) :: proof_tail
   5.758 -              | NONE =>
   5.759 -                [Have (case_split_qualifiers proofs @ end_qs, no_label,
   5.760 -                       concl_t, smart_case_split proofs facts)],
   5.761 -              patches)
   5.762 -             |>> append assumes
   5.763 -           end
   5.764 -         | _ => raise Fail "malformed proof")
   5.765 -       | second_pass _ _ = raise Fail "malformed proof"
   5.766 -    val proof_bottom =
   5.767 -      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   5.768 -  in proof_top @ proof_bottom end
   5.769 -
   5.770 -(* FIXME: Still needed? Probably not. *)
   5.771 -val kill_duplicate_assumptions_in_proof =
   5.772 -  let
   5.773 -    fun relabel_facts subst =
   5.774 -      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   5.775 -    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   5.776 -        (case AList.lookup (op aconv) assums t of
   5.777 -           SOME l' => (proof, (l, l') :: subst, assums)
   5.778 -         | NONE => (step :: proof, subst, (t, l) :: assums))
   5.779 -      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   5.780 -        (Have (qs, l, t,
   5.781 -               case by of
   5.782 -                 ByMetis facts => ByMetis (relabel_facts subst facts)
   5.783 -               | CaseSplit (proofs, facts) =>
   5.784 -                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   5.785 -         proof, subst, assums)
   5.786 -      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   5.787 -    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   5.788 -  in do_proof end
   5.789 -
   5.790 -val then_chain_proof =
   5.791 -  let
   5.792 -    fun aux _ [] = []
   5.793 -      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   5.794 -      | aux l' (Have (qs, l, t, by) :: proof) =
   5.795 -        (case by of
   5.796 -           ByMetis (ls, ss) =>
   5.797 -           Have (if member (op =) ls l' then
   5.798 -                   (Then :: qs, l, t,
   5.799 -                    ByMetis (filter_out (curry (op =) l') ls, ss))
   5.800 -                 else
   5.801 -                   (qs, l, t, ByMetis (ls, ss)))
   5.802 -         | CaseSplit (proofs, facts) =>
   5.803 -           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   5.804 -        aux l proof
   5.805 -      | aux _ (step :: proof) = step :: aux no_label proof
   5.806 -  in aux no_label end
   5.807 -
   5.808 -fun kill_useless_labels_in_proof proof =
   5.809 -  let
   5.810 -    val used_ls = used_labels_of proof
   5.811 -    fun do_label l = if member (op =) used_ls l then l else no_label
   5.812 -    fun do_step (Assume (l, t)) = Assume (do_label l, t)
   5.813 -      | do_step (Have (qs, l, t, by)) =
   5.814 -        Have (qs, do_label l, t,
   5.815 -              case by of
   5.816 -                CaseSplit (proofs, facts) =>
   5.817 -                CaseSplit (map (map do_step) proofs, facts)
   5.818 -              | _ => by)
   5.819 -      | do_step step = step
   5.820 -  in map do_step proof end
   5.821 -
   5.822 -fun prefix_for_depth n = replicate_string (n + 1)
   5.823 -
   5.824 -val relabel_proof =
   5.825 -  let
   5.826 -    fun aux _ _ _ [] = []
   5.827 -      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   5.828 -        if l = no_label then
   5.829 -          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   5.830 -        else
   5.831 -          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   5.832 -            Assume (l', t) ::
   5.833 -            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   5.834 -          end
   5.835 -      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   5.836 -        let
   5.837 -          val (l', subst, next_fact) =
   5.838 -            if l = no_label then
   5.839 -              (l, subst, next_fact)
   5.840 -            else
   5.841 -              let
   5.842 -                val l' = (prefix_for_depth depth fact_prefix, next_fact)
   5.843 -              in (l', (l, l') :: subst, next_fact + 1) end
   5.844 -          val relabel_facts =
   5.845 -            apfst (maps (the_list o AList.lookup (op =) subst))
   5.846 -          val by =
   5.847 -            case by of
   5.848 -              ByMetis facts => ByMetis (relabel_facts facts)
   5.849 -            | CaseSplit (proofs, facts) =>
   5.850 -              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   5.851 -                         relabel_facts facts)
   5.852 -        in
   5.853 -          Have (qs, l', t, by) ::
   5.854 -          aux subst depth (next_assum, next_fact) proof
   5.855 -        end
   5.856 -      | aux subst depth nextp (step :: proof) =
   5.857 -        step :: aux subst depth nextp proof
   5.858 -  in aux [] 0 (1, 1) end
   5.859 -
   5.860 -fun string_for_proof ctxt0 full_types i n =
   5.861 -  let
   5.862 -    val ctxt = ctxt0
   5.863 -      |> Config.put show_free_types false
   5.864 -      |> Config.put show_types true
   5.865 -    fun fix_print_mode f x =
   5.866 -      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   5.867 -                               (print_mode_value ())) f x
   5.868 -    fun do_indent ind = replicate_string (ind * indent_size) " "
   5.869 -    fun do_free (s, T) =
   5.870 -      maybe_quote s ^ " :: " ^
   5.871 -      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   5.872 -    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   5.873 -    fun do_have qs =
   5.874 -      (if member (op =) qs Moreover then "moreover " else "") ^
   5.875 -      (if member (op =) qs Ultimately then "ultimately " else "") ^
   5.876 -      (if member (op =) qs Then then
   5.877 -         if member (op =) qs Show then "thus" else "hence"
   5.878 -       else
   5.879 -         if member (op =) qs Show then "show" else "have")
   5.880 -    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   5.881 -    fun do_facts (ls, ss) =
   5.882 -      metis_command full_types 1 1
   5.883 -                    (ls |> sort_distinct (prod_ord string_ord int_ord),
   5.884 -                     ss |> sort_distinct string_ord)
   5.885 -    and do_step ind (Fix xs) =
   5.886 -        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   5.887 -      | do_step ind (Let (t1, t2)) =
   5.888 -        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   5.889 -      | do_step ind (Assume (l, t)) =
   5.890 -        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   5.891 -      | do_step ind (Have (qs, l, t, ByMetis facts)) =
   5.892 -        do_indent ind ^ do_have qs ^ " " ^
   5.893 -        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   5.894 -      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   5.895 -        space_implode (do_indent ind ^ "moreover\n")
   5.896 -                      (map (do_block ind) proofs) ^
   5.897 -        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   5.898 -        do_facts facts ^ "\n"
   5.899 -    and do_steps prefix suffix ind steps =
   5.900 -      let val s = implode (map (do_step ind) steps) in
   5.901 -        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   5.902 -        String.extract (s, ind * indent_size,
   5.903 -                        SOME (size s - ind * indent_size - 1)) ^
   5.904 -        suffix ^ "\n"
   5.905 -      end
   5.906 -    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   5.907 -    (* One-step proofs are pointless; better use the Metis one-liner
   5.908 -       directly. *)
   5.909 -    and do_proof [Have (_, _, _, ByMetis _)] = ""
   5.910 -      | do_proof proof =
   5.911 -        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   5.912 -        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   5.913 -        (if n <> 1 then "next" else "qed")
   5.914 -  in do_proof end
   5.915 -
   5.916 -fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   5.917 -                    (other_params as (_, full_types, _, tstplike_proof,
   5.918 -                                      axiom_names, goal, i)) =
   5.919 -  let
   5.920 -    val (params, hyp_ts, concl_t) = strip_subgoal goal i
   5.921 -    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   5.922 -    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   5.923 -    val n = Logic.count_prems (prop_of goal)
   5.924 -    val (one_line_proof, lemma_names) = metis_proof_text other_params
   5.925 -    fun isar_proof_for () =
   5.926 -      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   5.927 -               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   5.928 -               params frees
   5.929 -           |> redirect_proof hyp_ts concl_t
   5.930 -           |> kill_duplicate_assumptions_in_proof
   5.931 -           |> then_chain_proof
   5.932 -           |> kill_useless_labels_in_proof
   5.933 -           |> relabel_proof
   5.934 -           |> string_for_proof ctxt full_types i n of
   5.935 -        "" => "\nNo structured proof available."
   5.936 -      | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   5.937 -    val isar_proof =
   5.938 -      if debug then
   5.939 -        isar_proof_for ()
   5.940 -      else
   5.941 -        try isar_proof_for ()
   5.942 -        |> the_default "\nWarning: The Isar proof construction failed."
   5.943 -  in (one_line_proof ^ isar_proof, lemma_names) end
   5.944 -
   5.945 -fun proof_text isar_proof isar_params other_params =
   5.946 -  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   5.947 -      other_params
   5.948 -
   5.949 -end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Oct 22 13:49:44 2010 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,533 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     6.5 -    Author:     Fabian Immler, TU Muenchen
     6.6 -    Author:     Makarius
     6.7 -    Author:     Jasmin Blanchette, TU Muenchen
     6.8 -
     6.9 -Translation of HOL to FOL for Sledgehammer.
    6.10 -*)
    6.11 -
    6.12 -signature SLEDGEHAMMER_TRANSLATE =
    6.13 -sig
    6.14 -  type 'a problem = 'a ATP_Problem.problem
    6.15 -  type fol_formula
    6.16 -
    6.17 -  val axiom_prefix : string
    6.18 -  val conjecture_prefix : string
    6.19 -  val prepare_axiom :
    6.20 -    Proof.context -> (string * 'a) * thm
    6.21 -    -> term * ((string * 'a) * fol_formula) option
    6.22 -  val prepare_atp_problem :
    6.23 -    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    6.24 -    -> (term * ((string * 'a) * fol_formula) option) list
    6.25 -    -> string problem * string Symtab.table * int * (string * 'a) list vector
    6.26 -end;
    6.27 -
    6.28 -structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    6.29 -struct
    6.30 -
    6.31 -open ATP_Problem
    6.32 -open Metis_Translate
    6.33 -open Sledgehammer_Util
    6.34 -
    6.35 -val axiom_prefix = "ax_"
    6.36 -val conjecture_prefix = "conj_"
    6.37 -val helper_prefix = "help_"
    6.38 -val class_rel_clause_prefix = "clrel_";
    6.39 -val arity_clause_prefix = "arity_"
    6.40 -val tfree_prefix = "tfree_"
    6.41 -
    6.42 -(* Freshness almost guaranteed! *)
    6.43 -val sledgehammer_weak_prefix = "Sledgehammer:"
    6.44 -
    6.45 -type fol_formula =
    6.46 -  {name: string,
    6.47 -   kind: kind,
    6.48 -   combformula: (name, combterm) formula,
    6.49 -   ctypes_sorts: typ list}
    6.50 -
    6.51 -fun mk_anot phi = AConn (ANot, [phi])
    6.52 -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    6.53 -fun mk_ahorn [] phi = phi
    6.54 -  | mk_ahorn (phi :: phis) psi =
    6.55 -    AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    6.56 -
    6.57 -fun combformula_for_prop thy =
    6.58 -  let
    6.59 -    val do_term = combterm_from_term thy ~1
    6.60 -    fun do_quant bs q s T t' =
    6.61 -      let val s = Name.variant (map fst bs) s in
    6.62 -        do_formula ((s, T) :: bs) t'
    6.63 -        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    6.64 -      end
    6.65 -    and do_conn bs c t1 t2 =
    6.66 -      do_formula bs t1 ##>> do_formula bs t2
    6.67 -      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    6.68 -    and do_formula bs t =
    6.69 -      case t of
    6.70 -        @{const Not} $ t1 =>
    6.71 -        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    6.72 -      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    6.73 -        do_quant bs AForall s T t'
    6.74 -      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    6.75 -        do_quant bs AExists s T t'
    6.76 -      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
    6.77 -      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
    6.78 -      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
    6.79 -      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    6.80 -        do_conn bs AIff t1 t2
    6.81 -      | _ => (fn ts => do_term bs (Envir.eta_contract t)
    6.82 -                       |>> AAtom ||> union (op =) ts)
    6.83 -  in do_formula [] end
    6.84 -
    6.85 -val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
    6.86 -
    6.87 -fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    6.88 -fun conceal_bounds Ts t =
    6.89 -  subst_bounds (map (Free o apfst concealed_bound_name)
    6.90 -                    (0 upto length Ts - 1 ~~ Ts), t)
    6.91 -fun reveal_bounds Ts =
    6.92 -  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
    6.93 -                    (0 upto length Ts - 1 ~~ Ts))
    6.94 -
    6.95 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
    6.96 -   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
    6.97 -fun extensionalize_term t =
    6.98 -  let
    6.99 -    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
   6.100 -      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
   6.101 -                                        Type (_, [_, res_T])]))
   6.102 -                    $ t2 $ Abs (var_s, var_T, t')) =
   6.103 -        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
   6.104 -          let val var_t = Var ((var_s, j), var_T) in
   6.105 -            Const (s, T' --> T' --> res_T)
   6.106 -              $ betapply (t2, var_t) $ subst_bound (var_t, t')
   6.107 -            |> aux (j + 1)
   6.108 -          end
   6.109 -        else
   6.110 -          t
   6.111 -      | aux _ t = t
   6.112 -  in aux (maxidx_of_term t + 1) t end
   6.113 -
   6.114 -fun introduce_combinators_in_term ctxt kind t =
   6.115 -  let val thy = ProofContext.theory_of ctxt in
   6.116 -    if Meson.is_fol_term thy t then
   6.117 -      t
   6.118 -    else
   6.119 -      let
   6.120 -        fun aux Ts t =
   6.121 -          case t of
   6.122 -            @{const Not} $ t1 => @{const Not} $ aux Ts t1
   6.123 -          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   6.124 -            t0 $ Abs (s, T, aux (T :: Ts) t')
   6.125 -          | (t0 as Const (@{const_name All}, _)) $ t1 =>
   6.126 -            aux Ts (t0 $ eta_expand Ts t1 1)
   6.127 -          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   6.128 -            t0 $ Abs (s, T, aux (T :: Ts) t')
   6.129 -          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   6.130 -            aux Ts (t0 $ eta_expand Ts t1 1)
   6.131 -          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.132 -          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.133 -          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   6.134 -          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   6.135 -              $ t1 $ t2 =>
   6.136 -            t0 $ aux Ts t1 $ aux Ts t2
   6.137 -          | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   6.138 -                   t
   6.139 -                 else
   6.140 -                   t |> conceal_bounds Ts
   6.141 -                     |> Envir.eta_contract
   6.142 -                     |> cterm_of thy
   6.143 -                     |> Meson_Clausify.introduce_combinators_in_cterm
   6.144 -                     |> prop_of |> Logic.dest_equals |> snd
   6.145 -                     |> reveal_bounds Ts
   6.146 -        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   6.147 -      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   6.148 -      handle THM _ =>
   6.149 -             (* A type variable of sort "{}" will make abstraction fail. *)
   6.150 -             if kind = Conjecture then HOLogic.false_const
   6.151 -             else HOLogic.true_const
   6.152 -  end
   6.153 -
   6.154 -(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   6.155 -   same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   6.156 -fun freeze_term t =
   6.157 -  let
   6.158 -    fun aux (t $ u) = aux t $ aux u
   6.159 -      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   6.160 -      | aux (Var ((s, i), T)) =
   6.161 -        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   6.162 -      | aux t = t
   6.163 -  in t |> exists_subterm is_Var t ? aux end
   6.164 -
   6.165 -(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
   6.166 -    it leaves metaequalities over "prop"s alone. *)
   6.167 -val atomize_term =
   6.168 -  let
   6.169 -    fun aux (@{const Trueprop} $ t1) = t1
   6.170 -      | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
   6.171 -        HOLogic.all_const T $ Abs (s, T, aux t')
   6.172 -      | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
   6.173 -      | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
   6.174 -        HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
   6.175 -      | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   6.176 -        HOLogic.eq_const T $ t1 $ t2
   6.177 -      | aux _ = raise Fail "aux"
   6.178 -  in perhaps (try aux) end
   6.179 -
   6.180 -(* making axiom and conjecture formulas *)
   6.181 -fun make_formula ctxt presimp name kind t =
   6.182 -  let
   6.183 -    val thy = ProofContext.theory_of ctxt
   6.184 -    val t = t |> Envir.beta_eta_contract
   6.185 -              |> transform_elim_term
   6.186 -              |> atomize_term
   6.187 -    val need_trueprop = (fastype_of t = HOLogic.boolT)
   6.188 -    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   6.189 -              |> extensionalize_term
   6.190 -              |> presimp ? presimplify_term thy
   6.191 -              |> perhaps (try (HOLogic.dest_Trueprop))
   6.192 -              |> introduce_combinators_in_term ctxt kind
   6.193 -              |> kind <> Axiom ? freeze_term
   6.194 -    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   6.195 -  in
   6.196 -    {name = name, combformula = combformula, kind = kind,
   6.197 -     ctypes_sorts = ctypes_sorts}
   6.198 -  end
   6.199 -
   6.200 -fun make_axiom ctxt presimp ((name, loc), th) =
   6.201 -  case make_formula ctxt presimp name Axiom (prop_of th) of
   6.202 -    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   6.203 -  | formula => SOME ((name, loc), formula)
   6.204 -fun make_conjecture ctxt ts =
   6.205 -  let val last = length ts - 1 in
   6.206 -    map2 (fn j => make_formula ctxt true (Int.toString j)
   6.207 -                               (if j = last then Conjecture else Hypothesis))
   6.208 -         (0 upto last) ts
   6.209 -  end
   6.210 -
   6.211 -(** Helper facts **)
   6.212 -
   6.213 -fun count_combterm (CombConst ((s, _), _, _)) =
   6.214 -    Symtab.map_entry s (Integer.add 1)
   6.215 -  | count_combterm (CombVar _) = I
   6.216 -  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   6.217 -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   6.218 -  | count_combformula (AConn (_, phis)) = fold count_combformula phis
   6.219 -  | count_combformula (AAtom tm) = count_combterm tm
   6.220 -fun count_fol_formula ({combformula, ...} : fol_formula) =
   6.221 -  count_combformula combformula
   6.222 -
   6.223 -val optional_helpers =
   6.224 -  [(["c_COMBI"], @{thms Meson.COMBI_def}),
   6.225 -   (["c_COMBK"], @{thms Meson.COMBK_def}),
   6.226 -   (["c_COMBB"], @{thms Meson.COMBB_def}),
   6.227 -   (["c_COMBC"], @{thms Meson.COMBC_def}),
   6.228 -   (["c_COMBS"], @{thms Meson.COMBS_def})]
   6.229 -val optional_typed_helpers =
   6.230 -  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
   6.231 -   (["c_If"], @{thms if_True if_False})]
   6.232 -val mandatory_helpers = @{thms Metis.fequal_def}
   6.233 -
   6.234 -val init_counters =
   6.235 -  [optional_helpers, optional_typed_helpers] |> maps (maps fst)
   6.236 -  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
   6.237 -
   6.238 -fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   6.239 -  let
   6.240 -    val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
   6.241 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   6.242 -    fun baptize th = ((Thm.get_name_hint th, false), th)
   6.243 -  in
   6.244 -    (optional_helpers
   6.245 -     |> full_types ? append optional_typed_helpers
   6.246 -     |> maps (fn (ss, ths) =>
   6.247 -                 if exists is_needed ss then map baptize ths else [])) @
   6.248 -    (if is_FO then [] else map baptize mandatory_helpers)
   6.249 -    |> map_filter (Option.map snd o make_axiom ctxt false)
   6.250 -  end
   6.251 -
   6.252 -fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
   6.253 -
   6.254 -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   6.255 -  let
   6.256 -    val thy = ProofContext.theory_of ctxt
   6.257 -    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
   6.258 -    (* Remove existing axioms from the conjecture, as this can dramatically
   6.259 -       boost an ATP's performance (for some reason). *)
   6.260 -    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
   6.261 -    val goal_t = Logic.list_implies (hyp_ts, concl_t)
   6.262 -    val is_FO = Meson.is_fol_term thy goal_t
   6.263 -    val subs = tfree_classes_of_terms [goal_t]
   6.264 -    val supers = tvar_classes_of_terms axiom_ts
   6.265 -    val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   6.266 -    (* TFrees in the conjecture; TVars in the axioms *)
   6.267 -    val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   6.268 -    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
   6.269 -    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   6.270 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   6.271 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   6.272 -  in
   6.273 -    (axiom_names |> map single |> Vector.fromList,
   6.274 -     (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   6.275 -  end
   6.276 -
   6.277 -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   6.278 -
   6.279 -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   6.280 -  | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   6.281 -  | fo_term_for_combtyp (CombType (name, tys)) =
   6.282 -    ATerm (name, map fo_term_for_combtyp tys)
   6.283 -
   6.284 -fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   6.285 -    (true, ATerm (class, [ATerm (name, [])]))
   6.286 -  | fo_literal_for_type_literal (TyLitFree (class, name)) =
   6.287 -    (true, ATerm (class, [ATerm (name, [])]))
   6.288 -
   6.289 -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   6.290 -
   6.291 -fun fo_term_for_combterm full_types =
   6.292 -  let
   6.293 -    fun aux top_level u =
   6.294 -      let
   6.295 -        val (head, args) = strip_combterm_comb u
   6.296 -        val (x, ty_args) =
   6.297 -          case head of
   6.298 -            CombConst (name as (s, s'), _, ty_args) =>
   6.299 -            let val ty_args = if full_types then [] else ty_args in
   6.300 -              if s = "equal" then
   6.301 -                if top_level andalso length args = 2 then (name, [])
   6.302 -                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
   6.303 -              else if top_level then
   6.304 -                case s of
   6.305 -                  "c_False" => (("$false", s'), [])
   6.306 -                | "c_True" => (("$true", s'), [])
   6.307 -                | _ => (name, ty_args)
   6.308 -              else
   6.309 -                (name, ty_args)
   6.310 -            end
   6.311 -          | CombVar (name, _) => (name, [])
   6.312 -          | CombApp _ => raise Fail "impossible \"CombApp\""
   6.313 -        val t = ATerm (x, map fo_term_for_combtyp ty_args @
   6.314 -                          map (aux false) args)
   6.315 -    in
   6.316 -      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   6.317 -    end
   6.318 -  in aux true end
   6.319 -
   6.320 -fun formula_for_combformula full_types =
   6.321 -  let
   6.322 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   6.323 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   6.324 -      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   6.325 -  in aux end
   6.326 -
   6.327 -fun formula_for_axiom full_types
   6.328 -                      ({combformula, ctypes_sorts, ...} : fol_formula) =
   6.329 -  mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   6.330 -                (type_literals_for_types ctypes_sorts))
   6.331 -           (formula_for_combformula full_types combformula)
   6.332 -
   6.333 -fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   6.334 -  Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   6.335 -
   6.336 -fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   6.337 -                                                       superclass, ...}) =
   6.338 -  let val ty_arg = ATerm (("T", "T"), []) in
   6.339 -    Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   6.340 -         AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   6.341 -                           AAtom (ATerm (superclass, [ty_arg]))]))
   6.342 -  end
   6.343 -
   6.344 -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   6.345 -    (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   6.346 -  | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   6.347 -    (false, ATerm (c, [ATerm (sort, [])]))
   6.348 -
   6.349 -fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   6.350 -                                                ...}) =
   6.351 -  Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   6.352 -       mk_ahorn (map (formula_for_fo_literal o apfst not
   6.353 -                      o fo_literal_for_arity_literal) premLits)
   6.354 -                (formula_for_fo_literal
   6.355 -                     (fo_literal_for_arity_literal conclLit)))
   6.356 -
   6.357 -fun problem_line_for_conjecture full_types
   6.358 -                                ({name, kind, combformula, ...} : fol_formula) =
   6.359 -  Fof (conjecture_prefix ^ name, kind,
   6.360 -       formula_for_combformula full_types combformula)
   6.361 -
   6.362 -fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
   6.363 -  map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   6.364 -
   6.365 -fun problem_line_for_free_type j lit =
   6.366 -  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
   6.367 -fun problem_lines_for_free_types conjectures =
   6.368 -  let
   6.369 -    val litss = map free_type_literals_for_conjecture conjectures
   6.370 -    val lits = fold (union (op =)) litss []
   6.371 -  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
   6.372 -
   6.373 -(** "hBOOL" and "hAPP" **)
   6.374 -
   6.375 -type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   6.376 -
   6.377 -fun consider_term top_level (ATerm ((s, _), ts)) =
   6.378 -  (if is_atp_variable s then
   6.379 -     I
   6.380 -   else
   6.381 -     let val n = length ts in
   6.382 -       Symtab.map_default
   6.383 -           (s, {min_arity = n, max_arity = 0, sub_level = false})
   6.384 -           (fn {min_arity, max_arity, sub_level} =>
   6.385 -               {min_arity = Int.min (n, min_arity),
   6.386 -                max_arity = Int.max (n, max_arity),
   6.387 -                sub_level = sub_level orelse not top_level})
   6.388 -     end)
   6.389 -  #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   6.390 -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   6.391 -  | consider_formula (AConn (_, phis)) = fold consider_formula phis
   6.392 -  | consider_formula (AAtom tm) = consider_term true tm
   6.393 -
   6.394 -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   6.395 -fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   6.396 -
   6.397 -fun const_table_for_problem explicit_apply problem =
   6.398 -  if explicit_apply then NONE
   6.399 -  else SOME (Symtab.empty |> consider_problem problem)
   6.400 -
   6.401 -fun min_arity_of thy full_types NONE s =
   6.402 -    (if s = "equal" orelse s = type_wrapper_name orelse
   6.403 -        String.isPrefix type_const_prefix s orelse
   6.404 -        String.isPrefix class_prefix s then
   6.405 -       16383 (* large number *)
   6.406 -     else if full_types then
   6.407 -       0
   6.408 -     else case strip_prefix_and_unascii const_prefix s of
   6.409 -       SOME s' => num_type_args thy (invert_const s')
   6.410 -     | NONE => 0)
   6.411 -  | min_arity_of _ _ (SOME the_const_tab) s =
   6.412 -    case Symtab.lookup the_const_tab s of
   6.413 -      SOME ({min_arity, ...} : const_info) => min_arity
   6.414 -    | NONE => 0
   6.415 -
   6.416 -fun full_type_of (ATerm ((s, _), [ty, _])) =
   6.417 -    if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   6.418 -  | full_type_of _ = raise Fail "expected type wrapper"
   6.419 -
   6.420 -fun list_hAPP_rev _ t1 [] = t1
   6.421 -  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   6.422 -    ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   6.423 -  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   6.424 -    let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   6.425 -                         [full_type_of t2, ty]) in
   6.426 -      ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   6.427 -    end
   6.428 -
   6.429 -fun repair_applications_in_term thy full_types const_tab =
   6.430 -  let
   6.431 -    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   6.432 -      if s = type_wrapper_name then
   6.433 -        case ts of
   6.434 -          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   6.435 -        | _ => raise Fail "malformed type wrapper"
   6.436 -      else
   6.437 -        let
   6.438 -          val ts = map (aux NONE) ts
   6.439 -          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   6.440 -        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   6.441 -  in aux NONE end
   6.442 -
   6.443 -fun boolify t = ATerm (`I "hBOOL", [t])
   6.444 -
   6.445 -(* True if the constant ever appears outside of the top-level position in
   6.446 -   literals, or if it appears with different arities (e.g., because of different
   6.447 -   type instantiations). If false, the constant always receives all of its
   6.448 -   arguments and is used as a predicate. *)
   6.449 -fun is_predicate NONE s =
   6.450 -    s = "equal" orelse s = "$false" orelse s = "$true" orelse
   6.451 -    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   6.452 -  | is_predicate (SOME the_const_tab) s =
   6.453 -    case Symtab.lookup the_const_tab s of
   6.454 -      SOME {min_arity, max_arity, sub_level} =>
   6.455 -      not sub_level andalso min_arity = max_arity
   6.456 -    | NONE => false
   6.457 -
   6.458 -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   6.459 -  if s = type_wrapper_name then
   6.460 -    case ts of
   6.461 -      [_, t' as ATerm ((s', _), _)] =>
   6.462 -      if is_predicate const_tab s' then t' else boolify t
   6.463 -    | _ => raise Fail "malformed type wrapper"
   6.464 -  else
   6.465 -    t |> not (is_predicate const_tab s) ? boolify
   6.466 -
   6.467 -fun close_universally phi =
   6.468 -  let
   6.469 -    fun term_vars bounds (ATerm (name as (s, _), tms)) =
   6.470 -        (is_atp_variable s andalso not (member (op =) bounds name))
   6.471 -          ? insert (op =) name
   6.472 -        #> fold (term_vars bounds) tms
   6.473 -    fun formula_vars bounds (AQuant (_, xs, phi)) =
   6.474 -        formula_vars (xs @ bounds) phi
   6.475 -      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   6.476 -      | formula_vars bounds (AAtom tm) = term_vars bounds tm
   6.477 -  in
   6.478 -    case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   6.479 -  end
   6.480 -
   6.481 -fun repair_formula thy explicit_forall full_types const_tab =
   6.482 -  let
   6.483 -    fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   6.484 -      | aux (AConn (c, phis)) = AConn (c, map aux phis)
   6.485 -      | aux (AAtom tm) =
   6.486 -        AAtom (tm |> repair_applications_in_term thy full_types const_tab
   6.487 -                  |> repair_predicates_in_term const_tab)
   6.488 -  in aux #> explicit_forall ? close_universally end
   6.489 -
   6.490 -fun repair_problem_line thy explicit_forall full_types const_tab
   6.491 -                        (Fof (ident, kind, phi)) =
   6.492 -  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   6.493 -fun repair_problem_with_const_table thy =
   6.494 -  map o apsnd o map ooo repair_problem_line thy
   6.495 -
   6.496 -fun repair_problem thy explicit_forall full_types explicit_apply problem =
   6.497 -  repair_problem_with_const_table thy explicit_forall full_types
   6.498 -      (const_table_for_problem explicit_apply problem) problem
   6.499 -
   6.500 -fun prepare_atp_problem ctxt readable_names explicit_forall full_types
   6.501 -                        explicit_apply hyp_ts concl_t axioms =
   6.502 -  let
   6.503 -    val thy = ProofContext.theory_of ctxt
   6.504 -    val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   6.505 -                       arity_clauses)) =
   6.506 -      prepare_formulas ctxt full_types hyp_ts concl_t axioms
   6.507 -    val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   6.508 -    val helper_lines =
   6.509 -      map (problem_line_for_fact helper_prefix full_types) helper_facts
   6.510 -    val conjecture_lines =
   6.511 -      map (problem_line_for_conjecture full_types) conjectures
   6.512 -    val tfree_lines = problem_lines_for_free_types conjectures
   6.513 -    val class_rel_lines =
   6.514 -      map problem_line_for_class_rel_clause class_rel_clauses
   6.515 -    val arity_lines = map problem_line_for_arity_clause arity_clauses
   6.516 -    (* Reordering these might or might not confuse the proof reconstruction
   6.517 -       code or the SPASS Flotter hack. *)
   6.518 -    val problem =
   6.519 -      [("Relevant facts", axiom_lines),
   6.520 -       ("Class relationships", class_rel_lines),
   6.521 -       ("Arity declarations", arity_lines),
   6.522 -       ("Helper facts", helper_lines),
   6.523 -       ("Conjectures", conjecture_lines),
   6.524 -       ("Type variables", tfree_lines)]
   6.525 -      |> repair_problem thy explicit_forall full_types explicit_apply
   6.526 -    val (problem, pool) = nice_atp_problem readable_names problem
   6.527 -    val conjecture_offset =
   6.528 -      length axiom_lines + length class_rel_lines + length arity_lines
   6.529 -      + length helper_lines
   6.530 -  in
   6.531 -    (problem,
   6.532 -     case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   6.533 -     conjecture_offset, axiom_names)
   6.534 -  end
   6.535 -
   6.536 -end;