--- a/src/HOL/TPTP/mash_eval.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Mon Jan 07 19:47:46 2013 +0100
@@ -79,7 +79,7 @@
| NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
- val isar_deps = isar_dependencies_of name_tabs th |> these
+ val isar_deps = isar_dependencies_of name_tabs th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
val mepo_facts =
mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
--- a/src/HOL/TPTP/mash_export.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Mon Jan 07 19:47:46 2013 +0100
@@ -81,14 +81,13 @@
fun isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
isar_deps_opt =
- (case params_opt of
- SOME (params as {provers = prover :: _, ...}) =>
- prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
- | NONE =>
- case isar_deps_opt of
- SOME deps => deps
- | NONE => isar_dependencies_of name_tabs th)
- |> these
+ case params_opt of
+ SOME (params as {provers = prover :: _, ...}) =>
+ prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
+ | NONE =>
+ case isar_deps_opt of
+ SOME deps => deps
+ | NONE => isar_dependencies_of name_tabs th
fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
file_name =
@@ -143,9 +142,11 @@
escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
encode_features (sort_wrt fst feats)
val query =
- if is_bad_query ctxt ho_atp th (these isar_deps) then ""
+ if is_bad_query ctxt ho_atp th isar_deps then ""
else "? " ^ core ^ "\n"
- val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
+ val update =
+ "! " ^ core ^ "; " ^
+ escape_metas (these (trim_dependencies th deps)) ^ "\n"
in query ^ update end
else
""
@@ -177,7 +178,7 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
in
- if is_bad_query ctxt ho_atp th (these isar_deps) then
+ if is_bad_query ctxt ho_atp th isar_deps then
""
else
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jan 07 19:47:46 2013 +0100
@@ -453,13 +453,13 @@
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
in
pair n
- #> fold_rev (fn th => fn (j, (multis, unis)) =>
+ #> fold_rev (fn th => fn (j, accum) =>
(j - 1,
if not (member Thm.eq_thm_prop add_ths th) andalso
(is_likely_tautology_too_meta_or_too_technical th orelse
(not generous andalso
is_too_complex ho_atp (prop_of th))) then
- (multis, unis)
+ accum
else
let
val new =
@@ -469,23 +469,24 @@
else
[Facts.extern ctxt facts name0,
Name_Space.extern ctxt full_space name0]
+ |> distinct (op =)
|> find_first check_thms
|> the_default name0
|> make_name reserved multi j),
stature_of_thm global assms chained css name0 th),
th)
in
- if multi then (new :: multis, unis)
- else (multis, new :: unis)
+ accum |> (if multi then apsnd else apfst) (cons new)
end)) ths
#> snd
end)
in
- (* The single-name theorems go after the multiple-name ones, so that single
- names are preferred when both are available. *)
- ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
- |> add_facts true Facts.fold_static global_facts global_facts
- |> op @
+ (* The single-theorem names go before the multiple-theorem ones (e.g.,
+ "xxx" vs. "xxx(3)"), so that single names are preferred when both are
+ available. *)
+ `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+ |> add_facts true Facts.fold_static global_facts global_facts
+ |> op @
end
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 07 19:47:46 2013 +0100
@@ -59,12 +59,13 @@
val features_of :
Proof.context -> string -> theory -> stature -> term list
-> (string * real) list
+ val trim_dependencies : thm -> string list -> string list option
val isar_dependencies_of :
- string Symtab.table * string Symtab.table -> thm -> string list option
+ string Symtab.table * string Symtab.table -> thm -> string list
val prover_dependencies_of :
Proof.context -> params -> string -> int -> fact list
-> string Symtab.table * string Symtab.table -> thm
- -> bool * string list option
+ -> bool * string list
val weight_mash_facts : 'a list -> ('a * real) list
val find_mash_suggestions :
int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
@@ -613,7 +614,10 @@
val prover_dependency_default_max_facts = 50
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
-val typedef_deps = [@{thm CollectI} |> nickname_of_thm]
+val typedef_dep = nickname_of_thm @{thm CollectI}
+(* Mysterious parts of the class machinery create lots of proofs that refer
+ exclusively to "someI_e" (and to some internal constructions). *)
+val class_some_dep = nickname_of_thm @{thm someI_ex}
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
val typedef_ths =
@@ -635,23 +639,23 @@
| is_size_def _ _ = false
fun trim_dependencies th deps =
- if length deps > max_dependencies then
- NONE
- else
- SOME (if deps = typedef_deps orelse
- exists (member (op =) typedef_ths) deps orelse
- is_size_def deps th then
- []
- else
- deps)
+ if length deps > max_dependencies then NONE else SOME deps
fun isar_dependencies_of name_tabs th =
- th |> thms_in_proof (SOME name_tabs) |> trim_dependencies th
+ let
+ val deps = thms_in_proof (SOME name_tabs) th
+ in
+ if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
+ exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
+ []
+ else
+ deps
+ end
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
auto_level facts name_tabs th =
case isar_dependencies_of name_tabs th of
- SOME [] => (false, SOME [])
+ [] => (false, [])
| isar_deps =>
let
val thy = Proof_Context.theory_of ctxt
@@ -672,7 +676,7 @@
|> mepo_suggested_facts ctxt params prover
(max_facts |> the_default prover_dependency_default_max_facts)
NONE hyp_ts concl_t
- |> fold (add_isar_dep facts) (these isar_deps)
+ |> fold (add_isar_dep facts) isar_deps
|> map nickify
in
if verbose andalso auto_level = 0 then
@@ -694,9 +698,7 @@
end
else
();
- case used_facts |> map fst |> trim_dependencies th of
- NONE => (false, isar_deps)
- | prover_deps => (true, prover_deps))
+ (true, map fst used_facts))
| _ => (false, isar_deps)
end
@@ -880,9 +882,11 @@
else if run_prover then
prover_dependencies_of ctxt params prover auto_level facts name_tabs
th
- |> (fn (false, _) => NONE | (true, deps) => deps)
+ |> (fn (false, _) => NONE
+ | (true, deps) => trim_dependencies th deps)
else
isar_dependencies_of name_tabs th
+ |> trim_dependencies th
fun do_commit [] [] [] state = state
| do_commit learns relearns flops {access_G, dirty} =
let
@@ -987,9 +991,7 @@
Isar_Proof => 0
| Automatic_Proof => 2 * max_isar
| Isar_Proof_wegen_Prover_Flop => max_isar)
- - 500 * (th |> isar_dependencies_of name_tabs
- |> Option.map length
- |> the_default max_dependencies)
+ - 500 * length (isar_dependencies_of name_tabs th)
val old_facts =
old_facts |> map (`priority_of)
|> sort (int_ord o pairself fst)
--- a/src/Pure/ROOT.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/Pure/ROOT.ML Mon Jan 07 19:47:46 2013 +0100
@@ -301,7 +301,10 @@
use "ProofGeneral/pgip_isabelle.ML";
-use "ProofGeneral/preferences.ML";
+(use
+ |> Unsynchronized.setmp Proofterm.proofs 0
+ |> Unsynchronized.setmp Multithreading.max_threads 0)
+ "ProofGeneral/preferences.ML";
use "ProofGeneral/pgip_parser.ML";
--- a/src/Pure/axclass.ML Sun Jan 06 14:11:15 2013 +0100
+++ b/src/Pure/axclass.ML Mon Jan 07 19:47:46 2013 +0100
@@ -113,7 +113,7 @@
fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
params2 params1;
- (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
+ (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
val proven_arities' =
Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);