--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 09 05:06:48 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 09 06:33:46 2013 +0100
@@ -72,9 +72,10 @@
(* 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 =
- (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
- definitions. *)
- if role = Conjecture orelse role = Negated_Conjecture orelse role = Hypothesis then
+ (* 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
(name, role, t, rule, []) :: lines
else if role = Axiom then
(* Facts are not proof lines. *)
@@ -96,14 +97,12 @@
if is_only_type_information t then delete_dependency name lines else line :: lines
| add_nontrivial_line line lines = line :: lines
and delete_dependency name lines =
- fold_rev add_nontrivial_line
- (map (replace_dependencies_in_line (name, [])) lines) []
+ fold_rev add_nontrivial_line (map (replace_dependencies_in_line (name, [])) lines) []
val e_skolemize_rule = "skolemize"
val vampire_skolemisation_rule = "skolemisation"
-val is_skolemize_rule =
- member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
+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,
@@ -119,22 +118,23 @@
else
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
-
val add_labels_of_proof =
- steps_of_proof #> fold_isar_steps
- (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I))
+ steps_of_proof
+ #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
fun kill_useless_labels_in_proof proof =
let
val used_ls = add_labels_of_proof proof []
- fun do_label l = if member (op =) used_ls l then l else no_label
- fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
- fun do_step (Prove (qs, xs, l, t, subproofs, by)) =
- Prove (qs, xs, do_label l, t, map do_proof subproofs, by)
- | do_step step = step
- and do_proof (Proof (fix, assms, steps)) =
- Proof (fix, do_assms assms, map do_step steps)
- in do_proof proof end
+ fun kill_label l = if member (op =) used_ls l then l else no_label
+ fun kill_assms assms = map (apfst kill_label) assms
+ fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
+ | kill_step step = step
+ and kill_proof (Proof (fix, assms, steps)) =
+ Proof (fix, kill_assms assms, map kill_step steps)
+ in
+ kill_proof proof
+ end
fun prefix_of_depth n = replicate_string (n + 1)
@@ -150,51 +150,53 @@
let val l' = (prefix_of_depth depth prefix, next) in
(l', (l, l') :: subst, next + 1)
end
- fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
- fun do_assm depth (l, t) (subst, next) =
+
+ fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
+
+ fun relabel_assm depth (l, t) (subst, next) =
let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
((l, t), (subst, next))
end
- fun do_assms subst depth (Assume assms) =
- fold_map (do_assm depth) assms (subst, 1) |>> Assume ||> fst
- fun do_steps _ _ _ [] = []
- | do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
+
+ fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
+
+ fun relabel_steps _ _ _ [] = []
+ | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
let
val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
- val sub = do_proofs subst depth sub
- val by = by |> do_byline subst
- in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
- | do_steps subst depth next (step :: steps) =
- step :: do_steps subst depth next steps
- and do_proof subst depth (Proof (fix, assms, steps)) =
- let val (assms, subst) = do_assms subst depth assms in
- Proof (fix, assms, do_steps subst depth 1 steps)
+ val sub = relabel_proofs subst depth sub
+ val by = by |> relabel_byline subst
+ in
+ Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+ end
+ | relabel_steps subst depth next (step :: steps) =
+ step :: relabel_steps subst depth next steps
+ and relabel_proof subst depth (Proof (fix, assms, steps)) =
+ let val (assms, subst) = relabel_assms subst depth assms in
+ Proof (fix, assms, relabel_steps subst depth 1 steps)
end
- and do_byline subst byline =
- map_facts_of_byline (do_facts subst) byline
- and do_proofs subst depth = map (do_proof subst (depth + 1))
- in do_proof [] 0 end
+ and relabel_byline subst byline = apfst (relabel_facts subst) byline
+ and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
+ in
+ relabel_proof [] 0
+ end
val chain_direct_proof =
let
- fun do_qs_lfs NONE lfs = ([], lfs)
- | do_qs_lfs (SOME l0) lfs =
- if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
- else ([], lfs)
- fun chain_step lbl
- (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
- let val (qs', lfs) = do_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, chain_proofs subproofs,
- By ((lfs, gfs), method))
- end
+ fun chain_qs_lfs NONE lfs = ([], lfs)
+ | chain_qs_lfs (SOME l0) lfs =
+ if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
+ fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
+ let val (qs', lfs) = chain_qs_lfs lbl lfs in
+ Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), method))
+ end
| chain_step _ step = step
and chain_steps _ [] = []
| chain_steps (prev as SOME _) (i :: is) =
chain_step prev i :: chain_steps (label_of_step i) is
| chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
- and chain_proof (Proof (fix, Assume assms, steps)) =
- Proof (fix, Assume assms,
- chain_steps (try (List.last #> fst) assms) steps)
+ and chain_proof (Proof (fix, assms, steps)) =
+ Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
and chain_proofs proofs = map (chain_proof) proofs
in chain_proof end
@@ -217,6 +219,9 @@
val one_line_proof = one_line_proof_text 0 one_line_params
val do_preplay = preplay_timeout <> SOME Time.zeroTime
+ fun get_role keep_role ((num, _), role, t, _, _) =
+ if keep_role role then SOME (raw_label_of_num num, t) else NONE
+
fun isar_proof_of () =
let
val atp_proof =
@@ -226,19 +231,26 @@
|> rpair (0, [])
|-> fold_rev add_desired_line
|> snd
+
val conjs =
- atp_proof |> map_filter (fn (name, role, _, _, _) =>
- if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE)
- val assms =
- atp_proof
- |> map_filter (try (fn ((num, _), Hypothesis, t, _, _) => (raw_label_of_num num, t)))
+ map_filter (fn (name, role, _, _, _) =>
+ if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
+ atp_proof
+ val assms = map_filter (get_role (curry (op =) Hypothesis)) atp_proof
+ val lems =
+ map_filter (get_role (curry (op =) Lemma)) atp_proof
+ |> map (fn (l, t) => Prove ([], [], l, t, [], (([], []), ArithM)))
+
val bot = atp_proof |> List.last |> #1
+
val refute_graph =
atp_proof
|> map (fn (name, _, _, _, from) => (from, name))
|> make_refute_graph bot
|> fold (Atom_Graph.default_node o rpair ()) conjs
+
val axioms = axioms_of_refute_graph refute_graph conjs
+
val tainted = tainted_atoms_of_refute_graph refute_graph conjs
val is_clause_tainted = exists (member (op =) tainted)
val steps =
@@ -251,9 +263,11 @@
else
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
+
(* The assumptions and conjecture are "prop"s; the other formulas are "bool"s. *)
fun prop_of_clause [(num, _)] =
Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
@@ -267,65 +281,64 @@
| _ => fold (curry s_disj) lits @{term False}
end
|> HOLogic.mk_Trueprop |> close_form
- fun isar_proof_of_direct_proof infs =
- let
- fun maybe_show outer c =
- (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
- val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
- fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
- fun do_steps outer predecessor accum [] =
- accum
- |> (if tainted = [] then
- cons (Prove (if outer then [Show] else [], Fix [], no_label, concl_t, [],
- By (([the predecessor], []), MetisM)))
- else
- I)
- |> rev
- | do_steps outer _ accum (Have (gamma, c) :: infs) =
- let
- val l = label_of_clause c
- val t = prop_of_clause c
- val by = By (fold add_fact_of_dependencies gamma no_facts, MetisM)
- fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by)
- fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs
- in
- if is_clause_tainted c then
- case gamma of
- [g] =>
- if is_clause_skolemize_rule g andalso is_clause_tainted g then
- let
- val subproof =
- Proof (Fix (skolems_of (prop_of_clause g)), Assume [], rev accum)
- in
- do_steps outer (SOME l) [prove [subproof] (By (no_facts, MetisM))] []
- end
- else
- do_rest l (prove [] by)
- | _ => do_rest l (prove [] by)
+
+ val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+ fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
+
+ fun maybe_show outer c =
+ (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
+
+ fun isar_steps outer predecessor accum [] =
+ accum
+ |> (if tainted = [] then
+ cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
+ (([the predecessor], []), MetisM)))
+ else
+ I)
+ |> rev
+ | isar_steps outer _ accum (Have (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)
+ 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
+ in
+ if is_clause_tainted c then
+ case gamma of
+ [g] =>
+ if is_clause_skolemize_rule g 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
else
- if is_clause_skolemize_rule c then
- do_rest l (Prove ([], Fix (skolems_of t), l, t, [], by))
- else
- do_rest l (prove [] by)
- end
- | do_steps outer predecessor accum (Cases cases :: infs) =
- let
- fun do_case (c, infs) =
- do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
- val c = succedent_of_cases cases
- val l = label_of_clause c
- val t = prop_of_clause c
- val step =
- Prove (maybe_show outer c [], Fix [], l, t, map do_case cases,
- By ((the_list predecessor, []), MetisM))
- in
- do_steps outer (SOME l) (step :: accum) infs
- end
- and do_proof outer fix assms infs =
- Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)
- in
- do_proof true params assms infs
- end
+ do_rest l (prove [] by)
+ | _ => do_rest l (prove [] by)
+ else
+ if is_clause_skolemize_rule c then
+ do_rest l (Prove ([], skolems_of t, l, t, [], by))
+ else
+ do_rest l (prove [] by)
+ end
+ | isar_steps outer predecessor accum (Cases cases :: infs) =
+ let
+ fun isar_case (c, infs) =
+ isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] infs
+ val c = succedent_of_cases cases
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val step =
+ Prove (maybe_show outer c [], [], l, t, map isar_case cases,
+ ((the_list predecessor, []), MetisM))
+ in
+ isar_steps outer (SOME l) (step :: accum) infs
+ end
+ and isar_proof outer fix assms lems infs =
+ Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
+
+ val isar_proof_of_direct_proof = isar_proof true params assms lems
(* 60 seconds seems like a good interpreation of "no timeout" *)
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)