1.1 --- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 01 16:08:31 2014 +0100
1.2 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 01 16:09:51 2014 +0100
1.3 @@ -948,6 +948,13 @@
1.4 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
1.5 prove $m$ properties simultaneously.
1.6
1.7 +\item[@{text "t."}\hthm{rel\_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct pred]"}\rm:] ~ \\
1.8 +@{thm list.rel_induct[no_vars]}
1.9 +
1.10 +\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel\_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
1.11 +Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
1.12 +prove $m$ properties simultaneously.
1.13 +
1.14 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
1.15 @{thm list.rec(1)[no_vars]} \\
1.16 @{thm list.rec(2)[no_vars]}
2.1 --- a/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 16:08:31 2014 +0100
2.2 +++ b/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 16:09:51 2014 +0100
2.3 @@ -1059,22 +1059,26 @@
2.4 The MaSh machine learner. Three learning engines are provided:
2.5
2.6 \begin{enum}
2.7 -\item[\labelitemi] \textbf{\textit{nb}} (also called \textbf{\textit{sml}}
2.8 -and \textbf{\textit{yes}}) is a Standard ML implementation of naive Bayes.
2.9 +\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
2.10
2.11 -\item[\labelitemi] \textbf{\textit{knn}} is a Standard ML implementation of
2.12 -$k$-nearest neighbors.
2.13 +\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest
2.14 +neighbors.
2.15 +
2.16 +\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}}
2.17 +and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest
2.18 +neighbors.
2.19 \end{enum}
2.20
2.21 In addition, the special value \textit{none} is used to disable machine learning by
2.22 default (cf.\ \textit{smart} below).
2.23
2.24 -The engine can be selected by setting \texttt{MASH} to the name of the desired
2.25 -engine---either in the environment in which Isabelle is launched, in your
2.26 -\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
2.27 -under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
2.28 -Persistent data for both engines is stored in the directory
2.29 -\texttt{\$ISABELLE\_HOME\_USER/mash}.
2.30 +The default engine is \textit{nb\_knn}. The engine can be selected by setting
2.31 +\texttt{MASH} to the name of the desired engine---either in the environment in
2.32 +which Isabelle is launched, in your
2.33 +\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
2.34 +file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
2.35 +General'' in Isabelle/jEdit. Persistent data for both engines is stored in the
2.36 +directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
2.37
2.38 \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
2.39 rankings from MePo and MaSh.
3.1 --- a/src/HOL/BNF_FP_Base.thy Tue Jul 01 16:08:31 2014 +0100
3.2 +++ b/src/HOL/BNF_FP_Base.thy Tue Jul 01 16:09:51 2014 +0100
3.3 @@ -89,6 +89,9 @@
3.4 lemma Inl_Inr_False: "(Inl x = Inr y) = False"
3.5 by simp
3.6
3.7 +lemma Inr_Inl_False: "(Inr x = Inl y) = False"
3.8 + by simp
3.9 +
3.10 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
3.11 by blast
3.12
4.1 --- a/src/HOL/BNF_LFP.thy Tue Jul 01 16:08:31 2014 +0100
4.2 +++ b/src/HOL/BNF_LFP.thy Tue Jul 01 16:09:51 2014 +0100
4.3 @@ -1,3 +1,4 @@
4.4 +
4.5 (* Title: HOL/BNF_LFP.thy
4.6 Author: Dmitriy Traytel, TU Muenchen
4.7 Author: Lorenz Panny, TU Muenchen
4.8 @@ -194,4 +195,5 @@
4.9
4.10 hide_fact (open) id_transfer
4.11
4.12 +
4.13 end
5.1 --- a/src/HOL/TPTP/MaSh_Eval.thy Tue Jul 01 16:08:31 2014 +0100
5.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy Tue Jul 01 16:09:51 2014 +0100
5.3 @@ -11,11 +11,8 @@
5.4 ML_file "mash_eval.ML"
5.5
5.6 sledgehammer_params
5.7 - [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
5.8 - lam_trans = lifting, timeout = 15, dont_preplay, minimize]
5.9 -
5.10 -declare [[sledgehammer_fact_duplicates = true]]
5.11 -declare [[sledgehammer_instantiate_inducts = false]]
5.12 + [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
5.13 + lam_trans = combs, timeout = 30, dont_preplay, minimize]
5.14
5.15 ML {*
5.16 Multithreading.max_threads_value ()
5.17 @@ -43,15 +40,13 @@
5.18
5.19 ML {*
5.20 if do_it then
5.21 - evaluate_mash_suggestions @{context} params range
5.22 - [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
5.23 - (SOME prob_dir)
5.24 - (prefix ^ "mepo_suggestions")
5.25 - (prefix ^ "mash_suggestions")
5.26 - (prefix ^ "mash_prover_suggestions")
5.27 - (prefix ^ "mesh_suggestions")
5.28 - (prefix ^ "mesh_prover_suggestions")
5.29 - (prefix ^ "mash_eval")
5.30 + evaluate_mash_suggestions @{context} params range (SOME prob_dir)
5.31 + [prefix ^ "mepo_suggestions",
5.32 + prefix ^ "mash_suggestions",
5.33 + prefix ^ "mash_prover_suggestions",
5.34 + prefix ^ "mesh_suggestions",
5.35 + prefix ^ "mesh_prover_suggestions"]
5.36 + (prefix ^ "mash_eval")
5.37 else
5.38 ()
5.39 *}
6.1 --- a/src/HOL/TPTP/MaSh_Export.thy Tue Jul 01 16:08:31 2014 +0100
6.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Tue Jul 01 16:09:51 2014 +0100
6.3 @@ -46,32 +46,74 @@
6.4 ()
6.5 *}
6.6
6.7 -ML {* Options.put_default @{system_option MaSh} "nb" *}
6.8 -
6.9 ML {*
6.10 if do_it then
6.11 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
6.12 + generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions
6.13 (prefix ^ "mash_nb_suggestions")
6.14 else
6.15 ()
6.16 *}
6.17
6.18 -ML {* Options.put_default @{system_option MaSh} "knn" *}
6.19 -
6.20 ML {*
6.21 if do_it then
6.22 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
6.23 + generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions
6.24 (prefix ^ "mash_knn_suggestions")
6.25 else
6.26 ()
6.27 *}
6.28
6.29 -ML {* Options.put_default @{system_option MaSh} "py" *}
6.30 +ML {*
6.31 +if do_it then
6.32 + generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
6.33 + (prefix ^ "mepo_suggestions")
6.34 +else
6.35 + ()
6.36 +*}
6.37
6.38 ML {*
6.39 if do_it then
6.40 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
6.41 - (prefix ^ "mash_py_suggestions")
6.42 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions")
6.43 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions")
6.44 +else
6.45 + ()
6.46 +*}
6.47 +
6.48 +ML {*
6.49 +if do_it then
6.50 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions")
6.51 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions")
6.52 +else
6.53 + ()
6.54 +*}
6.55 +
6.56 +ML {*
6.57 +if do_it then
6.58 + generate_prover_dependencies @{context} params range thys
6.59 + (prefix ^ "mash_nb_prover_dependencies")
6.60 +else
6.61 + ()
6.62 +*}
6.63 +
6.64 +ML {*
6.65 +if do_it then
6.66 + generate_prover_dependencies @{context} params range thys
6.67 + (prefix ^ "mash_knn_prover_dependencies")
6.68 +else
6.69 + ()
6.70 +*}
6.71 +
6.72 +ML {*
6.73 +if do_it then
6.74 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions")
6.75 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions")
6.76 +else
6.77 + ()
6.78 +*}
6.79 +
6.80 +ML {*
6.81 +if do_it then
6.82 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions")
6.83 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions")
6.84 else
6.85 ()
6.86 *}
6.87 @@ -107,41 +149,10 @@
6.88
6.89 ML {*
6.90 if do_it then
6.91 - generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
6.92 - (prefix ^ "mepo_suggestions")
6.93 -else
6.94 - ()
6.95 -*}
6.96 -
6.97 -ML {*
6.98 -if do_it then
6.99 - generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
6.100 - (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
6.101 -else
6.102 - ()
6.103 -*}
6.104 -
6.105 -ML {*
6.106 -if do_it then
6.107 - generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies")
6.108 -else
6.109 - ()
6.110 -*}
6.111 -
6.112 -ML {*
6.113 -if do_it then
6.114 generate_prover_commands @{context} params (range, step) thys max_suggestions
6.115 (prefix ^ "mash_prover_commands")
6.116 else
6.117 ()
6.118 *}
6.119
6.120 -ML {*
6.121 -if do_it then
6.122 - generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
6.123 - (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
6.124 -else
6.125 - ()
6.126 -*}
6.127 -
6.128 end
7.1 --- a/src/HOL/TPTP/mash_eval.ML Tue Jul 01 16:08:31 2014 +0100
7.2 +++ b/src/HOL/TPTP/mash_eval.ML Tue Jul 01 16:09:51 2014 +0100
7.3 @@ -9,14 +9,8 @@
7.4 sig
7.5 type params = Sledgehammer_Prover.params
7.6
7.7 - val MePoN : string
7.8 - val MaSh_IsarN : string
7.9 - val MaSh_ProverN : string
7.10 - val MeSh_IsarN : string
7.11 - val MeSh_ProverN : string
7.12 - val IsarN : string
7.13 - val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string list ->
7.14 - string option -> string -> string -> string -> string -> string -> string -> unit
7.15 + val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string option ->
7.16 + string list -> string -> unit
7.17 end;
7.18
7.19 structure MaSh_Eval : MASH_EVAL =
7.20 @@ -33,15 +27,7 @@
7.21
7.22 val prefix = Library.prefix
7.23
7.24 -val MaSh_IsarN = MaShN ^ "-Isar"
7.25 -val MaSh_ProverN = MaShN ^ "-Prover"
7.26 -val MeSh_IsarN = MeShN ^ "-Isar"
7.27 -val MeSh_ProverN = MeShN ^ "-Prover"
7.28 -val IsarN = "Isar"
7.29 -
7.30 -fun evaluate_mash_suggestions ctxt params range methods prob_dir_name mepo_file_name
7.31 - mash_isar_file_name mash_prover_file_name mesh_isar_file_name mesh_prover_file_name
7.32 - report_file_name =
7.33 +fun evaluate_mash_suggestions ctxt params range prob_dir_name file_names report_file_name =
7.34 let
7.35 val thy = Proof_Context.theory_of ctxt
7.36 val zeros = [0, 0, 0, 0, 0, 0]
7.37 @@ -53,20 +39,19 @@
7.38 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
7.39 val prover = hd provers
7.40 val max_suggs = generous_max_suggestions (the max_facts)
7.41 +
7.42 + val method_of_file_name =
7.43 + perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
7.44 +
7.45 + val methods = "isar" :: map method_of_file_name file_names
7.46 val lines_of = Path.explode #> try File.read_lines #> these
7.47 - val file_names =
7.48 - [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
7.49 - mesh_isar_file_name, mesh_prover_file_name]
7.50 - val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
7.51 - mesh_isar_lines, mesh_prover_lines] =
7.52 - map lines_of file_names
7.53 - val num_lines = fold (Integer.max o length) lines 0
7.54 + val liness0 = map lines_of file_names
7.55 + val num_lines = fold (Integer.max o length) liness0 0
7.56
7.57 fun pad lines = lines @ replicate (num_lines - length lines) ""
7.58
7.59 - val lines =
7.60 - pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
7.61 - pad mesh_isar_lines ~~ pad mesh_prover_lines
7.62 + val liness = map pad liness0
7.63 +
7.64 val css = clasimpset_rule_table_of ctxt
7.65 val facts = all_facts ctxt true false Symtab.empty [] [] css
7.66 val name_tabs = build_name_tables nickname_of_thm facts
7.67 @@ -95,19 +80,12 @@
7.68 |> space_implode " "))
7.69 end
7.70
7.71 - fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), mesh_isar_line),
7.72 - mesh_prover_line)) =
7.73 + fun solve_goal (j, lines) =
7.74 if in_range range j then
7.75 let
7.76 val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
7.77 - val (name1, mepo_suggs) = get_suggs mepo_line
7.78 - val (name2, mash_isar_suggs) = get_suggs mash_isar_line
7.79 - val (name3, mash_prover_suggs) = get_suggs mash_prover_line
7.80 - val (name4, mesh_isar_suggs) = get_suggs mesh_isar_line
7.81 - val (name5, mesh_prover_suggs) = get_suggs mesh_prover_line
7.82 - val [name] =
7.83 - [name1, name2, name3, name4, name5]
7.84 - |> filter (curry (op <>) "") |> distinct (op =)
7.85 + val (names, suggss0) = split_list (map get_suggs lines)
7.86 + val [name] = names |> filter (curry (op <>) "") |> distinct (op =)
7.87 handle General.Match => error "Input files out of sync."
7.88 val th =
7.89 case find_first (fn (_, th) => nickname_of_thm th = name) facts of
7.90 @@ -116,6 +94,7 @@
7.91 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
7.92 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
7.93 val isar_deps = these (isar_dependencies_of name_tabs th)
7.94 + val suggss = isar_deps :: suggss0
7.95 val facts = facts |> filter (fn (_, th') => thm_less (th', th))
7.96
7.97 (* adapted from "mirabelle_sledgehammer.ML" *)
7.98 @@ -130,7 +109,7 @@
7.99 | set_file_name _ NONE = I
7.100
7.101 fun prove method suggs =
7.102 - if not (member (op =) methods method) orelse (null facts andalso method <> IsarN) then
7.103 + if null facts then
7.104 (str_of_method method ^ "Skipped", 0)
7.105 else
7.106 let
7.107 @@ -151,14 +130,7 @@
7.108 (str_of_result method facts res, ok)
7.109 end
7.110
7.111 - val ress =
7.112 - [fn () => prove MePoN mepo_suggs,
7.113 - fn () => prove MaSh_IsarN mash_isar_suggs,
7.114 - fn () => prove MaSh_ProverN mash_prover_suggs,
7.115 - fn () => prove MeSh_IsarN mesh_isar_suggs,
7.116 - fn () => prove MeSh_ProverN mesh_prover_suggs,
7.117 - fn () => prove IsarN isar_deps]
7.118 - |> (* Par_List. *) map (fn f => f ())
7.119 + val ress = map2 prove methods suggss
7.120 in
7.121 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
7.122 |> cat_lines |> print;
7.123 @@ -167,10 +139,6 @@
7.124 else
7.125 zeros
7.126
7.127 - fun total_of method ok n =
7.128 - str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
7.129 - (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
7.130 -
7.131 val inst_inducts = Config.get ctxt instantiate_inducts
7.132 val options =
7.133 ["prover = " ^ prover,
7.134 @@ -182,18 +150,17 @@
7.135 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
7.136 val _ = print " * * *";
7.137 val _ = print ("Options: " ^ commas options);
7.138 - val oks = Par_List.map solve_goal (tag_list 1 lines)
7.139 + val oks = Par_List.map solve_goal (tag_list 1 liness)
7.140 val n = length oks
7.141 - val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, isar_ok] =
7.142 - if n = 0 then zeros else map Integer.sum (map_transpose I oks)
7.143 +
7.144 + fun total_of method ok =
7.145 + str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
7.146 + (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
7.147 +
7.148 + val oks' = if n = 0 then zeros else map Integer.sum (map_transpose I oks)
7.149 in
7.150 - ["Successes (of " ^ string_of_int n ^ " goals)",
7.151 - total_of MePoN mepo_ok n,
7.152 - total_of MaSh_IsarN mash_isar_ok n,
7.153 - total_of MaSh_ProverN mash_prover_ok n,
7.154 - total_of MeSh_IsarN mesh_isar_ok n,
7.155 - total_of MeSh_ProverN mesh_prover_ok n,
7.156 - total_of IsarN isar_ok n]
7.157 + "Successes (of " ^ string_of_int n ^ " goals)" ::
7.158 + map2 total_of methods oks'
7.159 |> cat_lines |> print
7.160 end
7.161
8.1 --- a/src/HOL/TPTP/mash_export.ML Tue Jul 01 16:08:31 2014 +0100
8.2 +++ b/src/HOL/TPTP/mash_export.ML Tue Jul 01 16:09:51 2014 +0100
8.3 @@ -24,7 +24,7 @@
8.4 theory list -> int -> string -> unit
8.5 val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
8.6 theory list -> int -> string -> unit
8.7 - val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int ->
8.8 + val generate_mash_suggestions : string -> Proof.context -> params -> (int * int option) * int ->
8.9 theory list -> int -> string -> unit
8.10 val generate_mesh_suggestions : int -> string -> string -> string -> unit
8.11 end;
8.12 @@ -284,15 +284,16 @@
8.13 not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
8.14 #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
8.15
8.16 -fun generate_mash_suggestions ctxt params =
8.17 - (Sledgehammer_MaSh.mash_unlearn ();
8.18 +fun generate_mash_suggestions engine =
8.19 + (Options.put_default @{system_option MaSh} engine;
8.20 + Sledgehammer_MaSh.mash_unlearn ();
8.21 generate_mepo_or_mash_suggestions
8.22 (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
8.23 fn concl_t =>
8.24 tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
8.25 Sledgehammer_Util.one_year)
8.26 #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
8.27 - #> fst) ctxt params)
8.28 + #> fst))
8.29
8.30 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
8.31 let
9.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 01 16:08:31 2014 +0100
9.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 01 16:09:51 2014 +0100
9.3 @@ -749,11 +749,9 @@
9.4
9.5 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
9.6 fun conceal_bounds Ts t =
9.7 - subst_bounds (map (Free o apfst concealed_bound_name)
9.8 - (0 upto length Ts - 1 ~~ Ts), t)
9.9 + subst_bounds (map_index (Free o apfst concealed_bound_name) Ts, t)
9.10 fun reveal_bounds Ts =
9.11 - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
9.12 - (0 upto length Ts - 1 ~~ Ts))
9.13 + subst_atomic (map_index (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) Ts)
9.14
9.15 fun do_introduce_combinators ctxt Ts t =
9.16 let val thy = Proof_Context.theory_of ctxt in
9.17 @@ -1327,7 +1325,7 @@
9.18 if forall null footprint then
9.19 []
9.20 else
9.21 - 0 upto length footprint - 1 ~~ footprint
9.22 + map_index I footprint
9.23 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
9.24 |> cover []
9.25 end
9.26 @@ -1878,7 +1876,7 @@
9.27 val conjs =
9.28 map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
9.29 |> map (apsnd freeze_term)
9.30 - |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
9.31 + |> map_index (uncurry (pair o rpair (Local, General) o string_of_int))
9.32 val ((conjs, facts), lam_facts) =
9.33 (conjs, facts)
9.34 |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
9.35 @@ -1930,7 +1928,7 @@
9.36 val cover = type_arg_cover thy pos s ary
9.37 in
9.38 exists (fn (j, tm) => tm = var andalso member (op =) cover j)
9.39 - (0 upto ary - 1 ~~ tms) orelse
9.40 + (0 upto ary - 1 ~~ tms) orelse
9.41 exists is_undercover tms
9.42 end
9.43 | is_undercover _ = true
9.44 @@ -1984,7 +1982,7 @@
9.45 val ary = length args
9.46 fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
9.47 in
9.48 - map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
9.49 + map_index (uncurry (term o arg_site)) args
9.50 |> mk_aterm type_enc name T_args
9.51 end
9.52 | IVar (name, _) =>
9.53 @@ -2102,7 +2100,7 @@
9.54 if is_type_enc_polymorphic type_enc then
9.55 let
9.56 val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
9.57 - fun line j (cl, T) =
9.58 + fun line (j, (cl, T)) =
9.59 if type_classes then
9.60 Class_Memb (class_memb_prefix ^ string_of_int j, [],
9.61 native_atp_type_of_typ type_enc false 0 T, `make_class cl)
9.62 @@ -2113,7 +2111,7 @@
9.63 fold (union (op =)) (map #atomic_types facts) []
9.64 |> class_membs_of_types type_enc add_sorts_on_tfree
9.65 in
9.66 - map2 line (0 upto length membs - 1) membs
9.67 + map_index line membs
9.68 end
9.69 else
9.70 []
9.71 @@ -2314,8 +2312,7 @@
9.72
9.73 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
9.74
9.75 -fun line_of_guards_sym_decl ctxt mono type_enc n s j
9.76 - (s', T_args, T, _, ary, in_conj) =
9.77 +fun line_of_guards_sym_decl ctxt mono type_enc n s j (s', T_args, T, _, ary, in_conj) =
9.78 let
9.79 val thy = Proof_Context.theory_of ctxt
9.80 val (role, maybe_negate) = honor_conj_sym_role in_conj
9.81 @@ -2328,7 +2325,7 @@
9.82 All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
9.83 | Undercover_Types =>
9.84 let val cover = type_arg_cover thy NONE s ary in
9.85 - map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts
9.86 + map_index (uncurry (fn j => if member (op =) cover j then SOME else K NONE)) arg_Ts
9.87 end
9.88 | _ => replicate ary NONE)
9.89 in
9.90 @@ -2372,7 +2369,7 @@
9.91 let
9.92 val cover = type_arg_cover thy NONE s ary
9.93 fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
9.94 - val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
9.95 + val bounds = map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts) bounds
9.96 in formula (cst bounds) end
9.97 else
9.98 formula (cst bounds)
9.99 @@ -2399,14 +2396,14 @@
9.100 val n = length decls
9.101 val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
9.102 in
9.103 - (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
9.104 + map_index (uncurry (line_of_guards_sym_decl ctxt mono type_enc n s)) decls
9.105 end
9.106 | Tags (_, level) =>
9.107 if is_type_level_uniform level then
9.108 []
9.109 else
9.110 let val n = length decls in
9.111 - (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
9.112 + maps (lines_of_tags_sym_decl ctxt mono type_enc n s) (0 upto n - 1 ~~ decls)
9.113 end)
9.114
9.115 fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
9.116 @@ -2603,6 +2600,7 @@
9.117 val thy = Proof_Context.theory_of ctxt
9.118 val type_enc = type_enc |> adjust_type_enc format
9.119 val completish = (mode = Sledgehammer_Completish)
9.120 +
9.121 (* Forcing explicit applications is expensive for polymorphic encodings,
9.122 because it takes only one existential variable ranging over "'a => 'b" to
9.123 ruin everything. Hence we do it only if there are few facts (which is
9.124 @@ -2614,32 +2612,45 @@
9.125 if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op
9.126 else
9.127 Sufficient_App_Op_And_Predicator
9.128 +
9.129 val lam_trans =
9.130 if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
9.131 else lam_trans
9.132 +
9.133 val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
9.134 translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
9.135 +
9.136 val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
9.137 - val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
9.138 val ctrss = all_ctrss_of_datatypes ctxt
9.139 +
9.140 fun firstorderize in_helper =
9.141 firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish
9.142 sym_tab0
9.143 +
9.144 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
9.145 val (ho_stuff, sym_tab) =
9.146 sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
9.147 + val helpers =
9.148 + sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
9.149 + |> map (firstorderize true)
9.150 +
9.151 + val all_facts = helpers @ conjs @ facts
9.152 + val mono = mononotonicity_info_of_facts ctxt type_enc completish all_facts
9.153 + val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
9.154 +
9.155 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
9.156 uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab
9.157 val (_, sym_tab) =
9.158 (ho_stuff, sym_tab)
9.159 |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
9.160 uncurried_alias_eq_tms
9.161 - val helpers =
9.162 - sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
9.163 - |> map (firstorderize true)
9.164 - val all_facts = helpers @ conjs @ facts
9.165 - val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
9.166 val datatypes = datatypes_of_sym_table ctxt ctrss format type_enc uncurried_aliases sym_tab
9.167 +
9.168 + val num_facts = length facts
9.169 + val freshen = mode <> Exporter andalso mode <> Translator
9.170 + val pos = mode <> Exporter
9.171 + val rank_of = rank_of_fact_num num_facts
9.172 +
9.173 val class_decl_lines = decl_lines_of_classes type_enc classes
9.174 val sym_decl_lines =
9.175 (conjs, helpers @ facts, uncurried_alias_eq_tms)
9.176 @@ -2647,22 +2658,18 @@
9.177 |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
9.178 val datatype_decl_lines = map decl_line_of_datatype datatypes
9.179 val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
9.180 - val num_facts = length facts
9.181 - val freshen = mode <> Exporter andalso mode <> Translator
9.182 - val pos = mode <> Exporter
9.183 - val rank_of = rank_of_fact_num num_facts
9.184 val fact_lines =
9.185 - map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
9.186 - (0 upto num_facts - 1 ~~ facts)
9.187 + map_index (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of) facts
9.188 val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
9.189 val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
9.190 val helper_lines =
9.191 - 0 upto length helpers - 1 ~~ helpers
9.192 - |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
9.193 + map_index (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
9.194 + helpers
9.195 val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
9.196 val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
9.197 +
9.198 (* Reordering these might confuse the proof reconstruction code. *)
9.199 - val problem =
9.200 + val (problem, pool) =
9.201 [(explicit_declsN, decl_lines),
9.202 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
9.203 (factsN, fact_lines),
9.204 @@ -2671,14 +2678,13 @@
9.205 (helpersN, helper_lines),
9.206 (free_typesN, free_type_lines),
9.207 (conjsN, conj_lines)]
9.208 - val problem =
9.209 - problem
9.210 |> (case format of
9.211 CNF => ensure_cnf_problem
9.212 | CNF_UEQ => filter_cnf_ueq_problem
9.213 | FOF => I
9.214 | _ => declare_undeclared_in_problem implicit_declsN)
9.215 - val (problem, pool) = problem |> nice_atp_problem readable_names format
9.216 + |> nice_atp_problem readable_names format
9.217 +
9.218 fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
9.219 in
9.220 (problem, Option.map snd pool |> the_default Symtab.empty, lifted,
9.221 @@ -2715,7 +2721,7 @@
9.222 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
9.223 / Real.fromInt num_facts
9.224 in
9.225 - map weight_of (0 upto num_facts - 1) ~~ facts
9.226 + map_index (apfst weight_of) facts
9.227 |> fold (uncurry add_line_weights)
9.228 end
9.229 val get = these o AList.lookup (op =) problem
10.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 16:08:31 2014 +0100
10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 01 16:09:51 2014 +0100
10.3 @@ -243,10 +243,6 @@
10.4 fun merge_type_args fp (As, As') =
10.5 if length As = length As' then map2 (merge_type_arg fp) As As' else cannot_merge_types fp;
10.6
10.7 -fun reassoc_conjs thm =
10.8 - reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
10.9 - handle THM _ => thm;
10.10 -
10.11 fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
10.12 fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
10.13 fun mixfix_of_spec ((((_, mx), _), _), _) = mx;
10.14 @@ -444,6 +440,69 @@
10.15 map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
10.16 end;
10.17
10.18 +fun postproc_co_induct lthy nn prop prop_conj =
10.19 + Drule.zero_var_indexes
10.20 + #> `(conj_dests nn)
10.21 + #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
10.22 + ##> (fn thm => Thm.permute_prems 0 (~nn)
10.23 + (if nn = 1 then thm RS prop
10.24 + else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
10.25 +
10.26 +fun mk_induct_attrs ctrss =
10.27 + let
10.28 + val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
10.29 + val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
10.30 + in
10.31 + [induct_case_names_attr]
10.32 + end;
10.33 +
10.34 +fun derive_rel_induct_thm_for_types lthy fpA_Ts ns As Bs mss ctrAss ctrAs_Tsss ctr_sugars
10.35 + ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
10.36 + let
10.37 + val B_ify = typ_subst_nonatomic (As ~~ Bs)
10.38 + val fpB_Ts = map B_ify fpA_Ts;
10.39 + val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
10.40 + val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
10.41 +
10.42 + val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
10.43 + |> mk_Frees "R" (map2 mk_pred2T As Bs)
10.44 + ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts)
10.45 + ||>> mk_Freesss "a" ctrAs_Tsss
10.46 + ||>> mk_Freesss "b" ctrBs_Tsss;
10.47 +
10.48 + fun choose_relator AB = the (find_first
10.49 + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
10.50 +
10.51 + val premises =
10.52 + let
10.53 + fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
10.54 + fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) $ a $ b;
10.55 +
10.56 + fun mk_prem ctrA ctrB argAs argBs =
10.57 + fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies)
10.58 + (map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs)
10.59 + (HOLogic.mk_Trueprop
10.60 + (build_rel_app (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs)))));
10.61 + in
10.62 + flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
10.63 + end;
10.64 +
10.65 + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
10.66 + (map2 mk_leq (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)) IRs));
10.67 +
10.68 + val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
10.69 + (fn {context = ctxt, prems = prems} =>
10.70 + mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs)
10.71 + (map #exhaust ctr_sugars) ctor_defss ctor_injects pre_rel_defs abs_inverses
10.72 + live_nesting_rel_eqs)
10.73 + |> singleton (Proof_Context.export names_lthy lthy)
10.74 + |> Thm.close_derivation;
10.75 + in
10.76 + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
10.77 + rel_induct0_thm,
10.78 + mk_induct_attrs ctrAss)
10.79 + end;
10.80 +
10.81 fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
10.82 live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
10.83 abs_inverses ctrss ctr_defss recs rec_defs lthy =
10.84 @@ -552,9 +611,6 @@
10.85 `(conj_dests nn) thm
10.86 end;
10.87
10.88 - val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
10.89 - val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
10.90 -
10.91 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
10.92
10.93 fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms =
10.94 @@ -594,11 +650,11 @@
10.95
10.96 val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
10.97 in
10.98 - ((induct_thms, induct_thm, [induct_case_names_attr]),
10.99 + ((induct_thms, induct_thm, mk_induct_attrs ctrss),
10.100 (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
10.101 end;
10.102
10.103 -fun coinduct_attrs fpTs ctr_sugars mss =
10.104 +fun mk_coinduct_attrs fpTs ctr_sugars mss =
10.105 let
10.106 val nn = length fpTs;
10.107 val fp_b_names = map base_name_of_typ fpTs;
10.108 @@ -635,16 +691,8 @@
10.109 (coinduct_attrs, common_coinduct_attrs)
10.110 end;
10.111
10.112 -fun postproc_coinduct nn prop prop_conj =
10.113 - Drule.zero_var_indexes
10.114 - #> `(conj_dests nn)
10.115 - #>> map (fn thm => Thm.permute_prems 0 nn (thm RS prop))
10.116 - ##> (fn thm => Thm.permute_prems 0 nn
10.117 - (if nn = 1 then thm RS prop
10.118 - else funpow nn (fn thm => reassoc_conjs (thm RS prop_conj)) thm));
10.119 -
10.120 -fun derive_rel_coinduct0_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
10.121 - ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct =
10.122 +fun derive_rel_coinduct_thm_for_types lthy fpA_Ts ns As Bs mss ctr_sugars abs_inverses abs_injects
10.123 + ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs =
10.124 let
10.125 val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
10.126
10.127 @@ -713,12 +761,13 @@
10.128 mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
10.129 (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
10.130 (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
10.131 - rel_pre_defs abs_inverses)
10.132 + rel_pre_defs abs_inverses live_nesting_rel_eqs)
10.133 |> singleton (Proof_Context.export names_lthy lthy)
10.134 |> Thm.close_derivation;
10.135 in
10.136 - (postproc_coinduct (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
10.137 - coinduct_attrs fpA_Ts ctr_sugars mss)
10.138 + (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
10.139 + rel_coinduct0_thm,
10.140 + mk_coinduct_attrs fpA_Ts ctr_sugars mss)
10.141 end;
10.142
10.143 fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
10.144 @@ -817,7 +866,7 @@
10.145 val dtor_coinducts =
10.146 [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos mk_vimage2p lthy]
10.147 in
10.148 - map2 (postproc_coinduct nn mp mp_conj oo prove) dtor_coinducts goals
10.149 + map2 (postproc_co_induct lthy nn mp mp_conj oo prove) dtor_coinducts goals
10.150 end;
10.151
10.152 fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
10.153 @@ -912,7 +961,7 @@
10.154
10.155 val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
10.156 in
10.157 - ((coinduct_thms_pairs, coinduct_attrs fpTs ctr_sugars mss),
10.158 + ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss),
10.159 (corec_thmss, code_nitpicksimp_attrs),
10.160 (disc_corec_thmss, []),
10.161 (disc_corec_iff_thmss, simp_attrs),
10.162 @@ -1531,17 +1580,37 @@
10.163 abs_inverses ctrss ctr_defss recs rec_defs lthy;
10.164
10.165 val induct_type_attr = Attrib.internal o K o Induct.induct_type;
10.166 + val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
10.167 +
10.168 + val ((rel_induct_thmss, common_rel_induct_thms),
10.169 + (rel_induct_attrs, common_rel_induct_attrs)) =
10.170 + if live = 0 then
10.171 + ((replicate nn [], []), ([], []))
10.172 + else
10.173 + let
10.174 + val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
10.175 + derive_rel_induct_thm_for_types lthy fpTs ns As Bs mss ctrss ctr_Tsss ctr_sugars
10.176 + rel_xtor_co_induct_thm ctr_defss ctor_injects pre_rel_defs abs_inverses
10.177 + (map rel_eq_of_bnf live_nesting_bnfs);
10.178 + in
10.179 + ((map single rel_induct_thms, single common_rel_induct_thm),
10.180 + (rel_induct_attrs, rel_induct_attrs))
10.181 + end;
10.182
10.183 val simp_thmss =
10.184 map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
10.185
10.186 val common_notes =
10.187 - (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
10.188 + (if nn > 1 then
10.189 + [(inductN, [induct_thm], induct_attrs),
10.190 + (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)]
10.191 + else [])
10.192 |> massage_simple_notes fp_common_name;
10.193
10.194 val notes =
10.195 [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
10.196 (recN, rec_thmss, K rec_attrs),
10.197 + (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
10.198 (simpsN, simp_thmss, K [])]
10.199 |> massage_multi_notes;
10.200 in
10.201 @@ -1567,11 +1636,6 @@
10.202 ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
10.203 (Proof_Context.export lthy' no_defs_lthy) lthy;
10.204
10.205 - val ((rel_coinduct_thms, rel_coinduct_thm),
10.206 - (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
10.207 - derive_rel_coinduct0_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
10.208 - abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm;
10.209 -
10.210 val sel_corec_thmss = map flat sel_corec_thmsss;
10.211
10.212 val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
10.213 @@ -1579,6 +1643,22 @@
10.214
10.215 val flat_corec_thms = append oo append;
10.216
10.217 + val ((rel_coinduct_thmss, common_rel_coinduct_thms),
10.218 + (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
10.219 + if live = 0 then
10.220 + ((replicate nn [], []), ([], []))
10.221 + else
10.222 + let
10.223 + val ((rel_coinduct_thms, common_rel_coinduct_thm),
10.224 + (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
10.225 + derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
10.226 + abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm
10.227 + (map rel_eq_of_bnf live_nesting_bnfs)
10.228 + in
10.229 + ((map single rel_coinduct_thms, single common_rel_coinduct_thm),
10.230 + (rel_coinduct_attrs, common_rel_coinduct_attrs))
10.231 + end;
10.232 +
10.233 val simp_thmss =
10.234 map6 mk_simp_thms ctr_sugars
10.235 (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
10.236 @@ -1586,21 +1666,19 @@
10.237
10.238 val common_notes =
10.239 (if nn > 1 then
10.240 - [(rel_coinductN, [rel_coinduct_thm], common_rel_coinduct_attrs),
10.241 - (coinductN, [coinduct_thm], common_coinduct_attrs),
10.242 + [(coinductN, [coinduct_thm], common_coinduct_attrs),
10.243 + (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs),
10.244 (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
10.245 - else
10.246 - [])
10.247 + else [])
10.248 |> massage_simple_notes fp_common_name;
10.249
10.250 val notes =
10.251 [(coinductN, map single coinduct_thms,
10.252 fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
10.253 - (rel_coinductN, map single rel_coinduct_thms,
10.254 - K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
10.255 (corecN, corec_thmss, K corec_attrs),
10.256 (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
10.257 (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
10.258 + (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
10.259 (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
10.260 (simpsN, simp_thmss, K []),
10.261 (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
11.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 16:08:31 2014 +0100
11.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 01 16:09:51 2014 +0100
11.3 @@ -28,7 +28,9 @@
11.4 tactic
11.5 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
11.6 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
11.7 - thm list -> thm list -> tactic
11.8 + thm list -> thm list -> thm list -> tactic
11.9 + val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list ->
11.10 + thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
11.11 val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
11.12 val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
11.13 val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
11.14 @@ -210,7 +212,7 @@
11.15 selsss));
11.16
11.17 fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
11.18 - dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses =
11.19 + dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
11.20 rtac dtor_rel_coinduct 1 THEN
11.21 EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
11.22 fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
11.23 @@ -222,14 +224,29 @@
11.24 Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
11.25 @ simp_thms') THEN
11.26 Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
11.27 - abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
11.28 - rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
11.29 - prod.inject}) THEN
11.30 + abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
11.31 + rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
11.32 + sum.inject prod.inject}) THEN
11.33 REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
11.34 (rtac refl ORELSE' atac))))
11.35 cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
11.36 abs_inverses);
11.37
11.38 +fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects
11.39 + rel_pre_list_defs Abs_inverses nesting_rel_eqs =
11.40 + rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs =>
11.41 + fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
11.42 + HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
11.43 + (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
11.44 + THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
11.45 + unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
11.46 + @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
11.47 + TRYALL (hyp_subst_tac ctxt) THEN
11.48 + unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
11.49 + Inr_Inl_False sum.inject prod.inject}) THEN
11.50 + TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
11.51 + cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
11.52 +
11.53 fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
11.54 TRYALL Goal.conjunction_tac THEN
11.55 ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
12.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jul 01 16:08:31 2014 +0100
12.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jul 01 16:09:51 2014 +0100
12.3 @@ -190,10 +190,9 @@
12.4 (* Given the definition of a Skolem function, return a theorem to replace
12.5 an existential formula by a use of that function.
12.6 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
12.7 -fun old_skolem_theorem_of_def thy rhs0 =
12.8 +fun old_skolem_theorem_of_def ctxt rhs0 =
12.9 let
12.10 - val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
12.11 -
12.12 + val thy = Proof_Context.theory_of ctxt
12.13 val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
12.14 val rhs' = rhs |> Thm.dest_comb |> snd
12.15 val (ch, frees) = c_variant_abs_multi (rhs', [])
12.16 @@ -201,8 +200,7 @@
12.17 val T =
12.18 case hilbert of
12.19 Const (_, Type (@{type_name fun}, [_, T])) => T
12.20 - | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
12.21 - [hilbert])
12.22 + | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
12.23 val cex = cterm_of thy (HOLogic.exists_const T)
12.24 val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
12.25 val conc =
12.26 @@ -373,7 +371,7 @@
12.27 nnf_axiom choice_ths new_skolem ax_no th ctxt0
12.28 fun clausify th =
12.29 make_cnf (if new_skolem orelse null choice_ths then []
12.30 - else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
12.31 + else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
12.32 th ctxt ctxt
12.33 val (cnf_ths, ctxt) = clausify nnf_th
12.34 fun intr_imp ct th =
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 01 16:08:31 2014 +0100
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 01 16:09:51 2014 +0100
13.3 @@ -196,8 +196,11 @@
13.4 (facts |> map (fst o fst) |> space_implode " ") ^ "."
13.5
13.6 fun string_of_factss factss =
13.7 - if forall (null o snd) factss then "Found no relevant facts."
13.8 - else cat_lines (map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) factss)
13.9 + if forall (null o snd) factss then
13.10 + "Found no relevant facts."
13.11 + else
13.12 + cat_lines (map (fn (filter, facts) =>
13.13 + (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
13.14
13.15 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
13.16 output_result i (fact_override as {only, ...}) minimize_command state =
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 16:08:31 2014 +0100
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 16:09:51 2014 +0100
14.3 @@ -84,6 +84,7 @@
14.4 val risky_defs = @{thms Bit0_def Bit1_def}
14.5
14.6 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
14.7 +
14.8 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
14.9 | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
14.10 | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
14.11 @@ -114,6 +115,7 @@
14.12 ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
14.13 | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
14.14 | normT (T as TFree _) = pair T
14.15 +
14.16 fun norm (t $ u) = norm t ##>> norm u #>> op $
14.17 | norm (Const (s, T)) = normT T #>> curry Const s
14.18 | norm (Var (z as (_, T))) =
14.19 @@ -164,6 +166,7 @@
14.20 val bracket =
14.21 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
14.22 |> implode
14.23 +
14.24 fun nth_name j =
14.25 (case xref of
14.26 Facts.Fact s => backquote s ^ bracket
14.27 @@ -173,12 +176,15 @@
14.28 | Facts.Named ((name, _), SOME intervals) =>
14.29 make_name reserved true
14.30 (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
14.31 +
14.32 fun add_nth th (j, rest) =
14.33 let val name = nth_name j in
14.34 (j + 1, ((name, stature_of_thm false [] chained css name th), th)
14.35 :: rest)
14.36 end
14.37 - in (0, []) |> fold add_nth ths |> snd end
14.38 + in
14.39 + (0, []) |> fold add_nth ths |> snd
14.40 + end
14.41
14.42 (* Reject theorems with names like "List.filter.filter_list_def" or
14.43 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
14.44 @@ -222,6 +228,7 @@
14.45
14.46 (* FIXME: make more reliable *)
14.47 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
14.48 +
14.49 fun is_low_level_class_const (s, _) =
14.50 s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
14.51
14.52 @@ -250,6 +257,7 @@
14.53 not (member (op =) atp_widely_irrelevant_consts s)
14.54 | is_interesting_subterm (Free _) = true
14.55 | is_interesting_subterm _ = false
14.56 +
14.57 fun interest_of_bool t =
14.58 if exists_Const (is_technical_const orf is_low_level_class_const orf
14.59 type_has_top_sort o snd) t then
14.60 @@ -259,6 +267,7 @@
14.61 Boring
14.62 else
14.63 Interesting
14.64 +
14.65 fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
14.66 | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
14.67 combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
14.68 @@ -269,6 +278,7 @@
14.69 | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
14.70 combine_interests (interest_of_bool t) (interest_of_bool u)
14.71 | interest_of_prop _ _ = Deal_Breaker
14.72 +
14.73 val t = prop_of th
14.74 in
14.75 (interest_of_prop [] t <> Interesting andalso
14.76 @@ -277,11 +287,9 @@
14.77 end
14.78
14.79 fun is_blacklisted_or_something ctxt ho_atp =
14.80 - let
14.81 - val blist = multi_base_blacklist ctxt ho_atp
14.82 - fun is_blisted name =
14.83 - is_package_def name orelse exists (fn s => String.isSuffix s name) blist
14.84 - in is_blisted end
14.85 + let val blist = multi_base_blacklist ctxt ho_atp in
14.86 + fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
14.87 + end
14.88
14.89 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
14.90 they are displayed as "M" and we want to avoid clashes with these. But
14.91 @@ -316,6 +324,7 @@
14.92 let
14.93 fun add stature th =
14.94 Termtab.update (normalize_vars (prop_of th), stature)
14.95 +
14.96 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
14.97 ctxt |> claset_of |> Classical.rep_cs
14.98 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
14.99 @@ -331,18 +340,18 @@
14.100 |> filter_out (member Thm.eq_thm_prop risky_defs)
14.101 |> List.partition (is_rec_def o prop_of)
14.102 val spec_intros =
14.103 - specs |> filter (member (op =) [Spec_Rules.Inductive,
14.104 - Spec_Rules.Co_Inductive] o fst)
14.105 + specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
14.106 |> maps (snd o snd)
14.107 in
14.108 - Termtab.empty |> fold (add Simp o snd) simps
14.109 - |> fold (add Rec_Def) rec_defs
14.110 - |> fold (add Non_Rec_Def) nonrec_defs
14.111 + Termtab.empty
14.112 + |> fold (add Simp o snd) simps
14.113 + |> fold (add Rec_Def) rec_defs
14.114 + |> fold (add Non_Rec_Def) nonrec_defs
14.115 (* Add once it is used:
14.116 - |> fold (add Elim) elims
14.117 + |> fold (add Elim) elims
14.118 *)
14.119 - |> fold (add Intro) intros
14.120 - |> fold (add Inductive) spec_intros
14.121 + |> fold (add Intro) intros
14.122 + |> fold (add Inductive) spec_intros
14.123 end
14.124 end
14.125
14.126 @@ -359,9 +368,8 @@
14.127 fun if_thm_before th th' =
14.128 if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
14.129
14.130 -(* Hack: Conflate the facts about a class as seen from the outside with the
14.131 - corresponding low-level facts, so that MaSh can learn from the low-level
14.132 - proofs. *)
14.133 +(* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
14.134 + facts, so that MaSh can learn from the low-level proofs. *)
14.135 fun un_class_ify s =
14.136 (case first_field "_class" s of
14.137 SOME (pref, suf) => [s, pref ^ suf]
14.138 @@ -407,6 +415,7 @@
14.139 fun varify_noninducts (t as Free (s, T)) =
14.140 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
14.141 | varify_noninducts t = t
14.142 +
14.143 val p_inst =
14.144 concl_prop |> map_aterms varify_noninducts |> close_form
14.145 |> lambda (Free ind_x)
14.146 @@ -455,40 +464,44 @@
14.147 val thy = Proof_Context.theory_of ctxt
14.148 val global_facts = Global_Theory.facts_of thy
14.149 val is_too_complex =
14.150 - if generous orelse
14.151 - fact_count global_facts >= max_facts_for_complex_check then
14.152 + if generous orelse fact_count global_facts >= max_facts_for_complex_check then
14.153 K false
14.154 else
14.155 is_too_complex
14.156 val local_facts = Proof_Context.facts_of ctxt
14.157 val named_locals = local_facts |> Facts.dest_static true [global_facts]
14.158 val assms = Assumption.all_assms_of ctxt
14.159 +
14.160 fun is_good_unnamed_local th =
14.161 not (Thm.has_name_hint th) andalso
14.162 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
14.163 +
14.164 val unnamed_locals =
14.165 union Thm.eq_thm_prop (Facts.props local_facts) chained
14.166 |> filter is_good_unnamed_local |> map (pair "" o single)
14.167 val full_space =
14.168 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
14.169 val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
14.170 +
14.171 fun add_facts global foldx facts =
14.172 foldx (fn (name0, ths) => fn accum =>
14.173 if name0 <> "" andalso
14.174 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
14.175 (Facts.is_concealed facts name0 orelse
14.176 + Long_Name.is_hidden (Facts.intern facts name0) orelse
14.177 (not generous andalso is_blacklisted_or_something name0)) then
14.178 accum
14.179 else
14.180 let
14.181 val n = length ths
14.182 val multi = n > 1
14.183 +
14.184 fun check_thms a =
14.185 (case try (Proof_Context.get_thms ctxt) a of
14.186 NONE => false
14.187 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
14.188 in
14.189 - snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) =>
14.190 + snd (fold_rev (fn th => fn (j, accum) =>
14.191 (j - 1,
14.192 if not (member Thm.eq_thm_prop add_ths th) andalso
14.193 (is_likely_tautology_too_meta_or_too_technical th orelse
14.194 @@ -496,21 +509,26 @@
14.195 accum
14.196 else
14.197 let
14.198 - val new =
14.199 - (((fn () =>
14.200 - if name0 = "" then
14.201 - backquote_thm ctxt th
14.202 - else
14.203 - [Facts.extern ctxt facts name0,
14.204 - Name_Space.extern ctxt full_space name0]
14.205 - |> find_first check_thms
14.206 - |> the_default name0
14.207 - |> make_name reserved multi j),
14.208 - stature_of_thm global assms chained css name0 th),
14.209 - th)
14.210 + fun get_name () =
14.211 + if name0 = "" then
14.212 + backquote_thm ctxt th
14.213 + else
14.214 + let val short_name = Facts.extern ctxt facts name0 in
14.215 + if check_thms short_name then
14.216 + short_name
14.217 + else
14.218 + let val long_name = Name_Space.extern ctxt full_space name0 in
14.219 + if check_thms long_name then
14.220 + long_name
14.221 + else
14.222 + name0
14.223 + end
14.224 + end
14.225 + |> make_name reserved multi j
14.226 + val stature = stature_of_thm global assms chained css name0 th
14.227 + val new = ((get_name, stature), th)
14.228 in
14.229 - if multi then (uni_accum, new :: multi_accum)
14.230 - else (new :: uni_accum, multi_accum)
14.231 + (if multi then apsnd else apfst) (cons new) accum
14.232 end)) ths (n, accum))
14.233 end)
14.234 in
14.235 @@ -522,8 +540,7 @@
14.236 |> op @
14.237 end
14.238
14.239 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
14.240 - concl_t =
14.241 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
14.242 if only andalso null add then
14.243 []
14.244 else
15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Tue Jul 01 16:08:31 2014 +0100
15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Tue Jul 01 16:09:51 2014 +0100
15.3 @@ -70,11 +70,10 @@
15.4 val thy = Proof_Context.theory_of ctxt
15.5 val get_types = post_fold_term_type (K cons) []
15.6 in
15.7 - fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
15.8 - handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
15.9 + fold (perhaps o try o Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
15.10 end
15.11
15.12 -fun handle_trivial_tfrees ctxt (t', subst) =
15.13 +fun handle_trivial_tfrees ctxt t' subst =
15.14 let
15.15 val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
15.16
15.17 @@ -181,10 +180,10 @@
15.18 let
15.19 val t' = generalize_types ctxt t
15.20 val subst = match_types ctxt t' t
15.21 - val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
15.22 - val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord
15.23 + val (t'', subst') = handle_trivial_tfrees ctxt t' subst
15.24 + val typing_spots = t'' |> typing_spot_table |> reverse_greedy |> sort int_ord
15.25 in
15.26 - introduce_annotations subst typing_spots t t'
15.27 + introduce_annotations subst' typing_spots t t''
15.28 end
15.29
15.30 end;
16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 16:08:31 2014 +0100
16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 16:09:51 2014 +0100
16.3 @@ -34,17 +34,18 @@
16.4 val decode_strs : string -> string list
16.5
16.6 datatype mash_engine =
16.7 - MaSh_kNN
16.8 + MaSh_NB
16.9 + | MaSh_kNN
16.10 + | MaSh_NB_kNN
16.11 + | MaSh_NB_Ext
16.12 | MaSh_kNN_Ext
16.13 - | MaSh_NB
16.14 - | MaSh_NB_Ext
16.15
16.16 val is_mash_enabled : unit -> bool
16.17 val the_mash_engine : unit -> mash_engine
16.18
16.19 + val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
16.20 val nickname_of_thm : thm -> string
16.21 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
16.22 - val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
16.23 val crude_thm_ord : thm * thm -> order
16.24 val thm_less : thm * thm -> bool
16.25 val goal_of_thm : theory -> thm -> thm
16.26 @@ -138,36 +139,70 @@
16.27 end
16.28
16.29 datatype mash_engine =
16.30 - MaSh_kNN
16.31 + MaSh_NB
16.32 +| MaSh_kNN
16.33 +| MaSh_NB_kNN
16.34 +| MaSh_NB_Ext
16.35 | MaSh_kNN_Ext
16.36 -| MaSh_NB
16.37 -| MaSh_NB_Ext
16.38
16.39 fun mash_engine () =
16.40 let val flag1 = Options.default_string @{system_option MaSh} in
16.41 (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
16.42 - "yes" => SOME MaSh_NB
16.43 - | "sml" => SOME MaSh_NB
16.44 + "yes" => SOME MaSh_NB_kNN
16.45 + | "sml" => SOME MaSh_NB_kNN
16.46 + | "nb" => SOME MaSh_NB
16.47 | "knn" => SOME MaSh_kNN
16.48 + | "nb_knn" => SOME MaSh_NB_kNN
16.49 + | "nb_ext" => SOME MaSh_NB_Ext
16.50 | "knn_ext" => SOME MaSh_kNN_Ext
16.51 - | "nb" => SOME MaSh_NB
16.52 - | "nb_ext" => SOME MaSh_NB_Ext
16.53 - | _ => NONE)
16.54 + | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
16.55 end
16.56
16.57 val is_mash_enabled = is_some o mash_engine
16.58 -val the_mash_engine = the_default MaSh_NB o mash_engine
16.59 +val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
16.60
16.61 +fun scaled_avg [] = 0
16.62 + | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
16.63
16.64 -(*** Isabelle-agnostic machine learning ***)
16.65 +fun avg [] = 0.0
16.66 + | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
16.67
16.68 -structure MaSh =
16.69 -struct
16.70 +fun normalize_scores _ [] = []
16.71 + | normalize_scores max_facts xs =
16.72 + map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
16.73
16.74 -fun heap cmp bnd al a =
16.75 +fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
16.76 + distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
16.77 + | mesh_facts fact_eq max_facts mess =
16.78 + let
16.79 + val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
16.80 +
16.81 + fun score_in fact (global_weight, (sels, unks)) =
16.82 + let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
16.83 + (case find_index (curry fact_eq fact o fst) sels of
16.84 + ~1 => if member fact_eq unks fact then NONE else SOME 0.0
16.85 + | rank => score_at rank)
16.86 + end
16.87 +
16.88 + fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
16.89 + in
16.90 + fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
16.91 + |> map (`weight_of) |> sort (int_ord o pairself fst o swap)
16.92 + |> map snd |> take max_facts
16.93 + end
16.94 +
16.95 +fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *)
16.96 +fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *)
16.97 +
16.98 +fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
16.99 +fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
16.100 +
16.101 +fun rev_sort_array_prefix cmp bnd a =
16.102 let
16.103 exception BOTTOM of int
16.104
16.105 + val al = Array.length a
16.106 +
16.107 fun maxson l i =
16.108 let val i31 = i + i + i + 1 in
16.109 if i31 + 2 < l then
16.110 @@ -231,7 +266,17 @@
16.111 ()
16.112 end
16.113
16.114 -val number_of_nearest_neighbors = 10 (* FUDGE *)
16.115 +fun rev_sort_list_prefix cmp bnd xs =
16.116 + let val ary = Array.fromList xs in
16.117 + rev_sort_array_prefix cmp bnd ary;
16.118 + Array.foldr (op ::) [] ary
16.119 + end
16.120 +
16.121 +
16.122 +(*** Isabelle-agnostic machine learning ***)
16.123 +
16.124 +structure MaSh =
16.125 +struct
16.126
16.127 fun select_visible_facts big_number recommends =
16.128 List.app (fn at =>
16.129 @@ -239,78 +284,6 @@
16.130 Array.update (recommends, at, (j, big_number + ov))
16.131 end)
16.132
16.133 -fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats =
16.134 - let
16.135 - exception EXIT of unit
16.136 -
16.137 - val ln_afreq = Math.ln (Real.fromInt num_facts)
16.138 - fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
16.139 -
16.140 - val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
16.141 -
16.142 - fun do_feat (s, sw0) =
16.143 - let
16.144 - val sw = sw0 * tfidf s
16.145 - val w2 = sw * sw
16.146 -
16.147 - fun inc_overlap j =
16.148 - let val (_, ov) = Array.sub (overlaps_sqr, j) in
16.149 - Array.update (overlaps_sqr, j, (j, w2 + ov))
16.150 - end
16.151 - in
16.152 - List.app inc_overlap (Array.sub (feat_facts, s))
16.153 - end
16.154 -
16.155 - val _ = List.app do_feat goal_feats
16.156 - val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
16.157 - val no_recommends = Unsynchronized.ref 0
16.158 - val recommends = Array.tabulate (num_facts, rpair 0.0)
16.159 - val age = Unsynchronized.ref 500000000.0
16.160 -
16.161 - fun inc_recommend j v =
16.162 - let val (_, ov) = Array.sub (recommends, j) in
16.163 - if ov <= 0.0 then
16.164 - (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
16.165 - else if ov < !age + 1000.0 then
16.166 - Array.update (recommends, j, (j, v + ov))
16.167 - else
16.168 - ()
16.169 - end
16.170 -
16.171 - val k = Unsynchronized.ref 0
16.172 - fun do_k k =
16.173 - if k >= num_facts then
16.174 - raise EXIT ()
16.175 - else
16.176 - let
16.177 - val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
16.178 - val o1 = Math.sqrt o2
16.179 - val _ = inc_recommend j o1
16.180 - val ds = Vector.sub (depss, j)
16.181 - val l = Real.fromInt (length ds)
16.182 - in
16.183 - List.app (fn d => inc_recommend d (o1 / l)) ds
16.184 - end
16.185 -
16.186 - fun while1 () =
16.187 - if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
16.188 - handle EXIT () => ()
16.189 -
16.190 - fun while2 () =
16.191 - if !no_recommends >= max_suggs then ()
16.192 - else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
16.193 - handle EXIT () => ()
16.194 -
16.195 - fun ret acc at =
16.196 - if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
16.197 - in
16.198 - while1 ();
16.199 - while2 ();
16.200 - select_visible_facts 1000000000.0 recommends visible_facts;
16.201 - heap (Real.compare o pairself snd) max_suggs num_facts recommends;
16.202 - ret [] (Integer.max 0 (num_facts - max_suggs))
16.203 - end
16.204 -
16.205 fun wider_array_of_vector init vec =
16.206 let val ary = Array.array init in
16.207 Array.copyVec {src = vec, dst = ary, di = 0};
16.208 @@ -389,10 +362,88 @@
16.209 if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
16.210 in
16.211 select_visible_facts 100000.0 posterior visible_facts;
16.212 - heap (Real.compare o pairself snd) max_suggs num_facts posterior;
16.213 + rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior;
16.214 ret (Integer.max 0 (num_facts - max_suggs)) []
16.215 end
16.216
16.217 +val number_of_nearest_neighbors = 10 (* FUDGE *)
16.218 +
16.219 +fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
16.220 + let
16.221 + exception EXIT of unit
16.222 +
16.223 + val ln_afreq = Math.ln (Real.fromInt num_facts)
16.224 + fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
16.225 +
16.226 + val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
16.227 +
16.228 + val feat_facts = Array.array (num_feats, [])
16.229 + val _ = Vector.foldl (fn (feats, fact) =>
16.230 + (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1)) 0 featss
16.231 +
16.232 + fun do_feat (s, sw0) =
16.233 + let
16.234 + val sw = sw0 * tfidf s
16.235 + val w2 = sw * sw
16.236 +
16.237 + fun inc_overlap j =
16.238 + let val (_, ov) = Array.sub (overlaps_sqr, j) in
16.239 + Array.update (overlaps_sqr, j, (j, w2 + ov))
16.240 + end
16.241 + in
16.242 + List.app inc_overlap (Array.sub (feat_facts, s))
16.243 + end
16.244 +
16.245 + val _ = List.app do_feat goal_feats
16.246 + val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr
16.247 + val no_recommends = Unsynchronized.ref 0
16.248 + val recommends = Array.tabulate (num_facts, rpair 0.0)
16.249 + val age = Unsynchronized.ref 500000000.0
16.250 +
16.251 + fun inc_recommend v j =
16.252 + let val (_, ov) = Array.sub (recommends, j) in
16.253 + if ov <= 0.0 then
16.254 + (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
16.255 + else if ov < !age + 1000.0 then
16.256 + Array.update (recommends, j, (j, v + ov))
16.257 + else
16.258 + ()
16.259 + end
16.260 +
16.261 + val k = Unsynchronized.ref 0
16.262 + fun do_k k =
16.263 + if k >= num_facts then
16.264 + raise EXIT ()
16.265 + else
16.266 + let
16.267 + val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
16.268 + val o1 = Math.sqrt o2
16.269 + val _ = inc_recommend o1 j
16.270 + val ds = Vector.sub (depss, j)
16.271 + val l = Real.fromInt (length ds)
16.272 + in
16.273 + List.app (inc_recommend (o1 / l)) ds
16.274 + end
16.275 +
16.276 + fun while1 () =
16.277 + if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
16.278 + handle EXIT () => ()
16.279 +
16.280 + fun while2 () =
16.281 + if !no_recommends >= max_suggs then ()
16.282 + else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
16.283 + handle EXIT () => ()
16.284 +
16.285 + fun ret acc at =
16.286 + if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
16.287 + in
16.288 + while1 ();
16.289 + while2 ();
16.290 + select_visible_facts 1000000000.0 recommends visible_facts;
16.291 + rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends;
16.292 + ret [] (Integer.max 0 (num_facts - max_suggs))
16.293 + end
16.294 +
16.295 (* experimental *)
16.296 fun external_tool tool max_suggs learns goal_feats =
16.297 let
16.298 @@ -435,26 +486,35 @@
16.299 fun query_external ctxt engine max_suggs learns goal_feats =
16.300 (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
16.301 (case engine of
16.302 - MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats
16.303 - | MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats))
16.304 + MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
16.305 + | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
16.306
16.307 fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
16.308 (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
16.309 - (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
16.310 - elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
16.311 - (case engine of
16.312 - MaSh_kNN =>
16.313 - let
16.314 - val feat_facts = Array.array (num_feats, [])
16.315 - val _ =
16.316 - Vector.foldl (fn (feats, fact) =>
16.317 - (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1))
16.318 - 0 featss
16.319 - in
16.320 - k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts int_goal_feats
16.321 - end
16.322 - | MaSh_NB => naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats)
16.323 - |> map (curry Vector.sub fact_names o fst))
16.324 + let
16.325 + fun nb () =
16.326 + naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats
16.327 + |> map fst
16.328 + fun knn () =
16.329 + k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts
16.330 + int_goal_feats
16.331 + |> map fst
16.332 + in
16.333 + (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
16.334 + elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
16.335 + (case engine of
16.336 + MaSh_NB => nb ()
16.337 + | MaSh_kNN => knn ()
16.338 + | MaSh_NB_kNN =>
16.339 + let
16.340 + val mess =
16.341 + [(0.5 (* FUDGE *), (weight_facts_steeply (nb ()), [])),
16.342 + (0.5 (* FUDGE *), (weight_facts_steeply (knn ()), []))]
16.343 + in
16.344 + mesh_facts (op =) max_suggs mess
16.345 + end)
16.346 + |> map (curry Vector.sub fact_names))
16.347 + end
16.348
16.349 end;
16.350
16.351 @@ -481,7 +541,7 @@
16.352 val decode_str = String.explode #> unmeta_chars []
16.353
16.354 val encode_strs = map encode_str #> space_implode " "
16.355 -val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
16.356 +val decode_strs = space_explode " " #> map decode_str
16.357
16.358 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
16.359
16.360 @@ -706,36 +766,6 @@
16.361 |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
16.362 in map_filter lookup end
16.363
16.364 -fun scaled_avg [] = 0
16.365 - | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
16.366 -
16.367 -fun avg [] = 0.0
16.368 - | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
16.369 -
16.370 -fun normalize_scores _ [] = []
16.371 - | normalize_scores max_facts xs =
16.372 - map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
16.373 -
16.374 -fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
16.375 - distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
16.376 - | mesh_facts fact_eq max_facts mess =
16.377 - let
16.378 - val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
16.379 -
16.380 - fun score_in fact (global_weight, (sels, unks)) =
16.381 - let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
16.382 - (case find_index (curry fact_eq fact o fst) sels of
16.383 - ~1 => if member fact_eq unks fact then NONE else SOME 0.0
16.384 - | rank => score_at rank)
16.385 - end
16.386 -
16.387 - fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
16.388 - in
16.389 - fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
16.390 - |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
16.391 - |> map snd |> take max_facts
16.392 - end
16.393 -
16.394 fun free_feature_of s = "f" ^ s
16.395 fun thy_feature_of s = "y" ^ s
16.396 fun type_feature_of s = "t" ^ s
16.397 @@ -1088,9 +1118,13 @@
16.398 find_maxes Symtab.empty ([], Graph.maximals G)
16.399 end
16.400
16.401 -fun maximal_wrt_access_graph access_G facts =
16.402 - map (nickname_of_thm o snd) facts
16.403 - |> maximal_wrt_graph access_G
16.404 +fun maximal_wrt_access_graph _ [] = []
16.405 + | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
16.406 + let val thy = theory_of_thm th in
16.407 + fact :: filter_out (fn (_, th') => Theory.subthy (theory_of_thm th', thy)) facts
16.408 + |> map (nickname_of_thm o snd)
16.409 + |> maximal_wrt_graph access_G
16.410 + end
16.411
16.412 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
16.413
16.414 @@ -1098,20 +1132,6 @@
16.415 val extra_feature_factor = 0.1 (* FUDGE *)
16.416 val num_extra_feature_facts = 10 (* FUDGE *)
16.417
16.418 -(* FUDGE *)
16.419 -fun weight_of_proximity_fact rank =
16.420 - Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
16.421 -
16.422 -fun weight_facts_smoothly facts =
16.423 - facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
16.424 -
16.425 -(* FUDGE *)
16.426 -fun steep_weight_of_fact rank =
16.427 - Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
16.428 -
16.429 -fun weight_facts_steeply facts =
16.430 - facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
16.431 -
16.432 val max_proximity_facts = 100
16.433
16.434 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
16.435 @@ -1136,8 +1156,11 @@
16.436 val thy_name = Context.theory_name thy
16.437 val engine = the_mash_engine ()
16.438
16.439 - val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
16.440 - val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
16.441 + val facts = facts
16.442 + |> rev_sort_list_prefix (crude_thm_ord o pairself snd)
16.443 + (Int.max (num_extra_feature_facts, max_proximity_facts))
16.444 +
16.445 + val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
16.446
16.447 fun fact_has_right_theory (_, th) =
16.448 thy_name = Context.theory_name (theory_of_thm th)
16.449 @@ -1147,53 +1170,44 @@
16.450 |> features_of ctxt (theory_of_thm th) stature
16.451 |> map (rpair (weight * factor))
16.452
16.453 - fun query_args access_G =
16.454 - let
16.455 - val parents = maximal_wrt_access_graph access_G facts
16.456 -
16.457 - val goal_feats = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
16.458 - val chained_feats = chained
16.459 - |> map (rpair 1.0)
16.460 - |> map (chained_or_extra_features_of chained_feature_factor)
16.461 - |> rpair [] |-> fold (union (eq_fst (op =)))
16.462 - val extra_feats =
16.463 - facts
16.464 - |> take (Int.max (0, num_extra_feature_facts - length chained))
16.465 - |> filter fact_has_right_theory
16.466 - |> weight_facts_steeply
16.467 - |> map (chained_or_extra_features_of extra_feature_factor)
16.468 - |> rpair [] |-> fold (union (eq_fst (op =)))
16.469 - val feats =
16.470 - fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats)
16.471 - |> debug ? sort (Real.compare o swap o pairself snd)
16.472 - in
16.473 - (parents, feats)
16.474 - end
16.475 -
16.476 val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
16.477 peek_state ctxt
16.478
16.479 + val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
16.480 + val chained_feats = chained
16.481 + |> map (rpair 1.0)
16.482 + |> map (chained_or_extra_features_of chained_feature_factor)
16.483 + |> rpair [] |-> fold (union (eq_fst (op =)))
16.484 + val extra_feats = facts
16.485 + |> take (Int.max (0, num_extra_feature_facts - length chained))
16.486 + |> filter fact_has_right_theory
16.487 + |> weight_facts_steeply
16.488 + |> map (chained_or_extra_features_of extra_feature_factor)
16.489 + |> rpair [] |-> fold (union (eq_fst (op =)))
16.490 +
16.491 + val goal_feats =
16.492 + fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
16.493 + |> debug ? sort (Real.compare o swap o pairself snd)
16.494 +
16.495 + val parents = maximal_wrt_access_graph access_G facts
16.496 + val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
16.497 +
16.498 val suggs =
16.499 - let
16.500 - val (parents, goal_feats) = query_args access_G
16.501 - val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
16.502 - in
16.503 - if engine = MaSh_kNN_Ext orelse engine = MaSh_NB_Ext then
16.504 - let
16.505 - val learns =
16.506 - Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
16.507 - in
16.508 - MaSh.query_external ctxt engine max_suggs learns goal_feats
16.509 - end
16.510 - else
16.511 - let
16.512 - val int_goal_feats =
16.513 - map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
16.514 - in
16.515 - MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
16.516 - goal_feats int_goal_feats
16.517 - end
16.518 - end
16.519 + if engine = MaSh_NB_Ext orelse engine = MaSh_kNN_Ext then
16.520 + let
16.521 + val learns =
16.522 + Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
16.523 + in
16.524 + MaSh.query_external ctxt engine max_suggs learns goal_feats
16.525 + end
16.526 + else
16.527 + let
16.528 + val int_goal_feats =
16.529 + map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
16.530 + in
16.531 + MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
16.532 + goal_feats int_goal_feats
16.533 + end
16.534
16.535 val unknown = filter_out (is_fact_in_graph access_G o snd) facts
16.536 in
16.537 @@ -1256,6 +1270,7 @@
16.538 let
16.539 val thy = Proof_Context.theory_of ctxt
16.540 val feats = features_of ctxt thy (Local, General) [t]
16.541 + val facts = rev_sort_list_prefix (crude_thm_ord o pairself snd) 1 facts
16.542 in
16.543 map_state ctxt
16.544 (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
16.545 @@ -1587,7 +1602,6 @@
16.546 end
16.547
16.548 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
16.549 -
16.550 fun running_learners () = Async_Manager.running_threads MaShN "learner"
16.551
16.552 end;
17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jul 01 16:08:31 2014 +0100
17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jul 01 16:09:51 2014 +0100
17.3 @@ -76,6 +76,7 @@
17.4 | is_proof_method_direct Meson_Method = true
17.5 | is_proof_method_direct SMT2_Method = true
17.6 | is_proof_method_direct Simp_Method = true
17.7 + | is_proof_method_direct Simp_Size_Method = true
17.8 | is_proof_method_direct _ = false
17.9
17.10 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
17.11 @@ -103,7 +104,7 @@
17.12 maybe_paren (space_implode " " (meth_s :: ss))
17.13 end
17.14
17.15 -val silence_unifier = Try0.silence_methods false
17.16 +val silence_methods = Try0.silence_methods false
17.17
17.18 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
17.19 Method.insert_tac local_facts THEN'
17.20 @@ -113,22 +114,22 @@
17.21 Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
17.22 (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
17.23 end
17.24 - | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
17.25 + | Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts
17.26 | SMT2_Method =>
17.27 let val ctxt = Config.put SMT2_Config.verbose false ctxt in
17.28 SMT2_Solver.smt2_tac ctxt global_facts
17.29 end
17.30 - | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
17.31 + | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
17.32 + | Simp_Size_Method =>
17.33 + Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps @{thms size_ne_size_imp_ne})
17.34 | _ =>
17.35 Method.insert_tac global_facts THEN'
17.36 (case meth of
17.37 SATx_Method => SAT.satx_tac ctxt
17.38 | Blast_Method => blast_tac ctxt
17.39 - | Simp_Size_Method =>
17.40 - Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
17.41 - | Auto_Method => K (Clasimp.auto_tac (silence_unifier ctxt))
17.42 - | Fastforce_Method => Clasimp.fast_force_tac (silence_unifier ctxt)
17.43 - | Force_Method => Clasimp.force_tac (silence_unifier ctxt)
17.44 + | Auto_Method => K (Clasimp.auto_tac (silence_methods ctxt))
17.45 + | Fastforce_Method => Clasimp.fast_force_tac (silence_methods ctxt)
17.46 + | Force_Method => Clasimp.force_tac (silence_methods ctxt)
17.47 | Linarith_Method =>
17.48 let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
17.49 | Presburger_Method => Cooper.tac true [] [] ctxt
18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 16:08:31 2014 +0100
18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 16:09:51 2014 +0100
18.3 @@ -383,7 +383,7 @@
18.4 val atp_proof =
18.5 atp_proof
18.6 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
18.7 - |> introduce_spass_skolem
18.8 + |> spass ? introduce_spass_skolem
18.9 |> factify_atp_proof (map fst used_from) hyp_ts concl_t
18.10 in
18.11 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
19.1 --- a/src/HOL/Tools/etc/options Tue Jul 01 16:08:31 2014 +0100
19.2 +++ b/src/HOL/Tools/etc/options Tue Jul 01 16:09:51 2014 +0100
19.3 @@ -36,4 +36,4 @@
19.4 -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
19.5
19.6 public option MaSh : string = "sml"
19.7 - -- "machine learning engine to use by Sledgehammer (sml, nb, knn, none)"
19.8 + -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"