correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
authorblanchet
Thu Mar 13 14:48:20 2014 +0100 (2014-03-13 ago)
changeset 56104fd6e132ee4fb
parent 56103 6689512f3710
child 56105 75dc126f5dcb
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_solver.ML
src/HOL/Tools/SMT2/smt2_translate.ML
src/HOL/Tools/SMT2/z3_new_isar.ML
src/HOL/Tools/SMT2/z3_new_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Mar 13 14:48:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -377,22 +377,12 @@
     1.4        union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts')
     1.5      accum fact_names
     1.6  
     1.7 -val isa_ext = Thm.get_name_hint @{thm ext}
     1.8 -val isa_short_ext = Long_Name.base_name isa_ext
     1.9 -
    1.10 -fun ext_name ctxt =
    1.11 -  if Thm.eq_thm_prop (@{thm ext},
    1.12 -       singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
    1.13 -    isa_short_ext
    1.14 -  else
    1.15 -    isa_ext
    1.16 -
    1.17  val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
    1.18  val leo2_unfold_def_rule = "unfold_def"
    1.19  
    1.20  fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
    1.21    (if rule = leo2_extcnf_equal_neg_rule then
    1.22 -     insert (op =) (ext_name ctxt, (Global, General))
    1.23 +     insert (op =) (short_thm_name ctxt ext, (Global, General))
    1.24     else if rule = leo2_unfold_def_rule then
    1.25       (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP
    1.26          proof. Remove the next line once this is fixed. *)
    1.27 @@ -401,7 +391,7 @@
    1.28       (fn [] =>
    1.29           (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we
    1.30              assume the worst and include them all here. *)
    1.31 -         [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
    1.32 +         [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names
    1.33         | facts => facts)
    1.34     else
    1.35       I)
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Mar 13 14:48:20 2014 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Mar 13 14:48:20 2014 +0100
     2.3 @@ -48,8 +48,8 @@
     2.4    val is_legitimate_tptp_def : term -> bool
     2.5    val transform_elim_prop : term -> term
     2.6    val specialize_type : theory -> (string * typ) -> term -> term
     2.7 -  val strip_subgoal :
     2.8 -    thm -> int -> Proof.context -> (string * typ) list * term list * term
     2.9 +  val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term
    2.10 +  val short_thm_name : Proof.context -> thm -> string
    2.11  end;
    2.12  
    2.13  structure ATP_Util : ATP_UTIL =
    2.14 @@ -425,4 +425,13 @@
    2.15      val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    2.16    in (rev params, hyp_ts, concl_t) end
    2.17  
    2.18 +fun short_thm_name ctxt th =
    2.19 +  let
    2.20 +    val long = Thm.get_name_hint th
    2.21 +    val short = Long_Name.base_name long
    2.22 +  in
    2.23 +    if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short
    2.24 +    else long
    2.25 +  end
    2.26 +
    2.27  end;
     3.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     3.3 @@ -497,7 +497,7 @@
     3.4    let
     3.5      val (is, thms) = split_list ithms
     3.6      val (thms', extra_thms) = f thms
     3.7 -  in (is ~~ thms') @ map (pair ~1) extra_thms end
     3.8 +  in (is ~~ thms') @ tag_list (length is) extra_thms end
     3.9  
    3.10  fun unfold2 ctxt ithms =
    3.11    ithms
     4.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 14:48:20 2014 +0100
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 14:48:20 2014 +0100
     4.3 @@ -20,20 +20,20 @@
     4.4      cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
     4.5        term list * term list) option,
     4.6      replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
     4.7 -      ((int * int) list * Z3_New_Proof.z3_step list) * thm) option }
     4.8 +      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
     4.9  
    4.10    (*registry*)
    4.11    val add_solver: solver_config -> theory -> theory
    4.12    val solver_name_of: Proof.context -> string
    4.13    val available_solvers_of: Proof.context -> string list
    4.14    val apply_solver: Proof.context -> (int * (int option * thm)) list ->
    4.15 -    ((int * int) list * Z3_New_Proof.z3_step list) * thm
    4.16 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
    4.17    val default_max_relevant: Proof.context -> string -> int
    4.18  
    4.19    (*filter*)
    4.20 -  val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int ->
    4.21 -    Time.time -> {outcome: SMT2_Failure.failure option, used_fact_infos: (int * ('a * thm)) list,
    4.22 -      z3_proof: Z3_New_Proof.z3_step list}
    4.23 +  val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time ->
    4.24 +    {outcome: SMT2_Failure.failure option, conjecture_id: int, helper_ids: (int * thm) list,
    4.25 +     fact_ids: (int * ('a * thm)) list, z3_proof: Z3_New_Proof.z3_step list}
    4.26  
    4.27    (*tactic*)
    4.28    val smt2_tac: Proof.context -> thm list -> int -> tactic
    4.29 @@ -152,7 +152,7 @@
    4.30    cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    4.31      term list * term list) option,
    4.32    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    4.33 -    ((int * int) list * Z3_New_Proof.z3_step list) * thm) option }
    4.34 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
    4.35  
    4.36  
    4.37  (* registry *)
    4.38 @@ -162,7 +162,7 @@
    4.39    default_max_relevant: int,
    4.40    supports_filter: bool,
    4.41    replay: Proof.context -> string list * SMT2_Translate.replay_data ->
    4.42 -    ((int * int) list * Z3_New_Proof.z3_step list) * thm }
    4.43 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm }
    4.44  
    4.45  structure Solvers = Generic_Data
    4.46  (
    4.47 @@ -258,7 +258,7 @@
    4.48  
    4.49  val cnot = Thm.cterm_of @{theory} @{const Not}
    4.50  
    4.51 -fun smt2_filter ctxt facts goal xwthms i time_limit =
    4.52 +fun smt2_filter ctxt goal xwfacts i time_limit =
    4.53    let
    4.54      val ctxt =
    4.55        ctxt
    4.56 @@ -273,53 +273,61 @@
    4.57          SOME ct => ct
    4.58        | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term"))
    4.59  
    4.60 -    val xthms = map (apsnd snd) xwthms
    4.61 +    val iwconjecture = (~1, (NONE, Thm.assume cprop))
    4.62 +    val iwprems = map (pair ~2 o pair NONE) prems
    4.63 +    val iwfacts = map_index I (map snd xwfacts)
    4.64  
    4.65 -    val used_fact_infos_of =
    4.66 -      if supports_filter ctxt then map_filter (try (apsnd (nth xthms)))
    4.67 -      else K (map (pair ~1) xthms)
    4.68 +    val n = length iwfacts
    4.69 +    val xfacts = map (apsnd snd) xwfacts
    4.70    in
    4.71 -    map snd xwthms
    4.72 -    |> map_index I
    4.73 -    |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
    4.74 +    iwconjecture :: iwprems @ iwfacts
    4.75      |> check_topsorts ctxt
    4.76      |> apply_solver ctxt
    4.77      |> fst
    4.78 -    |> (fn (idis, z3_proof) =>
    4.79 -      {outcome = NONE, used_fact_infos = used_fact_infos_of idis, z3_proof = z3_proof})
    4.80 +    |> (fn (iidths0, z3_proof) =>
    4.81 +      let val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K ~1))) iwfacts
    4.82 +      in
    4.83 +        {outcome = NONE, 
    4.84 +         conjecture_id =
    4.85 +           the_default ~1 (Option.map fst (AList.lookup (op =) iidths (fst iwconjecture))),
    4.86 +         helper_ids = map_filter (fn (i, (id, th)) => if i >= n then SOME (id, th) else NONE) iidths,
    4.87 +         fact_ids = map_filter (fn (i, (id, _)) => try (apsnd (nth xfacts)) (id, i)) iidths,
    4.88 +         z3_proof = z3_proof}
    4.89 +      end)
    4.90    end
    4.91 -  handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_fact_infos = [], z3_proof = []}
    4.92 +  handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = ~1, helper_ids = [],
    4.93 +    fact_ids = [], z3_proof = []}
    4.94  
    4.95  
    4.96  (* SMT tactic *)
    4.97  
    4.98  local
    4.99 -  fun trace_assumptions ctxt iwthms idis =
   4.100 +  fun trace_assumptions ctxt iwfacts iidths =
   4.101      let
   4.102 -      val wthms =
   4.103 -        idis
   4.104 -        |> map snd
   4.105 +      val wfacts =
   4.106 +        iidths
   4.107 +        |> map fst
   4.108          |> filter (fn i => i >= 0)
   4.109 -        |> map_filter (AList.lookup (op =) iwthms)
   4.110 +        |> map_filter (AList.lookup (op =) iwfacts)
   4.111      in
   4.112 -      if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 then
   4.113 +      if Config.get ctxt SMT2_Config.trace_used_facts andalso length wfacts > 0 then
   4.114          tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   4.115 -          (map (Display.pretty_thm ctxt o snd) wthms)))
   4.116 +          (map (Display.pretty_thm ctxt o snd) wfacts)))
   4.117        else ()
   4.118      end
   4.119  
   4.120 -  fun solve ctxt iwthms =
   4.121 -    iwthms
   4.122 +  fun solve ctxt iwfacts =
   4.123 +    iwfacts
   4.124      |> check_topsorts ctxt
   4.125      |> apply_solver ctxt
   4.126 -    |>> apfst (trace_assumptions ctxt iwthms)
   4.127 +    |>> apfst (trace_assumptions ctxt iwfacts)
   4.128      |> snd
   4.129  
   4.130    fun str_of ctxt fail =
   4.131      SMT2_Failure.string_of_failure ctxt fail
   4.132      |> prefix ("Solver " ^ SMT2_Config.solver_of ctxt ^ ": ")
   4.133  
   4.134 -  fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms)
   4.135 +  fun safe_solve ctxt iwfacts = SOME (solve ctxt iwfacts)
   4.136      handle
   4.137        SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) =>
   4.138          (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
     5.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 14:48:20 2014 +0100
     5.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Mar 13 14:48:20 2014 +0100
     5.3 @@ -321,8 +321,7 @@
     5.4    exception BAD_PATTERN of unit
     5.5  
     5.6    fun wrap_in_if pat t =
     5.7 -    if pat then raise BAD_PATTERN ()
     5.8 -    else @{const If (bool)} $ t $ @{const True} $ @{const False}
     5.9 +    if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False}
    5.10  
    5.11    fun is_builtin_conn_or_pred ctxt c ts =
    5.12      is_some (SMT2_Builtin.dest_builtin_conn ctxt c ts) orelse
    5.13 @@ -338,8 +337,7 @@
    5.14          (@{const True}, []) => t
    5.15        | (@{const False}, []) => t
    5.16        | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
    5.17 -          if pat then raise BAD_PATTERN ()
    5.18 -          else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
    5.19 +          if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
    5.20        | (Const (c as (n, _)), ts) =>
    5.21            if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
    5.22            else if is_quant n then wrap_in_if pat (in_form t)
    5.23 @@ -357,11 +355,9 @@
    5.24        | in_pat t = raise TERM ("bad pattern", [t])
    5.25  
    5.26      and in_pats ps =
    5.27 -      in_list @{typ "SMT2.pattern list"}
    5.28 -        (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps
    5.29 +      in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps
    5.30  
    5.31 -    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) =
    5.32 -          c $ in_pats p $ in_weight t
    5.33 +    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_weight t
    5.34        | in_trigger t = in_weight t
    5.35  
    5.36      and in_form t =
    5.37 @@ -462,7 +458,7 @@
    5.38        let val (Us, U) = SMT2_Util.dest_funT (length ts) T
    5.39        in
    5.40          fold_map transT Us ##>> transT U #-> (fn Up =>
    5.41 -        add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
    5.42 +          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
    5.43        end
    5.44  
    5.45      val (us, trx') = fold_map trans ts trx
    5.46 @@ -528,13 +524,12 @@
    5.47            |> pair ctxt')
    5.48  
    5.49      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
    5.50 -
    5.51 -    val rewrite_rules' = fun_app_eq :: rewrite_rules
    5.52 +      |>> apfst (cons fun_app_eq)
    5.53    in
    5.54      (ts4, tr_context)
    5.55      |-> intermediate header dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
    5.56      |>> uncurry (serialize comments)
    5.57 -    ||> replay_data_of ctxt2 rewrite_rules' ithms
    5.58 +    ||> replay_data_of ctxt2 rewrite_rules ithms
    5.59    end
    5.60  
    5.61  end
     6.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Mar 13 14:48:20 2014 +0100
     6.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Mar 13 14:48:20 2014 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  sig
     6.5    type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
     6.6  
     6.7 -  val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (int * string) list ->
     6.8 +  val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
     6.9      (term, string) atp_step list
    6.10  end;
    6.11  
    6.12 @@ -74,7 +74,7 @@
    6.13  
    6.14  fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
    6.15  
    6.16 -fun atp_proof_of_z3_proof thy proof fact_ids =
    6.17 +fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof =
    6.18    let
    6.19      fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    6.20        let
    6.21 @@ -84,7 +84,9 @@
    6.22          val role =
    6.23            (case rule of
    6.24              Z3_New_Proof.Asserted =>
    6.25 -              if null ss then Negated_Conjecture (* FIXME: or hypothesis! *) else Axiom
    6.26 +              if not (null ss) then Axiom
    6.27 +              else if id = conjecture_id then Negated_Conjecture
    6.28 +              else Hypothesis
    6.29            | Z3_New_Proof.Rewrite => Lemma
    6.30            | Z3_New_Proof.Rewrite_Star => Lemma
    6.31            | Z3_New_Proof.Skolemize => Lemma
     7.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 14:48:20 2014 +0100
     7.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Mar 13 14:48:20 2014 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  signature Z3_NEW_REPLAY =
     7.5  sig
     7.6    val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
     7.7 -    ((int * int) list * Z3_New_Proof.z3_step list) * thm
     7.8 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
     7.9  end
    7.10  
    7.11  structure Z3_New_Replay: Z3_NEW_REPLAY =
    7.12 @@ -106,14 +106,14 @@
    7.13          val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
    7.14        in (thm' RS thm, ctxt') end
    7.15  
    7.16 -    fun add1 id fixes thm1 ((i, th), exact) ((idis, thms), (ctxt, ptab)) =
    7.17 +    fun add1 id fixes thm1 ((i, th), exact) ((iidths, thms), (ctxt, ptab)) =
    7.18        let
    7.19          val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt
    7.20          val thms' = if exact then thms else th :: thms
    7.21 -      in (((id, i) :: idis, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
    7.22 +      in (((i, (id, th)) :: iidths, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
    7.23  
    7.24      fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
    7.25 -        (cx as ((idis, thms), (ctxt, ptab))) =
    7.26 +        (cx as ((iidths, thms), (ctxt, ptab))) =
    7.27        if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
    7.28          let
    7.29            val ct = SMT2_Util.certify ctxt concl
    7.30 @@ -123,7 +123,7 @@
    7.31            (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
    7.32              [] =>
    7.33                let val (thm, ctxt') = assume thm1 ctxt
    7.34 -              in ((idis, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
    7.35 +              in ((iidths, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
    7.36            | ithms => fold (add1 id fixes thm1) ithms cx)
    7.37          end
    7.38        else
    7.39 @@ -176,10 +176,10 @@
    7.40      ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
    7.41    let
    7.42      val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt
    7.43 -    val ((idis, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
    7.44 +    val ((iidths, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
    7.45    in
    7.46      if Config.get ctxt3 SMT2_Config.filter_only_facts then
    7.47 -      ((idis, steps), TrueI)
    7.48 +      ((iidths, steps), TrueI)
    7.49      else
    7.50        let
    7.51          val ctxt4 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 []) ctxt3
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 14:48:20 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 14:48:20 2014 +0100
     8.3 @@ -154,14 +154,14 @@
     8.4          val birth = Timer.checkRealTimer timer
     8.5          val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
     8.6  
     8.7 -        val {outcome, used_fact_infos, z3_proof} =
     8.8 -          SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout
     8.9 +        val filter_result as {outcome, ...} =
    8.10 +          SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
    8.11            handle exn =>
    8.12              if Exn.is_interrupt exn orelse debug then
    8.13                reraise exn
    8.14              else
    8.15                {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
    8.16 -               used_fact_infos = [], z3_proof = []}
    8.17 +               conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
    8.18  
    8.19          val death = Timer.checkRealTimer timer
    8.20          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    8.21 @@ -206,9 +206,8 @@
    8.22              do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
    8.23            end
    8.24          else
    8.25 -          {outcome = if is_none outcome then NONE else the outcome0,
    8.26 -           used_fact_infos = used_fact_infos, used_from = map (apsnd snd) weighted_facts,
    8.27 -           z3_proof = z3_proof, run_time = time_so_far}
    8.28 +          {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
    8.29 +           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
    8.30        end
    8.31    in
    8.32      do_slice timeout 1 NONE Time.zeroTime
    8.33 @@ -227,9 +226,9 @@
    8.34        end
    8.35  
    8.36      val weighted_factss = map (apsnd weight_facts) factss
    8.37 -    val {outcome, used_fact_infos, used_from, z3_proof, run_time} =
    8.38 -      smt2_filter_loop name params state goal subgoal weighted_factss
    8.39 -    val used_named_facts = map snd used_fact_infos
    8.40 +    val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
    8.41 +         used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
    8.42 +    val used_named_facts = map snd fact_ids
    8.43      val used_facts = map fst used_named_facts
    8.44      val outcome = Option.map failure_of_smt2_failure outcome
    8.45  
    8.46 @@ -241,8 +240,10 @@
    8.47               SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
    8.48           fn preplay =>
    8.49              let
    8.50 -              val fact_ids = map (fn (id, ((name, _), _)) => (id, name)) used_fact_infos
    8.51 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_proof fact_ids
    8.52 +              val fact_ids =
    8.53 +                map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    8.54 +                map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    8.55 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
    8.56                val isar_params =
    8.57                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    8.58                     minimize <> SOME false, atp_proof, goal)