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