# HG changeset patch # User wenzelm # Date 1357584466 -3600 # Node ID 7d89bb992f48a22d9fffc4b51b6e5463d90405f9 # Parent eee13361ec0a4a564459bf1ad6d0769e032cf885# Parent f6811984983b3bb6f76346315b933c6684590ad0 merged diff -r f6811984983b -r 7d89bb992f48 src/HOL/TPTP/mash_eval.ML --- 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 diff -r f6811984983b -r 7d89bb992f48 src/HOL/TPTP/mash_export.ML --- 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 diff -r f6811984983b -r 7d89bb992f48 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r f6811984983b -r 7d89bb992f48 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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) diff -r f6811984983b -r 7d89bb992f48 src/Pure/ROOT.ML --- 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"; diff -r f6811984983b -r 7d89bb992f48 src/Pure/axclass.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);