# HG changeset patch
# User blanchet
# Date 1645530314 -3600
# Node ID f12539c8de0cfdd6f06153239a3d1a2321592c8f
# Parent  66eb6fdfc24463b3af850f64719985a04f6d3fe0
more handling of Zipperposition definitions in Isar proof construction

diff -r 66eb6fdfc244 -r f12539c8de0c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 22 12:36:01 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 22 12:45:14 2022 +0100
@@ -59,15 +59,15 @@
 val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
 val zipperposition_cnf_rule = "cnf"
 
-val skolemize_rules =
+val symbol_introduction_rules =
   [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
    spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
-   zipperposition_cnf_rule] @ veriT_skolemize_rules
+   zipperposition_cnf_rule, zipperposition_define_rule] @ veriT_skolemize_rules
 
 fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
 val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix
 
-val is_skolemize_rule = member (op =) skolemize_rules
+val is_symbol_introduction_rule = member (op =) symbol_introduction_rules
 fun is_arith_rule rule =
   String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
   rule = veriT_la_generic_rule
@@ -114,15 +114,16 @@
 
       fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2
 
-      fun is_skolemizing_line (_, _, _, rule', deps') =
-        is_skolemize_rule rule' andalso member (op =) deps' name
+      fun is_symbol_introduction_line (_, _, _, rule', deps') =
+        is_symbol_introduction_rule rule' andalso member (op =) deps' name
 
-      fun is_before_skolemize_rule () = exists is_skolemizing_line lines
+      fun is_before_symbol_introduction_rule () = exists is_symbol_introduction_line lines
     in
       if is_duplicate orelse
-          (role = Plain andalso not (is_skolemize_rule rule) andalso
+          (role = Plain andalso not (is_symbol_introduction_rule rule) andalso
            not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
-           not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
+           not (null lines) andalso looks_boring () andalso
+           not (is_before_symbol_introduction_rule ())) then
         add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
       else
         add_lines_pass2 (line :: res) lines
@@ -175,7 +176,8 @@
               | SOME n => n)
 
             fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
-            fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
+            fun introduced_symbols_of ctxt t =
+              Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
 
             fun get_role keep_role ((num, _), role, t, rule, _) =
               if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
@@ -202,14 +204,14 @@
 
             fun add_lemma ((label, goal), rule) ctxt =
               let
-                val (skos, proof_methods) =
-                  (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods)
+                val (obtains, proof_methods) =
+                  (if is_symbol_introduction_rule rule then (introduced_symbols_of ctxt goal, skolem_methods)
                    else if is_arith_rule rule then ([], arith_methods)
                    else ([], rewrite_methods))
                   ||> massage_methods
                 val prove = Prove {
                   qualifiers = [],
-                  obtains = skos,
+                  obtains = obtains,
                   label = label,
                   goal = goal,
                   subproofs = [],
@@ -217,7 +219,7 @@
                   proof_methods = proof_methods,
                   comment = ""}
               in
-                (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+                (prove, ctxt |> not (null obtains) ? (Variable.add_fixes (map fst obtains) #> snd))
               end
 
             val (lems, _) =
@@ -328,14 +330,14 @@
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val rule = rule_of_clause_id id
-                  val skolem = is_skolemize_rule rule
+                  val introduces_symbols = is_symbol_introduction_rule rule
 
                   val deps = ([], [])
                     |> fold add_fact_of_dependency gamma
                     |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
                     |> sort_facts
                   val meths =
-                    (if skolem then skolem_methods
+                    (if introduces_symbols then skolem_methods
                      else if is_arith_rule rule then arith_methods
                      else systematic_methods')
                     |> massage_methods
@@ -354,10 +356,10 @@
                   if is_clause_tainted c then
                     (case gamma of
                       [g] =>
-                      if skolem andalso is_clause_tainted g andalso not (null accum) then
+                      if introduces_symbols andalso is_clause_tainted g andalso not (null accum) then
                         let
-                          val skos = skolems_of ctxt (prop_of_clause g)
-                          val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum}
+                          val fixes = introduced_symbols_of ctxt (prop_of_clause g)
+                          val subproof = Proof {fixes = fixes, assumptions = [], steps = rev accum}
                         in
                           isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
                         end
@@ -366,8 +368,8 @@
                     | _ => steps_of_rest (prove [] deps))
                   else
                     steps_of_rest
-                      (if skolem then
-                         (case skolems_of ctxt t of
+                      (if introduces_symbols then
+                         (case introduced_symbols_of ctxt t of
                            [] => prove [] deps
                          | skos => Prove {
                              qualifiers = [],