--- 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 = ""
--- 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, _, _, _) =>