merged
authorpaulson
Mon, 25 Sep 2023 17:06:11 +0100
changeset 78699 584159939058
parent 78697 8ca71c0ae31f (diff)
parent 78698 1b9388e6eb75 (current diff)
child 78700 4de5b127c124
merged
--- 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) ::