# HG changeset patch # User blanchet # Date 1386567226 -3600 # Node ID 64177ce0a7bdfeac88cced56aa5c8a2e59f93d57 # Parent 65c4fd04b5b26ed535d1c92eaa66af8ed8101b2f adapted code for Z3 proof reconstruction diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Dec 09 06:33:46 2013 +0100 @@ -101,13 +101,13 @@ (* tries merging the first step into the second step *) fun try_merge - (Prove (_, Fix [], lbl1, _, [], By ((lfs1, gfs1), MetisM))) - (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs2, gfs2), MetisM))) = + (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), MetisM))) + (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), MetisM))) = let val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 in - SOME (Prove (qs2, fix, lbl2, t, subproofs, By ((lfs, gfs), MetisM))) + SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), MetisM))) end | try_merge _ _ = NONE @@ -148,7 +148,7 @@ replace_successor: label -> label list -> label -> unit) = let fun add_refs (Let _) tab = tab - | add_refs (Prove (_, _, v, _, _, By ((lfs, _), _))) tab = + | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) tab = fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab val tab = @@ -177,16 +177,13 @@ fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs = if null subs orelse not (compress_further ()) then (set_preplay_time l (false, time); - Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), - By ((lfs, gfs), MetisM))) + Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), MetisM))) else case subs of - ((sub as Proof(_, Assume assms, sub_steps)) :: subs) => + ((sub as Proof (_, assms, sub_steps)) :: subs) => (let - (* trivial subproofs have exactly one Prove step *) - val SOME (Prove (_, Fix [], l', _, [], - By ((lfs', gfs'), MetisM))) = (try the_single) sub_steps + val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), MetisM))) = try the_single sub_steps (* only touch proofs that can be preplayed sucessfully *) val (false, time') = get_preplay_time l' @@ -197,7 +194,7 @@ subtract (op =) (map fst assms) lfs' |> union (op =) lfs val gfs'' = union (op =) gfs' gfs - val by = By ((lfs'', gfs''), MetisM) + val by = ((lfs'', gfs''), MetisM) val step'' = Prove (qs, fix, l, t, subs'', by) (* check if the modified step can be preplayed fast enough *) @@ -216,7 +213,7 @@ fun elim_subproofs (step as Let _) = step | elim_subproofs - (step as Prove (qs, fix, l, t, subproofs, By ((lfs, gfs), MetisM))) = + (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), MetisM))) = if subproofs = [] then step else case get_preplay_time l of (true, _) => step (* timeout or fail *) @@ -273,8 +270,7 @@ map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times - val ((cand as Prove (_, _, l, _, _, - By ((lfs, _), MetisM))) :: steps') = drop i steps + val ((cand as Prove (_, _, l, _, _, ((lfs, _), MetisM))) :: steps') = drop i steps (* FIXME: debugging *) val _ = (if (label_of_step cand |> the) <> l then diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Mon Dec 09 06:33:46 2013 +0100 @@ -24,14 +24,14 @@ fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...} - (step as Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) = + (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) = (case get_preplay_time l of (* don't touch steps that time out or fail; minimizing won't help *) (true, _) => step | (false, time) => let fun mk_step_lfs_gfs lfs gfs = - Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method)) + Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method)) val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs) fun minimize_facts _ time min_facts [] = (time, min_facts) @@ -90,14 +90,14 @@ |> do_refed_step' and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar" - | do_refed_step' (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m))) = + | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) = let val (refed, subproofs) = map do_proof subproofs |> split_list |>> Ord_List.unions label_ord |>> add_lfs lfs - val step = Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), m)) + val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m)) in (refed, step) end diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 09 06:33:46 2013 +0100 @@ -101,11 +101,13 @@ (* turn terms/proofs into theorems *) fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) -fun thm_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = + +fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = let - val concl = (case try List.last steps of - SOME (Prove (_, Fix [], _, t, _, _)) => t - | _ => raise Fail "preplay error: malformed subproof") + val concl = + (case try List.last steps of + SOME (Prove (_, [], _, t, _, _)) => t + | _ => raise Fail "preplay error: malformed subproof") val var_idx = maxidx_of_term concl + 1 fun var_of_free (x, T) = Var((x, var_idx), T) val substitutions = @@ -135,7 +137,7 @@ (* main function for preplaying isar_steps; may throw exceptions *) fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time | preplay_raw debug type_enc lam_trans ctxt timeout - (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) = + (Prove (_, xs, _, t, subproofs, (fact_names, proof_method))) = let val (prop, obtain) = (case xs of @@ -201,7 +203,7 @@ val enrich_with_assms = fold (uncurry enrich_with_fact) - fun enrich_with_proof (Proof (_, Assume assms, isar_steps)) = + fun enrich_with_proof (Proof (_, assms, isar_steps)) = enrich_with_assms assms #> fold enrich_with_step isar_steps and enrich_with_step (Let _) = I diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 09 06:33:46 2013 +0100 @@ -251,7 +251,7 @@ #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By (facts, method))) = + | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, method))) = (case xs of [] => (* have *) add_step_pre ind qs subproofs @@ -274,23 +274,16 @@ and add_steps ind = fold (add_step ind) - and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) = - ("", ctxt) - |> add_fix ind xs - |> add_assms ind assms - |> add_steps ind steps - |> fst - + and of_proof ind ctxt (Proof (xs, assms, steps)) = + ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst in - (* FIXME: sh_try0 might produce one-step proofs that are better than the - Metis one-liners *) - (* One-step proofs are pointless; better use the Metis one-liner - directly. *) - (*case proof of - Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => "" - | _ =>*) (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ - of_indent 0 ^ (if n <> 1 then "next" else "qed") + (* One-step Metis proofs are pointless; better use the one-liner directly. *) + (case proof of + Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => "" + | _ => + (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ + of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ + of_indent 0 ^ (if n <> 1 then "next" else "qed")) end end; diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 09 06:33:46 2013 +0100 @@ -13,17 +13,12 @@ datatype isar_qualifier = Show | Then - datatype fix = Fix of (string * typ) list - datatype assms = Assume of (label * term) list - datatype isar_proof = - Proof of fix * assms * isar_step list + Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = Let of term * term | - (* for |fix|>0, this is an obtain step; step may contain subproofs *) - Prove of isar_qualifier list * fix * label * term * isar_proof list * byline - and byline = - By of facts * proof_method + Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * + (facts * proof_method) and proof_method = MetisM | SimpM | @@ -42,13 +37,13 @@ val string_of_label : label -> string - val fix_of_proof : isar_proof -> fix - val assms_of_proof : isar_proof -> assms + val fix_of_proof : isar_proof -> (string * typ) list + val assms_of_proof : isar_proof -> (label * term) list val steps_of_proof : isar_proof -> isar_step list val label_of_step : isar_step -> label option val subproofs_of_step : isar_step -> isar_proof list option - val byline_of_step : isar_step -> byline option + val byline_of_step : isar_step -> (facts * proof_method) option val proof_method_of_step : isar_step -> proof_method option val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a @@ -57,8 +52,6 @@ val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof - val map_facts_of_byline : (facts -> facts) -> byline -> byline - val add_proof_steps : isar_step list -> int -> int (** canonical proof labels: 1, 2, 3, ... in postorder **) @@ -77,17 +70,12 @@ datatype isar_qualifier = Show | Then -datatype fix = Fix of (string * typ) list -datatype assms = Assume of (label * term) list - datatype isar_proof = - Proof of fix * assms * isar_step list + Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = Let of term * term | - (* for |fix|>0, this is an obtain step; step may contain subproofs *) - Prove of isar_qualifier list * fix * label * term * isar_proof list * byline -and byline = - By of facts * proof_method + Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * + (facts * proof_method) and proof_method = MetisM | SimpM | @@ -119,7 +107,7 @@ fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline | byline_of_step _ = NONE -fun proof_method_of_step (Prove (_, _, _, _, _, By(_, method))) = SOME method +fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method | proof_method_of_step _ = NONE fun fold_isar_steps f = fold (fold_isar_step f) @@ -130,23 +118,14 @@ fun map_isar_steps f proof = let - fun do_proof (Proof (fix, assms, steps)) = - Proof (fix, assms, map do_step steps) - + fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps) and do_step (step as Let _) = f step | do_step (Prove (qs, xs, l, t, subproofs, by)) = - let - val subproofs = map do_proof subproofs - val step = Prove (qs, xs, l, t, subproofs, by) - in - f step - end + f (Prove (qs, xs, l, t, map do_proof subproofs, by)) in do_proof proof end -fun map_facts_of_byline f (By (facts, method)) = By (f facts, method) - val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) @@ -163,8 +142,7 @@ fun next_label l (next, subst) = let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end - fun do_byline by (_, subst) = - by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the))) + fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by handle Option.Option => raise Fail "Sledgehammer_Proof: relabel_proof_canonically" @@ -173,12 +151,12 @@ val (l, state) = next_label l state in ((l, t), state) end - fun do_proof (Proof (fix, Assume assms, steps)) state = + fun do_proof (Proof (fix, assms, steps)) state = let val (assms, state) = fold_map do_assm assms state val (steps, state) = fold_map do_step steps state in - (Proof (fix, Assume assms, steps), state) + (Proof (fix, assms, steps), state) end and do_step (step as Let _) state = (step, state) diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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) diff -r 65c4fd04b5b2 -r 64177ce0a7bd src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 09 05:06:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 09 06:33:46 2013 +0100 @@ -21,12 +21,12 @@ open Sledgehammer_Preplay fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants" - | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) = + | variants (Prove (qs, xs, l, t, subproofs, (facts, _))) = let val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM] - fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method)) + fun step method = Prove (qs, xs, l, t, subproofs, (facts, method)) (*fun step_without_facts method = - Prove (qs, xs, l, t, subproofs, By (no_facts, method))*) + Prove (qs, xs, l, t, subproofs, (no_facts, method))*) in (* FIXME *) (* There seems to be a bias for methods earlier in the list, so we put