# HG changeset patch
# User blanchet
# Date 1352197256 -3600
# Node ID 01cb92151a539b0deae9da89c978a9be6ca2ead3
# Parent  f046cf7be176f44dd1544b9384bb5aafeadef860
track formula roles in proofs and use that to determine whether the conjecture should be negated or not

diff -r f046cf7be176 -r 01cb92151a53 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Nov 06 11:20:56 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Nov 06 11:20:56 2012 +0100
@@ -42,7 +42,10 @@
     THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
     DFG of polymorphism
 
-  datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
+  datatype formula_role =
+    Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
+    Plain | Unknown
+
   datatype 'a problem_line =
     Class_Decl of string * 'a * 'a list |
     Type_Decl of string * 'a * int |
@@ -178,7 +181,10 @@
   THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
   DFG of polymorphism
 
-datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
+datatype formula_role =
+  Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture |
+  Plain | Unknown
+
 datatype 'a problem_line =
   Class_Decl of string * 'a * 'a list |
   Type_Decl of string * 'a * int |
@@ -325,6 +331,9 @@
   | tptp_string_for_role Lemma = "lemma"
   | tptp_string_for_role Hypothesis = "hypothesis"
   | tptp_string_for_role Conjecture = "conjecture"
+  | tptp_string_for_role Negated_Conjecture = "negated_conjecture"
+  | tptp_string_for_role Plain = "plain"
+  | tptp_string_for_role Unknown = "unknown"
 
 fun tptp_string_for_app _ func [] = func
   | tptp_string_for_app format func args =
diff -r f046cf7be176 -r 01cb92151a53 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 06 11:20:56 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 06 11:20:56 2012 +0100
@@ -9,6 +9,7 @@
 signature ATP_PROOF =
 sig
   type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
+  type formula_role = ATP_Problem.formula_role
   type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
   type 'a problem = 'a ATP_Problem.problem
 
@@ -38,7 +39,7 @@
 
   datatype 'a step =
     Definition_Step of step_name * 'a * 'a |
-    Inference_Step of step_name * 'a * string * step_name list
+    Inference_Step of step_name * formula_role * 'a * string * step_name list
 
   type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
 
@@ -213,12 +214,12 @@
 
 datatype 'a step =
   Definition_Step of step_name * 'a * 'a |
-  Inference_Step of step_name * 'a * string * step_name list
+  Inference_Step of step_name * formula_role * 'a * string * step_name list
 
 type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
 
 fun step_name (Definition_Step (name, _, _)) = name
-  | step_name (Inference_Step (name, _, _, _)) = name
+  | step_name (Inference_Step (name, _, _, _, _)) = name
 
 (**** PARSING OF TSTP FORMAT ****)
 
@@ -374,6 +375,15 @@
 fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms))
   | commute_eq _ = raise Fail "expected equation"
 
+fun role_of_tptp_string "axiom" = Axiom
+  | role_of_tptp_string "definition" = Definition
+  | role_of_tptp_string "lemma" = Lemma
+  | role_of_tptp_string "hypothesis" = Hypothesis
+  | role_of_tptp_string "conjecture" = Conjecture
+  | role_of_tptp_string "negated_conjecture" = Negated_Conjecture
+  | role_of_tptp_string "plain" = Plain
+  | role_of_tptp_string _ = Unknown
+
 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
             <formula> <extra_arguments>\).
    The <num> could be an identifier, but we assume integers. *)
@@ -407,16 +417,18 @@
                   phi), "", [])
               | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
             fun mk_step () =
-              Inference_Step (name, phi, rule, map (rpair []) deps)
+              Inference_Step (name, role_of_tptp_string role, phi, rule,
+                              map (rpair []) deps)
           in
-            case role of
-              "definition" =>
+            case role_of_tptp_string role of
+              Definition =>
               (case phi of
                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
                  Definition_Step (name, phi1, phi2)
                | AAtom (ATerm (("equal", []), _)) =>
                  (* Vampire's equality proxy axiom *)
-                 Inference_Step (name, phi, rule, map (rpair []) deps)
+                 Inference_Step (name, Definition, phi, rule,
+                                 map (rpair []) deps)
                | _ => mk_step ())
             | _ => mk_step ()
           end)
@@ -462,7 +474,8 @@
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
    >> (fn ((((num, rule), deps), u), names) =>
-          Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x
+          Inference_Step ((num, these names), Unknown, u, rule,
+                          map (rpair []) deps))) x
 
 val satallax_coreN = "__satallax_core" (* arbitrary *)
 val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
