standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
--- 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)
--- 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
--- 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
--- 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;
--- 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
--- 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;