# HG changeset patch
# User blanchet
# Date 1413143565 -7200
# Node ID 4b44c227c0e0a88d9d1ef8e1d3e575d14ba8bf7d
# Parent  da12763acd6bf12cbbbd06b260ad8b3730a46eb1
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax

diff -r da12763acd6b -r 4b44c227c0e0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 21:52:44 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -28,6 +28,9 @@
   val partial_type_encs : string list
   val default_metis_lam_trans : string
 
+  val leo2_extcnf_equal_neg_rule : string
+  val satallax_tab_rule_prefix : string
+
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
   val simplify_bool : term -> term
@@ -91,6 +94,9 @@
 
 val default_metis_lam_trans = combsN
 
+val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
+val satallax_tab_rule_prefix = "tab_"
+
 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
   | term_name' _ = ""
 
@@ -499,10 +505,9 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
-val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
-
 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
-  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule then
+  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse
+      String.isPrefix satallax_tab_rule_prefix rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
    else
      I)
diff -r da12763acd6b -r 4b44c227c0e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Oct 12 21:52:44 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Oct 12 21:52:45 2014 +0200
@@ -66,6 +66,9 @@
    spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
    veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
 
+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
 fun is_arith_rule rule =
   String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
@@ -77,8 +80,10 @@
 fun label_of_clause [(num, _)] = raw_label_of_num num
   | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
 
-fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
-  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
+fun add_global_fact ss = apsnd (union (op =) ss)
+
+fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss
+  | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names))
 
 fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
     (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
@@ -118,8 +123,9 @@
     in
       if is_duplicate orelse
           (role = Plain andalso not (is_skolemize_rule rule) andalso
-           not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso
-           not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
+           not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
+           not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso
+           not (is_before_skolemize_rule ())) then
         add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
       else
         add_lines_pass2 (line :: res) lines
@@ -292,7 +298,8 @@
               val skolem = is_skolemize_rule rule
 
               val deps = ([], [])
-                |> fold add_fact_of_dependencies gamma
+                |> 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