--- a/NEWS Wed Jul 09 11:48:21 2014 +0200
+++ b/NEWS Wed Jul 09 18:57:20 2014 +0200
@@ -367,7 +367,7 @@
* Sledgehammer:
- Z3 can now produce Isar proofs.
- MaSh overhaul:
- . New SML-based learning engines eliminate the dependency on
+ . New SML-based learning algorithms eliminate the dependency on
Python and increase performance and reliability.
. MaSh and MeSh are now used by default together with the
traditional MePo (Meng-Paulson) relevance filter. To disable
--- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 11:48:21 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 18:57:20 2014 +0200
@@ -872,19 +872,12 @@
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
-\item[\labelitemi] \textbf{\textit{metis}:} Although it is less powerful than
-the external provers, Metis itself can be used for proof search.
-
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
-\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt2} proof method with the
-current settings (usually:\ Z3 with proof reconstruction) can be used for proof
-search.
-
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -909,7 +902,6 @@
via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
a pre-release version of 4.3.2.
-\end{enum}
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
@@ -917,10 +909,11 @@
version 4.3.1 of Z3 or above. To use it, set the environment variable
\texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp}
executable.
+\end{enum}
\end{sloppy}
-In addition to the local provers, the following remote provers are supported:
+Moreover, the following remote provers are supported:
\begin{enum}
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
@@ -980,6 +973,13 @@
SPASS, and Vampire for 5~seconds yields a similar success rate to running the
most effective of these for 120~seconds \cite{boehme-nipkow-2010}.
+In addition to the local and remote provers, the Isabelle proof methods
+\textit{metis} and \textit{smt2} can be specified as \textbf{\textit{metis}}
+and \textbf{\textit{smt}}, respectively. They are generally not recommended
+for proof search but occasionally arise in Sledgehammer-generated
+minimization commands (e.g.,
+``\textbf{sledgehammer} \textit{min} [\textit{prover} = \textit{metis}]'').
+
For the \textit{min} subcommand, the default prover is \textit{metis}. If
several provers are set, the first one is used.
@@ -1056,7 +1056,7 @@
The traditional memoryless MePo relevance filter.
\item[\labelitemi] \textbf{\textit{mash}:}
-The MaSh machine learner. Three learning engines are provided:
+The MaSh machine learner. Three learning algorithms are provided:
\begin{enum}
\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
@@ -1072,20 +1072,21 @@
In addition, the special value \textit{none} is used to disable machine learning by
default (cf.\ \textit{smart} below).
-The default engine is \textit{nb\_knn}. The engine can be selected by setting
-\texttt{MASH} to the name of the desired engine---either in the environment in
-which Isabelle is launched, in your
+The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
+setting \texttt{MASH}---either in the environment in which Isabelle is launched,
+in your
\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
-General'' in Isabelle/jEdit. Persistent data for both engines is stored in the
-directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
+General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
+the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
+mash}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.
\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
-MeSh. If the learning engine is set to be \textit{none}, \textit{smart} behaves
-like MePo.
+MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart}
+behaves like MePo.
\end{enum}
\opdefault{max\_facts}{smart\_int}{smart}
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 09 18:57:20 2014 +0200
@@ -284,8 +284,8 @@
not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
-fun generate_mash_suggestions engine =
- (Options.put_default @{system_option MaSh} engine;
+fun generate_mash_suggestions algorithm =
+ (Options.put_default @{system_option MaSh} algorithm;
Sledgehammer_MaSh.mash_unlearn ();
generate_mepo_or_mash_suggestions
(fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 09 18:57:20 2014 +0200
@@ -1452,7 +1452,7 @@
max_ary = max_ary, types = types, in_conj = in_conj}
val fun_var_Ts' = fun_var_Ts |> can dest_funT T ? insert_type thy I T
in
- if bool_vars' = bool_vars andalso pointer_eq (fun_var_Ts', fun_var_Ts) then accum
+ if bool_vars' = bool_vars andalso fun_var_Ts' = fun_var_Ts then accum
else ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
end
else
@@ -1477,7 +1477,7 @@
val min_ary =
if (app_op_level = Sufficient_App_Op orelse
app_op_level = Sufficient_App_Op_And_Predicator)
- andalso not (pointer_eq (types', types)) then
+ andalso types' <> types then
fold (consider_var_ary T) fun_var_Ts min_ary
else
min_ary
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Jul 09 18:57:20 2014 +0200
@@ -722,7 +722,8 @@
end;
fun maybe_restore lthy_old lthy =
- lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
+ lthy |> not (Theory.eq_thy (pairself Proof_Context.theory_of (lthy_old, lthy)))
+ ? Local_Theory.restore;
val map_bind_def =
(fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 09 18:57:20 2014 +0200
@@ -180,7 +180,6 @@
map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
end;
-val id_def = @{thm id_def};
val mp_conj = @{thm mp_conj};
val fundefcong_attrs = @{attributes [fundef_cong]};
@@ -461,8 +460,8 @@
[induct_case_names_attr]
end;
-fun derive_rel_induct_thm_for_types lthy fpA_Ts ns As Bs mss ctrAss ctrAs_Tsss ctr_sugars
- ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
+fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
+ ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
let
val B_ify = typ_subst_nonatomic (As ~~ Bs)
val fpB_Ts = map B_ify fpA_Ts;
@@ -494,9 +493,8 @@
val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
(fn {context = ctxt, prems = prems} =>
- mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs)
- (map #exhaust ctr_sugars) ctor_defss ctor_injects pre_rel_defs abs_inverses
- live_nesting_rel_eqs)
+ mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
+ ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
in
@@ -656,12 +654,11 @@
(rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
end;
-fun mk_coinduct_attrs fpTs ctr_sugars mss =
+fun mk_coinduct_attributes fpTs ctrss discss mss =
let
val nn = length fpTs;
val fp_b_names = map base_name_of_typ fpTs;
- val ctrss = map #ctrs ctr_sugars;
- val discss = map #discs ctr_sugars;
+
fun mk_coinduct_concls ms discs ctrs =
let
fun mk_disc_concl disc = [name_of_disc disc];
@@ -672,6 +669,7 @@
in
flat (map2 append disc_concls ctr_concls)
end;
+
val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
val coinduct_conclss =
map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
@@ -693,8 +691,9 @@
(coinduct_attrs, common_coinduct_attrs)
end;
-fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
- ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs =
+fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list)
+ abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
+ live_nesting_rel_eqs =
let
val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
@@ -766,7 +765,7 @@
in
(postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
rel_coinduct0_thm,
- mk_coinduct_attrs fpA_Ts ctr_sugars mss)
+ mk_coinduct_attributes fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
end;
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
@@ -960,7 +959,8 @@
val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
in
- ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss),
+ ((coinduct_thms_pairs,
+ mk_coinduct_attributes fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss),
corec_thmss,
disc_corec_thmss,
(disc_corec_iff_thmss, simp_attrs),
@@ -1655,9 +1655,9 @@
else
let
val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
- derive_rel_induct_thm_for_types lthy fpTs ns As Bs mss ctrss ctr_Tsss ctr_sugars
- rel_xtor_co_induct_thm ctr_defss ctor_injects pre_rel_defs abs_inverses
- (map rel_eq_of_bnf live_nesting_bnfs);
+ derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss
+ (map #exhaust ctr_sugars) rel_xtor_co_induct_thm ctr_defss ctor_injects
+ pre_rel_defs abs_inverses (map rel_eq_of_bnf live_nesting_bnfs);
in
((map single rel_induct_thms, single common_rel_induct_thm),
(rel_induct_attrs, rel_induct_attrs))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 09 18:57:20 2014 +0200
@@ -33,7 +33,7 @@
val decode_str : string -> string
val decode_strs : string -> string list
- datatype mash_engine =
+ datatype mash_algorithm =
MaSh_NB
| MaSh_kNN
| MaSh_NB_kNN
@@ -41,7 +41,7 @@
| MaSh_kNN_Ext
val is_mash_enabled : unit -> bool
- val the_mash_engine : unit -> mash_engine
+ val the_mash_algorithm : unit -> mash_algorithm
val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
val nickname_of_thm : thm -> string
@@ -138,14 +138,14 @@
()
end
-datatype mash_engine =
+datatype mash_algorithm =
MaSh_NB
| MaSh_kNN
| MaSh_NB_kNN
| MaSh_NB_Ext
| MaSh_kNN_Ext
-fun mash_engine () =
+fun mash_algorithm () =
let val flag1 = Options.default_string @{system_option MaSh} in
(case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
"yes" => SOME MaSh_NB_kNN
@@ -155,11 +155,11 @@
| "nb_knn" => SOME MaSh_NB_kNN
| "nb_ext" => SOME MaSh_NB_Ext
| "knn_ext" => SOME MaSh_kNN_Ext
- | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
+ | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
end
-val is_mash_enabled = is_some o mash_engine
-val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
+val is_mash_enabled = is_some o mash_algorithm
+val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
fun scaled_avg [] = 0
| scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
@@ -290,7 +290,7 @@
ary
end
-val nb_def_prior_weight = 21 (* FUDGE *)
+val nb_def_prior_weight = 1000 (* FUDGE *)
fun learn_facts (tfreq0, sfreq0, dffreq0) num_facts0 num_facts num_feats depss featss =
let
@@ -326,9 +326,10 @@
fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs visible_facts goal_feats =
let
- val tau = 0.05 (* FUDGE *)
- val pos_weight = 10.0 (* FUDGE *)
- val def_val = ~15.0 (* FUDGE *)
+ val tau = 0.2 (* FUDGE *)
+ val pos_weight = 5.0 (* FUDGE *)
+ val def_val = ~18.0 (* FUDGE *)
+ val init_val = 30.0 (* FUDGE *)
val ln_afreq = Math.ln (Real.fromInt num_facts)
val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) dffreq
@@ -339,14 +340,14 @@
let
val tfreq = Real.fromInt (Vector.sub (tfreq, i))
- fun fold_feats (f, fw0) (res, sfh) =
+ fun add_feat (f, fw0) (res, sfh) =
(case Inttab.lookup sfh f of
SOME sf =>
(res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
Inttab.delete f sfh)
| NONE => (res + fw0 * tfidf f * def_val, sfh))
- val (res, sfh) = fold fold_feats goal_feats (Math.ln tfreq, Vector.sub (sfreq, i))
+ val (res, sfh) = fold add_feat goal_feats (init_val * Math.ln tfreq, Vector.sub (sfreq, i))
fun fold_sfh (f, sf) sow =
sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
@@ -366,7 +367,7 @@
ret (Integer.max 0 (num_facts - max_suggs)) []
end
-val number_of_nearest_neighbors = 10 (* FUDGE *)
+val number_of_nearest_neighbors = 1 (* FUDGE *)
fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
let
@@ -384,11 +385,11 @@
fun do_feat (s, sw0) =
let
val sw = sw0 * tfidf s
- val w2 = sw * sw
+ val w6 = Math.pow (sw, 6.0)
fun inc_overlap j =
let val (_, ov) = Array.sub (overlaps_sqr, j) in
- Array.update (overlaps_sqr, j, (j, w2 + ov))
+ Array.update (overlaps_sqr, j, (j, w6 + ov))
end
in
List.app inc_overlap (Array.sub (feat_facts, s))
@@ -404,10 +405,7 @@
let val (_, ov) = Array.sub (recommends, j) in
if ov <= 0.0 then
(no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
- else if ov < !age + 1000.0 then
- Array.update (recommends, j, (j, v + ov))
- else
- ()
+ else Array.update (recommends, j, (j, v + ov))
end
val k = Unsynchronized.ref 0
@@ -416,13 +414,13 @@
raise EXIT ()
else
let
+ val deps_factor = 2.7 (* FUDGE *)
val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
- val o1 = Math.sqrt o2
- val _ = inc_recommend o1 j
+ val _ = inc_recommend o2 j
val ds = Vector.sub (depss, j)
val l = Real.fromInt (length ds)
in
- List.app (inc_recommend (o1 / l)) ds
+ List.app (inc_recommend (deps_factor * o2 / l)) ds
end
fun while1 () =
@@ -483,13 +481,13 @@
external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
val naive_bayes_ext = external_tool "predict/nbayes"
-fun query_external ctxt engine max_suggs learns goal_feats =
+fun query_external ctxt algorithm max_suggs learns goal_feats =
(trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
- (case engine of
+ (case algorithm of
MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
| MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
-fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
+fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss)
(freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
let
fun nb () =
@@ -502,7 +500,7 @@
in
(trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
- (case engine of
+ (case algorithm of
MaSh_NB => nb ()
| MaSh_kNN => knn ()
| MaSh_NB_kNN =>
@@ -1154,7 +1152,7 @@
fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
let
val thy_name = Context.theory_name thy
- val engine = the_mash_engine ()
+ val algorithm = the_mash_algorithm ()
val facts = facts
|> rev_sort_list_prefix (crude_thm_ord o pairself snd)
@@ -1193,19 +1191,19 @@
val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
val suggs =
- if engine = MaSh_NB_Ext orelse engine = MaSh_kNN_Ext then
+ if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
let
val learns =
Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
in
- MaSh.query_external ctxt engine max_suggs learns goal_feats
+ MaSh.query_external ctxt algorithm max_suggs learns goal_feats
end
else
let
val int_goal_feats =
map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
in
- MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
+ MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
goal_feats int_goal_feats
end
--- a/src/HOL/Tools/etc/options Wed Jul 09 11:48:21 2014 +0200
+++ b/src/HOL/Tools/etc/options Wed Jul 09 18:57:20 2014 +0200
@@ -36,4 +36,4 @@
-- "status of Z3 activation for non-commercial use (yes, no, unknown)"
public option MaSh : string = "sml"
- -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"
+ -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"