src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
author wenzelm
Sat Apr 16 16:15:37 2011 +0200 (2011-04-16)
changeset 42361 23f352990944
parent 42227 662b50b7126f
child 42449 494e4ac5b0f8
permissions -rw-r--r--
modernized structure Proof_Context;
     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, mangled_us) = b |> unmangled_const |>> invert_const
   349             val num_ty_args = num_atp_type_args thy type_sys c
   350             val (type_us, term_us) = chop num_ty_args us |>> append mangled_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               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 (Const (c, 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
   403                        |> Logic.dest_equals |> snd
   404      | NONE => t)
   405   | uncombine_term t = t
   406 
   407 (* Update schematic type variables with detected sort constraints. It's not
   408    totally clear when this code is necessary. *)
   409 fun repair_tvar_sorts (t, tvar_tab) =
   410   let
   411     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   412       | do_type (TVar (xi, s)) =
   413         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   414       | do_type (TFree z) = TFree z
   415     fun do_term (Const (a, T)) = Const (a, do_type T)
   416       | do_term (Free (a, T)) = Free (a, do_type T)
   417       | do_term (Var (xi, T)) = Var (xi, do_type T)
   418       | do_term (t as Bound _) = t
   419       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   420       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   421   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   422 
   423 fun quantify_over_var quant_of var_s t =
   424   let
   425     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   426                   |> map Var
   427   in fold_rev quant_of vars t end
   428 
   429 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   430    appear in the formula. *)
   431 fun prop_from_formula thy type_sys tfrees phi =
   432   let
   433     fun do_formula pos phi =
   434       case phi of
   435         AQuant (_, [], phi) => do_formula pos phi
   436       | AQuant (q, x :: xs, phi') =>
   437         do_formula pos (AQuant (q, xs, phi'))
   438         #>> quantify_over_var (case q of
   439                                  AForall => forall_of
   440                                | AExists => exists_of)
   441                               (repair_atp_variable_name Char.toLower x)
   442       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   443       | AConn (c, [phi1, phi2]) =>
   444         do_formula (pos |> c = AImplies ? not) phi1
   445         ##>> do_formula pos phi2
   446         #>> (case c of
   447                AAnd => s_conj
   448              | AOr => s_disj
   449              | AImplies => s_imp
   450              | AIf => s_imp o swap
   451              | AIff => s_iff
   452              | ANotIff => s_not o s_iff
   453              | _ => raise Fail "unexpected connective")
   454       | AAtom tm => term_from_pred thy type_sys tfrees pos tm
   455       | _ => raise FORMULA [phi]
   456   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   457 
   458 fun check_formula ctxt =
   459   Type.constraint HOLogic.boolT
   460   #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
   461 
   462 
   463 (**** Translation of TSTP files to Isar Proofs ****)
   464 
   465 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   466   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   467 
   468 fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt =
   469     let
   470       val thy = Proof_Context.theory_of ctxt
   471       val t1 = prop_from_formula thy type_sys tfrees phi1
   472       val vars = snd (strip_comb t1)
   473       val frees = map unvarify_term vars
   474       val unvarify_args = subst_atomic (vars ~~ frees)
   475       val t2 = prop_from_formula thy type_sys tfrees phi2
   476       val (t1, t2) =
   477         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   478         |> unvarify_args |> uncombine_term |> check_formula ctxt
   479         |> HOLogic.dest_eq
   480     in
   481       (Definition (name, t1, t2),
   482        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   483     end
   484   | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt =
   485     let
   486       val thy = Proof_Context.theory_of ctxt
   487       val t = u |> prop_from_formula thy type_sys tfrees
   488                 |> uncombine_term |> check_formula ctxt
   489     in
   490       (Inference (name, t, deps),
   491        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   492     end
   493 fun decode_lines ctxt type_sys tfrees lines =
   494   fst (fold_map (decode_line type_sys tfrees) lines ctxt)
   495 
   496 fun is_same_inference _ (Definition _) = false
   497   | is_same_inference t (Inference (_, t', _)) = t aconv t'
   498 
   499 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   500    clsarity). *)
   501 val is_only_type_information = curry (op aconv) HOLogic.true_const
   502 
   503 fun replace_one_dependency (old, new) dep =
   504   if is_same_step (dep, old) then new else [dep]
   505 fun replace_dependencies_in_line _ (line as Definition _) = line
   506   | replace_dependencies_in_line p (Inference (name, t, deps)) =
   507     Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   508 
   509 (* Discard facts; consolidate adjacent lines that prove the same formula, since
   510    they differ only in type information.*)
   511 fun add_line _ _ (line as Definition _) lines = line :: lines
   512   | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
   513     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   514        definitions. *)
   515     if is_fact fact_names name then
   516       (* Facts are not proof lines. *)
   517       if is_only_type_information t then
   518         map (replace_dependencies_in_line (name, [])) lines
   519       (* Is there a repetition? If so, replace later line by earlier one. *)
   520       else case take_prefix (not o is_same_inference t) lines of
   521         (_, []) => lines (* no repetition of proof line *)
   522       | (pre, Inference (name', _, _) :: post) =>
   523         pre @ map (replace_dependencies_in_line (name', [name])) post
   524       | _ => raise Fail "unexpected inference"
   525     else if is_conjecture conjecture_shape name then
   526       Inference (name, negate_term t, []) :: lines
   527     else
   528       map (replace_dependencies_in_line (name, [])) lines
   529   | add_line _ _ (Inference (name, t, deps)) lines =
   530     (* Type information will be deleted later; skip repetition test. *)
   531     if is_only_type_information t then
   532       Inference (name, t, deps) :: lines
   533     (* Is there a repetition? If so, replace later line by earlier one. *)
   534     else case take_prefix (not o is_same_inference t) lines of
   535       (* FIXME: Doesn't this code risk conflating proofs involving different
   536          types? *)
   537        (_, []) => Inference (name, t, deps) :: lines
   538      | (pre, Inference (name', t', _) :: post) =>
   539        Inference (name, t', deps) ::
   540        pre @ map (replace_dependencies_in_line (name', [name])) post
   541      | _ => raise Fail "unexpected inference"
   542 
   543 (* Recursively delete empty lines (type information) from the proof. *)
   544 fun add_nontrivial_line (Inference (name, t, [])) lines =
   545     if is_only_type_information t then delete_dependency name lines
   546     else Inference (name, t, []) :: lines
   547   | add_nontrivial_line line lines = line :: lines
   548 and delete_dependency name lines =
   549   fold_rev add_nontrivial_line
   550            (map (replace_dependencies_in_line (name, [])) lines) []
   551 
   552 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   553    offending lines often does the trick. *)
   554 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   555   | is_bad_free _ _ = false
   556 
   557 fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   558     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   559   | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
   560                      (Inference (name, t, deps)) (j, lines) =
   561     (j + 1,
   562      if is_fact fact_names name orelse
   563         is_conjecture conjecture_shape name orelse
   564         (* the last line must be kept *)
   565         j = 0 orelse
   566         (not (is_only_type_information t) andalso
   567          null (Term.add_tvars t []) andalso
   568          not (exists_subterm (is_bad_free frees) t) andalso
   569          length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   570          (* kill next to last line, which usually results in a trivial step *)
   571          j <> 1) then
   572        Inference (name, t, deps) :: lines  (* keep line *)
   573      else
   574        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   575 
   576 (** Isar proof construction and manipulation **)
   577 
   578 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   579   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   580 
   581 type label = string * int
   582 type facts = label list * string list
   583 
   584 datatype isar_qualifier = Show | Then | Moreover | Ultimately
   585 
   586 datatype isar_step =
   587   Fix of (string * typ) list |
   588   Let of term * term |
   589   Assume of label * term |
   590   Have of isar_qualifier list * label * term * byline
   591 and byline =
   592   ByMetis of facts |
   593   CaseSplit of isar_step list list * facts
   594 
   595 fun smart_case_split [] facts = ByMetis facts
   596   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   597 
   598 fun add_fact_from_dependency conjecture_shape fact_names name =
   599   if is_fact fact_names name then
   600     apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   601   else
   602     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   603 
   604 fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   605   | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   606     Assume (raw_label_for_name conjecture_shape name, t)
   607   | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   608     Have (if j = 1 then [Show] else [],
   609           raw_label_for_name conjecture_shape name,
   610           fold_rev forall_of (map Var (Term.add_vars t [])) t,
   611           ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   612                         deps ([], [])))
   613 
   614 fun repair_name "$true" = "c_True"
   615   | repair_name "$false" = "c_False"
   616   | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   617   | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   618   | repair_name s =
   619     if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   620       "c_equal" (* seen in Vampire proofs *)
   621     else
   622       s
   623 
   624 fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
   625         tstplike_proof conjecture_shape fact_names params frees =
   626   let
   627     val lines =
   628       tstplike_proof
   629       |> atp_proof_from_tstplike_string true
   630       |> nasty_atp_proof pool
   631       |> map_term_names_in_atp_proof repair_name
   632       |> decode_lines ctxt type_sys tfrees
   633       |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
   634       |> rpair [] |-> fold_rev add_nontrivial_line
   635       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   636                                              conjecture_shape fact_names frees)
   637       |> snd
   638   in
   639     (if null params then [] else [Fix params]) @
   640     map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   641          lines
   642   end
   643 
   644 (* When redirecting proofs, we keep information about the labels seen so far in
   645    the "backpatches" data structure. The first component indicates which facts
   646    should be associated with forthcoming proof steps. The second component is a
   647    pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   648    become assumptions and "drop_ls" are the labels that should be dropped in a
   649    case split. *)
   650 type backpatches = (label * facts) list * (label list * label list)
   651 
   652 fun used_labels_of_step (Have (_, _, _, by)) =
   653     (case by of
   654        ByMetis (ls, _) => ls
   655      | CaseSplit (proofs, (ls, _)) =>
   656        fold (union (op =) o used_labels_of) proofs ls)
   657   | used_labels_of_step _ = []
   658 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   659 
   660 fun new_labels_of_step (Fix _) = []
   661   | new_labels_of_step (Let _) = []
   662   | new_labels_of_step (Assume (l, _)) = [l]
   663   | new_labels_of_step (Have (_, l, _, _)) = [l]
   664 val new_labels_of = maps new_labels_of_step
   665 
   666 val join_proofs =
   667   let
   668     fun aux _ [] = NONE
   669       | aux proof_tail (proofs as (proof1 :: _)) =
   670         if exists null proofs then
   671           NONE
   672         else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   673           aux (hd proof1 :: proof_tail) (map tl proofs)
   674         else case hd proof1 of
   675           Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   676           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   677                       | _ => false) (tl proofs) andalso
   678              not (exists (member (op =) (maps new_labels_of proofs))
   679                          (used_labels_of proof_tail)) then
   680             SOME (l, t, map rev proofs, proof_tail)
   681           else
   682             NONE
   683         | _ => NONE
   684   in aux [] o map rev end
   685 
   686 fun case_split_qualifiers proofs =
   687   case length proofs of
   688     0 => []
   689   | 1 => [Then]
   690   | _ => [Ultimately]
   691 
   692 fun redirect_proof hyp_ts concl_t proof =
   693   let
   694     (* The first pass outputs those steps that are independent of the negated
   695        conjecture. The second pass flips the proof by contradiction to obtain a
   696        direct proof, introducing case splits when an inference depends on
   697        several facts that depend on the negated conjecture. *)
   698      val concl_l = (conjecture_prefix, length hyp_ts)
   699      fun first_pass ([], contra) = ([], contra)
   700        | first_pass ((step as Fix _) :: proof, contra) =
   701          first_pass (proof, contra) |>> cons step
   702        | first_pass ((step as Let _) :: proof, contra) =
   703          first_pass (proof, contra) |>> cons step
   704        | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   705          if l = concl_l then first_pass (proof, contra ||> cons step)
   706          else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   707        | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   708          let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   709            if exists (member (op =) (fst contra)) ls then
   710              first_pass (proof, contra |>> cons l ||> cons step)
   711            else
   712              first_pass (proof, contra) |>> cons step
   713          end
   714        | first_pass _ = raise Fail "malformed proof"
   715     val (proof_top, (contra_ls, contra_proof)) =
   716       first_pass (proof, ([concl_l], []))
   717     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   718     fun backpatch_labels patches ls =
   719       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   720     fun second_pass end_qs ([], assums, patches) =
   721         ([Have (end_qs, no_label, concl_t,
   722                 ByMetis (backpatch_labels patches (map snd assums)))], patches)
   723       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   724         second_pass end_qs (proof, (t, l) :: assums, patches)
   725       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   726                             patches) =
   727         (if member (op =) (snd (snd patches)) l andalso
   728             not (member (op =) (fst (snd patches)) l) andalso
   729             not (AList.defined (op =) (fst patches) l) then
   730            second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   731          else case List.partition (member (op =) contra_ls) ls of
   732            ([contra_l], co_ls) =>
   733            if member (op =) qs Show then
   734              second_pass end_qs (proof, assums,
   735                                  patches |>> cons (contra_l, (co_ls, ss)))
   736            else
   737              second_pass end_qs
   738                          (proof, assums,
   739                           patches |>> cons (contra_l, (l :: co_ls, ss)))
   740              |>> cons (if member (op =) (fst (snd patches)) l then
   741                          Assume (l, negate_term t)
   742                        else
   743                          Have (qs, l, negate_term t,
   744                                ByMetis (backpatch_label patches l)))
   745          | (contra_ls as _ :: _, co_ls) =>
   746            let
   747              val proofs =
   748                map_filter
   749                    (fn l =>
   750                        if l = concl_l then
   751                          NONE
   752                        else
   753                          let
   754                            val drop_ls = filter (curry (op <>) l) contra_ls
   755                          in
   756                            second_pass []
   757                                (proof, assums,
   758                                 patches ||> apfst (insert (op =) l)
   759                                         ||> apsnd (union (op =) drop_ls))
   760                            |> fst |> SOME
   761                          end) contra_ls
   762              val (assumes, facts) =
   763                if member (op =) (fst (snd patches)) l then
   764                  ([Assume (l, negate_term t)], (l :: co_ls, ss))
   765                else
   766                  ([], (co_ls, ss))
   767            in
   768              (case join_proofs proofs of
   769                 SOME (l, t, proofs, proof_tail) =>
   770                 Have (case_split_qualifiers proofs @
   771                       (if null proof_tail then end_qs else []), l, t,
   772                       smart_case_split proofs facts) :: proof_tail
   773               | NONE =>
   774                 [Have (case_split_qualifiers proofs @ end_qs, no_label,
   775                        concl_t, smart_case_split proofs facts)],
   776               patches)
   777              |>> append assumes
   778            end
   779          | _ => raise Fail "malformed proof")
   780        | second_pass _ _ = raise Fail "malformed proof"
   781     val proof_bottom =
   782       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   783   in proof_top @ proof_bottom end
   784 
   785 (* FIXME: Still needed? Probably not. *)
   786 val kill_duplicate_assumptions_in_proof =
   787   let
   788     fun relabel_facts subst =
   789       apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   790     fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   791         (case AList.lookup (op aconv) assums t of
   792            SOME l' => (proof, (l, l') :: subst, assums)
   793          | NONE => (step :: proof, subst, (t, l) :: assums))
   794       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   795         (Have (qs, l, t,
   796                case by of
   797                  ByMetis facts => ByMetis (relabel_facts subst facts)
   798                | CaseSplit (proofs, facts) =>
   799                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   800          proof, subst, assums)
   801       | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   802     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   803   in do_proof end
   804 
   805 val then_chain_proof =
   806   let
   807     fun aux _ [] = []
   808       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   809       | aux l' (Have (qs, l, t, by) :: proof) =
   810         (case by of
   811            ByMetis (ls, ss) =>
   812            Have (if member (op =) ls l' then
   813                    (Then :: qs, l, t,
   814                     ByMetis (filter_out (curry (op =) l') ls, ss))
   815                  else
   816                    (qs, l, t, ByMetis (ls, ss)))
   817          | CaseSplit (proofs, facts) =>
   818            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   819         aux l proof
   820       | aux _ (step :: proof) = step :: aux no_label proof
   821   in aux no_label end
   822 
   823 fun kill_useless_labels_in_proof proof =
   824   let
   825     val used_ls = used_labels_of proof
   826     fun do_label l = if member (op =) used_ls l then l else no_label
   827     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   828       | do_step (Have (qs, l, t, by)) =
   829         Have (qs, do_label l, t,
   830               case by of
   831                 CaseSplit (proofs, facts) =>
   832                 CaseSplit (map (map do_step) proofs, facts)
   833               | _ => by)
   834       | do_step step = step
   835   in map do_step proof end
   836 
   837 fun prefix_for_depth n = replicate_string (n + 1)
   838 
   839 val relabel_proof =
   840   let
   841     fun aux _ _ _ [] = []
   842       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   843         if l = no_label then
   844           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   845         else
   846           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   847             Assume (l', t) ::
   848             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   849           end
   850       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   851         let
   852           val (l', subst, next_fact) =
   853             if l = no_label then
   854               (l, subst, next_fact)
   855             else
   856               let
   857                 val l' = (prefix_for_depth depth have_prefix, next_fact)
   858               in (l', (l, l') :: subst, next_fact + 1) end
   859           val relabel_facts =
   860             apfst (maps (the_list o AList.lookup (op =) subst))
   861           val by =
   862             case by of
   863               ByMetis facts => ByMetis (relabel_facts facts)
   864             | CaseSplit (proofs, facts) =>
   865               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   866                          relabel_facts facts)
   867         in
   868           Have (qs, l', t, by) ::
   869           aux subst depth (next_assum, next_fact) proof
   870         end
   871       | aux subst depth nextp (step :: proof) =
   872         step :: aux subst depth nextp proof
   873   in aux [] 0 (1, 1) end
   874 
   875 fun string_for_proof ctxt0 type_sys i n =
   876   let
   877     val ctxt = ctxt0
   878       |> Config.put show_free_types false
   879       |> Config.put show_types true
   880     fun fix_print_mode f x =
   881       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   882                                (print_mode_value ())) f x
   883     fun do_indent ind = replicate_string (ind * indent_size) " "
   884     fun do_free (s, T) =
   885       maybe_quote s ^ " :: " ^
   886       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   887     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   888     fun do_have qs =
   889       (if member (op =) qs Moreover then "moreover " else "") ^
   890       (if member (op =) qs Ultimately then "ultimately " else "") ^
   891       (if member (op =) qs Then then
   892          if member (op =) qs Show then "thus" else "hence"
   893        else
   894          if member (op =) qs Show then "show" else "have")
   895     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   896     fun do_facts (ls, ss) =
   897       metis_command type_sys 1 1
   898                     (ls |> sort_distinct (prod_ord string_ord int_ord),
   899                      ss |> sort_distinct string_ord)
   900     and do_step ind (Fix xs) =
   901         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   902       | do_step ind (Let (t1, t2)) =
   903         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   904       | do_step ind (Assume (l, t)) =
   905         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   906       | do_step ind (Have (qs, l, t, ByMetis facts)) =
   907         do_indent ind ^ do_have qs ^ " " ^
   908         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   909       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   910         space_implode (do_indent ind ^ "moreover\n")
   911                       (map (do_block ind) proofs) ^
   912         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   913         do_facts facts ^ "\n"
   914     and do_steps prefix suffix ind steps =
   915       let val s = implode (map (do_step ind) steps) in
   916         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   917         String.extract (s, ind * indent_size,
   918                         SOME (size s - ind * indent_size - 1)) ^
   919         suffix ^ "\n"
   920       end
   921     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   922     (* One-step proofs are pointless; better use the Metis one-liner
   923        directly. *)
   924     and do_proof [Have (_, _, _, ByMetis _)] = ""
   925       | do_proof proof =
   926         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   927         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   928         (if n <> 1 then "next" else "qed")
   929   in do_proof end
   930 
   931 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   932                     (metis_params as (_, type_sys, _, tstplike_proof,
   933                                       fact_names, goal, i)) =
   934   let
   935     val (params, hyp_ts, concl_t) = strip_subgoal goal i
   936     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   937     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   938     val n = Logic.count_prems (prop_of goal)
   939     val (one_line_proof, lemma_names) = metis_proof_text metis_params
   940     fun isar_proof_for () =
   941       case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
   942                isar_shrink_factor tstplike_proof conjecture_shape fact_names
   943                params frees
   944            |> redirect_proof hyp_ts concl_t
   945            |> kill_duplicate_assumptions_in_proof
   946            |> then_chain_proof
   947            |> kill_useless_labels_in_proof
   948            |> relabel_proof
   949            |> string_for_proof ctxt type_sys i n of
   950         "" => "\nNo structured proof available."
   951       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   952     val isar_proof =
   953       if debug then
   954         isar_proof_for ()
   955       else
   956         try isar_proof_for ()
   957         |> the_default "\nWarning: The Isar proof construction failed."
   958   in (one_line_proof ^ isar_proof, lemma_names) end
   959 
   960 fun proof_text isar_proof isar_params metis_params =
   961   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   962       metis_params
   963 
   964 end;