@@ -471,12 +484,14 @@
 fun parse_z3_tptp_line x =
   (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
    >> (fn (name, names) =>
-          Inference_Step (("", name :: names), dummy_phi, z3_tptp_coreN, []))) x
+          Inference_Step (("", name :: names), Unknown, dummy_phi,
+                          z3_tptp_coreN, []))) x
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_coreN, []))) x
+   >> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN,
+                               []))) x
 
 fun parse_line problem =
   parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
@@ -499,8 +514,9 @@
   | clean_up_dependencies seen
                           ((step as Definition_Step (name, _, _)) :: steps) =
     step :: clean_up_dependencies (name :: seen) steps
-  | clean_up_dependencies seen (Inference_Step (name, u, rule, deps) :: steps) =
-    Inference_Step (name, u, rule,
+  | clean_up_dependencies seen
+        (Inference_Step (name, role, u, rule, deps) :: steps) =
+    Inference_Step (name, role, u, rule,
         map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
     clean_up_dependencies (name :: seen) steps
 
@@ -516,8 +532,8 @@
 fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) =
     Definition_Step (name, map_term_names_in_formula f phi1,
                      map_term_names_in_formula f phi2)
-  | map_term_names_in_step f (Inference_Step (name, phi, rule, deps)) =
-    Inference_Step (name, map_term_names_in_formula f phi, rule, deps)
+  | map_term_names_in_step f (Inference_Step (name, role, phi, rule, deps)) =
+    Inference_Step (name, role, map_term_names_in_formula f phi, rule, deps)
 fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
 
 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
diff -r f046cf7be176 -r 01cb92151a53 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 11:20:56 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 11:20:56 2012 +0100
@@ -129,7 +129,8 @@
 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
 
 fun is_axiom_used_in_proof pred =
-  exists (fn Inference_Step ((_, ss), _, _, []) => exists pred ss | _ => false)
+  exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
+           | _ => false)
 
 fun lam_trans_from_atp_proof atp_proof default =
   case (is_axiom_used_in_proof is_combinator_def atp_proof,
@@ -163,7 +164,7 @@
 val leo2_ext = "extcnf_equal_neg"
 val leo2_unfold_def = "unfold_def"
 
-fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
+fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
     (if rule = leo2_ext then
        insert (op =) (ext_name ctxt, (Global, General))
      else if rule = leo2_unfold_def then
@@ -367,13 +368,13 @@
       (Definition_Step (name, t1, t2),
        fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
     end
-  | decode_line sym_tab (Inference_Step (name, u, rule, deps)) ctxt =
+  | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
       val t = u |> prop_from_atp ctxt true sym_tab
                 |> uncombine_term thy |> infer_formula_types ctxt
     in
-      (Inference_Step (name, t, rule, deps),
+      (Inference_Step (name, role, t, rule, deps),
        fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
     end
 fun decode_lines ctxt sym_tab lines =
@@ -382,8 +383,9 @@
 fun replace_one_dependency (old, new) dep =
   if is_same_atp_step dep old then new else [dep]
 fun replace_dependencies_in_line _ (line as Definition_Step _) = line
-  | replace_dependencies_in_line p (Inference_Step (name, t, rule, deps)) =
-    Inference_Step (name, t, rule,
+  | replace_dependencies_in_line p
+        (Inference_Step (name, role, t, rule, deps)) =
+    Inference_Step (name, role, t, rule,
                     fold (union (op =) o replace_one_dependency p) deps [])
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
@@ -391,12 +393,13 @@
 fun is_only_type_information t = t aconv @{term True}
 
 fun is_same_inference _ (Definition_Step _) = false
-  | is_same_inference t (Inference_Step (_, t', _, _)) = t aconv t'
+  | is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t'
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
 fun add_line _ (line as Definition_Step _) lines = line :: lines
-  | add_line fact_names (Inference_Step (name as (_, ss), t, rule, [])) lines =
+  | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
+             lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
     if is_fact fact_names ss then
@@ -406,24 +409,24 @@
       (* Is there a repetition? If so, replace later line by earlier one. *)
       else case take_prefix (not o is_same_inference t) lines of
         (_, []) => lines (* no repetition of proof line *)
-      | (pre, Inference_Step (name', _, _, _) :: post) =>
+      | (pre, Inference_Step (name', _, _, _, _) :: post) =>
         pre @ map (replace_dependencies_in_line (name', [name])) post
       | _ => raise Fail "unexpected inference"
     else if is_conjecture ss then
-      Inference_Step (name, t, rule, []) :: lines
+      Inference_Step (name, role, t, rule, []) :: lines
     else
       map (replace_dependencies_in_line (name, [])) lines
-  | add_line _ (Inference_Step (name, t, rule, deps)) lines =
+  | add_line _ (Inference_Step (name, role, t, rule, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
-      Inference_Step (name, t, rule, deps) :: lines
+      Inference_Step (name, role, t, rule, deps) :: lines
     (* Is there a repetition? If so, replace later line by earlier one. *)
     else case take_prefix (not o is_same_inference t) lines of
       (* FIXME: Doesn't this code risk conflating proofs involving different
          types? *)
-       (_, []) => Inference_Step (name, t, rule, deps) :: lines
-     | (pre, Inference_Step (name', t', rule, _) :: post) =>
-       Inference_Step (name, t', rule, deps) ::
+       (_, []) => Inference_Step (name, role, t, rule, deps) :: lines
+     | (pre, Inference_Step (name', role, t', rule, _) :: post) =>
+       Inference_Step (name, role, t', rule, deps) ::
        pre @ map (replace_dependencies_in_line (name', [name])) post
      | _ => raise Fail "unexpected inference"
 
@@ -431,18 +434,18 @@
 
 val repair_waldmeister_endgame =
   let
-    fun do_tail (Inference_Step (name, t, rule, deps)) =
-        Inference_Step (name, s_not t, rule, deps)
+    fun do_tail (Inference_Step (name, role, t, rule, deps)) =
+        Inference_Step (name, role, s_not t, rule, deps)
       | do_tail line = line
     fun do_body [] = []
-      | do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) =
+      | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
         if num = waldmeister_conjecture_num then map do_tail (line :: lines)
         else line :: do_body lines
       | do_body (line :: lines) = line :: do_body lines
   in do_body end
 
 (* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines =
+fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
     if is_only_type_information t then delete_dependency name lines
     else line :: lines
   | add_nontrivial_line line lines = line :: lines
@@ -458,7 +461,7 @@
 fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   | add_desired_line fact_names frees
-        (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) =
+        (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
     (j + 1,
      if is_fact fact_names ss orelse
         is_conjecture ss orelse
@@ -470,7 +473,7 @@
          length deps >= 2 andalso
          (* kill next to last line, which usually results in a trivial step *)
          j <> 1) then
-       Inference_Step (name, t, rule, deps) :: lines  (* keep line *)
+       Inference_Step (name, role, t, rule, deps) :: lines  (* keep line *)
      else
        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
 
@@ -960,12 +963,12 @@
         val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
         val conjs =
           atp_proof |> map_filter
-            (fn Inference_Step (name as (_, ss), _, _, []) =>
+            (fn Inference_Step (name as (_, ss), _, _, _, []) =>
                 if member (op =) ss conj_name then SOME name else NONE
               | _ => NONE)
         val assms =
           atp_proof |> map_filter
-            (fn Inference_Step (name as (_, ss), t, _, []) =>
+            (fn Inference_Step (name as (_, ss), _, t, _, []) =>
                 if exists (String.isPrefix conjecture_prefix) ss andalso
                    not (member (op =) conjs name) then
                   SOME (Assume (raw_label_for_name name, t))
@@ -973,17 +976,18 @@
                   NONE
               | _ => NONE)
         fun dep_of_step (Definition_Step _) = NONE
-          | dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)
+          | dep_of_step (Inference_Step (name, _, _, _, from)) =
+            SOME (from, name)
         val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
         val axioms = axioms_of_ref_graph ref_graph conjs
         val tainted = tainted_atoms_of_ref_graph ref_graph conjs
         val props =
           Symtab.empty
           |> fold (fn Definition_Step _ => I (* FIXME *)
-                    | Inference_Step ((s, _), t, _, _) =>
+                    | Inference_Step ((s, _), role, t, _, _) =>
                       Symtab.update_new (s,
                           if member (op = o apsnd fst) tainted s then
-                            t |> s_not
+                            t |> role <> Conjecture ? s_not
                               |> fold exists_of (map Var (Term.add_vars t []))
                           else
                             t))