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