# HG changeset patch # User nipkow # Date 1404925040 -7200 # Node ID da5038b3886c5650cee6cb8f54d535cdeca155be # Parent 5e8317c5b689b0c7c6edd8d70821e9f8bc83873c# Parent 810bc6c41ebd09373d2b08745766bccaa55efc51 merged diff -r 810bc6c41ebd -r da5038b3886c NEWS --- 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 diff -r 810bc6c41ebd -r da5038b3886c src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 810bc6c41ebd -r da5038b3886c src/HOL/TPTP/mash_export.ML --- 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 => diff -r 810bc6c41ebd -r da5038b3886c src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 810bc6c41ebd -r da5038b3886c src/HOL/Tools/BNF/bnf_def.ML --- 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), diff -r 810bc6c41ebd -r da5038b3886c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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)) diff -r 810bc6c41ebd -r da5038b3886c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 810bc6c41ebd -r da5038b3886c src/HOL/Tools/etc/options --- 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)"