# HG changeset patch
# User blanchet
# Date 1358279490 -3600
# Node ID db99fcf697615afb4bb0a542d8d4d623a77ed9fd
# Parent  3d2d62d293029e598fef6fd73dece90f837f5890
more improvements to Isar proof reconstructions

diff -r 3d2d62d29302 -r db99fcf69761 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jan 15 20:51:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Jan 15 20:51:30 2013 +0100
@@ -365,8 +365,11 @@
    clsarity). *)
 fun is_only_type_information t = t aconv @{term True}
 
+fun s_maybe_not role = role <> Conjecture ? s_not
+
 fun is_same_inference _ (Definition_Step _) = false
-  | is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t'
+  | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
+    s_maybe_not role t aconv s_maybe_not role' t'
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
@@ -375,18 +378,14 @@
              lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if is_fact fact_names ss then
+    if is_conjecture ss then
+      Inference_Step (name, role, t, rule, []) :: lines
+    else if is_fact fact_names ss then
       (* Facts are not proof lines. *)
       if is_only_type_information t then
         map (replace_dependencies_in_line (name, [])) 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
-        (_, []) => lines (* no repetition of proof line *)
-      | (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, role, t, rule, []) :: lines
+      else
+        lines
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
@@ -394,7 +393,7 @@
     if is_only_type_information t then
       line :: 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
+    else case take_prefix (not o is_same_inference (role, t)) lines of
       (* FIXME: Doesn't this code risk conflating proofs involving different
          types? *)
       (_, []) => line :: lines
@@ -406,8 +405,8 @@
 
 val repair_waldmeister_endgame =
   let
-    fun do_tail (Inference_Step (name, role, t, rule, deps)) =
-        Inference_Step (name, role, s_not t, rule, deps)
+    fun do_tail (Inference_Step (name, _, t, rule, deps)) =
+        Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
       | do_tail line = line
     fun do_body [] = []
       | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
@@ -652,8 +651,8 @@
           |> nasty_atp_proof pool
           |> map_term_names_in_atp_proof repair_name
           |> decode_lines ctxt sym_tab
+          |> repair_waldmeister_endgame
           |> rpair [] |-> fold_rev (add_line fact_names)
-          |> repair_waldmeister_endgame
           |> rpair [] |-> fold_rev add_nontrivial_line
           |> rpair (0, [])
           |-> fold_rev (add_desired_line fact_names frees)
@@ -685,7 +684,7 @@
                     | Inference_Step (name as (s, ss), role, t, rule, _) =>
                       Symtab.update_new (s, (rule,
                         t |> (if member (op = o apsnd fst) tainted s then
-                                (role <> Conjecture ? s_not)
+                                s_maybe_not role
                                 #> fold exists_of (map Var (Term.add_vars t []))
                               else
                                 I))))
@@ -726,9 +725,9 @@
             in
               if is_clause_skolemize_rule c then
                 let
-                  val xs =
-                    Term.add_frees t []
-                    |> filter_out (Variable.is_declared ctxt o fst)
+                  val is_fixed =
+                    Variable.is_declared ctxt orf can Name.dest_skolem
+                  val xs = Term.add_frees t [] |> filter_out (is_fixed o fst)
                 in Obtain ([], xs, l, t, by) end
               else
                 Prove (maybe_show outer c [], l, t, by)