src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 40067 0783415ed7f0
parent 40064 db8413d82c3b
child 40068 ed2869dd9bfa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:54:51 2010 +0200
     1.3 @@ -0,0 +1,946 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.5 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     1.6 +    Author:     Claire Quigley, Cambridge University Computer Laboratory
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +
     1.9 +Proof reconstruction for Sledgehammer.
    1.10 +*)
    1.11 +
    1.12 +signature SLEDGEHAMMER_RECONSTRUCT =
    1.13 +sig
    1.14 +  type locality = Sledgehammer_Filter.locality
    1.15 +  type minimize_command = string list -> string
    1.16 +  type metis_params =
    1.17 +    string * bool * minimize_command * string * (string * locality) list vector
    1.18 +    * thm * int
    1.19 +  type isar_params =
    1.20 +    string Symtab.table * bool * int * Proof.context * int list list
    1.21 +  type text_result = string * (string * locality) list
    1.22 +
    1.23 +  val repair_conjecture_shape_and_axiom_names :
    1.24 +    string -> int list list -> (string * locality) list vector
    1.25 +    -> int list list * (string * locality) list vector
    1.26 +  val apply_on_subgoal : int -> int -> string
    1.27 +  val command_call : string -> string list -> string
    1.28 +  val try_command_line : string -> string -> string
    1.29 +  val minimize_line : ('a list -> string) -> 'a list -> string
    1.30 +  val metis_proof_text : metis_params -> text_result
    1.31 +  val isar_proof_text : isar_params -> metis_params -> text_result
    1.32 +  val proof_text : bool -> isar_params -> metis_params -> text_result
    1.33 +end;
    1.34 +
    1.35 +structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    1.36 +struct
    1.37 +
    1.38 +open ATP_Problem
    1.39 +open ATP_Proof
    1.40 +open Metis_Translate
    1.41 +open Sledgehammer_Util
    1.42 +open Sledgehammer_Filter
    1.43 +open Sledgehammer_Translate
    1.44 +
    1.45 +type minimize_command = string list -> string
    1.46 +type metis_params =
    1.47 +  string * bool * minimize_command * string * (string * locality) list vector
    1.48 +  * thm * int
    1.49 +type isar_params =
    1.50 +  string Symtab.table * bool * int * Proof.context * int list list
    1.51 +type text_result = string * (string * locality) list
    1.52 +
    1.53 +fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    1.54 +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    1.55 +
    1.56 +fun find_first_in_list_vector vec key =
    1.57 +  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    1.58 +                 | (_, value) => value) NONE vec
    1.59 +
    1.60 +
    1.61 +(** SPASS's Flotter hack **)
    1.62 +
    1.63 +(* This is a hack required for keeping track of axioms after they have been
    1.64 +   clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    1.65 +   part of this hack. *)
    1.66 +
    1.67 +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    1.68 +
    1.69 +fun extract_clause_sequence output =
    1.70 +  let
    1.71 +    val tokens_of = String.tokens (not o Char.isAlphaNum)
    1.72 +    fun extract_num ("clause" :: (ss as _ :: _)) =
    1.73 +    Int.fromString (List.last ss)
    1.74 +      | extract_num _ = NONE
    1.75 +  in output |> split_lines |> map_filter (extract_num o tokens_of) end
    1.76 +
    1.77 +val parse_clause_formula_pair =
    1.78 +  $$ "(" |-- scan_integer --| $$ ","
    1.79 +  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
    1.80 +  --| Scan.option ($$ ",")
    1.81 +val parse_clause_formula_relation =
    1.82 +  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    1.83 +  |-- Scan.repeat parse_clause_formula_pair
    1.84 +val extract_clause_formula_relation =
    1.85 +  Substring.full #> Substring.position set_ClauseFormulaRelationN
    1.86 +  #> snd #> Substring.position "." #> fst #> Substring.string
    1.87 +  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    1.88 +  #> fst
    1.89 +
    1.90 +fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    1.91 +                                            axiom_names =
    1.92 +  if String.isSubstring set_ClauseFormulaRelationN output then
    1.93 +    let
    1.94 +      val j0 = hd (hd conjecture_shape)
    1.95 +      val seq = extract_clause_sequence output
    1.96 +      val name_map = extract_clause_formula_relation output
    1.97 +      fun renumber_conjecture j =
    1.98 +        conjecture_prefix ^ string_of_int (j - j0)
    1.99 +        |> AList.find (fn (s, ss) => member (op =) ss s) name_map
   1.100 +        |> map (fn s => find_index (curry (op =) s) seq + 1)
   1.101 +      fun names_for_number j =
   1.102 +        j |> AList.lookup (op =) name_map |> these
   1.103 +          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   1.104 +          |> map (fn name =>
   1.105 +                     (name, name |> find_first_in_list_vector axiom_names
   1.106 +                                 |> the)
   1.107 +                     handle Option.Option =>
   1.108 +                            error ("No such fact: " ^ quote name ^ "."))
   1.109 +    in
   1.110 +      (conjecture_shape |> map (maps renumber_conjecture),
   1.111 +       seq |> map names_for_number |> Vector.fromList)
   1.112 +    end
   1.113 +  else
   1.114 +    (conjecture_shape, axiom_names)
   1.115 +
   1.116 +
   1.117 +(** Soft-core proof reconstruction: Metis one-liner **)
   1.118 +
   1.119 +fun string_for_label (s, num) = s ^ string_of_int num
   1.120 +
   1.121 +fun apply_on_subgoal _ 1 = "by "
   1.122 +  | apply_on_subgoal 1 _ = "apply "
   1.123 +  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
   1.124 +fun command_call name [] = name
   1.125 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   1.126 +fun try_command_line banner command =
   1.127 +  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   1.128 +fun using_labels [] = ""
   1.129 +  | using_labels ls =
   1.130 +    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   1.131 +fun metis_name full_types = if full_types then "metisFT" else "metis"
   1.132 +fun metis_call full_types ss = command_call (metis_name full_types) ss
   1.133 +fun metis_command full_types i n (ls, ss) =
   1.134 +  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
   1.135 +fun metis_line banner full_types i n ss =
   1.136 +  try_command_line banner (metis_command full_types i n ([], ss))
   1.137 +fun minimize_line _ [] = ""
   1.138 +  | minimize_line minimize_command ss =
   1.139 +    case minimize_command ss of
   1.140 +      "" => ""
   1.141 +    | command =>
   1.142 +      "\nTo minimize the number of lemmas, try this: " ^
   1.143 +      Markup.markup Markup.sendback command ^ "."
   1.144 +
   1.145 +fun resolve_axiom axiom_names ((_, SOME s)) =
   1.146 +    (case strip_prefix_and_unascii axiom_prefix s of
   1.147 +       SOME s' => (case find_first_in_list_vector axiom_names s' of
   1.148 +                     SOME x => [(s', x)]
   1.149 +                   | NONE => [])
   1.150 +     | NONE => [])
   1.151 +  | resolve_axiom axiom_names (num, NONE) =
   1.152 +    case Int.fromString num of
   1.153 +      SOME j =>
   1.154 +      if j > 0 andalso j <= Vector.length axiom_names then
   1.155 +        Vector.sub (axiom_names, j - 1)
   1.156 +      else
   1.157 +        []
   1.158 +    | NONE => []
   1.159 +
   1.160 +fun add_fact axiom_names (Inference (name, _, [])) =
   1.161 +    append (resolve_axiom axiom_names name)
   1.162 +  | add_fact _ _ = I
   1.163 +
   1.164 +fun used_facts_in_tstplike_proof axiom_names =
   1.165 +  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
   1.166 +
   1.167 +fun used_facts axiom_names =
   1.168 +  used_facts_in_tstplike_proof axiom_names
   1.169 +  #> List.partition (curry (op =) Chained o snd)
   1.170 +  #> pairself (sort_distinct (string_ord o pairself fst))
   1.171 +
   1.172 +fun metis_proof_text (banner, full_types, minimize_command,
   1.173 +                      tstplike_proof, axiom_names, goal, i) =
   1.174 +  let
   1.175 +    val (chained_lemmas, other_lemmas) =
   1.176 +      used_facts axiom_names tstplike_proof
   1.177 +    val n = Logic.count_prems (prop_of goal)
   1.178 +  in
   1.179 +    (metis_line banner full_types i n (map fst other_lemmas) ^
   1.180 +     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   1.181 +     other_lemmas @ chained_lemmas)
   1.182 +  end
   1.183 +
   1.184 +
   1.185 +(** Hard-core proof reconstruction: structured Isar proofs **)
   1.186 +
   1.187 +(* Simple simplifications to ensure that sort annotations don't leave a trail of
   1.188 +   spurious "True"s. *)
   1.189 +fun s_not @{const False} = @{const True}
   1.190 +  | s_not @{const True} = @{const False}
   1.191 +  | s_not (@{const Not} $ t) = t
   1.192 +  | s_not t = @{const Not} $ t
   1.193 +fun s_conj (@{const True}, t2) = t2
   1.194 +  | s_conj (t1, @{const True}) = t1
   1.195 +  | s_conj p = HOLogic.mk_conj p
   1.196 +fun s_disj (@{const False}, t2) = t2
   1.197 +  | s_disj (t1, @{const False}) = t1
   1.198 +  | s_disj p = HOLogic.mk_disj p
   1.199 +fun s_imp (@{const True}, t2) = t2
   1.200 +  | s_imp (t1, @{const False}) = s_not t1
   1.201 +  | s_imp p = HOLogic.mk_imp p
   1.202 +fun s_iff (@{const True}, t2) = t2
   1.203 +  | s_iff (t1, @{const True}) = t1
   1.204 +  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   1.205 +
   1.206 +fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   1.207 +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   1.208 +
   1.209 +fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   1.210 +    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   1.211 +  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   1.212 +    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   1.213 +  | negate_term (@{const HOL.implies} $ t1 $ t2) =
   1.214 +    @{const HOL.conj} $ t1 $ negate_term t2
   1.215 +  | negate_term (@{const HOL.conj} $ t1 $ t2) =
   1.216 +    @{const HOL.disj} $ negate_term t1 $ negate_term t2
   1.217 +  | negate_term (@{const HOL.disj} $ t1 $ t2) =
   1.218 +    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   1.219 +  | negate_term (@{const Not} $ t) = t
   1.220 +  | negate_term t = @{const Not} $ t
   1.221 +
   1.222 +val indent_size = 2
   1.223 +val no_label = ("", ~1)
   1.224 +
   1.225 +val raw_prefix = "X"
   1.226 +val assum_prefix = "A"
   1.227 +val fact_prefix = "F"
   1.228 +
   1.229 +fun resolve_conjecture conjecture_shape (num, s_opt) =
   1.230 +  let
   1.231 +    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   1.232 +              SOME s => Int.fromString s |> the_default ~1
   1.233 +            | NONE => case Int.fromString num of
   1.234 +                        SOME j => find_index (exists (curry (op =) j))
   1.235 +                                             conjecture_shape
   1.236 +                      | NONE => ~1
   1.237 +  in if k >= 0 then [k] else [] end
   1.238 +
   1.239 +fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   1.240 +fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   1.241 +
   1.242 +fun raw_label_for_name conjecture_shape name =
   1.243 +  case resolve_conjecture conjecture_shape name of
   1.244 +    [j] => (conjecture_prefix, j)
   1.245 +  | _ => case Int.fromString (fst name) of
   1.246 +           SOME j => (raw_prefix, j)
   1.247 +         | NONE => (raw_prefix ^ fst name, 0)
   1.248 +
   1.249 +(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   1.250 +
   1.251 +exception FO_TERM of string fo_term list
   1.252 +exception FORMULA of (string, string fo_term) formula list
   1.253 +exception SAME of unit
   1.254 +
   1.255 +(* Type variables are given the basic sort "HOL.type". Some will later be
   1.256 +   constrained by information from type literals, or by type inference. *)
   1.257 +fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   1.258 +  let val Ts = map (type_from_fo_term tfrees) us in
   1.259 +    case strip_prefix_and_unascii type_const_prefix a of
   1.260 +      SOME b => Type (invert_const b, Ts)
   1.261 +    | NONE =>
   1.262 +      if not (null us) then
   1.263 +        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   1.264 +      else case strip_prefix_and_unascii tfree_prefix a of
   1.265 +        SOME b =>
   1.266 +        let val s = "'" ^ b in
   1.267 +          TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   1.268 +        end
   1.269 +      | NONE =>
   1.270 +        case strip_prefix_and_unascii tvar_prefix a of
   1.271 +          SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   1.272 +        | NONE =>
   1.273 +          (* Variable from the ATP, say "X1" *)
   1.274 +          Type_Infer.param 0 (a, HOLogic.typeS)
   1.275 +  end
   1.276 +
   1.277 +(* Type class literal applied to a type. Returns triple of polarity, class,
   1.278 +   type. *)
   1.279 +fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   1.280 +  case (strip_prefix_and_unascii class_prefix a,
   1.281 +        map (type_from_fo_term tfrees) us) of
   1.282 +    (SOME b, [T]) => (pos, b, T)
   1.283 +  | _ => raise FO_TERM [u]
   1.284 +
   1.285 +(** Accumulate type constraints in a formula: negative type literals **)
   1.286 +fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   1.287 +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   1.288 +  | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   1.289 +  | add_type_constraint _ = I
   1.290 +
   1.291 +fun repair_atp_variable_name f s =
   1.292 +  let
   1.293 +    fun subscript_name s n = s ^ nat_subscript n
   1.294 +    val s = String.map f s
   1.295 +  in
   1.296 +    case space_explode "_" s of
   1.297 +      [_] => (case take_suffix Char.isDigit (String.explode s) of
   1.298 +                (cs1 as _ :: _, cs2 as _ :: _) =>
   1.299 +                subscript_name (String.implode cs1)
   1.300 +                               (the (Int.fromString (String.implode cs2)))
   1.301 +              | (_, _) => s)
   1.302 +    | [s1, s2] => (case Int.fromString s2 of
   1.303 +                     SOME n => subscript_name s1 n
   1.304 +                   | NONE => s)
   1.305 +    | _ => s
   1.306 +  end
   1.307 +
   1.308 +(* First-order translation. No types are known for variables. "HOLogic.typeT"
   1.309 +   should allow them to be inferred. *)
   1.310 +fun raw_term_from_pred thy full_types tfrees =
   1.311 +  let
   1.312 +    fun aux opt_T extra_us u =
   1.313 +      case u of
   1.314 +        ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   1.315 +      | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   1.316 +      | ATerm (a, us) =>
   1.317 +        if a = type_wrapper_name then
   1.318 +          case us of
   1.319 +            [typ_u, term_u] =>
   1.320 +            aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   1.321 +          | _ => raise FO_TERM us
   1.322 +        else case strip_prefix_and_unascii const_prefix a of
   1.323 +          SOME "equal" =>
   1.324 +          let val ts = map (aux NONE []) us in
   1.325 +            if length ts = 2 andalso hd ts aconv List.last ts then
   1.326 +              (* Vampire is keen on producing these. *)
   1.327 +              @{const True}
   1.328 +            else
   1.329 +              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   1.330 +          end
   1.331 +        | SOME b =>
   1.332 +          let
   1.333 +            val c = invert_const b
   1.334 +            val num_type_args = num_type_args thy c
   1.335 +            val (type_us, term_us) =
   1.336 +              chop (if full_types then 0 else num_type_args) us
   1.337 +            (* Extra args from "hAPP" come after any arguments given directly to
   1.338 +               the constant. *)
   1.339 +            val term_ts = map (aux NONE []) term_us
   1.340 +            val extra_ts = map (aux NONE []) extra_us
   1.341 +            val t =
   1.342 +              Const (c, if full_types then
   1.343 +                          case opt_T of
   1.344 +                            SOME T => map fastype_of term_ts ---> T
   1.345 +                          | NONE =>
   1.346 +                            if num_type_args = 0 then
   1.347 +                              Sign.const_instance thy (c, [])
   1.348 +                            else
   1.349 +                              raise Fail ("no type information for " ^ quote c)
   1.350 +                        else
   1.351 +                          Sign.const_instance thy (c,
   1.352 +                              map (type_from_fo_term tfrees) type_us))
   1.353 +          in list_comb (t, term_ts @ extra_ts) end
   1.354 +        | NONE => (* a free or schematic variable *)
   1.355 +          let
   1.356 +            val ts = map (aux NONE []) (us @ extra_us)
   1.357 +            val T = map fastype_of ts ---> HOLogic.typeT
   1.358 +            val t =
   1.359 +              case strip_prefix_and_unascii fixed_var_prefix a of
   1.360 +                SOME b => Free (b, T)
   1.361 +              | NONE =>
   1.362 +                case strip_prefix_and_unascii schematic_var_prefix a of
   1.363 +                  SOME b => Var ((b, 0), T)
   1.364 +                | NONE =>
   1.365 +                  if is_atp_variable a then
   1.366 +                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
   1.367 +                  else
   1.368 +                    (* Skolem constants? *)
   1.369 +                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   1.370 +          in list_comb (t, ts) end
   1.371 +  in aux (SOME HOLogic.boolT) [] end
   1.372 +
   1.373 +fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   1.374 +  if String.isPrefix class_prefix s then
   1.375 +    add_type_constraint (type_constraint_from_term pos tfrees u)
   1.376 +    #> pair @{const True}
   1.377 +  else
   1.378 +    pair (raw_term_from_pred thy full_types tfrees u)
   1.379 +
   1.380 +val combinator_table =
   1.381 +  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   1.382 +   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   1.383 +   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   1.384 +   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   1.385 +   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   1.386 +
   1.387 +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   1.388 +  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   1.389 +  | uncombine_term (t as Const (x as (s, _))) =
   1.390 +    (case AList.lookup (op =) combinator_table s of
   1.391 +       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   1.392 +     | NONE => t)
   1.393 +  | uncombine_term t = t
   1.394 +
   1.395 +(* Update schematic type variables with detected sort constraints. It's not
   1.396 +   totally clear when this code is necessary. *)
   1.397 +fun repair_tvar_sorts (t, tvar_tab) =
   1.398 +  let
   1.399 +    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   1.400 +      | do_type (TVar (xi, s)) =
   1.401 +        TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   1.402 +      | do_type (TFree z) = TFree z
   1.403 +    fun do_term (Const (a, T)) = Const (a, do_type T)
   1.404 +      | do_term (Free (a, T)) = Free (a, do_type T)
   1.405 +      | do_term (Var (xi, T)) = Var (xi, do_type T)
   1.406 +      | do_term (t as Bound _) = t
   1.407 +      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   1.408 +      | do_term (t1 $ t2) = do_term t1 $ do_term t2
   1.409 +  in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   1.410 +
   1.411 +fun quantify_over_var quant_of var_s t =
   1.412 +  let
   1.413 +    val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   1.414 +                  |> map Var
   1.415 +  in fold_rev quant_of vars t end
   1.416 +
   1.417 +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   1.418 +   appear in the formula. *)
   1.419 +fun prop_from_formula thy full_types tfrees phi =
   1.420 +  let
   1.421 +    fun do_formula pos phi =
   1.422 +      case phi of
   1.423 +        AQuant (_, [], phi) => do_formula pos phi
   1.424 +      | AQuant (q, x :: xs, phi') =>
   1.425 +        do_formula pos (AQuant (q, xs, phi'))
   1.426 +        #>> quantify_over_var (case q of
   1.427 +                                 AForall => forall_of
   1.428 +                               | AExists => exists_of)
   1.429 +                              (repair_atp_variable_name Char.toLower x)
   1.430 +      | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   1.431 +      | AConn (c, [phi1, phi2]) =>
   1.432 +        do_formula (pos |> c = AImplies ? not) phi1
   1.433 +        ##>> do_formula pos phi2
   1.434 +        #>> (case c of
   1.435 +               AAnd => s_conj
   1.436 +             | AOr => s_disj
   1.437 +             | AImplies => s_imp
   1.438 +             | AIf => s_imp o swap
   1.439 +             | AIff => s_iff
   1.440 +             | ANotIff => s_not o s_iff)
   1.441 +      | AAtom tm => term_from_pred thy full_types tfrees pos tm
   1.442 +      | _ => raise FORMULA [phi]
   1.443 +  in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   1.444 +
   1.445 +fun check_formula ctxt =
   1.446 +  Type.constraint HOLogic.boolT
   1.447 +  #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   1.448 +
   1.449 +
   1.450 +(**** Translation of TSTP files to Isar Proofs ****)
   1.451 +
   1.452 +fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   1.453 +  | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   1.454 +
   1.455 +fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   1.456 +    let
   1.457 +      val thy = ProofContext.theory_of ctxt
   1.458 +      val t1 = prop_from_formula thy full_types tfrees phi1
   1.459 +      val vars = snd (strip_comb t1)
   1.460 +      val frees = map unvarify_term vars
   1.461 +      val unvarify_args = subst_atomic (vars ~~ frees)
   1.462 +      val t2 = prop_from_formula thy full_types tfrees phi2
   1.463 +      val (t1, t2) =
   1.464 +        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   1.465 +        |> unvarify_args |> uncombine_term |> check_formula ctxt
   1.466 +        |> HOLogic.dest_eq
   1.467 +    in
   1.468 +      (Definition (name, t1, t2),
   1.469 +       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   1.470 +    end
   1.471 +  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   1.472 +    let
   1.473 +      val thy = ProofContext.theory_of ctxt
   1.474 +      val t = u |> prop_from_formula thy full_types tfrees
   1.475 +                |> uncombine_term |> check_formula ctxt
   1.476 +    in
   1.477 +      (Inference (name, t, deps),
   1.478 +       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   1.479 +    end
   1.480 +fun decode_lines ctxt full_types tfrees lines =
   1.481 +  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   1.482 +
   1.483 +fun is_same_inference _ (Definition _) = false
   1.484 +  | is_same_inference t (Inference (_, t', _)) = t aconv t'
   1.485 +
   1.486 +(* No "real" literals means only type information (tfree_tcs, clsrel, or
   1.487 +   clsarity). *)
   1.488 +val is_only_type_information = curry (op aconv) HOLogic.true_const
   1.489 +
   1.490 +fun replace_one_dependency (old, new) dep =
   1.491 +  if is_same_step (dep, old) then new else [dep]
   1.492 +fun replace_dependencies_in_line _ (line as Definition _) = line
   1.493 +  | replace_dependencies_in_line p (Inference (name, t, deps)) =
   1.494 +    Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   1.495 +
   1.496 +(* Discard axioms; consolidate adjacent lines that prove the same formula, since
   1.497 +   they differ only in type information.*)
   1.498 +fun add_line _ _ (line as Definition _) lines = line :: lines
   1.499 +  | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   1.500 +    (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   1.501 +       definitions. *)
   1.502 +    if is_axiom axiom_names name then
   1.503 +      (* Axioms are not proof lines. *)
   1.504 +      if is_only_type_information t then
   1.505 +        map (replace_dependencies_in_line (name, [])) lines
   1.506 +      (* Is there a repetition? If so, replace later line by earlier one. *)
   1.507 +      else case take_prefix (not o is_same_inference t) lines of
   1.508 +        (_, []) => lines (* no repetition of proof line *)
   1.509 +      | (pre, Inference (name', _, _) :: post) =>
   1.510 +        pre @ map (replace_dependencies_in_line (name', [name])) post
   1.511 +    else if is_conjecture conjecture_shape name then
   1.512 +      Inference (name, negate_term t, []) :: lines
   1.513 +    else
   1.514 +      map (replace_dependencies_in_line (name, [])) lines
   1.515 +  | add_line _ _ (Inference (name, t, deps)) lines =
   1.516 +    (* Type information will be deleted later; skip repetition test. *)
   1.517 +    if is_only_type_information t then
   1.518 +      Inference (name, t, deps) :: lines
   1.519 +    (* Is there a repetition? If so, replace later line by earlier one. *)
   1.520 +    else case take_prefix (not o is_same_inference t) lines of
   1.521 +      (* FIXME: Doesn't this code risk conflating proofs involving different
   1.522 +         types? *)
   1.523 +       (_, []) => Inference (name, t, deps) :: lines
   1.524 +     | (pre, Inference (name', t', _) :: post) =>
   1.525 +       Inference (name, t', deps) ::
   1.526 +       pre @ map (replace_dependencies_in_line (name', [name])) post
   1.527 +
   1.528 +(* Recursively delete empty lines (type information) from the proof. *)
   1.529 +fun add_nontrivial_line (Inference (name, t, [])) lines =
   1.530 +    if is_only_type_information t then delete_dependency name lines
   1.531 +    else Inference (name, t, []) :: lines
   1.532 +  | add_nontrivial_line line lines = line :: lines
   1.533 +and delete_dependency name lines =
   1.534 +  fold_rev add_nontrivial_line
   1.535 +           (map (replace_dependencies_in_line (name, [])) lines) []
   1.536 +
   1.537 +(* ATPs sometimes reuse free variable names in the strangest ways. Removing
   1.538 +   offending lines often does the trick. *)
   1.539 +fun is_bad_free frees (Free x) = not (member (op =) frees x)
   1.540 +  | is_bad_free _ _ = false
   1.541 +
   1.542 +fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   1.543 +    (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   1.544 +  | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   1.545 +                     (Inference (name, t, deps)) (j, lines) =
   1.546 +    (j + 1,
   1.547 +     if is_axiom axiom_names name orelse
   1.548 +        is_conjecture conjecture_shape name orelse
   1.549 +        (* the last line must be kept *)
   1.550 +        j = 0 orelse
   1.551 +        (not (is_only_type_information t) andalso
   1.552 +         null (Term.add_tvars t []) andalso
   1.553 +         not (exists_subterm (is_bad_free frees) t) andalso
   1.554 +         length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   1.555 +         (* kill next to last line, which usually results in a trivial step *)
   1.556 +         j <> 1) then
   1.557 +       Inference (name, t, deps) :: lines  (* keep line *)
   1.558 +     else
   1.559 +       map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   1.560 +
   1.561 +(** Isar proof construction and manipulation **)
   1.562 +
   1.563 +fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   1.564 +  (union (op =) ls1 ls2, union (op =) ss1 ss2)
   1.565 +
   1.566 +type label = string * int
   1.567 +type facts = label list * string list
   1.568 +
   1.569 +datatype isar_qualifier = Show | Then | Moreover | Ultimately
   1.570 +
   1.571 +datatype isar_step =
   1.572 +  Fix of (string * typ) list |
   1.573 +  Let of term * term |
   1.574 +  Assume of label * term |
   1.575 +  Have of isar_qualifier list * label * term * byline
   1.576 +and byline =
   1.577 +  ByMetis of facts |
   1.578 +  CaseSplit of isar_step list list * facts
   1.579 +
   1.580 +fun smart_case_split [] facts = ByMetis facts
   1.581 +  | smart_case_split proofs facts = CaseSplit (proofs, facts)
   1.582 +
   1.583 +fun add_fact_from_dependency conjecture_shape axiom_names name =
   1.584 +  if is_axiom axiom_names name then
   1.585 +    apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   1.586 +  else
   1.587 +    apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   1.588 +
   1.589 +fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.590 +  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   1.591 +    Assume (raw_label_for_name conjecture_shape name, t)
   1.592 +  | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   1.593 +    Have (if j = 1 then [Show] else [],
   1.594 +          raw_label_for_name conjecture_shape name,
   1.595 +          fold_rev forall_of (map Var (Term.add_vars t [])) t,
   1.596 +          ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   1.597 +                        deps ([], [])))
   1.598 +
   1.599 +fun repair_name "$true" = "c_True"
   1.600 +  | repair_name "$false" = "c_False"
   1.601 +  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   1.602 +  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   1.603 +  | repair_name s =
   1.604 +    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   1.605 +      "c_equal" (* seen in Vampire proofs *)
   1.606 +    else
   1.607 +      s
   1.608 +
   1.609 +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   1.610 +        tstplike_proof conjecture_shape axiom_names params frees =
   1.611 +  let
   1.612 +    val lines =
   1.613 +      tstplike_proof
   1.614 +      |> atp_proof_from_tstplike_string
   1.615 +      |> nasty_atp_proof pool
   1.616 +      |> map_term_names_in_atp_proof repair_name
   1.617 +      |> decode_lines ctxt full_types tfrees
   1.618 +      |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   1.619 +      |> rpair [] |-> fold_rev add_nontrivial_line
   1.620 +      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   1.621 +                                             conjecture_shape axiom_names frees)
   1.622 +      |> snd
   1.623 +  in
   1.624 +    (if null params then [] else [Fix params]) @
   1.625 +    map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   1.626 +         lines
   1.627 +  end
   1.628 +
   1.629 +(* When redirecting proofs, we keep information about the labels seen so far in
   1.630 +   the "backpatches" data structure. The first component indicates which facts
   1.631 +   should be associated with forthcoming proof steps. The second component is a
   1.632 +   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   1.633 +   become assumptions and "drop_ls" are the labels that should be dropped in a
   1.634 +   case split. *)
   1.635 +type backpatches = (label * facts) list * (label list * label list)
   1.636 +
   1.637 +fun used_labels_of_step (Have (_, _, _, by)) =
   1.638 +    (case by of
   1.639 +       ByMetis (ls, _) => ls
   1.640 +     | CaseSplit (proofs, (ls, _)) =>
   1.641 +       fold (union (op =) o used_labels_of) proofs ls)
   1.642 +  | used_labels_of_step _ = []
   1.643 +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   1.644 +
   1.645 +fun new_labels_of_step (Fix _) = []
   1.646 +  | new_labels_of_step (Let _) = []
   1.647 +  | new_labels_of_step (Assume (l, _)) = [l]
   1.648 +  | new_labels_of_step (Have (_, l, _, _)) = [l]
   1.649 +val new_labels_of = maps new_labels_of_step
   1.650 +
   1.651 +val join_proofs =
   1.652 +  let
   1.653 +    fun aux _ [] = NONE
   1.654 +      | aux proof_tail (proofs as (proof1 :: _)) =
   1.655 +        if exists null proofs then
   1.656 +          NONE
   1.657 +        else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   1.658 +          aux (hd proof1 :: proof_tail) (map tl proofs)
   1.659 +        else case hd proof1 of
   1.660 +          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   1.661 +          if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   1.662 +                      | _ => false) (tl proofs) andalso
   1.663 +             not (exists (member (op =) (maps new_labels_of proofs))
   1.664 +                         (used_labels_of proof_tail)) then
   1.665 +            SOME (l, t, map rev proofs, proof_tail)
   1.666 +          else
   1.667 +            NONE
   1.668 +        | _ => NONE
   1.669 +  in aux [] o map rev end
   1.670 +
   1.671 +fun case_split_qualifiers proofs =
   1.672 +  case length proofs of
   1.673 +    0 => []
   1.674 +  | 1 => [Then]
   1.675 +  | _ => [Ultimately]
   1.676 +
   1.677 +fun redirect_proof hyp_ts concl_t proof =
   1.678 +  let
   1.679 +    (* The first pass outputs those steps that are independent of the negated
   1.680 +       conjecture. The second pass flips the proof by contradiction to obtain a
   1.681 +       direct proof, introducing case splits when an inference depends on
   1.682 +       several facts that depend on the negated conjecture. *)
   1.683 +     val concl_l = (conjecture_prefix, length hyp_ts)
   1.684 +     fun first_pass ([], contra) = ([], contra)
   1.685 +       | first_pass ((step as Fix _) :: proof, contra) =
   1.686 +         first_pass (proof, contra) |>> cons step
   1.687 +       | first_pass ((step as Let _) :: proof, contra) =
   1.688 +         first_pass (proof, contra) |>> cons step
   1.689 +       | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   1.690 +         if l = concl_l then first_pass (proof, contra ||> cons step)
   1.691 +         else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   1.692 +       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   1.693 +         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   1.694 +           if exists (member (op =) (fst contra)) ls then
   1.695 +             first_pass (proof, contra |>> cons l ||> cons step)
   1.696 +           else
   1.697 +             first_pass (proof, contra) |>> cons step
   1.698 +         end
   1.699 +       | first_pass _ = raise Fail "malformed proof"
   1.700 +    val (proof_top, (contra_ls, contra_proof)) =
   1.701 +      first_pass (proof, ([concl_l], []))
   1.702 +    val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   1.703 +    fun backpatch_labels patches ls =
   1.704 +      fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   1.705 +    fun second_pass end_qs ([], assums, patches) =
   1.706 +        ([Have (end_qs, no_label, concl_t,
   1.707 +                ByMetis (backpatch_labels patches (map snd assums)))], patches)
   1.708 +      | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   1.709 +        second_pass end_qs (proof, (t, l) :: assums, patches)
   1.710 +      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   1.711 +                            patches) =
   1.712 +        (if member (op =) (snd (snd patches)) l andalso
   1.713 +            not (member (op =) (fst (snd patches)) l) andalso
   1.714 +            not (AList.defined (op =) (fst patches) l) then
   1.715 +           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   1.716 +         else case List.partition (member (op =) contra_ls) ls of
   1.717 +           ([contra_l], co_ls) =>
   1.718 +           if member (op =) qs Show then
   1.719 +             second_pass end_qs (proof, assums,
   1.720 +                                 patches |>> cons (contra_l, (co_ls, ss)))
   1.721 +           else
   1.722 +             second_pass end_qs
   1.723 +                         (proof, assums,
   1.724 +                          patches |>> cons (contra_l, (l :: co_ls, ss)))
   1.725 +             |>> cons (if member (op =) (fst (snd patches)) l then
   1.726 +                         Assume (l, negate_term t)
   1.727 +                       else
   1.728 +                         Have (qs, l, negate_term t,
   1.729 +                               ByMetis (backpatch_label patches l)))
   1.730 +         | (contra_ls as _ :: _, co_ls) =>
   1.731 +           let
   1.732 +             val proofs =
   1.733 +               map_filter
   1.734 +                   (fn l =>
   1.735 +                       if l = concl_l then
   1.736 +                         NONE
   1.737 +                       else
   1.738 +                         let
   1.739 +                           val drop_ls = filter (curry (op <>) l) contra_ls
   1.740 +                         in
   1.741 +                           second_pass []
   1.742 +                               (proof, assums,
   1.743 +                                patches ||> apfst (insert (op =) l)
   1.744 +                                        ||> apsnd (union (op =) drop_ls))
   1.745 +                           |> fst |> SOME
   1.746 +                         end) contra_ls
   1.747 +             val (assumes, facts) =
   1.748 +               if member (op =) (fst (snd patches)) l then
   1.749 +                 ([Assume (l, negate_term t)], (l :: co_ls, ss))
   1.750 +               else
   1.751 +                 ([], (co_ls, ss))
   1.752 +           in
   1.753 +             (case join_proofs proofs of
   1.754 +                SOME (l, t, proofs, proof_tail) =>
   1.755 +                Have (case_split_qualifiers proofs @
   1.756 +                      (if null proof_tail then end_qs else []), l, t,
   1.757 +                      smart_case_split proofs facts) :: proof_tail
   1.758 +              | NONE =>
   1.759 +                [Have (case_split_qualifiers proofs @ end_qs, no_label,
   1.760 +                       concl_t, smart_case_split proofs facts)],
   1.761 +              patches)
   1.762 +             |>> append assumes
   1.763 +           end
   1.764 +         | _ => raise Fail "malformed proof")
   1.765 +       | second_pass _ _ = raise Fail "malformed proof"
   1.766 +    val proof_bottom =
   1.767 +      second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   1.768 +  in proof_top @ proof_bottom end
   1.769 +
   1.770 +(* FIXME: Still needed? Probably not. *)
   1.771 +val kill_duplicate_assumptions_in_proof =
   1.772 +  let
   1.773 +    fun relabel_facts subst =
   1.774 +      apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   1.775 +    fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   1.776 +        (case AList.lookup (op aconv) assums t of
   1.777 +           SOME l' => (proof, (l, l') :: subst, assums)
   1.778 +         | NONE => (step :: proof, subst, (t, l) :: assums))
   1.779 +      | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   1.780 +        (Have (qs, l, t,
   1.781 +               case by of
   1.782 +                 ByMetis facts => ByMetis (relabel_facts subst facts)
   1.783 +               | CaseSplit (proofs, facts) =>
   1.784 +                 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   1.785 +         proof, subst, assums)
   1.786 +      | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   1.787 +    and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   1.788 +  in do_proof end
   1.789 +
   1.790 +val then_chain_proof =
   1.791 +  let
   1.792 +    fun aux _ [] = []
   1.793 +      | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   1.794 +      | aux l' (Have (qs, l, t, by) :: proof) =
   1.795 +        (case by of
   1.796 +           ByMetis (ls, ss) =>
   1.797 +           Have (if member (op =) ls l' then
   1.798 +                   (Then :: qs, l, t,
   1.799 +                    ByMetis (filter_out (curry (op =) l') ls, ss))
   1.800 +                 else
   1.801 +                   (qs, l, t, ByMetis (ls, ss)))
   1.802 +         | CaseSplit (proofs, facts) =>
   1.803 +           Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   1.804 +        aux l proof
   1.805 +      | aux _ (step :: proof) = step :: aux no_label proof
   1.806 +  in aux no_label end
   1.807 +
   1.808 +fun kill_useless_labels_in_proof proof =
   1.809 +  let
   1.810 +    val used_ls = used_labels_of proof
   1.811 +    fun do_label l = if member (op =) used_ls l then l else no_label
   1.812 +    fun do_step (Assume (l, t)) = Assume (do_label l, t)
   1.813 +      | do_step (Have (qs, l, t, by)) =
   1.814 +        Have (qs, do_label l, t,
   1.815 +              case by of
   1.816 +                CaseSplit (proofs, facts) =>
   1.817 +                CaseSplit (map (map do_step) proofs, facts)
   1.818 +              | _ => by)
   1.819 +      | do_step step = step
   1.820 +  in map do_step proof end
   1.821 +
   1.822 +fun prefix_for_depth n = replicate_string (n + 1)
   1.823 +
   1.824 +val relabel_proof =
   1.825 +  let
   1.826 +    fun aux _ _ _ [] = []
   1.827 +      | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   1.828 +        if l = no_label then
   1.829 +          Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   1.830 +        else
   1.831 +          let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   1.832 +            Assume (l', t) ::
   1.833 +            aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   1.834 +          end
   1.835 +      | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   1.836 +        let
   1.837 +          val (l', subst, next_fact) =
   1.838 +            if l = no_label then
   1.839 +              (l, subst, next_fact)
   1.840 +            else
   1.841 +              let
   1.842 +                val l' = (prefix_for_depth depth fact_prefix, next_fact)
   1.843 +              in (l', (l, l') :: subst, next_fact + 1) end
   1.844 +          val relabel_facts =
   1.845 +            apfst (maps (the_list o AList.lookup (op =) subst))
   1.846 +          val by =
   1.847 +            case by of
   1.848 +              ByMetis facts => ByMetis (relabel_facts facts)
   1.849 +            | CaseSplit (proofs, facts) =>
   1.850 +              CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   1.851 +                         relabel_facts facts)
   1.852 +        in
   1.853 +          Have (qs, l', t, by) ::
   1.854 +          aux subst depth (next_assum, next_fact) proof
   1.855 +        end
   1.856 +      | aux subst depth nextp (step :: proof) =
   1.857 +        step :: aux subst depth nextp proof
   1.858 +  in aux [] 0 (1, 1) end
   1.859 +
   1.860 +fun string_for_proof ctxt0 full_types i n =
   1.861 +  let
   1.862 +    val ctxt = ctxt0
   1.863 +      |> Config.put show_free_types false
   1.864 +      |> Config.put show_types true
   1.865 +    fun fix_print_mode f x =
   1.866 +      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   1.867 +                               (print_mode_value ())) f x
   1.868 +    fun do_indent ind = replicate_string (ind * indent_size) " "
   1.869 +    fun do_free (s, T) =
   1.870 +      maybe_quote s ^ " :: " ^
   1.871 +      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   1.872 +    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   1.873 +    fun do_have qs =
   1.874 +      (if member (op =) qs Moreover then "moreover " else "") ^
   1.875 +      (if member (op =) qs Ultimately then "ultimately " else "") ^
   1.876 +      (if member (op =) qs Then then
   1.877 +         if member (op =) qs Show then "thus" else "hence"
   1.878 +       else
   1.879 +         if member (op =) qs Show then "show" else "have")
   1.880 +    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   1.881 +    fun do_facts (ls, ss) =
   1.882 +      metis_command full_types 1 1
   1.883 +                    (ls |> sort_distinct (prod_ord string_ord int_ord),
   1.884 +                     ss |> sort_distinct string_ord)
   1.885 +    and do_step ind (Fix xs) =
   1.886 +        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   1.887 +      | do_step ind (Let (t1, t2)) =
   1.888 +        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   1.889 +      | do_step ind (Assume (l, t)) =
   1.890 +        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   1.891 +      | do_step ind (Have (qs, l, t, ByMetis facts)) =
   1.892 +        do_indent ind ^ do_have qs ^ " " ^
   1.893 +        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   1.894 +      | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   1.895 +        space_implode (do_indent ind ^ "moreover\n")
   1.896 +                      (map (do_block ind) proofs) ^
   1.897 +        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   1.898 +        do_facts facts ^ "\n"
   1.899 +    and do_steps prefix suffix ind steps =
   1.900 +      let val s = implode (map (do_step ind) steps) in
   1.901 +        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   1.902 +        String.extract (s, ind * indent_size,
   1.903 +                        SOME (size s - ind * indent_size - 1)) ^
   1.904 +        suffix ^ "\n"
   1.905 +      end
   1.906 +    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   1.907 +    (* One-step proofs are pointless; better use the Metis one-liner
   1.908 +       directly. *)
   1.909 +    and do_proof [Have (_, _, _, ByMetis _)] = ""
   1.910 +      | do_proof proof =
   1.911 +        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   1.912 +        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   1.913 +        (if n <> 1 then "next" else "qed")
   1.914 +  in do_proof end
   1.915 +
   1.916 +fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.917 +                    (other_params as (_, full_types, _, tstplike_proof,
   1.918 +                                      axiom_names, goal, i)) =
   1.919 +  let
   1.920 +    val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.921 +    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.922 +    val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   1.923 +    val n = Logic.count_prems (prop_of goal)
   1.924 +    val (one_line_proof, lemma_names) = metis_proof_text other_params
   1.925 +    fun isar_proof_for () =
   1.926 +      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   1.927 +               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   1.928 +               params frees
   1.929 +           |> redirect_proof hyp_ts concl_t
   1.930 +           |> kill_duplicate_assumptions_in_proof
   1.931 +           |> then_chain_proof
   1.932 +           |> kill_useless_labels_in_proof
   1.933 +           |> relabel_proof
   1.934 +           |> string_for_proof ctxt full_types i n of
   1.935 +        "" => "\nNo structured proof available."
   1.936 +      | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   1.937 +    val isar_proof =
   1.938 +      if debug then
   1.939 +        isar_proof_for ()
   1.940 +      else
   1.941 +        try isar_proof_for ()
   1.942 +        |> the_default "\nWarning: The Isar proof construction failed."
   1.943 +  in (one_line_proof ^ isar_proof, lemma_names) end
   1.944 +
   1.945 +fun proof_text isar_proof isar_params other_params =
   1.946 +  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   1.947 +      other_params
   1.948 +
   1.949 +end;