--- a/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Aug 03 17:56:35 2012 +0200
@@ -57,11 +57,6 @@
val all_names = map (rpair () o nickname_of) #> Symtab.make
-fun smart_dependencies_of ctxt params prover facts all_names th =
- case atp_dependencies_of ctxt params prover 0 facts all_names th of
- SOME deps => deps
- | NONE => isar_dependencies_of all_names th |> these
-
fun generate_accessibility ctxt thy include_thy file_name =
let
val path = file_name |> Path.explode
@@ -129,7 +124,9 @@
fun do_thm th =
let
val name = nickname_of th
- val deps = smart_dependencies_of ctxt params prover facts all_names th
+ val deps =
+ atp_dependencies_of ctxt params prover 0 facts all_names th
+ |> snd |> these
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
in List.app do_thm ths end
@@ -143,13 +140,14 @@
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
- val ths = facts |> map snd
- val all_names = all_names ths
+ val all_names = all_names (map snd facts)
fun do_fact ((_, stature), th) prevs =
let
val name = nickname_of th
val feats = features_of ctxt prover thy stature [prop_of th]
- val deps = smart_dependencies_of ctxt params prover facts all_names th
+ val deps =
+ atp_dependencies_of ctxt params prover 0 facts all_names th
+ |> snd |> these
val kind = Thm.legacy_get_kind th
val core =
escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 17:56:35 2012 +0200
@@ -44,7 +44,7 @@
val isar_dependencies_of : unit Symtab.table -> thm -> string list option
val atp_dependencies_of :
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
- -> thm -> string list option
+ -> thm -> bool * string list option
val is_thm_technical : thm -> bool
val mash_CLEAR : Proof.context -> unit
val mash_ADD :
@@ -315,10 +315,10 @@
|> scope <> Global ? cons "local"
|> (case string_of_status status of "" => I | s => cons s)
-(* Too many dependencies is a sign that a decision procedure is at work. There
- isn't much too learn from such proofs. *)
-val max_dependencies = 20
-val atp_dependency_default_max_fact = 50
+(* Too many dependencies is a sign that a crazy decision procedure is at work.
+ There isn't much to learn from such proofs. *)
+val max_dependencies = 100
+val atp_dependency_default_max_facts = 50
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
val typedef_deps = [@{thm CollectI} |> nickname_of]
@@ -355,7 +355,7 @@
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
auto_level facts all_names th =
case isar_dependencies_of all_names th of
- SOME [] => NONE
+ SOME [] => (false, SOME [])
| isar_deps =>
let
val thy = Proof_Context.theory_of ctxt
@@ -372,7 +372,7 @@
| NONE => accum (* shouldn't happen *)
val facts =
facts |> mepo_suggested_facts ctxt params prover
- (max_facts |> the_default atp_dependency_default_max_fact)
+ (max_facts |> the_default atp_dependency_default_max_facts)
NONE hyp_ts concl_t
|> fold (add_isar_dep facts) (these isar_deps)
|> map fix_name
@@ -396,8 +396,10 @@
end
else
();
- used_facts |> map fst |> trim_dependencies th)
- | _ => NONE
+ case used_facts |> map fst |> trim_dependencies th of
+ NONE => (false, isar_deps)
+ | atp_deps => (true, atp_deps))
+ | _ => (false, isar_deps)
end
val technical_theories =
@@ -747,6 +749,7 @@
SOME []
else if atp then
atp_dependencies_of ctxt params prover auto_level facts all_names th
+ |> (fn (false, _) => NONE | (true, deps) => deps)
else
isar_dependencies_of all_names th
fun do_commit [] [] state = state