src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
author blanchet
Wed Dec 12 21:48:29 2012 +0100 (2012-12-12 ago)
changeset 50510 7e4f2f8d9b50
parent 50450 358b6020f8b6
child 50557 31313171deb5
permissions -rw-r--r--
export a pair of ML functions
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Isar proof reconstruction from ATP proofs.
     6 *)
     7 
     8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     9 sig
    10   type 'a proof = 'a ATP_Proof.proof
    11   type stature = ATP_Problem_Generate.stature
    12 
    13   datatype reconstructor =
    14     Metis of string * string |
    15     SMT
    16 
    17   datatype play =
    18     Played of reconstructor * Time.time |
    19     Trust_Playable of reconstructor * Time.time option |
    20     Failed_to_Play of reconstructor
    21 
    22   type minimize_command = string list -> string
    23   type one_line_params =
    24     play * string * (string * stature) list * minimize_command * int * int
    25   type isar_params =
    26     bool * bool * Time.time * real * string Symtab.table
    27     * (string * stature) list vector * int Symtab.table * string proof * thm
    28 
    29   val smtN : string
    30   val string_for_reconstructor : reconstructor -> string
    31   val lam_trans_from_atp_proof : string proof -> string -> string
    32   val is_typed_helper_used_in_atp_proof : string proof -> bool
    33   val used_facts_in_atp_proof :
    34     Proof.context -> (string * stature) list vector -> string proof ->
    35     (string * stature) list
    36   val used_facts_in_unsound_atp_proof :
    37     Proof.context -> (string * stature) list vector -> 'a proof ->
    38     string list option
    39   val one_line_proof_text : int -> one_line_params -> string
    40   val isar_proof_text :
    41     Proof.context -> bool -> isar_params -> one_line_params -> string
    42   val proof_text :
    43     Proof.context -> bool -> isar_params -> int -> one_line_params -> string
    44 end;
    45 
    46 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    47 struct
    48 
    49 open ATP_Util
    50 open ATP_Problem
    51 open ATP_Proof
    52 open ATP_Problem_Generate
    53 open ATP_Proof_Reconstruct
    54 open Sledgehammer_Util
    55 open Sledgehammer_Proof
    56 open Sledgehammer_Annotate
    57 open Sledgehammer_Shrink
    58 
    59 structure String_Redirect = ATP_Proof_Redirect(
    60   type key = step_name
    61   val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
    62   val string_of = fst)
    63 
    64 open String_Redirect
    65 
    66 
    67 (** reconstructors **)
    68 
    69 datatype reconstructor =
    70   Metis of string * string |
    71   SMT
    72 
    73 datatype play =
    74   Played of reconstructor * Time.time |
    75   Trust_Playable of reconstructor * Time.time option |
    76   Failed_to_Play of reconstructor
    77 
    78 val smtN = "smt"
    79 
    80 fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
    81     metis_call type_enc lam_trans
    82   | string_for_reconstructor SMT = smtN
    83 
    84 
    85 (** fact extraction from ATP proofs **)
    86 
    87 fun find_first_in_list_vector vec key =
    88   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    89                  | (_, value) => value) NONE vec
    90 
    91 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
    92 
    93 fun resolve_one_named_fact fact_names s =
    94   case try (unprefix fact_prefix) s of
    95     SOME s' =>
    96     let val s' = s' |> unprefix_fact_number |> unascii_of in
    97       s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
    98     end
    99   | NONE => NONE
   100 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
   101 fun is_fact fact_names = not o null o resolve_fact fact_names
   102 
   103 fun resolve_one_named_conjecture s =
   104   case try (unprefix conjecture_prefix) s of
   105     SOME s' => Int.fromString s'
   106   | NONE => NONE
   107 
   108 val resolve_conjecture = map_filter resolve_one_named_conjecture
   109 val is_conjecture = not o null o resolve_conjecture
   110 
   111 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
   112 
   113 (* overapproximation (good enough) *)
   114 fun is_lam_lifted s =
   115   String.isPrefix fact_prefix s andalso
   116   String.isSubstring ascii_of_lam_fact_prefix s
   117 
   118 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
   119 
   120 fun is_axiom_used_in_proof pred =
   121   exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
   122            | _ => false)
   123 
   124 fun lam_trans_from_atp_proof atp_proof default =
   125   case (is_axiom_used_in_proof is_combinator_def atp_proof,
   126         is_axiom_used_in_proof is_lam_lifted atp_proof) of
   127     (false, false) => default
   128   | (false, true) => liftingN
   129 (*  | (true, true) => combs_and_liftingN -- not supported by "metis" *)
   130   | (true, _) => combsN
   131 
   132 val is_typed_helper_name =
   133   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
   134 fun is_typed_helper_used_in_atp_proof atp_proof =
   135   is_axiom_used_in_proof is_typed_helper_name atp_proof
   136 
   137 fun add_non_rec_defs fact_names accum =
   138   Vector.foldl (fn (facts, facts') =>
   139       union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
   140             facts')
   141     accum fact_names
   142 
   143 val isa_ext = Thm.get_name_hint @{thm ext}
   144 val isa_short_ext = Long_Name.base_name isa_ext
   145 
   146 fun ext_name ctxt =
   147   if Thm.eq_thm_prop (@{thm ext},
   148          singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
   149     isa_short_ext
   150   else
   151     isa_ext
   152 
   153 val leo2_ext = "extcnf_equal_neg"
   154 val leo2_unfold_def = "unfold_def"
   155 
   156 fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
   157     (if rule = leo2_ext then
   158        insert (op =) (ext_name ctxt, (Global, General))
   159      else if rule = leo2_unfold_def then
   160        (* LEO 1.3.3 does not record definitions properly, leading to missing
   161          dependencies in the TSTP proof. Remove the next line once this is
   162          fixed. *)
   163        add_non_rec_defs fact_names
   164      else if rule = satallax_coreN then
   165        (fn [] =>
   166            (* Satallax doesn't include definitions in its unsatisfiable cores,
   167               so we assume the worst and include them all here. *)
   168            [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
   169          | facts => facts)
   170      else
   171        I)
   172     #> (if null deps then union (op =) (resolve_fact fact_names ss)
   173         else I)
   174   | add_fact _ _ _ = I
   175 
   176 fun used_facts_in_atp_proof ctxt fact_names atp_proof =
   177   if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
   178   else fold (add_fact ctxt fact_names) atp_proof []
   179 
   180 fun used_facts_in_unsound_atp_proof _ _ [] = NONE
   181   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
   182     let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
   183       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
   184          not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
   185         SOME (map fst used_facts)
   186       else
   187         NONE
   188     end
   189 
   190 
   191 (** one-liner reconstructor proofs **)
   192 
   193 fun show_time NONE = ""
   194   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
   195 
   196 (* FIXME: Various bugs, esp. with "unfolding"
   197 fun unusing_chained_facts _ 0 = ""
   198   | unusing_chained_facts used_chaineds num_chained =
   199     if length used_chaineds = num_chained then ""
   200     else if null used_chaineds then "(* using no facts *) "
   201     else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
   202 *)
   203 
   204 fun apply_on_subgoal _ 1 = "by "
   205   | apply_on_subgoal 1 _ = "apply "
   206   | apply_on_subgoal i n =
   207     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
   208 
   209 fun using_labels [] = ""
   210   | using_labels ls =
   211     "using " ^ space_implode " " (map string_for_label ls) ^ " "
   212 
   213 fun command_call name [] =
   214     name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
   215   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   216 
   217 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
   218   (* unusing_chained_facts used_chaineds num_chained ^ *)
   219   using_labels ls ^ apply_on_subgoal i n ^
   220   command_call (string_for_reconstructor reconstr) ss
   221 
   222 fun try_command_line banner time command =
   223   banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
   224 
   225 fun minimize_line _ [] = ""
   226   | minimize_line minimize_command ss =
   227     case minimize_command ss of
   228       "" => ""
   229     | command =>
   230       "\nTo minimize: " ^ Active.sendback_markup command ^ "."
   231 
   232 fun split_used_facts facts =
   233   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
   234         |> pairself (sort_distinct (string_ord o pairself fst))
   235 
   236 type minimize_command = string list -> string
   237 type one_line_params =
   238   play * string * (string * stature) list * minimize_command * int * int
   239 
   240 fun one_line_proof_text num_chained
   241         (preplay, banner, used_facts, minimize_command, subgoal,
   242          subgoal_count) =
   243   let
   244     val (chained, extra) = split_used_facts used_facts
   245     val (failed, reconstr, ext_time) =
   246       case preplay of
   247         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
   248       | Trust_Playable (reconstr, time) =>
   249         (false, reconstr,
   250          case time of
   251            NONE => NONE
   252          | SOME time =>
   253            if time = Time.zeroTime then NONE else SOME (true, time))
   254       | Failed_to_Play reconstr => (true, reconstr, NONE)
   255     val try_line =
   256       ([], map fst extra)
   257       |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
   258                                num_chained
   259       |> (if failed then
   260             enclose "One-line proof reconstruction failed: "
   261                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
   262                      \solve this.)"
   263           else
   264             try_command_line banner ext_time)
   265   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
   266 
   267 
   268 (** Isar proof construction and manipulation **)
   269 
   270 val assume_prefix = "a"
   271 val have_prefix = "f"
   272 val raw_prefix = "x"
   273 
   274 fun raw_label_for_name (num, ss) =
   275   case resolve_conjecture ss of
   276     [j] => (conjecture_prefix, j)
   277   | _ => (raw_prefix ^ ascii_of num, 0)
   278 
   279 fun label_of_clause [name] = raw_label_for_name name
   280   | label_of_clause c = (space_implode "___" (map (fst o raw_label_for_name) c), 0)
   281 
   282 fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
   283     if is_fact fact_names ss then
   284       apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
   285     else
   286       apfst (insert (op =) (label_of_clause names))
   287   | add_fact_from_dependencies fact_names names =
   288     apfst (insert (op =) (label_of_clause names))
   289 
   290 fun repair_name "$true" = "c_True"
   291   | repair_name "$false" = "c_False"
   292   | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
   293   | repair_name s =
   294     if is_tptp_equal s orelse
   295        (* seen in Vampire proofs *)
   296        (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
   297       tptp_equal
   298     else
   299       s
   300 
   301 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   302   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   303 
   304 fun infer_formula_types ctxt =
   305   Type.constraint HOLogic.boolT
   306   #> Syntax.check_term
   307          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
   308 
   309 val combinator_table =
   310   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
   311    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
   312    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
   313    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
   314    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
   315 
   316 fun uncombine_term thy =
   317   let
   318     fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
   319       | aux (Abs (s, T, t')) = Abs (s, T, aux t')
   320       | aux (t as Const (x as (s, _))) =
   321         (case AList.lookup (op =) combinator_table s of
   322            SOME thm => thm |> prop_of |> specialize_type thy x
   323                            |> Logic.dest_equals |> snd
   324          | NONE => t)
   325       | aux t = t
   326   in aux end
   327 
   328 fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =
   329     let
   330       val thy = Proof_Context.theory_of ctxt
   331       val t1 = prop_from_atp ctxt true sym_tab phi1
   332       val vars = snd (strip_comb t1)
   333       val frees = map unvarify_term vars
   334       val unvarify_args = subst_atomic (vars ~~ frees)
   335       val t2 = prop_from_atp ctxt true sym_tab phi2
   336       val (t1, t2) =
   337         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   338         |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
   339         |> HOLogic.dest_eq
   340     in
   341       (Definition_Step (name, t1, t2),
   342        fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
   343     end
   344   | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
   345     let
   346       val thy = Proof_Context.theory_of ctxt
   347       val t = u |> prop_from_atp ctxt true sym_tab
   348                 |> uncombine_term thy |> infer_formula_types ctxt
   349     in
   350       (Inference_Step (name, role, t, rule, deps),
   351        fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
   352     end
   353 fun decode_lines ctxt sym_tab lines =
   354   fst (fold_map (decode_line sym_tab) lines ctxt)
   355 
   356 fun replace_one_dependency (old, new) dep =
   357   if is_same_atp_step dep old then new else [dep]
   358 fun replace_dependencies_in_line _ (line as Definition_Step _) = line
   359   | replace_dependencies_in_line p
   360         (Inference_Step (name, role, t, rule, deps)) =
   361     Inference_Step (name, role, t, rule,
   362                     fold (union (op =) o replace_one_dependency p) deps [])
   363 
   364 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   365    clsarity). *)
   366 fun is_only_type_information t = t aconv @{term True}
   367 
   368 fun is_same_inference _ (Definition_Step _) = false
   369   | is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t'
   370 
   371 (* Discard facts; consolidate adjacent lines that prove the same formula, since
   372    they differ only in type information.*)
   373 fun add_line _ (line as Definition_Step _) lines = line :: lines
   374   | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
   375              lines =
   376     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   377        definitions. *)
   378     if is_fact fact_names ss then
   379       (* Facts are not proof lines. *)
   380       if is_only_type_information t then
   381         map (replace_dependencies_in_line (name, [])) lines
   382       (* Is there a repetition? If so, replace later line by earlier one. *)
   383       else case take_prefix (not o is_same_inference t) lines of
   384         (_, []) => lines (* no repetition of proof line *)
   385       | (pre, Inference_Step (name', _, _, _, _) :: post) =>
   386         pre @ map (replace_dependencies_in_line (name', [name])) post
   387       | _ => raise Fail "unexpected inference"
   388     else if is_conjecture ss then
   389       Inference_Step (name, role, t, rule, []) :: lines
   390     else
   391       map (replace_dependencies_in_line (name, [])) lines
   392   | add_line _ (Inference_Step (name, role, t, rule, deps)) lines =
   393     (* Type information will be deleted later; skip repetition test. *)
   394     if is_only_type_information t then
   395       Inference_Step (name, role, t, rule, deps) :: lines
   396     (* Is there a repetition? If so, replace later line by earlier one. *)
   397     else case take_prefix (not o is_same_inference t) lines of
   398       (* FIXME: Doesn't this code risk conflating proofs involving different
   399          types? *)
   400        (_, []) => Inference_Step (name, role, t, rule, deps) :: lines
   401      | (pre, Inference_Step (name', role, t', rule, _) :: post) =>
   402        Inference_Step (name, role, t', rule, deps) ::
   403        pre @ map (replace_dependencies_in_line (name', [name])) post
   404      | _ => raise Fail "unexpected inference"
   405 
   406 val waldmeister_conjecture_num = "1.0.0.0"
   407 
   408 val repair_waldmeister_endgame =
   409   let
   410     fun do_tail (Inference_Step (name, role, t, rule, deps)) =
   411         Inference_Step (name, role, s_not t, rule, deps)
   412       | do_tail line = line
   413     fun do_body [] = []
   414       | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
   415         if num = waldmeister_conjecture_num then map do_tail (line :: lines)
   416         else line :: do_body lines
   417       | do_body (line :: lines) = line :: do_body lines
   418   in do_body end
   419 
   420 (* Recursively delete empty lines (type information) from the proof. *)
   421 fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
   422     if is_only_type_information t then delete_dependency name lines
   423     else line :: lines
   424   | add_nontrivial_line line lines = line :: lines
   425 and delete_dependency name lines =
   426   fold_rev add_nontrivial_line
   427            (map (replace_dependencies_in_line (name, [])) lines) []
   428 
   429 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   430    offending lines often does the trick. *)
   431 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   432   | is_bad_free _ _ = false
   433 
   434 fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
   435     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   436   | add_desired_line fact_names frees
   437         (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
   438     (j + 1,
   439      if is_fact fact_names ss orelse
   440         is_conjecture ss orelse
   441         (* the last line must be kept *)
   442         j = 0 orelse
   443         (not (is_only_type_information t) andalso
   444          null (Term.add_tvars t []) andalso
   445          not (exists_subterm (is_bad_free frees) t) andalso
   446          length deps >= 2 andalso
   447          (* kill next to last line, which usually results in a trivial step *)
   448          j <> 1) then
   449        Inference_Step (name, role, t, rule, deps) :: lines  (* keep line *)
   450      else
   451        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   452 
   453 val indent_size = 2
   454 val no_label = ("", ~1)
   455 
   456 fun string_for_proof ctxt type_enc lam_trans i n =
   457   let
   458     fun do_indent ind = replicate_string (ind * indent_size) " "
   459     fun do_free (s, T) =
   460       maybe_quote s ^ " :: " ^
   461       maybe_quote (simplify_spaces (with_vanilla_print_mode
   462         (Syntax.string_of_typ ctxt) T))
   463     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   464     fun do_have qs =
   465       (if member (op =) qs Ultimately then "ultimately " else "") ^
   466       (if member (op =) qs Then then
   467          if member (op =) qs Show then "thus" else "hence"
   468        else
   469          if member (op =) qs Show then "show" else "have")
   470     val do_term =
   471       annotate_types ctxt
   472       #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
   473       #> simplify_spaces
   474       #> maybe_quote
   475     val reconstr = Metis (type_enc, lam_trans)
   476     fun do_facts ind (ls, ss) =
   477       "\n" ^ do_indent (ind + 1) ^
   478       reconstructor_command reconstr 1 1 [] 0
   479           (ls |> sort_distinct (prod_ord string_ord int_ord),
   480            ss |> sort_distinct string_ord)
   481     and do_step ind (Fix xs) =
   482         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   483       | do_step ind (Let (t1, t2)) =
   484         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   485       | do_step ind (Assume (l, t)) =
   486         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   487       | do_step ind (Prove (qs, l, t, By_Metis facts)) =
   488         do_indent ind ^ do_have qs ^ " " ^
   489         do_label l ^ do_term t ^ do_facts ind facts ^ "\n"
   490       | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
   491         implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
   492                      proofs) ^
   493         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
   494         do_facts ind facts ^ "\n"
   495     and do_steps prefix suffix ind steps =
   496       let val s = implode (map (do_step ind) steps) in
   497         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   498         String.extract (s, ind * indent_size,
   499                         SOME (size s - ind * indent_size - 1)) ^
   500         suffix ^ "\n"
   501       end
   502     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   503     (* One-step proofs are pointless; better use the Metis one-liner
   504        directly. *)
   505     and do_proof [Prove (_, _, _, By_Metis _)] = ""
   506       | do_proof proof =
   507         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   508         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   509         (if n <> 1 then "next" else "qed")
   510   in do_proof end
   511 
   512 fun used_labels_of_step (Prove (_, _, _, by)) =
   513     (case by of
   514        By_Metis (ls, _) => ls
   515      | Case_Split (proofs, (ls, _)) =>
   516        fold (union (op =) o used_labels_of) proofs ls)
   517   | used_labels_of_step _ = []
   518 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   519 
   520 fun kill_useless_labels_in_proof proof =
   521   let
   522     val used_ls = used_labels_of proof
   523     fun do_label l = if member (op =) used_ls l then l else no_label
   524     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   525       | do_step (Prove (qs, l, t, by)) =
   526         Prove (qs, do_label l, t,
   527                case by of
   528                  Case_Split (proofs, facts) =>
   529                  Case_Split (map (map do_step) proofs, facts)
   530                | _ => by)
   531       | do_step step = step
   532   in map do_step proof end
   533 
   534 fun prefix_for_depth n = replicate_string (n + 1)
   535 
   536 val relabel_proof =
   537   let
   538     fun aux _ _ _ [] = []
   539       | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
   540         if l = no_label then
   541           Assume (l, t) :: aux subst depth (next_assum, next_have) proof
   542         else
   543           let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
   544             Assume (l', t) ::
   545             aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof
   546           end
   547       | aux subst depth (next_assum, next_have)
   548             (Prove (qs, l, t, by) :: proof) =
   549         let
   550           val (l', subst, next_have) =
   551             if l = no_label then
   552               (l, subst, next_have)
   553             else
   554               let val l' = (prefix_for_depth depth have_prefix, next_have) in
   555                 (l', (l, l') :: subst, next_have + 1)
   556               end
   557           val relabel_facts =
   558             apfst (maps (the_list o AList.lookup (op =) subst))
   559           val by =
   560             case by of
   561               By_Metis facts => By_Metis (relabel_facts facts)
   562             | Case_Split (proofs, facts) =>
   563               Case_Split (map (aux subst (depth + 1) (1, 1)) proofs,
   564                           relabel_facts facts)
   565         in
   566           Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof
   567         end
   568       | aux subst depth nextp (step :: proof) =
   569         step :: aux subst depth nextp proof
   570   in aux [] 0 (1, 1) end
   571 
   572 val chain_direct_proof =
   573   let
   574     fun succedent_of_step (Prove (_, label, _, _)) = SOME label
   575       | succedent_of_step (Assume (label, _)) = SOME label
   576       | succedent_of_step _ = NONE
   577     fun chain_inf (SOME label0)
   578                   (step as Prove (qs, label, t, By_Metis (lfs, gfs))) =
   579         if member (op =) lfs label0 then
   580           Prove (Then :: qs, label, t,
   581                  By_Metis (filter_out (curry (op =) label0) lfs, gfs))
   582         else
   583           step
   584       | chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) =
   585         Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts))
   586       | chain_inf _ step = step
   587     and chain_proof _ [] = []
   588       | chain_proof (prev as SOME _) (i :: is) =
   589         chain_inf prev i :: chain_proof (succedent_of_step i) is
   590       | chain_proof _ (i :: is) =
   591         i :: chain_proof (succedent_of_step i) is
   592   in chain_proof NONE end
   593 
   594 type isar_params =
   595   bool * bool * Time.time * real * string Symtab.table
   596   * (string * stature) list vector * int Symtab.table * string proof * thm
   597 
   598 fun isar_proof_text ctxt isar_proofs
   599     (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
   600      atp_proof, goal)
   601     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   602   let
   603     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
   604     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   605     val one_line_proof = one_line_proof_text 0 one_line_params
   606     val type_enc =
   607       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
   608       else partial_typesN
   609     val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
   610     val preplay = preplay_timeout <> seconds 0.0
   611 
   612     fun isar_proof_of () =
   613       let
   614         val atp_proof =
   615           atp_proof
   616           |> clean_up_atp_proof_dependencies
   617           |> nasty_atp_proof pool
   618           |> map_term_names_in_atp_proof repair_name
   619           |> decode_lines ctxt sym_tab
   620           |> rpair [] |-> fold_rev (add_line fact_names)
   621           |> repair_waldmeister_endgame
   622           |> rpair [] |-> fold_rev add_nontrivial_line
   623           |> rpair (0, [])
   624           |-> fold_rev (add_desired_line fact_names frees)
   625           |> snd
   626         val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
   627         val conjs =
   628           atp_proof |> map_filter
   629             (fn Inference_Step (name as (_, ss), _, _, _, []) =>
   630                 if member (op =) ss conj_name then SOME name else NONE
   631               | _ => NONE)
   632         val assms =
   633           atp_proof |> map_filter
   634             (fn Inference_Step (name as (_, ss), _, _, _, []) =>
   635                 (case resolve_conjecture ss of
   636                    [j] =>
   637                    if j = length hyp_ts then NONE
   638                    else SOME (Assume (raw_label_for_name name, nth hyp_ts j))
   639                  | _ => NONE)
   640               | _ => NONE)
   641         fun dep_of_step (Definition_Step _) = NONE
   642           | dep_of_step (Inference_Step (name, _, _, _, from)) =
   643             SOME (from, name)
   644         val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
   645         val axioms = axioms_of_ref_graph ref_graph conjs
   646         val tainted = tainted_atoms_of_ref_graph ref_graph conjs
   647         val props =
   648           Symtab.empty
   649           |> fold (fn Definition_Step _ => I (* FIXME *)
   650                     | Inference_Step (name as (s, ss), role, t, _, _) =>
   651                       Symtab.update_new (s,
   652                         if member (op = o apsnd fst) tainted s then
   653                           t |> role <> Conjecture ? s_not
   654                             |> fold exists_of (map Var (Term.add_vars t []))
   655                         else
   656                           t))
   657                   atp_proof
   658         (* The assumptions and conjecture are props; the rest are bools. *)
   659         fun prop_of_clause [name as (s, ss)] =
   660             (case resolve_conjecture ss of
   661                [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
   662              | _ => the_default @{term False} (Symtab.lookup props s)
   663                     |> HOLogic.mk_Trueprop |> close_form)
   664           | prop_of_clause names =
   665             let val lits = map_filter (Symtab.lookup props o fst) names in
   666               case List.partition (can HOLogic.dest_not) lits of
   667                 (negs as _ :: _, pos as _ :: _) =>
   668                 HOLogic.mk_imp
   669                   (Library.foldr1 s_conj (map HOLogic.dest_not negs),
   670                    Library.foldr1 s_disj pos)
   671               | _ => fold (curry s_disj) lits @{term False}
   672             end
   673             |> HOLogic.mk_Trueprop |> close_form
   674         fun maybe_show outer c =
   675           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
   676           ? cons Show
   677         fun do_have outer qs (gamma, c) =
   678           Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
   679                  By_Metis (fold (add_fact_from_dependencies fact_names) gamma
   680                                 ([], [])))
   681         fun do_inf outer (Have z) = do_have outer [] z
   682           | do_inf outer (Cases cases) =
   683             let val c = succedent_of_cases cases in
   684               Prove (maybe_show outer c [Ultimately], label_of_clause c,
   685                      prop_of_clause c,
   686                      Case_Split (map (do_case false) cases, ([], [])))
   687             end
   688         and do_case outer (c, infs) =
   689           Assume (label_of_clause c, prop_of_clause c) ::
   690           map (do_inf outer) infs
   691         val (isar_proof, (preplay_fail, ext_time)) =
   692           ref_graph
   693           |> redirect_graph axioms tainted
   694           |> map (do_inf true)
   695           |> append assms
   696           |> (if not preplay andalso isar_shrink <= 1.0
   697               then pair (false, (true, seconds 0.0)) #> swap
   698               else shrink_proof debug ctxt type_enc lam_trans preplay
   699                 preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
   700        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
   701           |>> chain_direct_proof
   702           |>> kill_useless_labels_in_proof
   703           |>> relabel_proof
   704           |>> not (null params) ? cons (Fix params)
   705         val isar_text =
   706           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
   707                            isar_proof
   708       in
   709         case isar_text of
   710           "" =>
   711           if isar_proofs then
   712             "\nNo structured proof available (proof too short)."
   713           else
   714             ""
   715         | _ =>
   716           let 
   717             val msg = 
   718               (if preplay then 
   719                 [if preplay_fail 
   720                  then "may fail" 
   721                  else string_from_ext_time ext_time]
   722                else [])
   723               @ 
   724                (if verbose then
   725                   [let val num_steps = metis_steps_total isar_proof
   726                    in string_of_int num_steps ^ plural_s num_steps end]
   727                 else [])
   728           in
   729             "\n\nStructured proof "
   730               ^ (commas msg |> not (null msg) ? enclose "(" ")")
   731               ^ ":\n" ^ Active.sendback_markup isar_text
   732           end
   733       end
   734     val isar_proof =
   735       if debug then
   736         isar_proof_of ()
   737       else case try isar_proof_of () of
   738         SOME s => s
   739       | NONE => if isar_proofs then
   740                   "\nWarning: The Isar proof construction failed."
   741                 else
   742                   ""
   743   in one_line_proof ^ isar_proof end
   744 
   745 fun proof_text ctxt isar_proofs isar_params num_chained
   746                (one_line_params as (preplay, _, _, _, _, _)) =
   747   (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then
   748      isar_proof_text ctxt isar_proofs isar_params
   749    else
   750      one_line_proof_text num_chained) one_line_params
   751 
   752 end;