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