--- a/src/HOL/ATP.thy Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/ATP.thy Mon Jun 16 19:40:59 2014 +0200
@@ -9,8 +9,8 @@
imports Meson
begin
-ML_file "Tools/lambda_lifting.ML"
-ML_file "Tools/monomorph.ML"
+subsection {* ATP problems and proofs *}
+
ML_file "Tools/ATP/atp_util.ML"
ML_file "Tools/ATP/atp_problem.ML"
ML_file "Tools/ATP/atp_proof.ML"
@@ -137,8 +137,10 @@
eq_ac disj_comms disj_assoc conj_comms conj_assoc
-subsection {* Setup *}
+subsection {* Basic connection between ATPs and HOL *}
+ML_file "Tools/lambda_lifting.ML"
+ML_file "Tools/monomorph.ML"
ML_file "Tools/ATP/atp_problem_generate.ML"
ML_file "Tools/ATP/atp_proof_reconstruct.ML"
ML_file "Tools/ATP/atp_systems.ML"
--- a/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 16 19:40:59 2014 +0200
@@ -33,4 +33,8 @@
ML_file "Tools/Sledgehammer/sledgehammer.ML"
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
+lemma "1 + 1 = (2::nat)"
+sledgehammer [vampire, max_facts = 3]
+oops
+
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jun 16 19:40:59 2014 +0200
@@ -110,12 +110,9 @@
Proof.context -> type_enc -> string -> term list -> term list * term list
val string_of_status : status -> string
val factsN : string
- val prepare_atp_problem :
- Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode
- -> string -> bool -> bool -> bool -> term list -> term
- -> ((string * stature) * term) list
- -> string atp_problem * string Symtab.table * (string * stature) list vector
- * (string * term) list * int Symtab.table
+ val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
+ string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
+ string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
val atp_problem_selection_weights : string atp_problem -> (string * real) list
val atp_problem_term_order_info : string atp_problem -> (string * int) list
end;
@@ -1279,8 +1276,7 @@
iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
|>> close_universally add_iterm_vars
in
- {name = name, stature = stature, role = role, iformula = iformula,
- atomic_types = atomic_Ts}
+ {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts}
end
fun is_format_with_defs (THF _) = true
@@ -1295,7 +1291,7 @@
else
Axiom
in
- (case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
+ (case make_formula ctxt format type_enc iff_for_eq name stature role t of
formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
if s = tptp_true then NONE else SOME formula
| formula => SOME formula)
@@ -1303,13 +1299,10 @@
fun make_conjecture ctxt format type_enc =
map (fn ((name, stature), (role, t)) =>
- let
- val role =
- if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
- in
- t |> role = Conjecture ? s_not
- |> make_formula ctxt format type_enc true name stature role
- end)
+ let
+ val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
+ val t' = t |> role' = Conjecture ? s_not
+ in make_formula ctxt format type_enc true name stature role' t' end)
(** Finite and infinite type inference **)
@@ -1907,10 +1900,8 @@
conjs |> make_conjecture ctxt format type_enc
|> pull_and_reorder_definitions
val facts =
- facts |> map_filter (fn (name, (_, t)) =>
- make_fact ctxt format type_enc true (name, t))
+ facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t))
|> pull_and_reorder_definitions
- val fact_names = facts |> map (fn {name, stature, ...} : ifact => (name, stature))
val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
val all_ts = concl_t :: hyp_ts @ fact_ts
@@ -1922,8 +1913,7 @@
else make_tcon_clauses thy tycons supers
val subclass_pairs = make_subclass_pairs thy subs supers
in
- (fact_names |> map single, union (op =) subs supers, conjs,
- facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
+ (union (op =) subs supers, conjs, facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
end
val type_guard = `(make_fixed_const NONE) type_guard_name
@@ -2616,7 +2606,7 @@
val app_op_and_predicator_threshold = 45
-fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
+fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
readable_names presimp hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
@@ -2636,7 +2626,7 @@
val lam_trans =
if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
else lam_trans
- val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
+ val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
@@ -2700,8 +2690,8 @@
val (problem, pool) = problem |> nice_atp_problem readable_names format
fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
in
- (problem, pool |> Option.map snd |> the_default Symtab.empty, fact_names |> Vector.fromList,
- lifted, Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
+ (problem, Option.map snd pool |> the_default Symtab.empty, lifted,
+ Symtab.fold add_sym_ary sym_tab Symtab.empty)
end
(* FUDGE *)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:40:59 2014 +0200
@@ -38,10 +38,10 @@
bool -> int Symtab.table ->
(string, string, (string, string atp_type) atp_term, string) atp_formula -> term
- val used_facts_in_atp_proof :
- Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
- val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->
- 'a atp_proof -> string list option
+ val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
+ (string * stature) list
+ val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof ->
+ string list option
val atp_proof_prefers_lifting : string atp_proof -> bool
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
@@ -50,8 +50,8 @@
ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
- val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
- (term, string) atp_step list -> (term, string) atp_step list
+ val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
+ (term, string) atp_step list
end;
structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -452,66 +452,58 @@
repair_tvar_sorts (do_formula true phi Vartab.empty)
end
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
-fun resolve_one_named_fact fact_names s =
+fun resolve_fact facts s =
(case try (unprefix fact_prefix) s of
SOME s' =>
let val s' = s' |> unprefix_fact_number |> unascii_of in
- s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
+ AList.lookup (op =) facts s' |> Option.map (pair s')
end
| NONE => NONE)
-fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
-
-fun resolve_one_named_conjecture s =
+fun resolve_conjecture s =
(case try (unprefix conjecture_prefix) s of
SOME s' => Int.fromString s'
| NONE => NONE)
-val resolve_conjecture = map_filter resolve_one_named_conjecture
+fun resolve_facts facts = map_filter (resolve_fact facts)
+val resolve_conjectures = map_filter resolve_conjecture
fun is_axiom_used_in_proof pred =
exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
-fun add_non_rec_defs fact_names accum =
- Vector.foldl (fn (facts, facts') =>
- union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts')
- accum fact_names
+fun add_non_rec_defs facts =
+ fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts
val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
val leo2_unfold_def_rule = "unfold_def"
-fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
+fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
(if rule = leo2_extcnf_equal_neg_rule then
insert (op =) (short_thm_name ctxt ext, (Global, General))
else if rule = leo2_unfold_def_rule then
(* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP
proof. Remove the next line once this is fixed. *)
- add_non_rec_defs fact_names
+ add_non_rec_defs facts
else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then
(fn [] =>
(* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we
assume the worst and include them all here. *)
- [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names
+ [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts
| facts => facts)
else
I)
- #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
+ #> (if null deps then union (op =) (resolve_facts facts ss) else I)
-fun used_facts_in_atp_proof ctxt fact_names atp_proof =
- if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
- else fold (add_fact ctxt fact_names) atp_proof []
+fun used_facts_in_atp_proof ctxt facts atp_proof =
+ if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof []
fun used_facts_in_unsound_atp_proof _ _ [] = NONE
- | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
- let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
+ | used_facts_in_unsound_atp_proof ctxt facts atp_proof =
+ let val used_facts = used_facts_in_atp_proof ctxt facts atp_proof in
if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
- not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then
+ not (is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof) then
SOME (map fst used_facts)
else
NONE
@@ -716,16 +708,16 @@
else
proof
-fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
+fun factify_atp_proof facts hyp_ts concl_t atp_proof =
let
fun factify_step ((num, ss), _, t, rule, deps) =
let
val (ss', role', t') =
- (case resolve_conjecture ss of
+ (case resolve_conjectures ss of
[j] =>
if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
| _ =>
- (case resolve_fact fact_names ss of
+ (case resolve_facts facts ss of
[] => (ss, Plain, t)
| facts => (map fst facts, Axiom, t)))
in
--- a/src/HOL/Tools/Metis/metis_generate.ML Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Jun 16 19:40:59 2014 +0200
@@ -29,11 +29,9 @@
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val reveal_lam_lifted : (string * term) list -> term -> term
- val prepare_metis_problem :
- Proof.context -> type_enc -> string -> thm list -> thm list
- -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
- * (unit -> (string * int) list)
- * ((string * term) list * (string * term) list)
+ val generate_metis_problem : Proof.context -> type_enc -> string -> thm list -> thm list ->
+ int Symtab.table * (Metis_Thm.thm * isa_thm) list * (unit -> (string * int) list)
+ * ((string * term) list * (string * term) list)
end
structure Metis_Generate : METIS_GENERATE =
@@ -172,42 +170,33 @@
else if String.isPrefix conjecture_prefix ident then
NONE
else if String.isPrefix helper_prefix ident then
- case (String.isSuffix typed_helper_suffix ident,
- space_explode "_" ident) of
+ case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
(needs_fairly_sound, _ :: const :: j :: _) =>
- nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
- |> the)
- (the (Int.fromString j) - 1)
+ nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
+ (the (Int.fromString j) - 1)
|> snd |> prepare_helper ctxt
|> Isa_Raw |> some
| _ => raise Fail ("malformed helper identifier " ^ quote ident)
else case try (unprefix fact_prefix) ident of
SOME s =>
- let val s = s |> space_explode "_" |> tl |> space_implode "_"
- in
+ let val s = s |> space_explode "_" |> tl |> space_implode "_" in
case Int.fromString s of
- SOME j =>
- Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
+ SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
| NONE =>
- if String.isPrefix lam_fact_prefix (unascii_of s) then
- Isa_Lambda_Lifted |> some
- else
- raise Fail ("malformed fact identifier " ^ quote ident)
+ if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
+ else raise Fail ("malformed fact identifier " ^ quote ident)
end
| NONE => TrueI |> Isa_Raw |> some
end
| metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
-fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
- eliminate_lam_wrappers t
- | eliminate_lam_wrappers (t $ u) =
- eliminate_lam_wrappers t $ eliminate_lam_wrappers u
- | eliminate_lam_wrappers (Abs (s, T, t)) =
- Abs (s, T, eliminate_lam_wrappers t)
+fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) = eliminate_lam_wrappers t
+ | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
+ | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
| eliminate_lam_wrappers t = t
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
+fun generate_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
val (conj_clauses, fact_clauses) =
if is_type_enc_polymorphic type_enc then
@@ -221,34 +210,31 @@
val num_conjs = length conj_clauses
(* Pretend every clause is a "simp" rule, to guide the term ordering. *)
val clauses =
- map2 (fn j => pair (Int.toString j, (Local, Simp)))
- (0 upto num_conjs - 1) conj_clauses @
+ map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
- (0 upto length fact_clauses - 1) fact_clauses
+ (0 upto length fact_clauses - 1) fact_clauses
val (old_skolems, props) =
fold_rev (fn (name, th) => fn (old_skolems, props) =>
- th |> prop_of |> Logic.strip_imp_concl
- |> conceal_old_skolem_terms (length clauses) old_skolems
- ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN)
- ? eliminate_lam_wrappers
- ||> (fn prop => (name, prop) :: props))
- clauses ([], [])
+ th |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms (length clauses) old_skolems
+ ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? eliminate_lam_wrappers
+ ||> (fn prop => (name, prop) :: props))
+ clauses ([], [])
(*
val _ =
tracing ("PROPS:\n" ^
cat_lines (map (Syntax.string_of_term ctxt o snd) props))
*)
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
- val (atp_problem, _, _, lifted, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false
- false false [] @{prop False} props
+ val (atp_problem, _, lifted, sym_tab) =
+ generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
+ @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_of_atp_problem CNF atp_problem))
*)
(* "rev" is for compatibility with existing proof scripts. *)
- val axioms =
- atp_problem
+ val axioms = atp_problem
|> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
fun ord_info () = atp_problem_term_order_info atp_problem
in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Jun 16 19:40:59 2014 +0200
@@ -156,8 +156,7 @@
map2 (fn j => fn th =>
(Thm.get_name_hint th,
th |> Drule.eta_contraction_rule
- |> Meson_Clausify.cnf_axiom ctxt new_skolem
- (lam_trans = combsN) j
+ |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j
||> map do_lams))
(0 upto length ths0 - 1) ths0
val ths = maps (snd o snd) th_cls_pairs
@@ -168,7 +167,7 @@
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_of_string Strict type_enc
val (sym_tab, axioms, ord_info, concealed) =
- prepare_metis_problem ctxt type_enc lam_trans cls ths
+ generate_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm mth Isa_Lambda_Lifted =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:40:04 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:40:59 2014 +0200
@@ -252,7 +252,7 @@
val readable_names = not (Config.get ctxt atp_full_names)
val lam_trans = lam_trans |> the_default best_lam_trans
val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
- val value as (atp_problem, _, fact_names, _, _) =
+ val value as (atp_problem, _, _, _) =
if cache_key = SOME key then
cache_value
else
@@ -261,8 +261,8 @@
|> take num_facts
|> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
|> map (apsnd prop_of)
- |> prepare_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
- uncurried_aliases readable_names true hyp_ts concl_t
+ |> generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
+ uncurried_aliases readable_names true hyp_ts concl_t
fun sel_weights () = atp_problem_selection_weights atp_problem
fun ord_info () = atp_problem_term_order_info atp_problem
@@ -275,11 +275,13 @@
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
+
val _ =
atp_problem
|> lines_of_atp_problem format ord ord_info
|> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
|> File.write_list prob_path
+
val ((output, run_time), (atp_proof, outcome)) =
TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
|>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
@@ -290,10 +292,11 @@
|>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
+
val outcome =
(case outcome of
NONE =>
- (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
+ (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof
|> Option.map (sort string_ord) of
SOME facts =>
let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
@@ -321,7 +324,7 @@
end
| maybe_run_slice _ result = result
in
- ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
+ ((NONE, ([], Symtab.empty, [], Symtab.empty)),
("", Time.zeroTime, [], [], SOME InternalError), NONE)
|> fold maybe_run_slice actual_slices
end
@@ -333,8 +336,8 @@
if dest_dir = "" then ()
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
- val ((_, (_, pool, fact_names, lifted, sym_tab)),
- (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) =
+ val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),
+ SOME (format, type_enc)) =
with_cleanup clean_up run () |> tap export
val important_message =
@@ -347,7 +350,7 @@
(case outcome of
NONE =>
let
- val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
+ val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val meths =
bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
@@ -362,6 +365,7 @@
fn preplay =>
let
val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+
fun isar_params () =
let
val metis_type_enc =
@@ -372,11 +376,12 @@
atp_proof
|> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
|> introduce_spass_skolem
- |> factify_atp_proof fact_names hyp_ts concl_t
+ |> factify_atp_proof (map fst used_from) hyp_ts concl_t
in
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
minimize <> SOME false, atp_proof, goal)
end
+
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command thy params minimize_command name preplay, subgoal,