--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100
@@ -17,14 +17,14 @@
structure Atom_Graph : GRAPH
- type ref_sequent = atom list * atom
+ type refute_sequent = atom list * atom
type refute_graph = unit Atom_Graph.T
type clause = atom list
- type direct_sequent = atom list * clause
+ type direct_sequent = atom * (atom list * clause)
type direct_graph = unit Atom_Graph.T
- type rich_sequent = clause list * clause
+ type rich_sequent = atom * (clause list * clause)
datatype direct_inference =
Have of rich_sequent |
@@ -35,9 +35,9 @@
val make_refute_graph : atom -> (atom list * atom) list -> refute_graph
val axioms_of_refute_graph : refute_graph -> atom list -> atom list
val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list
- val sequents_of_refute_graph : refute_graph -> ref_sequent list
+ val sequents_of_refute_graph : refute_graph -> refute_sequent list
val string_of_refute_graph : refute_graph -> string
- val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
+ val redirect_sequent : atom list -> atom -> refute_sequent -> direct_sequent
val direct_graph : direct_sequent list -> direct_graph
val redirect_graph : atom list -> atom list -> atom -> refute_graph -> direct_proof
val succedent_of_cases : (clause * direct_inference list) list -> clause
@@ -51,14 +51,14 @@
structure Atom_Graph = Graph(Atom)
-type ref_sequent = atom list * atom
+type refute_sequent = atom list * atom
type refute_graph = unit Atom_Graph.T
type clause = atom list
-type direct_sequent = atom list * clause
+type direct_sequent = atom * (atom list * clause)
type direct_graph = unit Atom_Graph.T
-type rich_sequent = clause list * clause
+type rich_sequent = atom * (clause list * clause)
datatype direct_inference =
Have of rich_sequent |
@@ -69,7 +69,7 @@
val atom_eq = is_equal o Atom.ord
val clause_ord = dict_ord Atom.ord
val clause_eq = is_equal o clause_ord
-val direct_sequent_ord = prod_ord clause_ord clause_ord
+val direct_sequent_ord = prod_ord clause_ord clause_ord o pairself snd
val direct_sequent_eq = is_equal o direct_sequent_ord
fun make_refute_graph bot infers =
@@ -106,11 +106,12 @@
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
- gamma |> List.partition (not o member atom_eq tainted)
- |>> not (atom_eq (c, bot)) ? cons c
- else
- (gamma, [c])
+ (c,
+ if member atom_eq tainted c then
+ gamma |> List.partition (not o member atom_eq tainted)
+ |>> not (atom_eq (c, bot)) ? cons c
+ else
+ (gamma, [c]))
fun direct_graph seqs =
let
@@ -118,26 +119,19 @@
Atom_Graph.default_node (from, ())
#> Atom_Graph.default_node (to, ())
#> Atom_Graph.add_edge_acyclic (from, to)
- fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma
+ fun add_seq (_, (gamma, c)) = fold (fn l => fold (add_edge l) c) gamma
in
fold add_seq seqs Atom_Graph.empty
end
fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord
-fun succedent_of_inference (Have (_, c)) = c
+fun succedent_of_inference (Have (_, (_, c))) = c
| succedent_of_inference (Cases cases) = succedent_of_cases cases
and succedent_of_case (c, []) = c
| succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
and succedent_of_cases cases = disj (map succedent_of_case cases)
-fun dest_Have (Have z) = z
- | dest_Have _ = raise Fail "non-Have"
-
-fun enrich_Have nontrivs trivs (cs, c) =
- Have (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs) else c),
- disj (c :: trivs))
-
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
@@ -156,20 +150,20 @@
else if length c < 2 then
let
val proved = c @ proved
- val provable = filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs
- val horn_provable = filter (fn (_, [_]) => true | _ => false) provable
- val seq as (gamma, c) =
+ val provable = filter (fn (_, (gamma, _)) => subset atom_eq (gamma, proved)) seqs
+ val horn_provable = filter (fn (_, (_, [_])) => true | _ => false) provable
+ val seq as (id, (gamma, c)) =
(case horn_provable @ provable of
[] => raise Fail "ill-formed refutation graph"
| next :: _ => next)
in
- Have (map single gamma, c) ::
+ Have (id, (map single gamma, c)) ::
redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs)
end
else
let
fun subsequents seqs zone =
- filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs
+ filter (fn (_, (gamma, _)) => subset atom_eq (gamma, zone @ proved)) seqs
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
@@ -187,9 +181,9 @@
fun string_of_clause [] = "\<bottom>"
| string_of_clause ls = space_implode " \<or> " (map Atom.string_of ls)
-fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c
- | string_of_rich_sequent ch (cs, c) =
- commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c
+fun string_of_rich_sequent ch (id, (cs, c)) =
+ (if null cs then "" else commas (map string_of_clause cs) ^ " ") ^ ch ^ " " ^ string_of_clause c ^
+ " (* " ^ Atom.string_of id ^ "*)"
fun string_of_case depth (c, proof) =
indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100
@@ -63,6 +63,8 @@
val is_skolemize_rule =
member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+val is_arith_rule = String.isPrefix z3_th_lemma_rule
+
fun raw_label_of_num num = (num, 0)
fun label_of_clause [(num, _)] = raw_label_of_num num
@@ -122,38 +124,38 @@
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
-fun add_line (line as (name as (_, ss), role, t, rule, [])) lines =
+fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
internal facts or definitions. *)
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
- role = Hypothesis then
+ role = Hypothesis orelse is_arith_rule rule then
line :: lines
else if role = Axiom then
(* Facts are not proof lines. *)
lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line line lines = line :: lines
+ | add_line_pass1 line lines = line :: lines
(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
+fun add_line_pass2 (line as (name, _, t, _, [])) lines =
if is_only_type_information t then delete_dependency name lines else line :: lines
- | add_nontrivial_line line lines = line :: lines
+ | add_line_pass2 line lines = line :: lines
and delete_dependency name lines =
- fold_rev add_nontrivial_line (map (replace_dependencies_in_line (name, [])) lines) []
+ fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) []
-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
+fun add_line_pass3 res [] = rev res
+ | add_line_pass3 res ((line as (name as (_, ss), role, t, rule, deps)) :: lines) =
+ if role <> Plain orelse is_skolemize_rule rule orelse is_arith_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
+ add_line_pass3 (line :: res) lines
else
- add_desired_lines res (map (replace_dependencies_in_line (name, deps)) lines)
+ add_line_pass3 res (map (replace_dependencies_in_line (name, deps)) lines)
val add_labels_of_proof =
steps_of_proof
@@ -266,9 +268,9 @@
atp_proof
|> inline_z3_defs []
|> inline_z3_hypotheses [] []
- |> rpair [] |-> fold_rev add_line
- |> rpair [] |-> fold_rev add_nontrivial_line
- |> add_desired_lines []
+ |> rpair [] |-> fold_rev add_line_pass1
+ |> rpair [] |-> fold_rev add_line_pass2
+ |> add_line_pass3 []
val conjs =
map_filter (fn (name, role, _, _, _) =>
@@ -281,8 +283,8 @@
let
val (skos, meth) =
if is_skolemize_rule rule then (skolems_of t, MetisM)
- else if rule = z3_th_lemma_rule then ([], ArithM)
- else ([], SimpM)
+ else if is_arith_rule rule then ([], ArithM)
+ else ([], AutoM)
in
Prove ([], skos, l, maybe_mk_Trueprop t, [], (([], []), meth))
end)
@@ -310,9 +312,7 @@
I))))
atp_proof
- fun is_clause_skolemize_rule [(s, _)] =
- Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
- | is_clause_skolemize_rule _ = false
+ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
(* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or
"prop"s (for Z3). TODO: Always use "prop". *)
@@ -337,22 +337,28 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- (([the predecessor], []), MetisM)))
+ ((the_list predecessor, []), MetisM)))
else
I)
|> rev
- | isar_steps outer _ accum (Have (gamma, c) :: infs) =
+ | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
let
val l = label_of_clause c
val t = prop_of_clause c
- val by = (fold add_fact_of_dependencies gamma no_facts, MetisM)
+ val rule = rule_of_clause_id id
+ val skolem = is_skolemize_rule rule
+
fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
+
+ val deps = fold add_fact_of_dependencies gamma no_facts
+ val meth = if is_arith_rule rule then ArithM else MetisM
+ val by = (deps, meth)
in
if is_clause_tainted c then
(case gamma of
[g] =>
- if is_clause_skolemize_rule g andalso is_clause_tainted g then
+ if skolem andalso is_clause_tainted g then
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
isar_steps outer (SOME l) [prove [subproof] (no_facts, MetisM)] []
end
@@ -360,7 +366,7 @@
do_rest l (prove [] by)
| _ => do_rest l (prove [] by))
else
- (if is_clause_skolemize_rule c then Prove ([], skolems_of t, l, t, [], by)
+ (if skolem then Prove ([], skolems_of t, l, t, [], by)
else prove [] by)
|> do_rest l
end