# HG changeset patch # User blanchet # Date 1288119688 -7200 # Node ID da97d75e20e6f6ff445bddcdb9d2c1a69c4a23f3 # Parent aff7d1471b620b44c55bc37e86a0e144cddd3208 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 21:01:28 2010 +0200 @@ -357,25 +357,25 @@ val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val axioms = + val facts = Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds (the_default default_max_relevant max_relevant) irrelevant_consts relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - axioms = axioms |> map Sledgehammer.Untranslated, only = true} + facts = facts |> map Sledgehammer.Untranslated, only = true} val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...} + val ({outcome, message, used_facts, run_time_in_msecs = SOME time_prover, ...} : Sledgehammer.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (prover params (K ""))) problem in case outcome of - NONE => (message, SH_OK (time_isa, time_prover, used_axioms)) + NONE => (message, SH_OK (time_isa, time_prover, used_facts)) | SOME _ => (message, SH_FAIL (time_isa, time_prover)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 21:01:28 2010 +0200 @@ -30,7 +30,7 @@ timeout: Time.time, expect: string} - datatype axiom = + datatype fact = Untranslated of (string * locality) * thm | Translated of term * ((string * locality) * translated_formula) option @@ -39,12 +39,12 @@ goal: thm, subgoal: int, subgoal_count: int, - axioms: axiom list, + facts: fact list, only: bool} type prover_result = {outcome: failure option, - used_axioms: (string * locality) list, + used_facts: (string * locality) list, run_time_in_msecs: int option, message: string} @@ -194,7 +194,7 @@ timeout: Time.time, expect: string} -datatype axiom = +datatype fact = Untranslated of (string * locality) * thm | Translated of term * ((string * locality) * translated_formula) option @@ -203,13 +203,13 @@ goal: thm, subgoal: int, subgoal_count: int, - axioms: axiom list, + facts: fact list, only: bool} type prover_result = {outcome: failure option, message: string, - used_axioms: (string * locality) list, + used_facts: (string * locality) list, run_time_in_msecs: int option} type prover = params -> minimize_command -> prover_problem -> prover_result @@ -232,11 +232,11 @@ |> Exn.release |> tap (after path) -fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms - i n goal = +fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i + n goal = quote name ^ (if verbose then - " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms + " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "") ^ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ @@ -252,8 +252,8 @@ fun dest_Untranslated (Untranslated p) = p | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" -fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p - | translated_axiom _ (Translated p) = p +fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p + | translated_fact _ (Translated p) = p fun int_option_add (SOME m) (SOME n) = SOME (m + n) | int_option_add _ _ = NONE @@ -269,13 +269,13 @@ ({debug, verbose, overlord, full_types, explicit_apply, max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) minimize_command - ({state, goal, subgoal, axioms, only, ...} : prover_problem) = + ({state, goal, subgoal, facts, only, ...} : prover_problem) = let val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val axioms = - axioms |> not only ? take (the_default default_max_relevant max_relevant) - |> map (translated_axiom ctxt) + val facts = + facts |> not only ? take (the_default default_max_relevant max_relevant) + |> map (translated_fact ctxt) val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" else Config.get ctxt dest_dir val problem_prefix = Config.get ctxt problem_prefix @@ -334,9 +334,9 @@ proof_delims known_failures output in (output, msecs, tstplike_proof, outcome) end val readable_names = debug andalso overlord - val (atp_problem, pool, conjecture_offset, axiom_names) = + val (atp_problem, pool, conjecture_offset, fact_names) = prepare_atp_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t axioms + explicit_apply hyp_ts concl_t facts val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses atp_problem val _ = File.write_list probfile ss @@ -358,7 +358,7 @@ (output, int_option_add msecs0 msecs, tstplike_proof, outcome)) | result => result) - in ((pool, conjecture_shape, axiom_names), result) end + in ((pool, conjecture_shape, fact_names), result) end else error ("Bad executable: " ^ Path.implode command ^ ".") @@ -371,24 +371,23 @@ () else File.write (Path.explode (Path.implode probfile ^ "_proof")) output - val ((pool, conjecture_shape, axiom_names), + val ((pool, conjecture_shape, fact_names), (output, msecs, tstplike_proof, outcome)) = with_path cleanup export run_on problem_path_name - val (conjecture_shape, axiom_names) = - repair_conjecture_shape_and_axiom_names output conjecture_shape - axiom_names + val (conjecture_shape, fact_names) = + repair_conjecture_shape_and_fact_names output conjecture_shape fact_names val important_message = if random () <= important_message_keep_factor then extract_important_message output else "" - val (message, used_axioms) = + val (message, used_facts) = case outcome of NONE => proof_text isar_proof (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (proof_banner auto, full_types, minimize_command, tstplike_proof, - axiom_names, goal, subgoal) + fact_names, goal, subgoal) |>> (fn message => message ^ (if verbose then "\nATP real CPU time: " ^ @@ -402,7 +401,7 @@ "")) | SOME failure => (string_for_failure failure, []) in - {outcome = outcome, message = message, used_axioms = used_axioms, + {outcome = outcome, message = message, used_facts = used_facts, run_time_in_msecs = msecs} end @@ -411,12 +410,12 @@ | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError fun run_smt_solver remote ({timeout, ...} : params) minimize_command - ({state, subgoal, subgoal_count, axioms, ...} + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val {outcome, used_facts, run_time_in_msecs} = SMT_Solver.smt_filter remote timeout state - (map_filter (try dest_Untranslated) axioms) subgoal + (map_filter (try dest_Untranslated) facts) subgoal val message = case outcome of NONE => @@ -426,11 +425,11 @@ minimize_line minimize_command (map fst used_facts) | SOME SMT_Solver.Time_Out => "Timed out." | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable." - | SOME (failure as SMT_Solver.Other_Failure message) => message + | SOME (SMT_Solver.Other_Failure message) => message val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *) in - {outcome = outcome, used_axioms = used_facts, - run_time_in_msecs = SOME run_time_in_msecs, message = message} + {outcome = outcome, used_facts = used_facts, + run_time_in_msecs = run_time_in_msecs, message = message} end fun get_prover thy auto name = @@ -439,7 +438,7 @@ fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) auto minimize_command - (problem as {state, goal, subgoal, subgoal_count, axioms, ...}) + (problem as {state, goal, subgoal, subgoal_count, facts, ...}) name = let val thy = Proof.theory_of state @@ -448,9 +447,9 @@ val death_time = Time.+ (birth_time, timeout) val max_relevant = the_default (default_max_relevant_for_prover thy name) max_relevant - val num_axioms = Int.min (length axioms, max_relevant) + val num_facts = Int.min (length facts, max_relevant) val desc = - prover_description ctxt params name num_axioms subgoal subgoal_count goal + prover_description ctxt params name num_facts subgoal subgoal_count goal fun go () = let fun really_go () = @@ -522,14 +521,14 @@ 0 |> fold (Integer.max o default_max_relevant_for_prover thy) provers |> auto ? (fn n => n div auto_max_relevant_divisor) - val axioms = + val facts = relevant_facts ctxt full_types relevance_thresholds max_max_relevant irrelevant_consts relevance_fudge relevance_override chained_ths hyp_ts concl_t |> map maybe_translate val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - axioms = axioms, only = only} + facts = facts, only = only} val run_prover = run_prover params auto minimize_command in if auto then @@ -543,7 +542,7 @@ end val run_atps = run_provers full_types atp_irrelevant_consts atp_relevance_fudge - (Translated o translate_axiom ctxt) atps + (Translated o translate_fact ctxt) atps val run_smts = run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated smts diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue Oct 26 21:01:28 2010 +0200 @@ -17,7 +17,7 @@ string Symtab.table * bool * int * Proof.context * int list list type text_result = string * (string * locality) list - val repair_conjecture_shape_and_axiom_names : + val repair_conjecture_shape_and_fact_names : string -> int list list -> (string * locality) list vector -> int list list * (string * locality) list vector val apply_on_subgoal : int -> int -> string @@ -57,7 +57,7 @@ (** SPASS's Flotter hack **) -(* This is a hack required for keeping track of axioms after they have been +(* This is a hack required for keeping track of facts after they have been clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also part of this hack. *) @@ -84,8 +84,7 @@ #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation #> fst -fun repair_conjecture_shape_and_axiom_names output conjecture_shape - axiom_names = +fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names = if String.isSubstring set_ClauseFormulaRelationN output then let val j0 = hd (hd conjecture_shape) @@ -97,10 +96,9 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) fun names_for_number j = j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of + |> map_filter (try (unprefix fact_prefix)) |> map unascii_of |> map (fn name => - (name, name |> find_first_in_list_vector axiom_names - |> the) + (name, name |> find_first_in_list_vector fact_names |> the) handle Option.Option => error ("No such fact: " ^ quote name ^ ".")) in @@ -108,7 +106,7 @@ seq |> map names_for_number |> Vector.fromList) end else - (conjecture_shape, axiom_names) + (conjecture_shape, fact_names) (** Soft-core proof reconstruction: Metis one-liner **) @@ -139,38 +137,37 @@ "\nTo minimize the number of lemmas, try this: " ^ Markup.markup Markup.sendback command ^ "." -fun resolve_axiom axiom_names ((_, SOME s)) = - (case strip_prefix_and_unascii axiom_prefix s of - SOME s' => (case find_first_in_list_vector axiom_names s' of +fun resolve_fact fact_names ((_, SOME s)) = + (case strip_prefix_and_unascii fact_prefix s of + SOME s' => (case find_first_in_list_vector fact_names s' of SOME x => [(s', x)] | NONE => []) | NONE => []) - | resolve_axiom axiom_names (num, NONE) = + | resolve_fact fact_names (num, NONE) = case Int.fromString num of SOME j => - if j > 0 andalso j <= Vector.length axiom_names then - Vector.sub (axiom_names, j - 1) + if j > 0 andalso j <= Vector.length fact_names then + Vector.sub (fact_names, j - 1) else [] | NONE => [] -fun add_fact axiom_names (Inference (name, _, [])) = - append (resolve_axiom axiom_names name) +fun add_fact fact_names (Inference (name, _, [])) = + append (resolve_fact fact_names name) | add_fact _ _ = I -fun used_facts_in_tstplike_proof axiom_names = - atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names) +fun used_facts_in_tstplike_proof fact_names = + atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names) -fun used_facts axiom_names = - used_facts_in_tstplike_proof axiom_names +fun used_facts fact_names = + used_facts_in_tstplike_proof fact_names #> List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) fun metis_proof_text (banner, full_types, minimize_command, - tstplike_proof, axiom_names, goal, i) = + tstplike_proof, fact_names, goal, i) = let - val (chained_lemmas, other_lemmas) = - used_facts axiom_names tstplike_proof + val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof val n = Logic.count_prems (prop_of goal) in (metis_line banner full_types i n (map fst other_lemmas) ^ @@ -233,7 +230,7 @@ | NONE => ~1 in if k >= 0 then [k] else [] end -fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape fun raw_label_for_name conjecture_shape name = @@ -491,14 +488,14 @@ | replace_dependencies_in_line p (Inference (name, t, deps)) = Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) -(* Discard axioms; consolidate adjacent lines that prove the same formula, since +(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) fun add_line _ _ (line as Definition _) lines = line :: lines - | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines = - (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or + | add_line conjecture_shape fact_names (Inference (name, t, [])) lines = + (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) - if is_axiom axiom_names name then - (* Axioms are not proof lines. *) + if is_fact fact_names name then + (* Facts are not proof lines. *) if is_only_type_information t then map (replace_dependencies_in_line (name, [])) lines (* Is there a repetition? If so, replace later line by earlier one. *) @@ -541,10 +538,10 @@ fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees + | add_desired_line isar_shrink_factor conjecture_shape fact_names frees (Inference (name, t, deps)) (j, lines) = (j + 1, - if is_axiom axiom_names name orelse + if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse (* the last line must be kept *) j = 0 orelse @@ -580,20 +577,20 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) -fun add_fact_from_dependency conjecture_shape axiom_names name = - if is_axiom axiom_names name then - apsnd (union (op =) (map fst (resolve_axiom axiom_names name))) +fun add_fact_from_dependency conjecture_shape fact_names name = + if is_fact fact_names name then + apsnd (union (op =) (map fst (resolve_fact fact_names name))) else apfst (insert (op =) (raw_label_for_name conjecture_shape name)) fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) | step_for_line conjecture_shape _ _ (Inference (name, t, [])) = Assume (raw_label_for_name conjecture_shape name, t) - | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) = + | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) = Have (if j = 1 then [Show] else [], raw_label_for_name conjecture_shape name, fold_rev forall_of (map Var (Term.add_vars t [])) t, - ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names) + ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names) deps ([], []))) fun repair_name "$true" = "c_True" @@ -606,8 +603,9 @@ else s -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor - tstplike_proof conjecture_shape axiom_names params frees = +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees + isar_shrink_factor tstplike_proof conjecture_shape fact_names params + frees = let val lines = tstplike_proof @@ -615,14 +613,14 @@ |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name |> decode_lines ctxt full_types tfrees - |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) + |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor - conjecture_shape axiom_names frees) + conjecture_shape fact_names frees) |> snd in (if null params then [] else [Fix params]) @ - map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1) + map2 (step_for_line conjecture_shape fact_names) (length lines downto 1) lines end @@ -915,7 +913,7 @@ fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (other_params as (_, full_types, _, tstplike_proof, - axiom_names, goal, i)) = + fact_names, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] @@ -924,7 +922,7 @@ val (one_line_proof, lemma_names) = metis_proof_text other_params fun isar_proof_for () = case isar_proof_from_tstplike_proof pool ctxt full_types tfrees - isar_shrink_factor tstplike_proof conjecture_shape axiom_names + isar_shrink_factor tstplike_proof conjecture_shape fact_names params frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Oct 26 21:01:28 2010 +0200 @@ -11,9 +11,9 @@ type 'a problem = 'a ATP_Problem.problem type translated_formula - val axiom_prefix : string + val fact_prefix : string val conjecture_prefix : string - val translate_axiom : + val translate_fact : Proof.context -> (string * 'a) * thm -> term * ((string * 'a) * translated_formula) option val prepare_atp_problem : @@ -29,7 +29,7 @@ open Metis_Translate open Sledgehammer_Util -val axiom_prefix = "ax_" +val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" val class_rel_clause_prefix = "clrel_"; @@ -174,7 +174,7 @@ | aux _ = raise Fail "aux" in perhaps (try aux) end -(* making axiom and conjecture formulas *) +(* making fact and conjecture formulas *) fun make_formula ctxt presimp name kind t = let val thy = ProofContext.theory_of ctxt @@ -194,7 +194,7 @@ ctypes_sorts = ctypes_sorts} end -fun make_axiom ctxt presimp ((name, loc), th) = +fun make_fact ctxt presimp ((name, loc), th) = case make_formula ctxt presimp name Axiom (prop_of th) of {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE | formula => SOME ((name, loc), formula) @@ -232,10 +232,10 @@ [optional_helpers, optional_typed_helpers] |> maps (maps fst) |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make -fun get_helper_facts ctxt is_FO full_types conjectures axioms = +fun get_helper_facts ctxt is_FO full_types conjectures facts = let val ct = - fold (fold count_translated_formula) [conjectures, axioms] init_counters + fold (fold count_translated_formula) [conjectures, facts] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 fun baptize th = ((Thm.get_name_hint th, false), th) in @@ -244,32 +244,32 @@ |> maps (fn (ss, ths) => if exists is_needed ss then map baptize ths else [])) @ (if is_FO then [] else map baptize mandatory_helpers) - |> map_filter (Option.map snd o make_axiom ctxt false) + |> map_filter (Option.map snd o make_fact ctxt false) end -fun translate_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax) +fun translate_fact ctxt (ax as (_, th)) = (prop_of th, make_fact ctxt true ax) -fun translate_formulas ctxt full_types hyp_ts concl_t axioms = +fun translate_formulas ctxt full_types hyp_ts concl_t facts = let val thy = ProofContext.theory_of ctxt - val (axiom_ts, translated_axioms) = ListPair.unzip axioms - (* Remove existing axioms from the conjecture, as this can dramatically + val (fact_ts, translated_facts) = ListPair.unzip facts + (* Remove existing facts from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) - val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts) + val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts) val goal_t = Logic.list_implies (hyp_ts, concl_t) val is_FO = Meson.is_fol_term thy goal_t val subs = tfree_classes_of_terms [goal_t] - val supers = tvar_classes_of_terms axiom_ts - val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) - (* TFrees in the conjecture; TVars in the axioms *) + val supers = tvar_classes_of_terms fact_ts + val tycons = type_consts_of_terms thy (goal_t :: fact_ts) + (* TFrees in the conjecture; TVars in the facts *) val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) - val (axiom_names, axioms) = ListPair.unzip (map_filter I translated_axioms) - val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms + val (fact_names, facts) = ListPair.unzip (map_filter I translated_facts) + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in - (axiom_names |> map single |> Vector.fromList, - (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) + (fact_names |> map single |> Vector.fromList, + (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses)) end fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -322,14 +322,14 @@ | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) in aux end -fun formula_for_axiom full_types - ({combformula, ctypes_sorts, ...} : translated_formula) = +fun formula_for_fact full_types + ({combformula, ctypes_sorts, ...} : translated_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) + Fof (prefix ^ ascii_of name, kind, formula_for_fact full_types formula) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = @@ -497,13 +497,13 @@ (const_table_for_problem explicit_apply problem) problem fun prepare_atp_problem ctxt readable_names explicit_forall full_types - explicit_apply hyp_ts concl_t axioms = + explicit_apply hyp_ts concl_t facts = let val thy = ProofContext.theory_of ctxt - val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, - arity_clauses)) = - translate_formulas ctxt full_types hyp_ts concl_t axioms - val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms + val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses, + arity_clauses)) = + translate_formulas ctxt full_types hyp_ts concl_t facts + val fact_lines = map (problem_line_for_fact fact_prefix full_types) facts val helper_lines = map (problem_line_for_fact helper_prefix full_types) helper_facts val conjecture_lines = @@ -515,7 +515,7 @@ (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = - [("Relevant facts", axiom_lines), + [("Relevant facts", fact_lines), ("Class relationships", class_rel_lines), ("Arity declarations", arity_lines), ("Helper facts", helper_lines), @@ -524,12 +524,12 @@ |> repair_problem thy explicit_forall full_types explicit_apply val (problem, pool) = nice_atp_problem readable_names problem val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines + length fact_lines + length class_rel_lines + length arity_lines + length helper_lines in (problem, case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset, axiom_names) + conjecture_offset, fact_names) end end; diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 26 21:01:28 2010 +0200 @@ -283,7 +283,7 @@ structure PType_Tab = Table(type key = ptype val ord = ptype_ord) -fun count_axiom_consts thy fudge = +fun count_fact_consts thy fudge = let fun do_const const (s, T) ts = (* Two-dimensional table update. Constant maps to types maps to count. *) @@ -357,9 +357,9 @@ | locality_bonus {assum_bonus, ...} Assum = assum_bonus | locality_bonus {chained_bonus, ...} Chained = chained_bonus -fun axiom_weight fudge loc const_tab relevant_consts axiom_consts = - case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts) - ||> filter_out (pconst_hyper_mem swap relevant_consts) of +fun fact_weight fudge loc const_tab relevant_consts fact_consts = + case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts) + ||> filter_out (pconst_hyper_mem swap relevant_consts) of ([], _) => 0.0 | (rel, irrel) => let @@ -372,14 +372,14 @@ val res = rel_weight / (rel_weight + irrel_weight) in if Real.isFinite res then res else 0.0 end -fun pconsts_in_axiom thy irrelevant_consts t = +fun pconsts_in_fact thy irrelevant_consts t = Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) [] -fun pair_consts_axiom thy irrelevant_consts fudge axiom = - case axiom |> snd |> theory_const_prop_of fudge - |> pconsts_in_axiom thy irrelevant_consts of +fun pair_consts_fact thy irrelevant_consts fudge fact = + case fact |> snd |> theory_const_prop_of fudge + |> pconsts_in_fact thy irrelevant_consts of [] => NONE - | consts => SOME ((axiom, consts), NONE) + | consts => SOME ((fact, consts), NONE) type annotated_thm = (((unit -> string) * locality) * thm) * (string * ptype) list @@ -407,27 +407,27 @@ (accepts, more_rejects @ rejects) end -fun if_empty_replace_with_locality thy irrelevant_consts axioms loc tab = +fun if_empty_replace_with_locality thy irrelevant_consts facts loc tab = if Symtab.is_empty tab then pconsts_in_terms thy irrelevant_consts false (SOME false) (map_filter (fn ((_, loc'), th) => - if loc' = loc then SOME (prop_of th) else NONE) axioms) + if loc' = loc then SOME (prop_of th) else NONE) facts) else tab fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts (fudge as {threshold_divisor, ridiculous_threshold, ...}) - ({add, del, ...} : relevance_override) axioms goal_ts = + ({add, del, ...} : relevance_override) facts goal_ts = let val thy = ProofContext.theory_of ctxt - val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty + val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty val goal_const_tab = pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts - |> fold (if_empty_replace_with_locality thy irrelevant_consts axioms) + |> fold (if_empty_replace_with_locality thy irrelevant_consts facts) [Chained, Assum, Local] val add_ths = Attrib.eval_thms ctxt add val del_ths = Attrib.eval_thms ctxt del - val axioms = axioms |> filter_out (member Thm.eq_thm del_ths o snd) + val facts = facts |> filter_out (member Thm.eq_thm del_ths o snd) fun iter j remaining_max threshold rel_const_tab hopeless hopeful = let fun relevant [] _ [] = @@ -476,14 +476,14 @@ hopeless_rejects hopeful_rejects) end | relevant candidates rejects - (((ax as (((_, loc), _), axiom_consts)), cached_weight) + (((ax as (((_, loc), _), fact_consts)), cached_weight) :: hopeful) = let val weight = case cached_weight of SOME w => w - | NONE => axiom_weight fudge loc const_tab rel_const_tab - axiom_consts + | NONE => fact_weight fudge loc const_tab rel_const_tab + fact_consts in if weight >= threshold then relevant ((ax, weight) :: candidates) rejects hopeful @@ -500,16 +500,16 @@ relevant [] [] hopeful end fun add_add_ths accepts = - (axioms |> filter ((member Thm.eq_thm add_ths - andf (not o member (Thm.eq_thm o apsnd snd) accepts)) - o snd)) + (facts |> filter ((member Thm.eq_thm add_ths + andf (not o member (Thm.eq_thm o apsnd snd) accepts)) + o snd)) @ accepts in - axioms |> map_filter (pair_consts_axiom thy irrelevant_consts fudge) - |> iter 0 max_relevant threshold0 goal_const_tab [] - |> not (null add_ths) ? add_add_ths - |> tap (fn res => trace_msg (fn () => - "Total relevant: " ^ Int.toString (length res))) + facts |> map_filter (pair_consts_fact thy irrelevant_consts fudge) + |> iter 0 max_relevant threshold0 goal_const_tab [] + |> not (null add_ths) ? add_add_ths + |> tap (fn res => trace_msg (fn () => + "Total relevant: " ^ Int.toString (length res))) end @@ -793,7 +793,7 @@ 1.0 / Real.fromInt (max_relevant + 1)) val add_ths = Attrib.eval_thms ctxt add val reserved = reserved_isar_keyword_table () - val axioms = + val facts = (if only then maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) o name_thm_pairs_from_ref ctxt reserved chained_ths) add @@ -802,16 +802,16 @@ |> name_thm_pairs ctxt (respect_no_atp andalso not only) |> uniquify in - trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^ - " theorems"); + trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^ + " facts"); (if only orelse threshold1 < 0.0 then - axioms + facts else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse max_relevant = 0 then [] else relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts - fudge override axioms (concl_t :: hyp_ts)) + fudge override facts (concl_t :: hyp_ts)) |> map (apfst (apfst (fn f => f ()))) end diff -r aff7d1471b62 -r da97d75e20e6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 20:12:33 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 21:01:28 2010 +0200 @@ -44,42 +44,42 @@ fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof, isar_shrink_factor, ...} : params) (prover : prover) - explicit_apply timeout i n state axioms = + explicit_apply timeout i n state facts = let val _ = - Output.urgent_message ("Testing " ^ n_facts (map fst axioms) ^ "...") + Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...") val params = {blocking = true, debug = debug, verbose = verbose, overlord = overlord, provers = provers, full_types = full_types, explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), max_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} - val axioms = - axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n)) + val facts = + facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n)) val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - axioms = axioms, only = true} - val result as {outcome, used_axioms, ...} = prover params (K "") problem + facts = facts, only = true} + val result as {outcome, used_facts, ...} = prover params (K "") problem in Output.urgent_message (case outcome of SOME failure => string_for_failure failure | NONE => - if length used_axioms = length axioms then "Found proof." - else "Found proof with " ^ n_facts used_axioms ^ "."); + if length used_facts = length facts then "Found proof." + else "Found proof with " ^ n_facts used_facts ^ "."); result end -(* minimalization of thms *) +(* minimalization of facts *) -fun filter_used_axioms used = filter (member (op =) used o fst) +fun filter_used_facts used = filter (member (op =) used o fst) fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = case test (xs @ seen) of - result as {outcome = NONE, used_axioms, ...} : prover_result => - sublinear_minimize test (filter_used_axioms used_axioms xs) - (filter_used_axioms used_axioms seen, result) + result as {outcome = NONE, used_facts, ...} : prover_result => + sublinear_minimize test (filter_used_facts used_facts xs) + (filter_used_facts used_facts seen, result) | _ => sublinear_minimize test xs (x :: seen, result) (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer @@ -89,7 +89,7 @@ fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set." | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n - state axioms = + state facts = let val thy = Proof.theory_of state val prover = get_prover thy false prover_name @@ -99,13 +99,13 @@ val (_, hyp_ts, concl_t) = strip_subgoal goal i val explicit_apply = not (forall (Meson.is_fol_term thy) - (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) + (concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) fun do_test timeout = test_facts params prover explicit_apply timeout i n state val timer = Timer.startRealTimer () in - (case do_test timeout axioms of - result as {outcome = NONE, used_axioms, ...} => + (case do_test timeout facts of + result as {outcome = NONE, used_facts, ...} => let val time = Timer.checkRealTimer timer val new_timeout = @@ -113,7 +113,7 @@ |> Time.fromMilliseconds val (min_thms, {message, ...}) = sublinear_minimize (do_test new_timeout) - (filter_used_axioms used_axioms axioms) ([], result) + (filter_used_facts used_facts facts) ([], result) val n = length min_thms val _ = Output.urgent_message (cat_lines ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ @@ -140,7 +140,7 @@ val ctxt = Proof.context_of state val reserved = reserved_isar_keyword_table () val chained_ths = #facts (Proof.goal state) - val axioms = + val facts = maps (map (apsnd single) o name_thm_pairs_from_ref ctxt reserved chained_ths) refs in @@ -148,7 +148,7 @@ 0 => Output.urgent_message "No subgoal!" | n => (kill_provers (); - Output.urgent_message (#2 (minimize_facts params i n state axioms))) + Output.urgent_message (#2 (minimize_facts params i n state facts))) end end;