src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
author blanchet
Fri Oct 22 16:45:55 2010 +0200 (2010-10-22)
changeset 40074 87edcef4fab0
parent 40069 6f7bf79b1506
child 40114 acb75271cdce
permissions -rw-r--r--
compile
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_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_axiom_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 axioms 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   #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    85   #> fst
    86 
    87 fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    88                                             axiom_names =
    89   if String.isSubstring set_ClauseFormulaRelationN output then
    90     let
    91       val j0 = hd (hd conjecture_shape)
    92       val seq = extract_clause_sequence output
    93       val name_map = extract_clause_formula_relation output
    94       fun renumber_conjecture j =
    95         conjecture_prefix ^ string_of_int (j - j0)
    96         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
    97         |> map (fn s => find_index (curry (op =) s) seq + 1)
    98       fun names_for_number j =
    99         j |> AList.lookup (op =) name_map |> these
   100           |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   101           |> map (fn name =>
   102                      (name, name |> find_first_in_list_vector axiom_names
   103                                  |> 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, axiom_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_axiom axiom_names ((_, SOME s)) =
   143     (case strip_prefix_and_unascii axiom_prefix s of
   144        SOME s' => (case find_first_in_list_vector axiom_names s' of
   145                      SOME x => [(s', x)]
   146                    | NONE => [])
   147      | NONE => [])
   148   | resolve_axiom axiom_names (num, NONE) =
   149     case Int.fromString num of
   150       SOME j =>
   151       if j > 0 andalso j <= Vector.length axiom_names then
   152         Vector.sub (axiom_names, j - 1)
   153       else
   154         []
   155     | NONE => []
   156 
   157 fun add_fact axiom_names (Inference (name, _, [])) =
   158     append (resolve_axiom axiom_names name)
   159   | add_fact _ _ = I
   160 
   161 fun used_facts_in_tstplike_proof axiom_names =
   162   atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
   163 
   164 fun used_facts axiom_names =
   165   used_facts_in_tstplike_proof axiom_names
   166   #> List.partition (curry (op =) Chained o snd)
   167   #> pairself (sort_distinct (string_ord o pairself fst))
   168 
   169 fun metis_proof_text (banner, full_types, minimize_command,
   170                       tstplike_proof, axiom_names, goal, i) =
   171   let
   172     val (chained_lemmas, other_lemmas) =
   173       used_facts axiom_names tstplike_proof
   174     val n = Logic.count_prems (prop_of goal)
   175   in
   176     (metis_line banner full_types i n (map fst other_lemmas) ^
   177      minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   178      other_lemmas @ chained_lemmas)
   179   end
   180 
   181 
   182 (** Hard-core proof reconstruction: structured Isar proofs **)
   183 
   184 (* Simple simplifications to ensure that sort annotations don't leave a trail of
   185    spurious "True"s. *)
   186 fun s_not @{const False} = @{const True}
   187   | s_not @{const True} = @{const False}
   188   | s_not (@{const Not} $ t) = t
   189   | s_not t = @{const Not} $ t
   190 fun s_conj (@{const True}, t2) = t2
   191   | s_conj (t1, @{const True}) = t1
   192   | s_conj p = HOLogic.mk_conj p
   193 fun s_disj (@{const False}, t2) = t2
   194   | s_disj (t1, @{const False}) = t1
   195   | s_disj p = HOLogic.mk_disj p
   196 fun s_imp (@{const True}, t2) = t2
   197   | s_imp (t1, @{const False}) = s_not t1
   198   | s_imp p = HOLogic.mk_imp p
   199 fun s_iff (@{const True}, t2) = t2
   200   | s_iff (t1, @{const True}) = t1
   201   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   202 
   203 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   204 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   205 
   206 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   207     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   208   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   209     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   210   | negate_term (@{const HOL.implies} $ t1 $ t2) =
   211     @{const HOL.conj} $ t1 $ negate_term t2
   212   | negate_term (@{const HOL.conj} $ t1 $ t2) =
   213     @{const HOL.disj} $ negate_term t1 $ negate_term t2
   214   | negate_term (@{const HOL.disj} $ t1 $ t2) =
   215     @{const HOL.conj} $ negate_term t1 $ negate_term t2
   216   | negate_term (@{const Not} $ t) = t
   217   | negate_term t = @{const Not} $ t
   218 
   219 val indent_size = 2
   220 val no_label = ("", ~1)
   221 
   222 val raw_prefix = "X"
   223 val assum_prefix = "A"
   224 val fact_prefix = "F"
   225 
   226 fun resolve_conjecture conjecture_shape (num, s_opt) =
   227   let
   228     val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   229               SOME s => Int.fromString s |> the_default ~1
   230             | NONE => case Int.fromString num of
   231                         SOME j => find_index (exists (curry (op =) j))
   232                                              conjecture_shape
   233                       | NONE => ~1
   234   in if k >= 0 then [k] else [] end
   235 
   236 fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   237 fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   238 
   239 fun raw_label_for_name conjecture_shape name =
   240   case resolve_conjecture conjecture_shape name of
   241     [j] => (conjecture_prefix, j)
   242   | _ => case Int.fromString (fst name) of
   243            SOME j => (raw_prefix, j)
   244          | NONE => (raw_prefix ^ fst name, 0)
   245 
   246 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   247 
   248 exception FO_TERM of string fo_term list
   249 exception FORMULA of (string, string fo_term) formula list
   250 exception SAME of unit
   251 
   252 (* Type variables are given the basic sort "HOL.type". Some will later be
   253    constrained by information from type literals, or by type inference. *)
   254 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   255   let val Ts = map (type_from_fo_term tfrees) us in
   256     case strip_prefix_and_unascii type_const_prefix a of
   257       SOME b => Type (invert_const b, Ts)
   258     | NONE =>
   259       if not (null us) then
   260         raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   261       else case strip_prefix_and_unascii tfree_prefix a of
   262         SOME b =>
   263         let val s = "'" ^ b in
   264           TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   265         end
   266       | NONE =>
   267         case strip_prefix_and_unascii tvar_prefix a of
   268           SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   269         | NONE =>
   270           (* Variable from the ATP, say "X1" *)
   271           Type_Infer.param 0 (a, HOLogic.typeS)
   272   end
   273 
   274 (* Type class literal applied to a type. Returns triple of polarity, class,
   275    type. *)
   276 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   277   case (strip_prefix_and_unascii class_prefix a,
   278         map (type_from_fo_term tfrees) us) of
   279     (SOME b, [T]) => (pos, b, T)
   280   | _ => raise FO_TERM [u]
   281 
   282 (** Accumulate type constraints in a formula: negative type literals **)
   283 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   284 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   285   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   286   | add_type_constraint _ = I
   287 
   288 fun repair_atp_variable_name f s =
   289   let
   290     fun subscript_name s n = s ^ nat_subscript n
   291     val s = String.map f s
   292   in
   293     case space_explode "_" s of
   294       [_] => (case take_suffix Char.isDigit (String.explode s) of
   295                 (cs1 as _ :: _, cs2 as _ :: _) =>
   296                 subscript_name (String.implode cs1)
   297                                (the (Int.fromString (String.implode cs2)))
   298               | (_, _) => s)
   299     | [s1, s2] => (case Int.fromString s2 of
   300                      SOME n => subscript_name s1 n
   301                    | NONE => s)
   302     | _ => s
   303   end
   304 
   305 (* First-order translation. No types are known for variables. "HOLogic.typeT"
   306    should allow them to be inferred. *)
   307 fun raw_term_from_pred thy full_types tfrees =
   308   let
   309     fun aux opt_T extra_us u =
   310       case u of
   311         ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   312       | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   313       | ATerm (a, us) =>
   314         if a = type_wrapper_name then
   315           case us of
   316             [typ_u, term_u] =>
   317             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   318           | _ => raise FO_TERM us
   319         else case strip_prefix_and_unascii const_prefix a of
   320           SOME "equal" =>
   321           let val ts = map (aux NONE []) us in
   322             if length ts = 2 andalso hd ts aconv List.last ts then
   323               (* Vampire is keen on producing these. *)
   324               @{const True}
   325             else
   326               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   327           end
   328         | SOME b =>
   329           let
   330             val c = invert_const b
   331             val num_type_args = num_type_args thy c
   332             val (type_us, term_us) =
   333               chop (if full_types then 0 else num_type_args) us
   334             (* Extra args from "hAPP" come after any arguments given directly to
   335                the constant. *)
   336             val term_ts = map (aux NONE []) term_us
   337             val extra_ts = map (aux NONE []) extra_us
   338             val t =
   339               Const (c, if full_types then
   340                           case opt_T of
   341                             SOME T => map fastype_of term_ts ---> T
   342                           | NONE =>
   343                             if num_type_args = 0 then
   344                               Sign.const_instance thy (c, [])
   345                             else
   346                               raise Fail ("no type information for " ^ quote c)
   347                         else
   348                           Sign.const_instance thy (c,
   349                               map (type_from_fo_term tfrees) type_us))
   350           in list_comb (t, term_ts @ extra_ts) end
   351         | NONE => (* a free or schematic variable *)
   352           let
   353             val ts = map (aux NONE []) (us @ extra_us)
   354             val T = map fastype_of ts ---> HOLogic.typeT
   355             val t =
   356               case strip_prefix_and_unascii fixed_var_prefix a of
   357                 SOME b => Free (b, T)
   358               | NONE =>
   359                 case strip_prefix_and_unascii schematic_var_prefix a of
   360                   SOME b => Var ((b, 0), T)
   361                 | NONE =>
   362                   if is_atp_variable a then
   363                     Var ((repair_atp_variable_name Char.toLower a, 0), T)
   364                   else
   365                     (* Skolem constants? *)
   366                     Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   367           in list_comb (t, ts) end
   368   in aux (SOME HOLogic.boolT) [] end
   369 
   370 fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   371   if String.isPrefix class_prefix s then
   372     add_type_constraint (type_constraint_from_term pos tfrees u)
   373     #> pair @{const True}
   374   else
   375     pair (raw_term_from_pred thy full_types tfrees u)
   376 
   377 val combinator_table =
   378   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   379    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   380    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   381    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   382    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   383 
   384 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   385   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   386   | uncombine_term (t as Const (x as (s, _))) =
   387     (case AList.lookup (op =) combinator_table s of
   388        SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   389      | NONE => t)
   390   | uncombine_term t = t
   391 
   392 (* Update schematic type variables with detected sort constraints. It's not
   393    totally clear when this code is necessary. *)
   394 fun repair_tvar_sorts (t, tvar_tab) =
   395   let
   396     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   397       | do_type (TVar (xi, s)) =
   398         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   399       | do_type (TFree z) = TFree z
   400     fun do_term (Const (a, T)) = Const (a, do_type T)
   401       | do_term (Free (a, T)) = Free (a, do_type T)
   402       | do_term (Var (xi, T)) = Var (xi, do_type T)
   403       | do_term (t as Bound _) = t
   404       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   405       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   406   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   407 
   408 fun quantify_over_var quant_of var_s t =
   409   let
   410     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   411                   |> map Var
   412   in fold_rev quant_of vars t end
   413 
   414 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   415    appear in the formula. *)
   416 fun prop_from_formula thy full_types tfrees phi =
   417   let
   418     fun do_formula pos phi =
   419       case phi of
   420         AQuant (_, [], phi) => do_formula pos phi
   421       | AQuant (q, x :: xs, phi') =>
   422         do_formula pos (AQuant (q, xs, phi'))
   423         #>> quantify_over_var (case q of
   424                                  AForall => forall_of
   425                                | AExists => exists_of)
   426                               (repair_atp_variable_name Char.toLower x)
   427       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   428       | AConn (c, [phi1, phi2]) =>
   429         do_formula (pos |> c = AImplies ? not) phi1
   430         ##>> do_formula pos phi2
   431         #>> (case c of
   432                AAnd => s_conj
   433              | AOr => s_disj
   434              | AImplies => s_imp
   435              | AIf => s_imp o swap
   436              | AIff => s_iff
   437              | ANotIff => s_not o s_iff
   438              | _ => raise Fail "unexpected connective")
   439       | AAtom tm => term_from_pred thy full_types tfrees pos tm
   440       | _ => raise FORMULA [phi]
   441   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   442 
   443 fun check_formula ctxt =
   444   Type.constraint HOLogic.boolT
   445   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   446 
   447 
   448 (**** Translation of TSTP files to Isar Proofs ****)
   449 
   450 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   451   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   452 
   453 fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   454     let
   455       val thy = ProofContext.theory_of ctxt
   456       val t1 = prop_from_formula thy full_types tfrees phi1
   457       val vars = snd (strip_comb t1)
   458       val frees = map unvarify_term vars
   459       val unvarify_args = subst_atomic (vars ~~ frees)
   460       val t2 = prop_from_formula thy full_types tfrees phi2
   461       val (t1, t2) =
   462         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   463         |> unvarify_args |> uncombine_term |> check_formula ctxt
   464         |> HOLogic.dest_eq
   465     in
   466       (Definition (name, t1, t2),
   467        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   468     end
   469   | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   470     let
   471       val thy = ProofContext.theory_of ctxt
   472       val t = u |> prop_from_formula thy full_types tfrees
   473                 |> uncombine_term |> check_formula ctxt
   474     in
   475       (Inference (name, t, deps),
   476        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   477     end
   478 fun decode_lines ctxt full_types tfrees lines =
   479   fst (fold_map (decode_line full_types tfrees) lines ctxt)
   480 
   481 fun is_same_inference _ (Definition _) = false
   482   | is_same_inference t (Inference (_, t', _)) = t aconv t'
   483 
   484 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   485    clsarity). *)
   486 val is_only_type_information = curry (op aconv) HOLogic.true_const
   487 
   488 fun replace_one_dependency (old, new) dep =
   489   if is_same_step (dep, old) then new else [dep]
   490 fun replace_dependencies_in_line _ (line as Definition _) = line
   491   | replace_dependencies_in_line p (Inference (name, t, deps)) =
   492     Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   493 
   494 (* Discard axioms; consolidate adjacent lines that prove the same formula, since
   495    they differ only in type information.*)
   496 fun add_line _ _ (line as Definition _) lines = line :: lines
   497   | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   498     (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   499        definitions. *)
   500     if is_axiom axiom_names name then
   501       (* Axioms are not proof lines. *)
   502       if is_only_type_information t then
   503         map (replace_dependencies_in_line (name, [])) lines
   504       (* Is there a repetition? If so, replace later line by earlier one. *)
   505       else case take_prefix (not o is_same_inference t) lines of
   506         (_, []) => lines (* no repetition of proof line *)
   507       | (pre, Inference (name', _, _) :: post) =>
   508         pre @ map (replace_dependencies_in_line (name', [name])) post
   509       | _ => raise Fail "unexpected inference"
   510     else if is_conjecture conjecture_shape name then
   511       Inference (name, negate_term t, []) :: lines
   512     else
   513       map (replace_dependencies_in_line (name, [])) lines
   514   | add_line _ _ (Inference (name, t, deps)) lines =
   515     (* Type information will be deleted later; skip repetition test. *)
   516     if is_only_type_information t then
   517       Inference (name, t, deps) :: lines
   518     (* Is there a repetition? If so, replace later line by earlier one. *)
   519     else case take_prefix (not o is_same_inference t) lines of
   520       (* FIXME: Doesn't this code risk conflating proofs involving different
   521          types? *)
   522        (_, []) => Inference (name, t, deps) :: lines
   523      | (pre, Inference (name', t', _) :: post) =>
   524        Inference (name, t', deps) ::
   525        pre @ map (replace_dependencies_in_line (name', [name])) post
   526      | _ => raise Fail "unexpected inference"
   527 
   528 (* Recursively delete empty lines (type information) from the proof. *)
   529 fun add_nontrivial_line (Inference (name, t, [])) lines =
   530     if is_only_type_information t then delete_dependency name lines
   531     else Inference (name, t, []) :: lines
   532   | add_nontrivial_line line lines = line :: lines
   533 and delete_dependency name lines =
   534   fold_rev add_nontrivial_line
   535            (map (replace_dependencies_in_line (name, [])) lines) []
   536 
   537 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   538    offending lines often does the trick. *)
   539 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   540   | is_bad_free _ _ = false
   541 
   542 fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   543     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   544   | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   545                      (Inference (name, t, deps)) (j, lines) =
   546     (j + 1,
   547      if is_axiom axiom_names name orelse
   548         is_conjecture conjecture_shape name orelse
   549         (* the last line must be kept *)
   550         j = 0 orelse
   551         (not (is_only_type_information t) andalso
   552          null (Term.add_tvars t []) andalso
   553          not (exists_subterm (is_bad_free frees) t) andalso
   554          length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   555          (* kill next to last line, which usually results in a trivial step *)
   556          j <> 1) then
   557        Inference (name, t, deps) :: lines  (* keep line *)
   558      else
   559        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   560 
   561 (** Isar proof construction and manipulation **)
   562 
   563 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   564   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   565 
   566 type label = string * int
   567 type facts = label list * string list
   568 
   569 datatype isar_qualifier = Show | Then | Moreover | Ultimately
   570 
   571 datatype isar_step =
   572   Fix of (string * typ) list |
   573   Let of term * term |
   574   Assume of label * term |
   575   Have of isar_qualifier list * label * term * byline
   576 and byline =
   577   ByMetis of facts |
   578   CaseSplit of isar_step list list * facts
   579 
   580 fun smart_case_split [] facts = ByMetis facts
   581   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   582 
   583 fun add_fact_from_dependency conjecture_shape axiom_names name =
   584   if is_axiom axiom_names name then
   585     apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   586   else
   587     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   588 
   589 fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   590   | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   591     Assume (raw_label_for_name conjecture_shape name, t)
   592   | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   593     Have (if j = 1 then [Show] else [],
   594           raw_label_for_name conjecture_shape name,
   595           fold_rev forall_of (map Var (Term.add_vars t [])) t,
   596           ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   597                         deps ([], [])))
   598 
   599 fun repair_name "$true" = "c_True"
   600   | repair_name "$false" = "c_False"
   601   | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   602   | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   603   | repair_name s =
   604     if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   605       "c_equal" (* seen in Vampire proofs *)
   606     else
   607       s
   608 
   609 fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   610         tstplike_proof conjecture_shape axiom_names params 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 axiom_names)
   619       |> rpair [] |-> fold_rev add_nontrivial_line
   620       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   621                                              conjecture_shape axiom_names frees)
   622       |> snd
   623   in
   624     (if null params then [] else [Fix params]) @
   625     map2 (step_for_line conjecture_shape axiom_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                     (other_params as (_, full_types, _, tstplike_proof,
   918                                       axiom_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 other_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 axiom_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 other_params =
   946   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   947       other_params
   948 
   949 end;