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