--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 20:07:31 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jul 26 22:22:23 2010 +0200
@@ -29,8 +29,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: ((string * int) * thm) list option,
- filtered_clauses: ((string * int) * thm) list option}
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
@@ -44,7 +44,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list,
- filtered_clauses: ((string * int) * thm) list}
+ filtered_clauses: (string * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -96,8 +96,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: ((string * int) * thm) list option,
- filtered_clauses: ((string * int) * thm) list option}
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
@@ -113,7 +113,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list,
- filtered_clauses: ((string * int) * thm) list}
+ filtered_clauses: (string * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 20:07:31 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 22:22:23 2010 +0200
@@ -220,8 +220,8 @@
(* making axiom and conjecture clauses *)
fun make_clause thy (formula_id, formula_name, kind, t) =
let
- (* ### FIXME: introduce combinators and perform other transformations
- previously done by Clausifier.to_nnf *)
+ (* ### FIXME: perform other transformations previously done by
+ "Clausifier.to_nnf", e.g. "HOL.If" *)
val t = t |> transform_elim_term
|> Object_Logic.atomize_term thy
|> extensionalize_term
@@ -233,8 +233,8 @@
ctypes_sorts = ctypes_sorts}
end
-fun add_axiom_clause thy ((name, k), th) =
- cons (name, make_clause thy (k, name, Axiom, prop_of th))
+fun add_axiom_clause thy (name, th) =
+ cons (name, make_clause thy (0, name, Axiom, prop_of th))
fun make_axiom_clauses thy clauses = fold_rev (add_axiom_clause thy) clauses []
@@ -254,17 +254,13 @@
fun count_fol_formula (FOLFormula {combformula, ...}) =
count_combformula combformula
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
-
val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
+ [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
+ (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ (["c_COMBS"], @{thms COMBS_def})]
val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+ [(["c_True", "c_False"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False True_or_False})]
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
val init_counters =
@@ -280,14 +276,14 @@
val cnfs =
(optional_helpers
|> full_types ? append optional_typed_helpers
- |> maps (fn (ss, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map (`Thm.get_name_hint) ths
+ else [])) @
+ (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
in map snd (make_axiom_clauses thy cnfs) end
-fun negate_term (@{const Not} $ t) = t
- | negate_term t = @{const Not} $ t
+fun s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
@@ -300,9 +296,8 @@
val subs = tfree_classes_of_terms [goal_t]
val supers = tvar_classes_of_terms axtms
val tycons = type_consts_of_terms thy (goal_t :: axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures =
- make_conjecture_clauses thy (map negate_term hyp_ts @ [concl_t])
+ (* TFrees in conjecture clauses; TVars in axiom clauses *)
+ val conjectures = make_conjecture_clauses thy (map s_not hyp_ts @ [concl_t])
val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
val helper_clauses =
@@ -384,7 +379,6 @@
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
- |> Clausifier.cnf_rules_pairs thy true
val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
prepare_clauses full_types hyp_ts concl_t the_axiom_clauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 20:07:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Jul 26 22:22:23 2010 +0200
@@ -55,13 +55,12 @@
val _ = priority ("Testing " ^ string_of_int num_theorems ^
" theorem" ^ plural_s num_theorems ^ "...")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME axclauses,
- filtered_clauses = SOME (the_default axclauses filtered_clauses)}
+ axiom_clauses = SOME name_thm_pairs,
+ filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
in
prover params (K "") timeout problem
|> tap (fn result : prover_result =>