# HG changeset patch
# User wenzelm
# Date 1386791867 -3600
# Node ID 5cfcb71779881fd06d43b05f3fd018b0b761215c
# Parent  55ed20a29a8c04e18e42ec1517ffeb084cdd57b1# Parent  8c5221d698cdcb867d1ede37647d93cb41942a97
merged

diff -r 8c5221d698cd -r 5cfcb7177988 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Dec 11 20:38:39 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Dec 11 20:57:47 2013 +0100
@@ -39,8 +39,7 @@
   val string_of_refute_graph : refute_graph -> string
   val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
   val direct_graph : direct_sequent list -> direct_graph
-  val redirect_graph :
-    atom list -> atom list -> atom -> refute_graph -> direct_proof
+  val redirect_graph : atom list -> atom list -> atom -> refute_graph -> direct_proof
   val succedent_of_cases : (clause * direct_inference list) list -> clause
   val string_of_direct_proof : direct_proof -> string
 end;
@@ -82,7 +81,9 @@
     fun add_infer (froms, to) = fold (add_edge to) froms
     val graph = fold add_infer infers Atom_Graph.empty
     val reachable = Atom_Graph.all_preds graph [bot]
-  in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end
+  in
+    graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable)
+  end
 
 fun axioms_of_refute_graph refute_graph conjs =
   subtract atom_eq conjs (Atom_Graph.minimals refute_graph)
@@ -91,17 +92,16 @@
   Atom_Graph.all_succs refute_graph
 
 fun sequents_of_refute_graph refute_graph =
-  map (`(Atom_Graph.immediate_preds refute_graph))
-      (filter_out (Atom_Graph.is_minimal refute_graph)
-                  (Atom_Graph.keys refute_graph))
+  Atom_Graph.keys refute_graph
+  |> filter_out (Atom_Graph.is_minimal refute_graph)
+  |> map (`(Atom_Graph.immediate_preds refute_graph))
 
 val string_of_context = map Atom.string_of #> space_implode ", "
 
 fun string_of_sequent (gamma, c) =
   string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
 
-fun string_of_refute_graph refute_graph =
-  refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines
+val string_of_refute_graph = sequents_of_refute_graph #> map string_of_sequent #> cat_lines
 
 fun redirect_sequent tainted bot (gamma, c) =
   if member atom_eq tainted c then
@@ -131,28 +131,15 @@
   | dest_Have _ = raise Fail "non-Have"
 
 fun enrich_Have nontrivs trivs (cs, c) =
-  (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs)
-                      else c),
+  Have (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs) else c),
    disj (c :: trivs))
-  |> Have
 
-fun s_cases cases =
-  case cases |> List.partition (null o snd) of
-    (trivs, nontrivs as [(nontriv0, proof)]) =>
-    if forall (can dest_Have) proof then
-      let val seqs = proof |> map dest_Have in
-        seqs |> map (enrich_Have (nontriv0 :: map snd seqs) (map fst trivs))
-      end
-    else
-      [Cases nontrivs]
-  | (_, nontrivs) => [Cases nontrivs]
+fun s_cases cases = [Cases (filter_out (null o snd) cases)]
 
-fun descendants direct_graph =
-  these o try (Atom_Graph.all_succs direct_graph) o single
+fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single
 
 fun zones_of 0 _ = []
-  | zones_of n (bs :: bss) =
-    (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
+  | zones_of n (bs :: bss) = (fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
 
 fun redirect_graph axioms tainted bot refute_graph =
   let
@@ -165,13 +152,12 @@
       else if length c < 2 then
         let
           val proved = c @ proved
-          val provable =
-            filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
+          val provable = filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
           val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
           val seq as (gamma, c) =
-            case horn_provable @ provable of
+            (case horn_provable @ provable of
               [] => raise Fail "ill-formed refutation graph"
-            | next :: _ => next
+            | next :: _ => next)
         in
           Have (map single gamma, c) ::
           redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
@@ -183,10 +169,10 @@
           val zones = zones_of (length c) (map (descendants direct_graph) c)
           val subseqss = map (subsequents seqs) zones
           val seqs = fold (subtract direct_sequent_eq) subseqss seqs
-          val cases =
-            map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs))
-                 c subseqss
-        in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end
+          val cases = map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs)) c subseqss
+        in
+          s_cases cases @ redirect (succedent_of_cases cases) proved seqs
+        end
   in redirect [] axioms seqs end
 
 fun indent 0 = ""
diff -r 8c5221d698cd -r 5cfcb7177988 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 20:38:39 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 11 20:57:47 2013 +0100
@@ -67,6 +67,12 @@
 fun is_same_inference (role, t) (_, role', t', _, _) =
   (t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)
 
+fun is_False t = t aconv @{term False} orelse t aconv @{prop False}
+
+fun truncate_at_false [] = []
+  | truncate_at_false ((line as (_, role, t, _, _)) :: lines) =
+    line :: (if role <> Conjecture andalso is_False t then [] else truncate_at_false lines)
+
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
 fun add_line (name as (_, ss), role, t, rule, []) lines =
@@ -103,19 +109,19 @@
 
 val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
 
-fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) =
-  (j + 1,
-   if role <> Plain orelse is_skolemize_rule rule orelse
-      (* the last line must be kept *)
-      j = 0 orelse
-      (not (is_only_type_information t) andalso
-       null (Term.add_tvars t []) andalso
-       length deps >= 2 andalso
-       (* kill next to last line, which usually results in a trivial step *)
-       j <> 1) then
-     (name, role, t, rule, deps) :: lines  (* keep line *)
-   else
-     map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
+fun add_desired_lines res [] = rev res
+  | add_desired_lines res ((name as (_, ss), role, t, rule, deps) :: lines) =
+    if role <> Plain orelse is_skolemize_rule rule orelse
+       (* the last line must be kept *)
+       null lines orelse
+       (not (is_only_type_information t) andalso
+        null (Term.add_tvars t []) andalso
+        length deps >= 2 andalso
+        (* don't keep next to last line, which usually results in a trivial step *)
+        not (can the_single lines)) then
+      add_desired_lines ((name, role, t, rule, deps) :: res) lines
+    else
+      add_desired_lines res (map (replace_dependencies_in_line (name, deps)) lines)
 
 val add_labels_of_proof =
   steps_of_proof
@@ -226,11 +232,10 @@
       let
         val atp_proof =
           atp_proof
+          |> truncate_at_false
           |> rpair [] |-> fold_rev add_line
           |> rpair [] |-> fold_rev add_nontrivial_line
-          |> rpair (0, [])
-          |-> fold_rev add_desired_line
-          |> snd
+          |> add_desired_lines []
 
         val conjs =
           map_filter (fn (name, role, _, _, _) =>