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