# HG changeset patch # User blanchet # Date 1360926609 -3600 # Node ID 65b7ccb1d96a8c8a0ce029f6bd90e5c04da12b41 # Parent 43502299c9350167002f82ad8d1b0a3aee48bf5c# Parent 0ede9e2266a8cd60f66fbad15ace387ce368d1c1 merge diff -r 0ede9e2266a8 -r 65b7ccb1d96a src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Fri Feb 15 12:10:09 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 ^ " \ " ^ 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 diff -r 0ede9e2266a8 -r 65b7ccb1d96a src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 12:10:09 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 diff -r 0ede9e2266a8 -r 65b7ccb1d96a src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 12:10:09 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 diff -r 0ede9e2266a8 -r 65b7ccb1d96a src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 12:10:09 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) diff -r 0ede9e2266a8 -r 65b7ccb1d96a src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 08:31:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 12:10:09 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