author blanchet Tue, 15 Jan 2013 20:51:30 +0100 changeset 50905 db99fcf69761 parent 50904 3d2d62d29302 child 50906 67b04a8375b0 child 50909 b2fb1ab1475d
more improvements to Isar proof reconstructions
```--- 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, [])
@@ -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 =