--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 25 17:06:11 2023 +0100
@@ -514,8 +514,9 @@
|| $$ "(" |-- parse_hol_typed_var --| $$ ")") x
fun parse_simple_hol_term x =
- (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term
- >> (fn ((q, ys), t) =>
+ (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":")
+ -- parse_simple_hol_term
+ >> (fn ((q, ys), t) =>
fold_rev
(fn (var, ty) => fn r =>
AAbs (((var, the_default dummy_atype ty), r), [])
@@ -524,11 +525,12 @@
else
I))
ys t)
- || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not)
+ || Scan.this_string tptp_not |-- parse_simple_hol_term >> mk_app (mk_simple_aterm tptp_not)
|| scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
>> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
|| parse_hol_quantifier >> mk_simple_aterm
|| $$ "(" |-- parse_hol_term --| $$ ")"
+ || Scan.this_string tptp_not >> mk_simple_aterm
|| parse_literal_binary_op >> mk_simple_aterm
|| parse_nonliteral_binary_op >> mk_simple_aterm) x
and parse_applied_hol_term x =
@@ -541,7 +543,14 @@
and parse_hol_term x =
(parse_literal_hol_term -- Scan.repeat (parse_nonliteral_binary_op -- parse_literal_hol_term)
>> (fn (t1, c_ti_s) =>
- fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x
+ let
+ val cs = map fst c_ti_s
+ val tis = t1 :: map snd c_ti_s
+ val (tis_but_k, tk) = split_last tis
+ in
+ fold_rev (fn (ti, c) => fn right => mk_apps (mk_simple_aterm c) [ti, right])
+ (tis_but_k ~~ cs) tk
+ end)) x
fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x
@@ -624,7 +633,7 @@
val parse_spass_annotations =
Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
-(* We ignore the stars and the pluses that follow literals. *)
+(* We ignore the stars and the pluses that follow literals in SPASS's output. *)
fun parse_decorated_atom x =
(parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 25 17:06:11 2023 +0100
@@ -107,6 +107,8 @@
fun lambda' v = Term.lambda_name (term_name' v, v)
+fun If_const T = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T)
+
fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
@@ -240,6 +242,8 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
+val zip_internal_ite_prefix = "zip_internal_ite_"
+
fun var_index_of_textual textual = if textual then 0 else 1
fun quantify_over_var textual quant_of var_s var_T t =
@@ -253,10 +257,12 @@
| norm_var_types t = t
in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
-(* This assumes that distinct names are mapped to distinct names by "Variable.variant_frees". This
- does not hold in general but should hold for ATP-generated Skolem function names, since these end
- with a digit and "variant_frees" appends letters. *)
-fun fresh_up ctxt s = fst (hd (Variable.variant_frees ctxt [] [(s, ())]))
+(* This assumes that distinct names are mapped to distinct names by
+ "Variable.variant_frees". This does not hold in general but should hold for
+ ATP-generated Skolem function names, since these end with a digit and
+ "variant_frees" appends letters. *)
+fun desymbolize_and_fresh_up ctxt s =
+ fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())]))
(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
are typed. The code is similar to "term_of_atp_fo". *)
@@ -267,12 +273,16 @@
fun do_term opt_T u =
(case u of
- AAbs (((var, ty), term), []) =>
+ AAbs (((var, ty), term), us) =>
let
val typ = typ_of_atp_type ctxt ty
val var_name = repair_var_name var
val tm = do_term NONE term
- in quantify_over_var true lambda' var_name typ tm end
+ val lam = quantify_over_var true lambda' var_name typ tm
+ val args = map (do_term NONE) us
+ in
+ list_comb (lam, args)
+ end
| ATerm ((s, tys), us) =>
if s = "" (* special marker generated on parse error *) then
error "Isar proof reconstruction failed because the ATP proof contains unparsable \
@@ -302,6 +312,7 @@
else if s = tptp_ho_exists then HOLogic.exists_const dummyT
else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
else if s = tptp_hilbert_the then \<^term>\<open>The\<close>
+ else if String.isPrefix zip_internal_ite_prefix s then If_const dummyT
else
(case unprefix_and_unascii const_prefix s of
SOME s' =>
@@ -337,7 +348,7 @@
(case unprefix_and_unascii fixed_var_prefix s of
SOME s => Free (s, T)
| NONE =>
- if not (is_tptp_variable s) then Free (fresh_up ctxt s, T)
+ if not (is_tptp_variable s) then Free (desymbolize_and_fresh_up ctxt s, T)
else Var ((repair_var_name s, var_index), T))
in list_comb (t, ts) end))
in do_term end
@@ -428,7 +439,7 @@
SOME s => Free (s, T)
| NONE =>
if textual andalso not (is_tptp_variable s) then
- Free (s |> textual ? fresh_up ctxt, T)
+ Free (desymbolize_and_fresh_up ctxt s, T)
else
Var ((repair_var_name s, var_index), T))
in list_comb (t, ts) end))
@@ -768,6 +779,17 @@
input_steps @ sko_steps @ map repair_deps other_steps
end
+val zf_stmt_prefix = "zf_stmt_"
+
+fun is_if_True_or_False_axiom true_or_false t =
+ (case t of
+ @{const Trueprop} $
+ (Const (@{const_name HOL.eq}, _) $
+ (Const (@{const_name If}, _) $ cond $ Var _ $ Var _) $
+ Var _) =>
+ cond aconv true_or_false
+ | _ => false)
+
fun factify_atp_proof facts hyp_ts concl_t atp_proof =
let
fun factify_step ((num, ss), role, t, rule, deps) =
@@ -779,7 +801,18 @@
else ([], Hypothesis, close_form (nth hyp_ts j))
| _ =>
(case resolve_facts facts (num :: ss) of
- [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t)
+ [] =>
+ if role = Axiom andalso String.isPrefix zf_stmt_prefix num
+ andalso is_if_True_or_False_axiom @{const True} t then
+ (["if_True"], Axiom, t)
+ else if role = Axiom andalso String.isPrefix zf_stmt_prefix num
+ andalso is_if_True_or_False_axiom @{const False} t then
+ (["if_False"], Axiom, t)
+ else
+ (ss,
+ if role = Definition then Definition
+ else if role = Lemma then Lemma
+ else Plain, t)
| facts => (map fst facts, Axiom, t)))
in
((num, ss'), role', t', rule, deps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 25 17:06:11 2023 +0100
@@ -134,9 +134,12 @@
bool * (string option * string option) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
-val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
-val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
+val basic_systematic_methods =
+ [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method, Argo_Method]
+val basic_simp_based_methods =
+ [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
+val basic_arith_methods =
+ [Linarith_Method, Presburger_Method, Algebra_Method]
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
val systematic_methods =
@@ -258,6 +261,8 @@
and is_referenced_in_proof l (Proof {steps, ...}) =
exists (is_referenced_in_step l) steps
+ (* We try to introduce pure lemmas (not "obtains") close to where
+ they are used. *)
fun insert_lemma_in_step lem
(step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs),
proof_methods, comment}) =
@@ -283,7 +288,8 @@
end
and insert_lemma_in_steps lem [] = [lem]
| insert_lemma_in_steps lem (step :: steps) =
- if is_referenced_in_step (the (label_of_isar_step lem)) step then
+ if not (null (obtains_of_isar_step lem))
+ orelse is_referenced_in_step (the (label_of_isar_step lem)) step then
insert_lemma_in_step lem step @ steps
else
step :: insert_lemma_in_steps lem steps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Sep 25 17:06:11 2023 +0100
@@ -46,6 +46,7 @@
val steps_of_isar_proof : isar_proof -> isar_step list
val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof
+ val obtains_of_isar_step : isar_step -> (string * typ) list
val label_of_isar_step : isar_step -> label option
val facts_of_isar_step : isar_step -> facts
val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -130,6 +131,9 @@
fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps =
Proof {fixes = fixes, assumptions = assumptions, steps = steps}
+fun obtains_of_isar_step (Prove {obtains, ...}) = obtains
+ | obtains_of_isar_step _ = []
+
fun label_of_isar_step (Prove {label, ...}) = SOME label
| label_of_isar_step _ = NONE
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Sep 25 17:06:11 2023 +0100
@@ -18,6 +18,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -60,6 +61,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -101,6 +103,7 @@
| SMT_Method (SMT_Verit strategy) =>
"smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
| SATx_Method => "satx"
+ | Argo_Method => "argo"
| Blast_Method => "blast"
| Simp_Method => if null ss then "simp" else "simp add:"
| Auto_Method => "auto"
@@ -141,6 +144,7 @@
Method.insert_tac ctxt global_facts THEN'
(case meth of
SATx_Method => SAT.satx_tac ctxt
+ | Argo_Method => Argo_Tactic.argo_tac ctxt []
| Blast_Method => blast_tac ctxt
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Sep 25 17:06:05 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Sep 25 17:06:11 2023 +0100
@@ -217,7 +217,8 @@
let
val misc_methodss =
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
- Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
+ Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
+ Argo_Method]]
val metis_methodss =
[Metis_Method (SOME full_typesN, NONE) ::