# HG changeset patch
# User blanchet
# Date 1272628715 -7200
# Node ID 9bebcb40599f3884ad79a97f8e4fefb5549f1345
# Parent  3a29eb7606c3a0ed34c598bbcd4634b5393cf6d0
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)

diff -r 3a29eb7606c3 -r 9bebcb40599f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 09:36:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 13:58:35 2010 +0200
@@ -48,8 +48,10 @@
   Long_Name.base_name
   #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
 
+val index_in_shape = find_index o exists o curry (op =)
 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
-val index_in_shape = find_index o exists o curry (op =)
+fun is_conjecture_clause_number conjecture_shape num =
+  index_in_shape num conjecture_shape >= 0
 
 fun ugly_name NONE s = s
   | ugly_name (SOME the_pool) s =
@@ -489,8 +491,8 @@
   only in type information.*)
 fun add_line _ _ (line as Definition _) lines = line :: lines
   | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
-    (* No dependencies: axiom, conjecture clause, or internal axioms
-       (Vampire 11). *)
+    (* No dependencies: axiom, conjecture clause, or internal axioms or
+       definitions (Vampire). *)
     if is_axiom_clause_number thm_names num then
       (* Axioms are not proof lines. *)
       if is_only_type_information t then
@@ -500,10 +502,10 @@
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
-    else if index_in_shape num conjecture_shape >= 0 then
+    else if is_conjecture_clause_number conjecture_shape num then
       Inference (num, t, []) :: lines
     else
-      lines
+      map (replace_deps_in_line (num, [])) lines
   | add_line _ _ (Inference (num, t, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
@@ -530,21 +532,27 @@
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
-fun add_desired_line _ _ _ (line as Definition _) (j, lines) =
+(* Vampire is keen on producing these. *)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+                                        $ t1 $ t2)) = (t1 aconv t2)
+  | is_trivial_formula t = false
+
+fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
     (j, line :: lines)
-  | add_desired_line ctxt _ _ (Inference (num, t, [])) (j, lines) =
-    (j, Inference (num, t, []) :: lines)  (* conjecture clauses must be kept *)
-  | add_desired_line ctxt shrink_factor frees (Inference (num, t, deps))
-                     (j, lines) =
+  | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees
+                     (Inference (num, t, deps)) (j, lines) =
     (j + 1,
-     if is_only_type_information t orelse
-        not (null (Term.add_tvars t [])) orelse
-        exists_subterm (is_bad_free frees) t orelse
-        (not (null lines) andalso (* last line must be kept *)
-         (length deps < 2 orelse j mod shrink_factor <> 0)) then
-       map (replace_deps_in_line (num, deps)) lines  (* delete line *)
+     if is_axiom_clause_number thm_names num orelse
+        is_conjecture_clause_number conjecture_shape num orelse
+        (not (is_only_type_information t) andalso
+         null (Term.add_tvars t []) andalso
+         not (exists_subterm (is_bad_free frees) t) andalso
+         not (is_trivial_formula t) andalso
+         (null lines orelse (* last line must be kept *)
+          (length deps >= 2 andalso j mod shrink_factor = 0))) then
+       Inference (num, t, deps) :: lines  (* keep line *)
      else
-       Inference (num, t, deps) :: lines)
+       map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
 
 (** EXTRACTING LEMMAS **)
 
@@ -557,8 +565,6 @@
   let
     val tokens_of = String.tokens (not o is_ident_char)
     fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
-      | extract_num ("cnf" :: num :: "negated_conjecture" :: _) =
-        Int.fromString num
       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
@@ -570,10 +576,9 @@
 fun apply_command _ 1 = "by "
   | apply_command 1 _ = "apply "
   | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_command i n [] =
-    apply_command i n ^ "metis"
-  | metis_command i n xs =
-    apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
+fun metis_command i n [] = apply_command i n ^ "metis"
+  | metis_command i n ss =
+    apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
 fun metis_line i n xs =
   "Try this command: " ^
   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
@@ -619,6 +624,8 @@
 val assum_prefix = "A"
 val fact_prefix = "F"
 
+fun string_for_label (s, num) = s ^ string_of_int num
+
 fun add_fact_from_dep thm_names num =
   if is_axiom_clause_number thm_names num then
     apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
@@ -643,7 +650,8 @@
       |> decode_lines ctxt
       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
-      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor frees)
+      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
+                                               conjecture_shape thm_names frees)
       |> snd
   in
     (if null frees then [] else [Fix frees]) @
@@ -865,7 +873,12 @@
               let
                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
               in (l', (l, l') :: subst, next_fact + 1) end
-          val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
+          val relabel_facts =
+            apfst (map (fn l =>
+                           case AList.lookup (op =) subst l of
+                             SOME l' => l'
+                           | NONE => raise Fail ("unknown label " ^
+                                                 quote (string_for_label l))))
           val by =
             case by of
               ByMetis facts => ByMetis (relabel_facts facts)
@@ -889,8 +902,7 @@
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
-    fun do_raw_label (s, num) = s ^ string_of_int num
-    fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
+    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
     fun do_have qs =
       (if member (op =) qs Moreover then "moreover " else "") ^
       (if member (op =) qs Ultimately then "ultimately " else "") ^
@@ -899,9 +911,11 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    fun do_facts ([], []) = "by metis"
-      | do_facts (ls, ss) =
-        "by (metis " ^ space_implode " " (map do_raw_label ls @ ss) ^ ")"
+    fun do_facts (ls, ss) =
+      let
+        val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
+        val ss = ss |> sort_distinct string_ord
+      in metis_command 1 1 (map string_for_label ls @ ss) end
     and do_step ind (Fix xs) =
         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
       | do_step ind (Let (t1, t2)) =