# HG changeset patch
# User blanchet
# Date 1407163989 -7200
# Node ID 0388026060d18e92a4b2c3a379181df5702a8ca6
# Parent  913b5dd101cbd7e8f7e81973f01cdaca47488672
deal with E definitions

diff -r 913b5dd101cb -r 0388026060d1 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 04 15:08:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 04 16:53:09 2014 +0200
@@ -305,7 +305,8 @@
 
 datatype source =
   File_Source of string * string option |
-  Inference_Source of string * string list
+  Inference_Source of string * string list |
+  Introduced_Source of string
 
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
@@ -326,13 +327,13 @@
   (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
    --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
    -- parse_dependencies --| $$ "]" --| $$ ")") x
-and skip_introduced x =
-  (Scan.this_string "introduced" |-- $$ "(" |-- skip_term
-   -- Scan.repeat ($$ "," |-- skip_term) --| $$ ")") x
+and parse_introduced_source x =
+  (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id
+   --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x
 and parse_source x =
   (parse_file_source >> File_Source
    || parse_inference_source >> Inference_Source
-   || skip_introduced >> K dummy_inference (* for Vampire *)
+   || parse_introduced_source >> Introduced_Source
    || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *)
    || skip_term >> K dummy_inference) x
 
@@ -571,11 +572,12 @@
     |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
     -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
     --| $$ ")" --| $$ "."
-   >> (fn (((num, role), phi), deps) =>
+   >> (fn (((num, role0), phi), src) =>
           let
-            val ((name, phi), rule, deps) =
+            val role = role_of_tptp_string role0
+            val ((name, phi), role', rule, deps) =
               (* Waldmeister isn't exactly helping. *)
-              (case deps of
+              (case src of
                 File_Source (_, SOME s) =>
                 (if s = waldmeister_conjecture_name then
                    (case find_formula_in_problem (mk_anot phi) problem of
@@ -588,13 +590,15 @@
                  else
                    ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
                     phi),
-                 "", [])
+                 role, "", [])
               | File_Source _ =>
-                (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
-              | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
-            fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
+                (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
+              | Inference_Source (rule, deps) => (((num, []), phi), role, rule, deps)
+              | Introduced_Source rule => (((num, []), phi), Lemma, rule, []))
+
+            fun mk_step () = (name, role', phi, rule, map (rpair []) deps)
           in
-            [(case role_of_tptp_string role of
+            [(case role' of
                Definition =>
                (case phi of
                  AAtom (ATerm (("equal", _), _)) =>
diff -r 913b5dd101cb -r 0388026060d1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Aug 04 15:08:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Aug 04 16:53:09 2014 +0200
@@ -740,7 +740,7 @@
 
 fun factify_atp_proof facts hyp_ts concl_t atp_proof =
   let
-    fun factify_step ((num, ss), _, t, rule, deps) =
+    fun factify_step ((num, ss), role, t, rule, deps) =
       let
         val (ss', role', t') =
           (case resolve_conjectures ss of
@@ -748,7 +748,7 @@
             if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
           | _ =>
             (case resolve_facts facts ss of
-              [] => (ss, Plain, t)
+              [] => (ss, if role = Lemma then Lemma else Plain, t)
             | facts => (map fst facts, Axiom, t)))
       in
         ((num, ss'), role', t', rule, deps)
diff -r 913b5dd101cb -r 0388026060d1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 04 15:08:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 04 16:53:09 2014 +0200
@@ -46,6 +46,7 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
 
+val e_definition_rule = "definition"
 val e_skolemize_rule = "skolemize"
 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
 val satallax_skolemize_rule = "tab_ex"
@@ -60,9 +61,9 @@
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
-  [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule,
-   vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
-   zipperposition_cnf_rule]
+  [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
+   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
+   veriT_tmp_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 fun is_arith_rule rule =