--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Feb 15 11:36:34 2013 +0100
@@ -18,7 +18,7 @@
structure Atom_Graph : GRAPH
type ref_sequent = atom list * atom
- type ref_graph = unit Atom_Graph.T
+ type refute_graph = unit Atom_Graph.T
type clause = atom list
type direct_sequent = atom list * clause
@@ -32,15 +32,15 @@
type direct_proof = direct_inference list
- val make_ref_graph : (atom list * atom) list -> ref_graph
- val axioms_of_ref_graph : ref_graph -> atom list -> atom list
- val tainted_atoms_of_ref_graph : ref_graph -> atom list -> atom list
- val sequents_of_ref_graph : ref_graph -> ref_sequent list
- val string_of_ref_graph : ref_graph -> string
+ val make_refute_graph : (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 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 -> ref_graph -> direct_proof
+ 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;
@@ -53,7 +53,7 @@
structure Atom_Graph = Graph(Atom)
type ref_sequent = atom list * atom
-type ref_graph = unit Atom_Graph.T
+type refute_graph = unit Atom_Graph.T
type clause = atom list
type direct_sequent = atom list * clause
@@ -72,7 +72,7 @@
fun direct_sequent_eq ((gamma, c), (delta, d)) =
clause_eq (gamma, delta) andalso clause_eq (c, d)
-fun make_ref_graph infers =
+fun make_refute_graph infers =
let
fun add_edge to from =
Atom_Graph.default_node (from, ())
@@ -81,21 +81,24 @@
fun add_infer (froms, to) = fold (add_edge to) froms
in Atom_Graph.empty |> fold add_infer infers end
-fun axioms_of_ref_graph ref_graph conjs =
- subtract atom_eq conjs (Atom_Graph.minimals ref_graph)
-fun tainted_atoms_of_ref_graph ref_graph = Atom_Graph.all_succs ref_graph
+fun axioms_of_refute_graph refute_graph conjs =
+ subtract atom_eq conjs (Atom_Graph.minimals refute_graph)
-fun sequents_of_ref_graph ref_graph =
- map (`(Atom_Graph.immediate_preds ref_graph))
- (filter_out (Atom_Graph.is_minimal ref_graph) (Atom_Graph.keys ref_graph))
+fun tainted_atoms_of_refute_graph refute_graph =
+ 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))
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_ref_graph ref_graph =
- ref_graph |> sequents_of_ref_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
@@ -148,10 +151,10 @@
| zones_of n (bs :: bss) =
(fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
-fun redirect_graph axioms tainted bot ref_graph =
+fun redirect_graph axioms tainted bot refute_graph =
let
val seqs =
- map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
+ map (redirect_sequent tainted bot) (sequents_of_refute_graph refute_graph)
val direct_graph = direct_graph seqs
fun redirect c proved seqs =
if null seqs then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 11:36:34 2013 +0100
@@ -89,8 +89,7 @@
(* proof references *)
fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
| refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
- | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
- lookup_indices lfs @ maps (maps refs) cases
+ | refs (Prove (_, _, _, Case_Split cases)) = maps (maps refs) cases
| refs (Prove (_, _, _, Subblock proof)) = maps refs proof
| refs _ = []
val refed_by_vect =
@@ -234,9 +233,9 @@
in fold_map f_m candidates zero_preplay_time end
val compress_subproof =
compress_each_and_collect_time (do_proof false ctxt)
- fun compress (Prove (qs, l, t, Case_Split (cases, facts))) =
+ fun compress (Prove (qs, l, t, Case_Split cases)) =
let val (cases, time) = compress_subproof cases
- in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+ in (Prove (qs, l, t, Case_Split cases), time) end
| compress (Prove (qs, l, t, Subblock proof)) =
let val ([proof], time) = compress_subproof [proof]
in (Prove (qs, l, t, Subblock proof), time) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 11:36:34 2013 +0100
@@ -84,17 +84,15 @@
val facts =
(case byline of
By_Metis fact_names => resolve_fact_names ctxt fact_names
- | Case_Split (cases, fact_names) =>
- resolve_fact_names ctxt fact_names
- @ (case the succedent of
- Assume (_, t) => make_thm t
- | Obtain (_, _, _, t, _) => make_thm t
- | Prove (_, _, t, _) => make_thm t
- | _ => error "preplay error: unexpected succedent of case split")
- :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
- | _ => error "preplay error: malformed case split")
- #> make_thm)
- cases
+ | Case_Split cases =>
+ (case the succedent of
+ Assume (_, t) => make_thm t
+ | Obtain (_, _, _, t, _) => make_thm t
+ | Prove (_, _, t, _) => make_thm t
+ | _ => error "preplay error: unexpected succedent of case split")
+ :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+ | _ => error "preplay error: malformed case split")
+ #> make_thm) cases
| Subblock proof =>
let
val (steps, last_step) = split_last proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 11:36:34 2013 +0100
@@ -22,7 +22,7 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts |
+ Case_Split of isar_step list list |
Subblock of isar_step list
val string_for_label : label -> string
@@ -46,7 +46,7 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts |
+ Case_Split of isar_step list list |
Subblock of isar_step list
fun string_for_label (s, num) = s ^ string_of_int num
@@ -57,7 +57,7 @@
fun metis_steps_total proof =
fold (fn Obtain _ => Integer.add 1
| Prove (_, _, _, By_Metis _) => Integer.add 1
- | Prove (_, _, _, Case_Split (cases, _)) =>
+ | Prove (_, _, _, Case_Split cases) =>
Integer.add (fold (Integer.add o metis_steps_total) cases 1)
| Prove (_, _, _, Subblock subproof) =>
Integer.add (metis_steps_total subproof + 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 11:31:59 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 11:36:34 2013 +0100
@@ -501,10 +501,10 @@
do_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
| do_step ind (Prove (qs, l, t, By_Metis facts)) =
do_prove ind qs l t facts
- | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
+ | do_step ind (Prove (qs, l, t, Case_Split proofs)) =
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
proofs) ^
- do_prove ind qs l t facts
+ do_prove ind qs l t ([], [])
| do_step ind (Prove (qs, l, t, Subblock proof)) =
do_block ind proof ^ do_prove ind qs l t ([], [])
and do_steps prefix suffix ind steps =
@@ -531,8 +531,7 @@
| used_labels_of_step (Prove (_, _, _, by)) =
(case by of
By_Metis (ls, _) => ls
- | Case_Split (proofs, (ls, _)) =>
- fold (union (op =) o used_labels_of) proofs ls
+ | Case_Split proofs => fold (union (op =) o used_labels_of) proofs []
| Subblock proof => used_labels_of proof)
| used_labels_of_step _ = []
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
@@ -546,8 +545,7 @@
| do_step (Prove (qs, l, t, by)) =
Prove (qs, do_label l, t,
case by of
- Case_Split (proofs, facts) =>
- Case_Split (map do_proof proofs, facts)
+ Case_Split proofs => Case_Split (map do_proof proofs)
| Subblock proof => Subblock (do_proof proof)
| _ => by)
| do_step step = step
@@ -570,9 +568,8 @@
fun do_byline subst depth nexts by =
case by of
By_Metis facts => By_Metis (do_facts subst facts)
- | Case_Split (proofs, facts) =>
- Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs,
- do_facts subst facts)
+ | Case_Split proofs =>
+ Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs)
| Subblock proof => Subblock (do_proof subst depth nexts proof)
and do_proof _ _ _ [] = []
| do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
@@ -623,8 +620,8 @@
Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
else
step
- | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) =
- Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs, facts))
+ | chain_step _ (Prove (qs, l, t, Case_Split proofs)) =
+ Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs))
| chain_step _ (Prove (qs, l, t, Subblock proof)) =
Prove (qs, l, t, Subblock (chain_proof NONE proof))
| chain_step _ step = step
@@ -684,9 +681,10 @@
fun dep_of_step (Definition_Step _) = NONE
| dep_of_step (Inference_Step (name, _, _, _, from)) =
SOME (from, name)
- val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
- val axioms = axioms_of_ref_graph ref_graph conjs
- val tainted = tainted_atoms_of_ref_graph ref_graph conjs
+ val refute_graph =
+ atp_proof |> map_filter dep_of_step |> make_refute_graph
+ val axioms = axioms_of_refute_graph refute_graph conjs
+ val tainted = tainted_atoms_of_refute_graph refute_graph conjs
val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
@@ -699,8 +697,7 @@
else
I))))
atp_proof
- fun is_clause_skolemize_rule [atom as (s, _)] =
- not (member (op =) tainted atom) andalso
+ fun is_clause_skolemize_rule [(s, _)] =
Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
SOME true
| is_clause_skolemize_rule _ = false
@@ -723,51 +720,77 @@
| _ => fold (curry s_disj) lits @{term False}
end
|> HOLogic.mk_Trueprop |> close_form
- fun maybe_show outer c =
- (outer andalso length c = 1 andalso subset (op =) (c, conjs))
- ? cons Show
- fun isar_step_of_direct_inf outer (Have (gamma, c)) =
+ fun isar_proof_of_direct_proof _ accum [] = assms @ rev accum
+ | isar_proof_of_direct_proof outer accum (inf :: infs) =
let
- val l = label_of_clause c
- val t = prop_of_clause c
- val by =
- By_Metis (fold (add_fact_from_dependencies fact_names) gamma
- ([], []))
+ fun maybe_show outer c =
+ (outer andalso length c = 1 andalso subset (op =) (c, conjs))
+ ? cons Show
+ fun do_rest step =
+ isar_proof_of_direct_proof outer (step :: accum) infs
+ 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)
in
- if is_clause_skolemize_rule c then
+ case inf of
+ Have (gamma, c) =>
let
- val is_fixed =
- Variable.is_declared ctxt orf can Name.dest_skolem
- val xs = Term.add_frees t [] |> filter_out (is_fixed o fst)
- in Obtain ([], xs, l, t, by) end
- else
- Prove (maybe_show outer c [], l, t, by)
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val by =
+ By_Metis (fold (add_fact_from_dependencies fact_names) gamma
+ ([], []))
+ fun prove outer = Prove (maybe_show outer c [], l, t, by)
+ val redirected = exists (member (op =) tainted) c
+ in
+ if redirected then
+ case gamma of
+ [g] =>
+ if is_clause_skolemize_rule g then
+ let
+ val proof =
+ Fix (skolems_of (prop_of_clause g)) :: rev accum
+ in
+ isar_proof_of_direct_proof outer
+ [Prove (maybe_show outer c [Then],
+ label_of_clause c, prop_of_clause c,
+ Subblock proof)] []
+ end
+ else
+ do_rest (prove outer)
+ | _ => do_rest (prove outer)
+ else
+ if is_clause_skolemize_rule c then
+ do_rest (Obtain ([], skolems_of t, l, t, by))
+ else
+ do_rest (prove outer)
+ end
+ | Cases cases =>
+ let
+ fun do_case (c, infs) =
+ Assume (label_of_clause c, prop_of_clause c) ::
+ isar_proof_of_direct_proof false [] infs
+ val c = succedent_of_cases cases
+ in
+ do_rest (Prove (maybe_show outer c [Ultimately],
+ label_of_clause c, prop_of_clause c,
+ Case_Split (map do_case cases)))
+ end
end
- | isar_step_of_direct_inf outer (Cases cases) =
- let val c = succedent_of_cases cases in
- Prove (maybe_show outer c [Ultimately], label_of_clause c,
- prop_of_clause c,
- Case_Split (map (do_case false) cases, ([], [])))
- end
- and do_case outer (c, infs) =
- Assume (label_of_clause c, prop_of_clause c) ::
- map (isar_step_of_direct_inf outer) infs
val (isar_proof, (preplay_fail, preplay_time)) =
- ref_graph
+ refute_graph
|> redirect_graph axioms tainted bot
- |> map (isar_step_of_direct_inf true)
- |> append assms
+ |> isar_proof_of_direct_proof true []
|> (if not preplay andalso isar_compress <= 1.0 then
rpair (false, (true, seconds 0.0))
else
compress_proof debug ctxt type_enc lam_trans preplay
preplay_timeout
(if isar_proofs then isar_compress else 1000.0))
- (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
- |>> chain_direct_proof
- |>> kill_useless_labels_in_proof
- |>> relabel_proof
- |>> not (null params) ? cons (Fix params)
+ |>> (chain_direct_proof
+ #> kill_useless_labels_in_proof
+ #> relabel_proof
+ #> not (null params) ? cons (Fix params))
val isar_text =
string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
isar_proof