--- 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
--- 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
--- 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
--- 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;
--- 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)
--- 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)
--- 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