src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
author wenzelm
Sat Nov 20 00:53:26 2010 +0100 (2010-11-20)
changeset 40627 becf5d5187cc
parent 40204 da97d75e20e6
child 40723 a82badd0e6ef
permissions -rw-r--r--
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Claire Quigley, Cambridge University Computer Laboratory
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Proof reconstruction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ATP_RECONSTRUCT =
    10 sig
    11   type locality = Sledgehammer_Filter.locality
    12   type minimize_command = string list -> string
    13   type metis_params =
    14     string * bool * minimize_command * string * (string * locality) list vector
    15     * thm * int
    16   type isar_params =
    17     string Symtab.table * bool * int * Proof.context * int list list
    18   type text_result = string * (string * locality) list
    19 
    20   val repair_conjecture_shape_and_fact_names :
    21     string -> int list list -> (string * locality) list vector
    22     -> int list list * (string * locality) list vector
    23   val apply_on_subgoal : int -> int -> string
    24   val command_call : string -> string list -> string
    25   val try_command_line : string -> string -> string
    26   val minimize_line : ('a list -> string) -> 'a list -> string
    27   val metis_proof_text : metis_params -> text_result
    28   val isar_proof_text : isar_params -> metis_params -> text_result
    29   val proof_text : bool -> isar_params -> metis_params -> text_result
    30 end;
    31 
    32 structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
    33 struct
    34 
    35 open ATP_Problem
    36 open ATP_Proof
    37 open Metis_Translate
    38 open Sledgehammer_Util
    39 open Sledgehammer_Filter
    40 open Sledgehammer_ATP_Translate
    41 
    42 type minimize_command = string list -> string
    43 type metis_params =
    44   string * bool * minimize_command * string * (string * locality) list vector
    45   * thm * int
    46 type isar_params =
    47   string Symtab.table * bool * int * Proof.context * int list list
    48 type text_result = string * (string * locality) list
    49 
    50 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    51 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    52 
    53 fun find_first_in_list_vector vec key =
    54   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    55                  | (_, value) => value) NONE vec
    56 
    57 
    58 (** SPASS's Flotter hack **)
    59 
    60 (* This is a hack required for keeping track of facts after they have been
    61    clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    62    part of this hack. *)
    63 
    64 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    65 
    66 fun extract_clause_sequence output =
    67   let
    68     val tokens_of = String.tokens (not o Char.isAlphaNum)
    69     fun extract_num ("clause" :: (ss as _ :: _)) =
    70     Int.fromString (List.last ss)
    71       | extract_num _ = NONE
    72   in output |> split_lines |> map_filter (extract_num o tokens_of) end
    73 
    74 val parse_clause_formula_pair =
    75   $$ "(" |-- scan_integer --| $$ ","
    76   -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
    77   --| Scan.option ($$ ",")
    78 val parse_clause_formula_relation =
    79   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    80   |-- Scan.repeat parse_clause_formula_pair
    81 val extract_clause_formula_relation =
    82   Substring.full #> Substring.position set_ClauseFormulaRelationN
    83   #> snd #> Substring.position "." #> fst #> Substring.string
    84   #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    85   #> fst
    86 
    87 fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    88   if String.isSubstring set_ClauseFormulaRelationN output then
    89     let
    90       val j0 = hd (hd conjecture_shape)
    91       val seq = extract_clause_sequence output
    92       val name_map = extract_clause_formula_relation output
    93       fun renumber_conjecture j =
    94         conjecture_prefix ^ string_of_int (j - j0)
    95         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
    96         |> map (fn s => find_index (curry (op =) s) seq + 1)
    97       fun names_for_number j =
    98         j |> AList.lookup (op =) name_map |> these
    99           |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
   100           |> map (fn name =>
   101                      (name, name |> find_first_in_list_vector fact_names |> the)
   102                      handle Option.Option =>
   103                             error ("No such fact: " ^ quote name ^ "."))
   104     in
   105       (conjecture_shape |> map (maps renumber_conjecture),
   106        seq |> map names_for_number |> Vector.fromList)
   107     end
   108   else
   109     (conjecture_shape, fact_names)
   110 
   111 
   112 (** Soft-core proof reconstruction: Metis one-liner **)
   113 
   114 fun string_for_label (s, num) = s ^ string_of_int num
   115 
   116 fun apply_on_subgoal _ 1 = "by "
   117   | apply_on_subgoal 1 _ = "apply "
   118   | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
   119 fun command_call name [] = name
   120   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   121 fun try_command_line banner command =
   122   banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   123 fun using_labels [] = ""
   124   | using_labels ls =
   125     "using " ^ space_implode " " (map string_for_label ls) ^ " "
   126 fun metis_name full_types = if full_types then "metisFT" else "metis"
   127 fun metis_call full_types ss = command_call (metis_name full_types) ss
   128 fun metis_command full_types i n (ls, ss) =
   129   using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
   130 fun metis_line banner full_types i n ss =
   131   try_command_line banner (metis_command full_types i n ([], ss))
   132 fun minimize_line _ [] = ""
   133   | minimize_line minimize_command ss =
   134     case minimize_command ss of
   135       "" => ""
   136     | command =>
   137       "\nTo minimize the number of lemmas, try this: " ^
   138       Markup.markup Markup.sendback command ^ "."
   139 
   140 fun resolve_fact fact_names ((_, SOME s)) =
   141     (case strip_prefix_and_unascii fact_prefix s of
   142        SOME s' => (case find_first_in_list_vector fact_names s' of
   143                      SOME x => [(s', x)]
   144                    | NONE => [])
   145      | NONE => [])
   146   | resolve_fact fact_names (num, NONE) =
   147     case Int.fromString num of
   148       SOME j =>
   149       if j > 0 andalso j <= Vector.length fact_names then
   150         Vector.sub (fact_names, j - 1)
   151       else
   152         []
   153     | NONE => []
   154 
   155 fun add_fact fact_names (Inference (name, _, [])) =
   156     append (resolve_fact fact_names name)
   157   | add_fact _ _ = I
   158 
   159 fun used_facts_in_tstplike_proof fact_names =
   160   atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
   161 
   162 fun used_facts fact_names =
   163   used_facts_in_tstplike_proof fact_names
   164   #> List.partition (curry (op =) Chained o snd)
   165   #> pairself (sort_distinct (string_ord o pairself fst))
   166 
   167 fun metis_proof_text (banner, full_types, minimize_command,
   168                       tstplike_proof, fact_names, goal, i) =
   169   let
   170     val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
   171     val n = Logic.count_prems (prop_of goal)
   172   in
   173     (metis_line banner full_types i n (map fst other_lemmas) ^
   174      minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   175      other_lemmas @ chained_lemmas)
   176   end
   177 
   178 
   179 (** Hard-core proof reconstruction: structured Isar proofs **)
   180 
   181 (* Simple simplifications to ensure that sort annotations don't leave a trail of
   182    spurious "True"s. *)
   183 fun s_not @{const False} = @{const True}
   184   | s_not @{const True} = @{const False}
   185   | s_not (@{const Not} $ t) = t
   186   | s_not t = @{const Not} $ t
   187 fun s_conj (@{const True}, t2) = t2
   188   | s_conj (t1, @{const True}) = t1
   189   | s_conj p = HOLogic.mk_conj p
   190 fun s_disj (@{const False}, t2) = t2
   191   | s_disj (t1, @{const False}) = t1
   192   | s_disj p = HOLogic.mk_disj p
   193 fun s_imp (@{const True}, t2) = t2
   194   | s_imp (t1, @{const False}) = s_not t1
   195   | s_imp p = HOLogic.mk_imp p
   196 fun s_iff (@{const True}, t2) = t2
   197   | s_iff (t1, @{const True}) = t1
   198   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   199 
   200 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   201 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   202 
   203 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   204     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   205   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   206     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   207   | negate_term (@{const HOL.implies} $ t1 $ t2) =
   208     @{const HOL.conj} $ t1 $ negate_term t2
   209   | negate_term (@{const HOL.conj} $ t1 $ t2) =
   210     @{const HOL.disj} $ negate_term t1 $ negate_term t2
   211   | negate_term (@{const HOL.disj} $ t1 $ t2) =
   212     @{const HOL.conj} $ negate_term t1 $ negate_term t2
   213   | negate_term (@{const Not} $ t) = t
   214   | negate_term t = @{const Not} $ t
   215 
   216 val indent_size = 2
   217 val no_label = ("", ~1)
   218 
   219 val raw_prefix = "X"
   220 val assum_prefix = "A"
   221 val fact_prefix = "F"
   222 
   223 fun resolve_conjecture conjecture_shape (num, s_opt) =
   224   let
   225     val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   226               SOME s => Int.fromString s |> the_default ~1
   227             | NONE => case Int.fromString num of
   228                         SOME j => find_index (exists (curry (op =) j))
   229                                              conjecture_shape
   230                       | NONE => ~1
   231   in if k >= 0 then [k] else [] end
   232 
   233 fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
   234 fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   235 
   236 fun raw_label_for_name conjecture_shape name =
   237   case resolve_conjecture conjecture_shape name of
   238     [j] => (conjecture_prefix, j)
   239   | _ => case Int.fromString (fst name) of
   240            SOME j => (raw_prefix, j)
   241          | NONE => (raw_prefix ^ fst name, 0)
   242 
   243 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   244 
   245 exception FO_TERM of string fo_term list
   246 exception FORMULA of (string, string fo_term) formula list
   247 exception SAME of unit
   248 
   249 (* Type variables are given the basic sort "HOL.type". Some will later be
   250    constrained by information from type literals, or by type inference. *)
   251 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   252   let val Ts = map (type_from_fo_term tfrees) us in
   253     case strip_prefix_and_unascii type_const_prefix a of
   254       SOME b => Type (invert_const b, Ts)
   255     | NONE =>
   256       if not (null us) then
   257         raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   258       else case strip_prefix_and_unascii tfree_prefix a of
   259         SOME b =>
   260         let val s = "'" ^ b in
   261           TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   262         end
   263       | NONE =>
   264         case strip_prefix_and_unascii tvar_prefix a of
   265           SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   266         | NONE =>
   267           (* Variable from the ATP, say "X1" *)
   268           Type_Infer.param 0 (a, HOLogic.typeS)
   269   end
   270 
   271 (* Type class literal applied to a type. Returns triple of polarity, class,
   272    type. *)
   273 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   274   case (strip_prefix_and_unascii class_prefix a,
   275         map (type_from_fo_term tfrees) us) of
   276     (SOME b, [T]) => (pos, b, T)
   277   | _ => raise FO_TERM [u]
   278 
   279 (** Accumulate type constraints in a formula: negative type literals **)
   280 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   281 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   282   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   283   | add_type_constraint _ = I
   284 
   285 fun repair_atp_variable_name f s =
   286   let
   287     fun subscript_name s n = s ^ nat_subscript n
   288     val s = String.map f s
   289   in
   290     case space_explode "_" s of
   291       [_] => (case take_suffix Char.isDigit (String.explode s) of
   292                 (cs1 as _ :: _, cs2 as _ :: _) =>
   293                 subscript_name (String.implode cs1)
   294                                (the (Int.fromString (String.implode cs2)))
   295               | (_, _) => s)
   296     | [s1, s2] => (case Int.fromString s2 of
   297                      SOME n => subscript_name s1 n
   298                    | NONE => s)
   299     | _ => s
   300   end
   301 
   302 (* First-order translation. No types are known for variables. "HOLogic.typeT"
   303    should allow them to be inferred. *)
   304 fun raw_term_from_pred thy full_types tfrees =
   305   let
   306     fun aux opt_T extra_us u =
   307       case u of
   308         ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   309       | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   310       | ATerm (a, us) =>
   311         if a = type_wrapper_name then
   312           case us of
   313             [typ_u, term_u] =>
   314             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   315           | _ => raise FO_TERM us
   316         else case strip_prefix_and_unascii const_prefix a of
   317           SOME "equal" =>
   318           let val ts = map (aux NONE []) us in
   319             if length ts = 2 andalso hd ts aconv List.last ts then
   320               (* Vampire is keen on producing these. *)
   321               @{const True}
   322             else
   323               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   324           end
   325         | SOME b =>
   326           let
   327             val c = invert_const b
   328             val num_type_args = num_type_args thy c
   329             val (type_us, term_us) =
   330               chop (if full_types then 0 else num_type_args) us
   331             (* Extra args from "hAPP" come after any arguments given directly to
   332                the constant. *)
   333             val term_ts = map (aux NONE []) term_us
   334             val extra_ts = map (aux NONE []) extra_us
   335             val t =
   336               Const (c, if full_types then
   337                           case opt_T of
   338                             SOME T => map fastype_of term_ts ---> T
   339                           | NONE =>
   340                             if num_type_args = 0 then
   341                               Sign.const_instance thy (c, [])
   342                             else
   343                               raise Fail ("no type information for " ^ quote c)
   344                         else
   345                           Sign.const_instance thy (c,
   346                               map (type_from_fo_term tfrees) type_us))
   347           in list_comb (t, term_ts @ extra_ts) end
   348         | NONE => (* a free or schematic variable *)
   349           let
   350             val ts = map (aux NONE []) (us @ extra_us)
   351             val T = map fastype_of ts ---> HOLogic.typeT
   352             val t =
   353               case strip_prefix_and_unascii fixed_var_prefix a of
   354                 SOME b => Free (b, T)
   355               | NONE =>
   356                 case strip_prefix_and_unascii schematic_var_prefix a of
   357                   SOME b => Var ((b, 0), T)
   358                 | NONE =>
   359                   if is_atp_variable a then
   360                     Var ((repair_atp_variable_name Char.toLower a, 0), T)
   361                   else
   362                     (* Skolem constants? *)
   363                     Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   364           in list_comb (t, ts) end
   365   in aux (SOME HOLogic.boolT) [] end
   366 
   367 fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   368   if String.isPrefix class_prefix s then
   369     add_type_constraint (type_constraint_from_term pos tfrees u)
   370     #> pair @{const True}
   371   else
   372     pair (raw_term_from_pred thy full_types tfrees u)
   373 
   374 val combinator_table =
   375   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   376    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   377    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   378    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   379    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   380 
   381 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   382   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   383   | uncombine_term (t as Const (x as (s, _))) =
   384     (case AList.lookup (op =) combinator_table s of
   385        SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   386      | NONE => t)
   387   | uncombine_term t = t
   388 
   389 (* Update schematic type variables with detected sort constraints. It's not
   390    totally clear when this code is necessary. *)
   391 fun repair_tvar_sorts (t, tvar_tab) =
   392   let
   393     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   394       | do_type (TVar (xi, s)) =
   395         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   396       | do_type (TFree z) = TFree z
   397     fun do_term (Const (a, T)) = Const (a, do_type T)
   398       | do_term (Free (a, T)) = Free (a, do_type T)
   399       | do_term (Var (xi, T)) = Var (xi, do_type T)
   400       | do_term (t as Bound _) = t
   401       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   402       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   403   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   404 
   405 fun quantify_over_var quant_of var_s t =
   406   let
   407     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   408                   |> map Var
   409   in fold_rev quant_of vars t end
   410 
   411 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   412    appear in the formula. *)
   413 fun prop_from_formula thy full_types tfrees phi =
   414   let
   415     fun do_formula pos phi =
   416       case phi of
   417         AQuant (_, [], phi) => do_formula pos phi
   418       | AQuant (q, x :: xs, phi') =>
   419         do_formula pos (AQuant (q, xs, phi'))
   420         #>> quantify_over_var (case q of
   421                                  AForall => forall_of
   422                                | AExists => exists_of)
   423                               (repair_atp_variable_name Char.toLower x)
   424       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   425       | AConn (c, [phi1, phi2]) =>
   426         do_formula (pos |> c = AImplies ? not) phi1
   427         ##>> do_formula pos phi2
   428         #>> (case c of
   429                AAnd => s_conj
   430              | AOr => s_disj
   431              | AImplies => s_imp
   432              | AIf => s_imp o swap
   433              | AIff => s_iff
   434              | ANotIff => s_not o s_iff
   435              | _ => raise Fail "unexpected connective")
   436       | AAtom tm => term_from_pred thy full_types tfrees pos tm
   437       | _ => raise FORMULA [phi]
   438   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   439 
   440 fun check_formula ctxt =
   441   Type.constraint HOLogic.boolT
   442   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   443 
   444 
   445 (**** Translation of TSTP files to Isar Proofs ****)
   446 
   447 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   448   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   449 
   450 fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   451     let
   452       val thy = ProofContext.theory_of ctxt
   453       val t1 = prop_from_formula thy full_types tfrees phi1
   454       val vars = snd (strip_comb t1)
   455       val frees = map unvarify_term vars
   456       val unvarify_args = subst_atomic (vars ~~ frees)
   457       val t2 = prop_from_formula thy full_types tfrees phi2
   458       val (t1, t2) =
   459         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   460         |> unvarify_args |> uncombine_term |> check_formula ctxt
   461         |> HOLogic.dest_eq
   462     in
   463       (Definition (name, t1, t2),
   464        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   465     end
   466   | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   467     let
   468       val thy = ProofContext.theory_of ctxt
   469       val t = u |> prop_from_formula thy full_types tfrees
   470                 |> uncombine_term |> check_formula ctxt
   471     in
   472       (Inference (name, t, deps),
   473        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   474     end
   475 fun decode_lines ctxt full_types tfrees lines =
   476   fst (fold_map (decode_line full_types tfrees) lines ctxt)
   477 
   478 fun is_same_inference _ (Definition _) = false
   479   | is_same_inference t (Inference (_, t', _)) = t aconv t'
   480 
   481 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   482    clsarity). *)
   483 val is_only_type_information = curry (op aconv) HOLogic.true_const
   484 
   485 fun replace_one_dependency (old, new) dep =
   486   if is_same_step (dep, old) then new else [dep]
   487 fun replace_dependencies_in_line _ (line as Definition _) = line
   488   | replace_dependencies_in_line p (Inference (name, t, deps)) =
   489     Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   490 
   491 (* Discard facts; consolidate adjacent lines that prove the same formula, since
   492    they differ only in type information.*)
   493 fun add_line _ _ (line as Definition _) lines = line :: lines
   494   | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
   495     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   496        definitions. *)
   497     if is_fact fact_names name then
   498       (* Facts are not proof lines. *)
   499       if is_only_type_information t then
   500         map (replace_dependencies_in_line (name, [])) lines
   501       (* Is there a repetition? If so, replace later line by earlier one. *)
   502       else case take_prefix (not o is_same_inference t) lines of
   503         (_, []) => lines (* no repetition of proof line *)
   504       | (pre, Inference (name', _, _) :: post) =>
   505         pre @ map (replace_dependencies_in_line (name', [name])) post
   506       | _ => raise Fail "unexpected inference"
   507     else if is_conjecture conjecture_shape name then
   508       Inference (name, negate_term t, []) :: lines
   509     else
   510       map (replace_dependencies_in_line (name, [])) lines
   511   | add_line _ _ (Inference (name, t, deps)) lines =
   512     (* Type information will be deleted later; skip repetition test. *)
   513     if is_only_type_information t then
   514       Inference (name, t, deps) :: lines
   515     (* Is there a repetition? If so, replace later line by earlier one. *)
   516     else case take_prefix (not o is_same_inference t) lines of
   517       (* FIXME: Doesn't this code risk conflating proofs involving different
   518          types? *)
   519        (_, []) => Inference (name, t, deps) :: lines
   520      | (pre, Inference (name', t', _) :: post) =>
   521        Inference (name, t', deps) ::
   522        pre @ map (replace_dependencies_in_line (name', [name])) post
   523      | _ => raise Fail "unexpected inference"
   524 
   525 (* Recursively delete empty lines (type information) from the proof. *)
   526 fun add_nontrivial_line (Inference (name, t, [])) lines =
   527     if is_only_type_information t then delete_dependency name lines
   528     else Inference (name, t, []) :: lines
   529   | add_nontrivial_line line lines = line :: lines
   530 and delete_dependency name lines =
   531   fold_rev add_nontrivial_line
   532            (map (replace_dependencies_in_line (name, [])) lines) []
   533 
   534 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   535    offending lines often does the trick. *)
   536 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   537   | is_bad_free _ _ = false
   538 
   539 fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   540     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   541   | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
   542                      (Inference (name, t, deps)) (j, lines) =
   543     (j + 1,
   544      if is_fact fact_names name orelse
   545         is_conjecture conjecture_shape name orelse
   546         (* the last line must be kept *)
   547         j = 0 orelse
   548         (not (is_only_type_information t) andalso
   549          null (Term.add_tvars t []) andalso
   550          not (exists_subterm (is_bad_free frees) t) andalso
   551          length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   552          (* kill next to last line, which usually results in a trivial step *)
   553          j <> 1) then
   554        Inference (name, t, deps) :: lines  (* keep line *)
   555      else
   556        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   557 
   558 (** Isar proof construction and manipulation **)
   559 
   560 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   561   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   562 
   563 type label = string * int
   564 type facts = label list * string list
   565 
   566 datatype isar_qualifier = Show | Then | Moreover | Ultimately
   567 
   568 datatype isar_step =
   569   Fix of (string * typ) list |
   570   Let of term * term |
   571   Assume of label * term |
   572   Have of isar_qualifier list * label * term * byline
   573 and byline =
   574   ByMetis of facts |
   575   CaseSplit of isar_step list list * facts
   576 
   577 fun smart_case_split [] facts = ByMetis facts
   578   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   579 
   580 fun add_fact_from_dependency conjecture_shape fact_names name =
   581   if is_fact fact_names name then
   582     apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   583   else
   584     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   585 
   586 fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   587   | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   588     Assume (raw_label_for_name conjecture_shape name, t)
   589   | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   590     Have (if j = 1 then [Show] else [],
   591           raw_label_for_name conjecture_shape name,
   592           fold_rev forall_of (map Var (Term.add_vars t [])) t,
   593           ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   594                         deps ([], [])))
   595 
   596 fun repair_name "$true" = "c_True"
   597   | repair_name "$false" = "c_False"
   598   | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   599   | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   600   | repair_name s =
   601     if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   602       "c_equal" (* seen in Vampire proofs *)
   603     else
   604       s
   605 
   606 fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   607         isar_shrink_factor tstplike_proof conjecture_shape fact_names params
   608         frees =
   609   let
   610     val lines =
   611       tstplike_proof
   612       |> atp_proof_from_tstplike_string
   613       |> nasty_atp_proof pool
   614       |> map_term_names_in_atp_proof repair_name
   615       |> decode_lines ctxt full_types tfrees
   616       |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
   617       |> rpair [] |-> fold_rev add_nontrivial_line
   618       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   619                                              conjecture_shape fact_names frees)
   620       |> snd
   621   in
   622     (if null params then [] else [Fix params]) @
   623     map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   624          lines
   625   end
   626 
   627 (* When redirecting proofs, we keep information about the labels seen so far in
   628    the "backpatches" data structure. The first component indicates which facts
   629    should be associated with forthcoming proof steps. The second component is a
   630    pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   631    become assumptions and "drop_ls" are the labels that should be dropped in a
   632    case split. *)
   633 type backpatches = (label * facts) list * (label list * label list)
   634 
   635 fun used_labels_of_step (Have (_, _, _, by)) =
   636     (case by of
   637        ByMetis (ls, _) => ls
   638      | CaseSplit (proofs, (ls, _)) =>
   639        fold (union (op =) o used_labels_of) proofs ls)
   640   | used_labels_of_step _ = []
   641 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   642 
   643 fun new_labels_of_step (Fix _) = []
   644   | new_labels_of_step (Let _) = []
   645   | new_labels_of_step (Assume (l, _)) = [l]
   646   | new_labels_of_step (Have (_, l, _, _)) = [l]
   647 val new_labels_of = maps new_labels_of_step
   648 
   649 val join_proofs =
   650   let
   651     fun aux _ [] = NONE
   652       | aux proof_tail (proofs as (proof1 :: _)) =
   653         if exists null proofs then
   654           NONE
   655         else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   656           aux (hd proof1 :: proof_tail) (map tl proofs)
   657         else case hd proof1 of
   658           Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   659           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   660                       | _ => false) (tl proofs) andalso
   661              not (exists (member (op =) (maps new_labels_of proofs))
   662                          (used_labels_of proof_tail)) then
   663             SOME (l, t, map rev proofs, proof_tail)
   664           else
   665             NONE
   666         | _ => NONE
   667   in aux [] o map rev end
   668 
   669 fun case_split_qualifiers proofs =
   670   case length proofs of
   671     0 => []
   672   | 1 => [Then]
   673   | _ => [Ultimately]
   674 
   675 fun redirect_proof hyp_ts concl_t proof =
   676   let
   677     (* The first pass outputs those steps that are independent of the negated
   678        conjecture. The second pass flips the proof by contradiction to obtain a
   679        direct proof, introducing case splits when an inference depends on
   680        several facts that depend on the negated conjecture. *)
   681      val concl_l = (conjecture_prefix, length hyp_ts)
   682      fun first_pass ([], contra) = ([], contra)
   683        | first_pass ((step as Fix _) :: proof, contra) =
   684          first_pass (proof, contra) |>> cons step
   685        | first_pass ((step as Let _) :: proof, contra) =
   686          first_pass (proof, contra) |>> cons step
   687        | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   688          if l = concl_l then first_pass (proof, contra ||> cons step)
   689          else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   690        | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   691          let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   692            if exists (member (op =) (fst contra)) ls then
   693              first_pass (proof, contra |>> cons l ||> cons step)
   694            else
   695              first_pass (proof, contra) |>> cons step
   696          end
   697        | first_pass _ = raise Fail "malformed proof"
   698     val (proof_top, (contra_ls, contra_proof)) =
   699       first_pass (proof, ([concl_l], []))
   700     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   701     fun backpatch_labels patches ls =
   702       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   703     fun second_pass end_qs ([], assums, patches) =
   704         ([Have (end_qs, no_label, concl_t,
   705                 ByMetis (backpatch_labels patches (map snd assums)))], patches)
   706       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   707         second_pass end_qs (proof, (t, l) :: assums, patches)
   708       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   709                             patches) =
   710         (if member (op =) (snd (snd patches)) l andalso
   711             not (member (op =) (fst (snd patches)) l) andalso
   712             not (AList.defined (op =) (fst patches) l) then
   713            second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   714          else case List.partition (member (op =) contra_ls) ls of
   715            ([contra_l], co_ls) =>
   716            if member (op =) qs Show then
   717              second_pass end_qs (proof, assums,
   718                                  patches |>> cons (contra_l, (co_ls, ss)))
   719            else
   720              second_pass end_qs
   721                          (proof, assums,
   722                           patches |>> cons (contra_l, (l :: co_ls, ss)))
   723              |>> cons (if member (op =) (fst (snd patches)) l then
   724                          Assume (l, negate_term t)
   725                        else
   726                          Have (qs, l, negate_term t,
   727                                ByMetis (backpatch_label patches l)))
   728          | (contra_ls as _ :: _, co_ls) =>
   729            let
   730              val proofs =
   731                map_filter
   732                    (fn l =>
   733                        if l = concl_l then
   734                          NONE
   735                        else
   736                          let
   737                            val drop_ls = filter (curry (op <>) l) contra_ls
   738                          in
   739                            second_pass []
   740                                (proof, assums,
   741                                 patches ||> apfst (insert (op =) l)
   742                                         ||> apsnd (union (op =) drop_ls))
   743                            |> fst |> SOME
   744                          end) contra_ls
   745              val (assumes, facts) =
   746                if member (op =) (fst (snd patches)) l then
   747                  ([Assume (l, negate_term t)], (l :: co_ls, ss))
   748                else
   749                  ([], (co_ls, ss))
   750            in
   751              (case join_proofs proofs of
   752                 SOME (l, t, proofs, proof_tail) =>
   753                 Have (case_split_qualifiers proofs @
   754                       (if null proof_tail then end_qs else []), l, t,
   755                       smart_case_split proofs facts) :: proof_tail
   756               | NONE =>
   757                 [Have (case_split_qualifiers proofs @ end_qs, no_label,
   758                        concl_t, smart_case_split proofs facts)],
   759               patches)
   760              |>> append assumes
   761            end
   762          | _ => raise Fail "malformed proof")
   763        | second_pass _ _ = raise Fail "malformed proof"
   764     val proof_bottom =
   765       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   766   in proof_top @ proof_bottom end
   767 
   768 (* FIXME: Still needed? Probably not. *)
   769 val kill_duplicate_assumptions_in_proof =
   770   let
   771     fun relabel_facts subst =
   772       apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   773     fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   774         (case AList.lookup (op aconv) assums t of
   775            SOME l' => (proof, (l, l') :: subst, assums)
   776          | NONE => (step :: proof, subst, (t, l) :: assums))
   777       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   778         (Have (qs, l, t,
   779                case by of
   780                  ByMetis facts => ByMetis (relabel_facts subst facts)
   781                | CaseSplit (proofs, facts) =>
   782                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   783          proof, subst, assums)
   784       | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   785     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   786   in do_proof end
   787 
   788 val then_chain_proof =
   789   let
   790     fun aux _ [] = []
   791       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   792       | aux l' (Have (qs, l, t, by) :: proof) =
   793         (case by of
   794            ByMetis (ls, ss) =>
   795            Have (if member (op =) ls l' then
   796                    (Then :: qs, l, t,
   797                     ByMetis (filter_out (curry (op =) l') ls, ss))
   798                  else
   799                    (qs, l, t, ByMetis (ls, ss)))
   800          | CaseSplit (proofs, facts) =>
   801            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   802         aux l proof
   803       | aux _ (step :: proof) = step :: aux no_label proof
   804   in aux no_label end
   805 
   806 fun kill_useless_labels_in_proof proof =
   807   let
   808     val used_ls = used_labels_of proof
   809     fun do_label l = if member (op =) used_ls l then l else no_label
   810     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   811       | do_step (Have (qs, l, t, by)) =
   812         Have (qs, do_label l, t,
   813               case by of
   814                 CaseSplit (proofs, facts) =>
   815                 CaseSplit (map (map do_step) proofs, facts)
   816               | _ => by)
   817       | do_step step = step
   818   in map do_step proof end
   819 
   820 fun prefix_for_depth n = replicate_string (n + 1)
   821 
   822 val relabel_proof =
   823   let
   824     fun aux _ _ _ [] = []
   825       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   826         if l = no_label then
   827           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   828         else
   829           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   830             Assume (l', t) ::
   831             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   832           end
   833       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   834         let
   835           val (l', subst, next_fact) =
   836             if l = no_label then
   837               (l, subst, next_fact)
   838             else
   839               let
   840                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
   841               in (l', (l, l') :: subst, next_fact + 1) end
   842           val relabel_facts =
   843             apfst (maps (the_list o AList.lookup (op =) subst))
   844           val by =
   845             case by of
   846               ByMetis facts => ByMetis (relabel_facts facts)
   847             | CaseSplit (proofs, facts) =>
   848               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   849                          relabel_facts facts)
   850         in
   851           Have (qs, l', t, by) ::
   852           aux subst depth (next_assum, next_fact) proof
   853         end
   854       | aux subst depth nextp (step :: proof) =
   855         step :: aux subst depth nextp proof
   856   in aux [] 0 (1, 1) end
   857 
   858 fun string_for_proof ctxt0 full_types i n =
   859   let
   860     val ctxt = ctxt0
   861       |> Config.put show_free_types false
   862       |> Config.put show_types true
   863     fun fix_print_mode f x =
   864       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   865                                (print_mode_value ())) f x
   866     fun do_indent ind = replicate_string (ind * indent_size) " "
   867     fun do_free (s, T) =
   868       maybe_quote s ^ " :: " ^
   869       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   870     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   871     fun do_have qs =
   872       (if member (op =) qs Moreover then "moreover " else "") ^
   873       (if member (op =) qs Ultimately then "ultimately " else "") ^
   874       (if member (op =) qs Then then
   875          if member (op =) qs Show then "thus" else "hence"
   876        else
   877          if member (op =) qs Show then "show" else "have")
   878     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   879     fun do_facts (ls, ss) =
   880       metis_command full_types 1 1
   881                     (ls |> sort_distinct (prod_ord string_ord int_ord),
   882                      ss |> sort_distinct string_ord)
   883     and do_step ind (Fix xs) =
   884         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   885       | do_step ind (Let (t1, t2)) =
   886         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   887       | do_step ind (Assume (l, t)) =
   888         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   889       | do_step ind (Have (qs, l, t, ByMetis facts)) =
   890         do_indent ind ^ do_have qs ^ " " ^
   891         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   892       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   893         space_implode (do_indent ind ^ "moreover\n")
   894                       (map (do_block ind) proofs) ^
   895         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   896         do_facts facts ^ "\n"
   897     and do_steps prefix suffix ind steps =
   898       let val s = implode (map (do_step ind) steps) in
   899         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   900         String.extract (s, ind * indent_size,
   901                         SOME (size s - ind * indent_size - 1)) ^
   902         suffix ^ "\n"
   903       end
   904     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   905     (* One-step proofs are pointless; better use the Metis one-liner
   906        directly. *)
   907     and do_proof [Have (_, _, _, ByMetis _)] = ""
   908       | do_proof proof =
   909         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   910         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   911         (if n <> 1 then "next" else "qed")
   912   in do_proof end
   913 
   914 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   915                     (other_params as (_, full_types, _, tstplike_proof,
   916                                       fact_names, goal, i)) =
   917   let
   918     val (params, hyp_ts, concl_t) = strip_subgoal goal i
   919     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   920     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   921     val n = Logic.count_prems (prop_of goal)
   922     val (one_line_proof, lemma_names) = metis_proof_text other_params
   923     fun isar_proof_for () =
   924       case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   925                isar_shrink_factor tstplike_proof conjecture_shape fact_names
   926                params frees
   927            |> redirect_proof hyp_ts concl_t
   928            |> kill_duplicate_assumptions_in_proof
   929            |> then_chain_proof
   930            |> kill_useless_labels_in_proof
   931            |> relabel_proof
   932            |> string_for_proof ctxt full_types i n of
   933         "" => "\nNo structured proof available."
   934       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   935     val isar_proof =
   936       if debug then
   937         isar_proof_for ()
   938       else
   939         try isar_proof_for ()
   940         |> the_default "\nWarning: The Isar proof construction failed."
   941   in (one_line_proof ^ isar_proof, lemma_names) end
   942 
   943 fun proof_text isar_proof isar_params other_params =
   944   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   945       other_params
   946 
   947 end;