handle Zipperposition definitions in Isar proof construction

--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Feb 22 09:58:25 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Feb 22 12:36:01 2022 +0100
@@ -563,20 +563,20 @@
      (if full then parse_hol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
      -- parse_tstp_extra_arguments --| $$ ")"
   --| $$ "."
-  >> (fn (((num, role), phi), src) =>
+  >> (fn (((num, role0), phi), src) =>
       let
-        val role' = role_of_tptp_string role
-        val ((name, phi), rule, deps) =
+        val role = role_of_tptp_string role0
+        val (name, phi, role', rule, deps) =
           (case src of
             SOME (File_Source (_, SOME s)) =>
-            if role' = Definition then
-              (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
+            if role = Definition then
+              ((num, map fst (find_formula_in_problem phi problem)), phi, role, "", [])
             else
-              (((num, [s]), phi), "", [])
-          | SOME (Inference_Source (rule, deps)) => (((num, []), phi), rule, deps)
-          | SOME (Introduced_Source rule) => (((num, []), phi), rule, [])
-          | SOME Define_Source => (((num, []), phi), zipperposition_define_rule, [])
-          | _ => (((num, [num]), phi), "", []))
+              ((num, [s]), phi, role, "", [])
+          | SOME (Inference_Source (rule, deps)) => ((num, []), phi, role, rule, deps)
+          | SOME (Introduced_Source rule) => ((num, []), phi, Definition, rule, [])
+          | SOME Define_Source => ((num, []), phi, Definition, zipperposition_define_rule, [])
+          | _ => ((num, [num]), phi, role, "", []))
       in
         [(name, role', phi, rule, map (rpair []) deps)]
       end)
@@ -607,8 +607,8 @@
               | SOME (File_Source _) =>
                 (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
               | SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps)
-              | SOME (Introduced_Source rule) => (((num, []), phi), Lemma, rule, [])
-              | SOME Define_Source => (((num, []), phi), Lemma, zipperposition_define_rule, [])
+              | SOME (Introduced_Source rule) => (((num, []), phi), Definition, rule, [])
+              | SOME Define_Source => (((num, []), phi), Definition, zipperposition_define_rule, [])
               | _ => (((num, [num]), phi), role, "", []))
 
             fun mk_step () = (name, role', phi, rule, map (rpair []) deps)

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 22 09:58:25 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Feb 22 12:36:01 2022 +0100
@@ -782,7 +782,7 @@
             else ([], Hypothesis, close_form (nth hyp_ts j))
           | _ =>
             (case resolve_facts facts (num :: ss) of
-              [] => (ss, if role = Lemma then Lemma else Plain, t)
+              [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t)
             | facts => (map fst facts, Axiom, t)))
       in
         ((num, ss'), role', t', rule, deps)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 22 09:58:25 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 22 12:36:01 2022 +0100
@@ -89,7 +89,8 @@
       line :: lines
     else if t aconv \<^prop>\<open>True\<close> then
       map (replace_dependencies_in_line (name, [])) lines
-    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
+    else if role = Definition orelse role = Lemma orelse role = Hypothesis
+        orelse is_arith_rule rule then
       line :: lines
     else if role = Axiom then
       lines (* axioms (facts) need no proof lines *)
@@ -220,7 +221,8 @@
               end
 
             val (lems, _) =
-              fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
+              fold_map add_lemma (map_filter (get_role (member (op =) [Definition, Lemma]))
+                atp_proof) ctxt
 
             val bot = #1 (List.last atp_proof)
 
@@ -453,7 +455,8 @@
                    (do_preplay ? keep_fastest_method_of_isar_step (!preplay_data)
                     #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
               |> tap (trace_isar_proof "Minimized")
-              |> `(preplay_outcome_of_isar_proof (!preplay_data))
+              |> `(if do_preplay then preplay_outcome_of_isar_proof (!preplay_data)
+                   else K (Play_Timed_Out Time.zeroTime))
               ||> (comment_isar_proof comment_of
                    #> chain_isar_proof
                    #> kill_useless_labels_in_isar_proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 22 09:58:25 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 22 12:36:01 2022 +0100
@@ -166,8 +166,12 @@
     play_outcome
   end
 
-fun preplay_isar_step_for_method ctxt chained timeout meth =
-  try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt chained timeout meth step =
+  if timeout = Time.zeroTime then
+    Play_Timed_Out Time.zeroTime
+  else
+    try (raw_preplay_step_for_method ctxt chained timeout meth) step
+    |> the_default Play_Failed
 
 val min_preplay_timeout = seconds 0.002