--- a/src/HOL/Metis_Examples/Tarski.thy Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy Tue Jun 29 11:38:51 2010 +0200
@@ -507,9 +507,8 @@
(*never proved, 2007-01-22*)
declare [[ atp_problem_prefix = "Tarski__CLF_lubH_is_fixp" ]]
-(*Single-step version fails. The conjecture clauses refer to local abstraction
-functions (Frees), which prevents expand_defs_tac from removing those
-"definitions" at the end of the proof. *)
+(* Single-step version fails. The conjecture clauses refer to local abstraction
+functions (Frees). *)
lemma (in CLF) lubH_is_fixp:
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
apply (simp add: fix_def)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 29 11:38:51 2010 +0200
@@ -299,7 +299,6 @@
fun run_sh prover hard_timeout timeout dir st =
let
- val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *)
val {context = ctxt, facts, goal} = Proof.goal st
val thy = ProofContext.theory_of ctxt
val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
@@ -325,7 +324,7 @@
NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
- handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
+ handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
--- a/src/HOL/Sledgehammer.thy Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jun 29 11:38:51 2010 +0200
@@ -86,8 +86,6 @@
done
use "Tools/Sledgehammer/clausifier.ML"
-setup Clausifier.setup
-
use "Tools/Sledgehammer/meson_tactic.ML"
setup Meson_Tactic.setup
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 29 11:38:51 2010 +0200
@@ -8,9 +8,8 @@
signature ATP_MANAGER =
sig
- type cnf_thm = Clausifier.cnf_thm
- type name_pool = Metis_Clauses.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type name_pool = Sledgehammer_TPTP_Format.name_pool
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
type params =
{debug: bool,
@@ -31,11 +30,11 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -46,9 +45,10 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
+ exception TRIVIAL of unit
val kill_atps: unit -> unit
val running_atps: unit -> unit
@@ -98,12 +98,12 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
- Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
- MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
@@ -115,11 +115,14 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
+(* Trivial problem, which resolution cannot handle (empty clause) *)
+exception TRIVIAL of unit
+
(* named provers *)
structure Data = Theory_Data
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 11:38:51 2010 +0200
@@ -7,13 +7,10 @@
signature ATP_SYSTEMS =
sig
- type prover = ATP_Manager.prover
-
- (* hooks for problem files *)
+ val trace : bool Unsynchronized.ref
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_runtime : bool Config.T
-
val refresh_systems_on_tptp : unit -> unit
val default_atps_param_value : unit -> string
val setup : theory -> theory
@@ -30,6 +27,9 @@
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
+
(** generic ATP **)
(* external problem files *)
@@ -95,6 +95,7 @@
fun string_for_failure Unprovable = "The ATP problem is unprovable."
| string_for_failure IncompleteUnprovable =
"The ATP cannot prove the problem."
+ | string_for_failure CantConnect = "Can't connect to remote ATP."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
@@ -121,6 +122,124 @@
(j :: hd shape) :: tl shape
end
+
+(* Clause preparation *)
+
+fun make_clause_table xs =
+ fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
+
+(* Remove existing axiom clauses from the conjecture clauses, as this can
+ dramatically boost an ATP's performance (for some reason). *)
+fun subtract_cls ax_clauses =
+ filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+
+fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) =
+ (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
+ | is_false_literal _ = false
+fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) =
+ (pol andalso c = "c_True") orelse
+ (not pol andalso c = "c_False")
+ | is_true_literal _ = false;
+fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
+
+(* making axiom and conjecture clauses *)
+fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
+ let
+ val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems
+ val (lits, ctypes_sorts) = literals_of_term thy t
+ in
+ if forall is_false_literal lits then
+ raise TRIVIAL ()
+ else
+ (skolems,
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
+ end
+
+fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
+ let
+ val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
+ in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end
+
+fun make_axiom_clauses thy clauses =
+ ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
+
+fun make_conjecture_clauses thy =
+ let
+ fun aux _ _ [] = []
+ | aux n skolems (th :: ths) =
+ let
+ val (skolems, cls) =
+ make_clause thy (n, "conjecture", Conjecture, th) skolems
+ in cls :: aux (n + 1) skolems ths end
+ in aux 0 [] end
+
+(** Helper clauses **)
+
+fun count_combterm (CombConst ((c, _), _, _)) =
+ Symtab.map_entry c (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
+fun count_literal (Literal (_, t)) = count_combterm t
+fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+
+fun cnf_helper_thms thy raw =
+ map (`Thm.get_name_hint)
+ #> (if raw then map (apfst (rpair 0)) else 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}))]
+val optional_typed_helpers =
+ [(["c_True", "c_False"], (true, @{thms True_or_False})),
+ (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+
+val init_counters =
+ Symtab.make (maps (maps (map (rpair 0) o fst))
+ [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses thy is_FO full_types conjectures axcls =
+ let
+ val axclauses = map snd (make_axiom_clauses thy axcls)
+ val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ 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)
+ in map snd (make_axiom_clauses thy cnfs) end
+
+(* prepare for passing to writer,
+ create additional clauses based on the information from extra_cls *)
+fun prepare_clauses full_types goal_cls axcls extra_cls thy =
+ let
+ val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
+ val ccls = subtract_cls extra_cls goal_cls
+ val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val ccltms = map prop_of ccls
+ and axtms = map (prop_of o snd) extra_cls
+ val subs = tfree_classes_of_terms ccltms
+ and supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms thy (ccltms @ axtms)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val conjectures = make_conjecture_clauses thy ccls
+ 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 =
+ get_helper_clauses thy is_FO full_types conjectures extra_cls
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val classrel_clauses = make_classrel_clauses thy subs supers'
+ in
+ (Vector.fromList clnames,
+ (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ end
+
+
(* generic TPTP-based provers *)
fun generic_tptp_prover
@@ -139,12 +258,13 @@
val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
- (case filtered_clauses of
- NONE => relevant_facts full_types relevance_threshold
+ case filtered_clauses of
+ SOME fcls => fcls
+ | NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
- | SOME fcls => fcls);
+ |> 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 goal_cls the_axiom_clauses the_filtered_clauses
@@ -346,7 +466,8 @@
case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
(answer, 0) => split_lines answer
| (answer, _) =>
- error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+ error ("Failed to get available systems at SystemOnTPTP:\n" ^
+ perhaps (try (unsuffix "\n")) answer)
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
@@ -361,7 +482,8 @@
| SOME sys => sys);
val remote_known_failures =
- [(TimedOut, "says Timeout"),
+ [(CantConnect, "HTTP-Error"),
+ (TimedOut, "says Timeout"),
(MalformedOutput, "Remote script could not extract proof")]
fun remote_config atp_prefix args
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 11:38:51 2010 +0200
@@ -7,63 +7,17 @@
signature CLAUSIFIER =
sig
- type cnf_thm = thm * ((string * int) * thm)
-
- val sledgehammer_prefix: string
- val chained_prefix: string
- val trace: bool Unsynchronized.ref
- val trace_msg: (unit -> string) -> unit
- val name_thms_pair_from_ref :
- Proof.context -> thm list -> Facts.ref -> string * thm list
- val skolem_theory_name: string
- val skolem_prefix: string
- val skolem_infix: string
- val is_skolem_const_name: string -> bool
- val num_type_args: theory -> string -> int
- val cnf_axiom: theory -> thm -> thm list
- val multi_base_blacklist: string list
- val is_theorem_bad_for_atps: thm -> bool
- val type_has_topsort: typ -> bool
- val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
- val saturate_cache: theory -> theory option
- val auto_saturate_cache: bool Unsynchronized.ref
+ val cnf_axiom: theory -> bool -> thm -> thm list
+ val cnf_rules_pairs :
+ theory -> bool -> (string * thm) list -> ((string * int) * thm) list
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
Proof.context -> thm -> int -> thm list list * (string * typ) list
- val setup: theory -> theory
end;
structure Clausifier : CLAUSIFIER =
struct
-type cnf_thm = thm * ((string * int) * thm)
-
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-
-(* Used to label theorems chained into the goal. *)
-val chained_prefix = sledgehammer_prefix ^ "chained_"
-
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if !trace then tracing (msg ()) else ();
-
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
-val skolem_theory_name = sledgehammer_prefix ^ "Sko"
-val skolem_prefix = "sko_"
-val skolem_infix = "$"
-
-val type_has_topsort = Term.exists_subtype
- (fn TFree (_, []) => true
- | TVar (_, []) => true
- | _ => false);
-
-
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -86,116 +40,39 @@
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-(*Keep the full complexity of the original name*)
-fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-
-fun skolem_name thm_name j var_name =
- skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
- skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_theory_name s then
- s |> unprefix skolem_theory_name
- |> space_explode skolem_infix |> hd
- |> space_explode "_" |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
-fun rhs_extra_types lhsT rhs =
- let val lhs_vars = Term.add_tfreesT lhsT []
- fun add_new_TFrees (TFree v) =
- if member (op =) lhs_vars v then I else insert (op =) (TFree v)
- | add_new_TFrees _ = I
- val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
- in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
-
-fun skolem_type_and_args bound_T body =
- let
- val args1 = OldTerm.term_frees body
- val Ts1 = map type_of args1
- val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
- val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
- in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
-
-(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
- suggested prefix for the Skolem constants. *)
-fun declare_skolem_funs s th thy =
- let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
- (axs, thy) =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val (cT, args) = skolem_type_and_args T body
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ body)
- (*Forms a lambda-abstraction over the formal parameters*)
- val (c, thy) =
- Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
- val cdef = id ^ "_def"
- val ((_, ax), thy) =
- Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
- val ax' = Drule.export_without_context ax
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
- | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
- in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
- | dec_sko _ thx = thx
- in dec_sko (prop_of th) ([], thy) end
-
fun mk_skolem_id t =
let val T = fastype_of t in
Const (@{const_name skolem_id}, T --> T) $ t
end
-fun quasi_beta_eta_contract (Abs (s, T, t')) =
- Abs (s, T, quasi_beta_eta_contract t')
- | quasi_beta_eta_contract t = Envir.beta_eta_contract t
+fun beta_eta_under_lambdas (Abs (s, T, t')) =
+ Abs (s, T, beta_eta_under_lambdas t')
+ | beta_eta_under_lambdas t = Envir.beta_eta_contract t
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs s th =
+fun assume_skolem_funs th =
let
- val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
+ val args = OldTerm.term_frees body
val Ts = map type_of args
val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
- val id = skolem_name s (Unsynchronized.inc skolem_count) s'
- val c = Free (id, cT) (* FIXME: needed? ### *)
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
list_abs_free (map dest_Free args,
- HOLogic.choice_const T
- $ quasi_beta_eta_contract body)
+ HOLogic.choice_const T $ beta_eta_under_lambdas body)
|> mk_skolem_id
- val def = Logic.mk_equals (c, rhs)
val comb = list_comb (rhs, args)
- in dec_sko (subst_bound (comb, p)) (def :: defs) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
+ in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko _ defs = defs
+ in dec_sko (subst_bound (Free(fname,T), p)) rhss end
+ | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
+ | dec_sko _ rhss = rhss
in dec_sko (prop_of th) [] end;
@@ -304,9 +181,6 @@
(*cterms are used throughout for efficiency*)
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
-(*cterm version of mk_cTrueprop*)
-fun c_mkTrueprop A = Thm.capply cTrueprop A;
-
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
fun c_variant_abs_multi (ct0, vars) =
@@ -314,38 +188,39 @@
in c_variant_abs_multi (ct, cv::vars) end
handle CTERM _ => (ct0, rev vars);
-(*Given the definition of a Skolem function, return a theorem to replace
- an existential formula by a use of that function.
+val skolem_id_def_raw = @{thms skolem_id_def_raw}
+
+(* Given the definition of a Skolem function, return a theorem to replace
+ an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def inline def =
+fun skolem_theorem_of_def thy cheat rhs0 =
let
- val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of
- |> Thm.dest_equals
- val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
- val (ch, frees) = c_variant_abs_multi (rhs', [])
- val (chilbert, cabs) = ch |> Thm.dest_comb
- val thy = Thm.theory_of_cterm chilbert
- val t = Thm.term_of chilbert
- val T =
- case t of
- Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
- val cex = Thm.cterm_of thy (HOLogic.exists_const T)
- val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
- and conc =
- Drule.list_comb (if inline then rhs else c, frees)
- |> Drule.beta_conv cabs |> c_mkTrueprop
- fun tacf [prem] =
- (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
- else rewrite_goals_tac [def])
- THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
+ val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
+ val rhs' = rhs |> Thm.dest_comb |> snd
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
+ val T =
+ case hilbert of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
+ val cex = Thm.cterm_of thy (HOLogic.exists_const T)
+ val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
+ val conc =
+ Drule.list_comb (rhs, frees)
+ |> Drule.beta_conv cabs |> Thm.capply cTrueprop
+ fun tacf [prem] =
+ if cheat then
+ Skip_Proof.cheat_tac thy
+ else
+ rewrite_goals_tac skolem_id_def_raw
+ THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
RS @{thm someI_ex}) 1
- in Goal.prove_internal [ex_tm] conc tacf
- |> forall_intr_list frees
- |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT_global
- end;
-
+ in
+ Goal.prove_internal [ex_tm] conc tacf
+ |> forall_intr_list frees
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.varifyT_global
+ end
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
fun to_nnf th ctxt0 =
@@ -356,192 +231,44 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end;
-(*Generate Skolem functions for a theorem supplied in nnf*)
-fun skolem_theorems_of_assume s th =
- map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th))
- (assume_skolem_funs s th)
-
-
-(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
-
-val max_lambda_nesting = 3
-
-fun term_has_too_many_lambdas max (t1 $ t2) =
- exists (term_has_too_many_lambdas max) [t1, t2]
- | term_has_too_many_lambdas max (Abs (_, _, t)) =
- max = 0 orelse term_has_too_many_lambdas (max - 1) t
- | term_has_too_many_lambdas _ _ = false
-
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
-(* Don't count nested lambdas at the level of formulas, since they are
- quantifiers. *)
-fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
- formula_has_too_many_lambdas (T :: Ts) t
- | formula_has_too_many_lambdas Ts t =
- if is_formula_type (fastype_of1 (Ts, t)) then
- exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
- else
- term_has_too_many_lambdas max_lambda_nesting t
-
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
- was 11. *)
-val max_apply_depth = 15
-
-fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
- | apply_depth (Abs (_, _, t)) = apply_depth t
- | apply_depth _ = 0
-
-fun is_formula_too_complex t =
- apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
- formula_has_too_many_lambdas [] t
-
-fun is_strange_thm th =
- case head_of (concl_of th) of
- Const (a, _) => (a <> @{const_name Trueprop} andalso
- a <> @{const_name "=="})
- | _ => false;
-
-fun is_theorem_bad_for_atps thm =
- let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_topsort t orelse
- is_strange_thm thm
+(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+fun skolemize_theorem thy cheat th =
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val (nnfth, ctxt) = to_nnf th ctxt0
+ val sko_ths = map (skolem_theorem_of_def thy cheat)
+ (assume_skolem_funs nnfth)
+ val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+ in
+ cnfs |> map introduce_combinators
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
end
-
-(* FIXME: put other record thms here, or declare as "no_atp" *)
-val multi_base_blacklist =
- ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases"];
-
-fun fake_name th =
- if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
- else gensym "unknown_thm_";
-
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolemize_theorem s th =
- if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
- is_theorem_bad_for_atps th then
- []
- else
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val defs = skolem_theorems_of_assume s nnfth
- val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
- in
- cnfs |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- end
- handle THM _ => []
-
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
- Skolem functions.*)
-structure ThmCache = Theory_Data
-(
- type T = thm list Thmtab.table * unit Symtab.table;
- val empty = (Thmtab.empty, Symtab.empty);
- val extend = I;
- fun merge ((cache1, seen1), (cache2, seen2)) : T =
- (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
-);
-
-val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
-val already_seen = Symtab.defined o #2 o ThmCache.get;
-
-val update_cache = ThmCache.map o apfst o Thmtab.update;
-fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
+ handle THM _ => []
(* Convert Isabelle theorems into axiom clauses. *)
-fun cnf_axiom thy th0 =
- let val th = Thm.transfer thy th0 in
- case lookup_cache thy th of
- SOME cls => cls
- | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
- end;
+(* FIXME: is transfer necessary? *)
+fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
(**** Translate a set of theorems into CNF ****)
(*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy =
+fun cnf_rules_pairs thy cheat =
let
fun do_one _ [] = []
| do_one ((name, k), th) (cls :: clss) =
- (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+ ((name, k), cls) :: do_one ((name, k + 1), th) clss
fun do_all pairs [] = pairs
| do_all pairs ((name, th) :: ths) =
let
- val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
+ val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
handle THM _ => []
in do_all (new_pairs @ pairs) ths end
in do_all [] o rev end
-(**** Convert all facts of the theory into FOL or HOL clauses ****)
-
-local
-
-fun skolem_def (name, th) thy =
- let val ctxt0 = Variable.global_thm_context th in
- case try (to_nnf th) ctxt0 of
- NONE => (NONE, thy)
- | SOME (nnfth, ctxt) =>
- let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
- in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
- end;
-
-fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
- let
- val (cnfs, ctxt) =
- Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
- val cnfs' = cnfs
- |> map introduce_combinators
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation;
- in (th, cnfs') end;
-
-in
-
-fun saturate_cache thy =
- let
- val facts = PureThy.facts_of thy;
- val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
- if Facts.is_concealed facts name orelse already_seen thy name then I
- else cons (name, ths));
- val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (Long_Name.base_name name) then
- I
- else
- fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse
- is_some (lookup_cache thy th) then
- I
- else
- cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
- in
- if null new_facts then
- NONE
- else
- let
- val (defs, thy') = thy
- |> fold (mark_seen o #1) new_facts
- |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
- |>> map_filter I;
- val cache_entries = Par_List.map skolem_cnfs defs;
- in SOME (fold update_cache cache_entries thy') end
- end;
-
-end;
-
-(* For emergency use where the Skolem cache causes problems. *)
-val auto_saturate_cache = Unsynchronized.ref true
-
-fun conditionally_saturate_cache thy =
- if !auto_saturate_cache then saturate_cache thy else NONE
-
-
(*** Converting a subgoal into negated conjecture clauses. ***)
fun neg_skolemize_tac ctxt =
@@ -562,10 +289,4 @@
in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-(** setup **)
-
-val setup =
- perhaps conditionally_saturate_cache
- #> Theory.at_end conditionally_saturate_cache
-
end;
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 29 11:38:51 2010 +0200
@@ -1,12 +1,12 @@
(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
MESON general tactic and proof method.
*)
signature MESON_TACTIC =
sig
- val expand_defs_tac : thm -> tactic
val meson_general_tac : Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -14,37 +14,11 @@
structure Meson_Tactic : MESON_TACTIC =
struct
-(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
- String.isPrefix Clausifier.skolem_prefix a
- | is_absko _ = false;
-
-fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*)
- is_Free t andalso not (member (op aconv) xs t)
- | is_okdef _ _ = false
-
-(*This function tries to cope with open locales, which introduce hypotheses of the form
- Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
- of sko_ functions. *)
-fun expand_defs_tac st0 st =
- let val hyps0 = #hyps (rep_thm st0)
- val hyps = #hyps (crep_thm st)
- val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
- val defs = filter (is_absko o Thm.term_of) newhyps
- val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
- (map Thm.term_of hyps)
- val fixed = OldTerm.term_frees (concl_of st) @
- fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
- in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
-
-fun meson_general_tac ctxt ths i st0 =
+fun meson_general_tac ctxt ths =
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in
- (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
- THEN expand_defs_tac st0) st0
- end
+ in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 11:38:51 2010 +0200
@@ -8,9 +8,7 @@
signature METIS_CLAUSES =
sig
- type cnf_thm = Clausifier.cnf_thm
type name = string * string
- type name_pool = string Symtab.table * string Symtab.table
datatype kind = Axiom | Conjecture
datatype type_literal =
TyLitVar of string * name |
@@ -34,7 +32,6 @@
datatype hol_clause =
HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
literals: literal list, ctypes_sorts: typ list}
- exception TRIVIAL of unit
val type_wrapper_name : string
val schematic_var_prefix: string
@@ -56,27 +53,23 @@
val make_fixed_const : string -> string
val make_fixed_type_const : string -> string
val make_type_class : string -> string
- val empty_name_pool : bool -> name_pool option
- val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
- val nice_name : name -> name_pool option -> string * name_pool option
+ val skolem_theory_name: string
+ val skolem_prefix: string
+ val skolem_infix: string
+ val is_skolem_const_name: string -> bool
+ val num_type_args: theory -> string -> int
val type_literals_for_types : typ list -> type_literal list
val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
val type_of_combterm : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
- val conceal_skolem_somes :
+ val conceal_skolem_terms :
int -> (string * term) list -> term -> (string * term) list * term
- val is_quasi_fol_theorem : theory -> thm -> bool
- val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
+ val reveal_skolem_terms : (string * term) list -> term -> term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val prepare_clauses :
- bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
- -> string vector
- * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
- * classrel_clause list * arity_clause list)
end
structure Metis_Clauses : METIS_CLAUSES =
@@ -206,70 +199,31 @@
fun make_type_class clas = class_prefix ^ ascii_of clas;
-
-(**** name pool ****)
-
-type name = string * string
-type name_pool = string Symtab.table * string Symtab.table
-
-fun empty_name_pool readable_names =
- if readable_names then SOME (`I Symtab.empty) else NONE
-
-fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val skolem_prefix = "sko_"
+val skolem_infix = "$"
-fun add_nice_name full_name nice_prefix j the_pool =
- let
- val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
- in
- case Symtab.lookup (snd the_pool) nice_name of
- SOME full_name' =>
- if full_name = full_name' then (nice_name, the_pool)
- else add_nice_name full_name nice_prefix (j + 1) the_pool
- | NONE =>
- (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
- Symtab.update_new (nice_name, full_name) (snd the_pool)))
- end
-
-fun translate_first_char f s =
- String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-fun readable_name full_name s =
- let
- val s = s |> Long_Name.base_name |> Name.desymbolize false
- val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
- val s' =
- (s' |> rev
- |> implode
- |> String.translate
- (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
- else ""))
- ^ replicate_string (String.size s - length s') "_"
- val s' =
- if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
- else s'
- (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
- ("op &", "op |", etc.). *)
- val s' = if s' = "equal" orelse s' = "op" then full_name else s'
- in
- case (Char.isLower (String.sub (full_name, 0)),
- Char.isLower (String.sub (s', 0))) of
- (true, false) => translate_first_char Char.toLower s'
- | (false, true) => translate_first_char Char.toUpper s'
- | _ => s'
- end
-
-fun nice_name (full_name, _) NONE = (full_name, NONE)
- | nice_name (full_name, desired_name) (SOME the_pool) =
- case Symtab.lookup (fst the_pool) full_name of
- SOME nice_name => (nice_name, SOME the_pool)
- | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
- the_pool
- |> apsnd SOME
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
(**** Definitions and functions for FOL clauses for TPTP format output ****)
+type name = string * string
+
datatype kind = Axiom | Conjecture
(**** Isabelle FOL clauses ****)
@@ -426,17 +380,6 @@
| stripc x = x
in stripc(u,[]) end
-fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
- | isFalse _ = false;
-
-fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_True") orelse
- (not pol andalso c = "c_False")
- | isTrue _ = false;
-
-fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
-
fun type_of (Type (a, Ts)) =
let val (folTypes,ts) = types_of Ts in
(TyConstr (`make_fixed_type_const a, folTypes), ts)
@@ -480,7 +423,7 @@
let val (P', tsP) = combterm_of thy P
val (Q', tsQ) = combterm_of thy Q
in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
+ | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs"
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
@@ -499,120 +442,46 @@
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
skolem_infix ^ "g"
-fun conceal_skolem_somes i skolem_somes t =
+fun conceal_skolem_terms i skolems t =
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
let
- fun aux skolem_somes
+ fun aux skolems
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
let
- val (skolem_somes, s) =
+ val (skolems, s) =
if i = ~1 then
- (skolem_somes, @{const_name undefined})
- else case AList.find (op aconv) skolem_somes t of
- s :: _ => (skolem_somes, s)
+ (skolems, @{const_name undefined})
+ else case AList.find (op aconv) skolems t of
+ s :: _ => (skolems, s)
| [] =>
let
val s = skolem_theory_name ^ "." ^
- skolem_name i (length skolem_somes)
+ skolem_name i (length skolems)
(length (Term.add_tvarsT T []))
- in ((s, t) :: skolem_somes, s) end
- in (skolem_somes, Const (s, T)) end
- | aux skolem_somes (t1 $ t2) =
+ in ((s, t) :: skolems, s) end
+ in (skolems, Const (s, T)) end
+ | aux skolems (t1 $ t2) =
let
- val (skolem_somes, t1) = aux skolem_somes t1
- val (skolem_somes, t2) = aux skolem_somes t2
- in (skolem_somes, t1 $ t2) end
- | aux skolem_somes (Abs (s, T, t')) =
- let val (skolem_somes, t') = aux skolem_somes t' in
- (skolem_somes, Abs (s, T, t'))
+ val (skolems, t1) = aux skolems t1
+ val (skolems, t2) = aux skolems t2
+ in (skolems, t1 $ t2) end
+ | aux skolems (Abs (s, T, t')) =
+ let val (skolems, t') = aux skolems t' in
+ (skolems, Abs (s, T, t'))
end
- | aux skolem_somes t = (skolem_somes, t)
- in aux skolem_somes t end
+ | aux skolems t = (skolems, t)
+ in aux skolems t end
else
- (skolem_somes, t)
-
-fun is_quasi_fol_theorem thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
-
-(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL of unit
-
-(* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
- let
- val (skolem_somes, t) =
- th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
- val (lits, ctypes_sorts) = literals_of_term thy t
- in
- if forall isFalse lits then
- raise TRIVIAL ()
- else
- (skolem_somes,
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
- end
-
-fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
- let
- val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
- in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
-
-fun make_axiom_clauses thy clauses =
- ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
+ (skolems, t)
-fun make_conjecture_clauses thy =
- let
- fun aux _ _ [] = []
- | aux n skolem_somes (th :: ths) =
- let
- val (skolem_somes, cls) =
- make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
- in cls :: aux (n + 1) skolem_somes ths end
- in aux 0 [] end
-
-(** Helper clauses **)
-
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-
-fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
-
-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}))]
-val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
-
-val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
-
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
- let
- val axclauses = map snd (make_axiom_clauses thy axcls)
- val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- 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)
- in map snd (make_axiom_clauses thy cnfs) end
-
-fun make_clause_table xs =
- fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
+fun reveal_skolem_terms skolems =
+ map_aterms (fn t as Const (s, _) =>
+ if String.isPrefix skolem_theory_name s then
+ AList.lookup (op =) skolems s |> the
+ |> map_types Type_Infer.paramify_vars
+ else
+ t
+ | t => t)
(***************************************************************)
@@ -652,34 +521,4 @@
fun type_consts_of_terms thy ts =
Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
-(* Remove existing axiom clauses from the conjecture clauses, as this can
- dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
- filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
-
-(* prepare for passing to writer,
- create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types goal_cls axcls extra_cls thy =
- let
- val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
- val ccls = subtract_cls extra_cls goal_cls
- val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
- val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) extra_cls
- val subs = tfree_classes_of_terms ccltms
- and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms @ axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = make_conjecture_clauses thy ccls
- 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 =
- get_helper_clauses thy is_FO full_types conjectures extra_cls
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val classrel_clauses = make_classrel_clauses thy subs supers'
- in
- (Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
- end
-
end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 11:38:51 2010 +0200
@@ -135,16 +135,16 @@
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
+fun hol_thm_to_fol is_conjecture ctxt mode j skolems th =
let
val thy = ProofContext.theory_of ctxt
- val (skolem_somes, (mlits, types_sorts)) =
- th |> prop_of |> conceal_skolem_somes j skolem_somes
+ val (skolems, (mlits, types_sorts)) =
+ th |> prop_of |> conceal_skolem_terms j skolems
||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, skolem_somes)
+ type_literals_for_types types_sorts, skolems)
else
let val tylits = filter_out (default_sort ctxt) types_sorts
|> type_literals_for_types
@@ -152,7 +152,7 @@
then map (metis_of_type_literals false) tylits else []
in
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
- skolem_somes)
+ skolems)
end
end;
@@ -235,15 +235,6 @@
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("fol_type_to_isa: " ^ x));
-fun reveal_skolem_somes skolem_somes =
- map_aterms (fn t as Const (s, _) =>
- if String.isPrefix skolem_theory_name s then
- AList.lookup (op =) skolem_somes s
- |> the |> map_types Type_Infer.paramify_vars
- else
- t
- | t => t)
-
(*Maps metis terms to isabelle terms*)
fun hol_term_from_fol_PT ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
@@ -345,11 +336,11 @@
fun hol_term_from_fol FT = hol_term_from_fol_FT
| hol_term_from_fol _ = hol_term_from_fol_PT
-fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
+fun hol_terms_from_fol ctxt mode skolems fol_tms =
let val ts = map (hol_term_from_fol mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
+ val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -391,22 +382,22 @@
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
-fun assume_inf ctxt mode skolem_somes atm =
+fun assume_inf ctxt mode skolems atm =
inst_excluded_middle
- (ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
+ (ProofContext.theory_of ctxt)
+ (singleton (hol_terms_from_fol ctxt mode skolems) (Metis.Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
that new TVars are distinct and that types can be inferred from terms.*)
-fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
+fun inst_inf ctxt mode skolems thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_skolem_somes" and "infer_types" below. *)
+ (* We call "reveal_skolem_terms" and "infer_types" below. *)
val t = hol_term_from_fol mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
@@ -422,8 +413,7 @@
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
- |> infer_types ctxt
+ val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg (fn () =>
@@ -451,7 +441,7 @@
end
handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
-fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
let
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
@@ -461,7 +451,7 @@
else if is_TrueI i_th2 then i_th1
else
let
- val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
(Metis.Term.Fn atm)
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -479,9 +469,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode skolem_somes t =
+fun refl_inf ctxt mode skolems t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -491,10 +481,10 @@
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
+fun equality_inf ctxt mode skolems (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis.Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -568,27 +558,27 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode skolem_somes thpairs p =
+fun step ctxt mode skolems thpairs p =
case p of
(fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
+ | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
| (_, Metis.Proof.Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
| (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
- | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
+ factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
+ | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
| (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode skolem_somes f_lit f_p f_r
+ equality_inf ctxt mode skolems f_lit f_p f_r
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
(* FIXME: use "fold" instead *)
fun translate _ _ _ thpairs [] = thpairs
- | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
+ | translate ctxt mode skolems thpairs ((fol_th, inf) :: infpairs) =
let val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
+ val th = Meson.flexflex_first_order (step ctxt mode skolems
thpairs (fol_th, inf))
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
@@ -597,7 +587,7 @@
in
if nprems_of th = n_metis_lits then ()
else raise METIS ("translate", "Proof reconstruction has gone wrong.");
- translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
+ translate ctxt mode skolems ((fol_th, th) :: thpairs) infpairs
end;
(*Determining which axiom clauses are actually used*)
@@ -609,7 +599,7 @@
(* ------------------------------------------------------------------------- *)
fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (cnf_axiom thy th)
+ if raw then th else the_single (cnf_axiom thy false th)
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
@@ -627,7 +617,7 @@
type logic_map =
{axioms: (Metis.Thm.thm * thm) list,
tfrees: type_literal list,
- skolem_somes: (string * term) list}
+ skolems: (string * term) list}
fun const_in_metis c (pred, tm_list) =
let
@@ -645,15 +635,15 @@
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
- skolem_somes = skolem_somes}
+ skolems = skolems}
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
+fun add_tfrees {axioms, tfrees, skolems} : logic_map =
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
axioms,
- tfrees = tfrees, skolem_somes = skolem_somes}
+ tfrees = tfrees, skolems = skolems}
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
@@ -670,27 +660,28 @@
("c_False", (true, @{thms True_or_False})),
("c_If", (true, @{thms if_True if_False True_or_False}))]
+fun is_quasi_fol_clause thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
+
(* Function to generate metis clauses, including comb and type clauses *)
fun build_map mode0 ctxt cls ths =
let val thy = ProofContext.theory_of ctxt
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
+ if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
+ fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
let
- val (mth, tfree_lits, skolem_somes) =
- hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
- ith
+ val (mth, tfree_lits, skolems) =
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees,
- skolem_somes = skolem_somes}
+ tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
end;
- val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
|> fold (add_thm true) cls
|> add_tfrees
|> fold (add_thm false) ths
@@ -724,13 +715,13 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
+ map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
+ val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
app (fn TyLitFree (s, (s', _)) =>
@@ -751,7 +742,7 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
- val result = translate ctxt' mode skolem_somes axioms proof
+ val result = translate ctxt' mode skolems axioms proof
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
@@ -779,17 +770,19 @@
raise METIS ("FOL_SOLVE", ""))
end;
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
fun generic_metis_tac mode ctxt ths i st0 =
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type type_has_topsort (prop_of st0) then
+ if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
(Meson.MESON (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt i
- THEN Meson_Tactic.expand_defs_tac st0) st0
+ ctxt i) st0
handle ERROR msg => raise METIS ("generic_metis_tac", msg)
end
handle METIS (loc, msg) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 29 11:38:51 2010 +0200
@@ -5,34 +5,46 @@
signature SLEDGEHAMMER_FACT_FILTER =
sig
- type cnf_thm = Clausifier.cnf_thm
-
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
only: bool}
- val use_natural_form : bool Unsynchronized.ref
+ val trace : bool Unsynchronized.ref
+ val chained_prefix : string
+ val name_thms_pair_from_ref :
+ Proof.context -> thm list -> Facts.ref -> string * thm list
val relevant_facts :
bool -> real -> real -> bool -> int -> bool -> relevance_override
- -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
+ -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
-open Clausifier
-open Metis_Clauses
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
val respect_no_atp = true
-(* Experimental feature: Filter theorems in natural form or in CNF? *)
-val use_natural_form = Unsynchronized.ref false
type relevance_override =
{add: Facts.ref list,
del: Facts.ref list,
only: bool}
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+(* Used to label theorems chained into the goal. *)
+val chained_prefix = sledgehammer_prefix ^ "chained_"
+
+fun name_thms_pair_from_ref ctxt chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix
+ in (name, ths) end
+
+
(***************************************************************)
(* Relevance Filtering *)
(***************************************************************)
@@ -137,17 +149,13 @@
| _ => do_term t
in
Symtab.empty
- |> (if !use_natural_form then
- fold (Symtab.update o rpair []) boring_natural_consts
- #> fold (do_formula pos) ts
- else
- fold (Symtab.update o rpair []) boring_cnf_consts
- #> fold do_term ts)
+ |> fold (Symtab.update o rpair []) boring_natural_consts
+ |> fold (do_formula pos) ts
end
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun const_prop_of theory_relevant th =
+fun theory_const_prop_of theory_relevant th =
if theory_relevant then
let
val name = Context.theory_name (theory_of_thm th)
@@ -156,10 +164,6 @@
else
prop_of th
-fun appropriate_prop_of theory_relevant (cnf_thm, (_, orig_thm)) =
- (if !use_natural_form then orig_thm else cnf_thm)
- |> const_prop_of theory_relevant
-
(**** Constant / Type Frequencies ****)
(*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
@@ -183,7 +187,7 @@
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts theory_relevant thy axiom =
+fun count_axiom_consts theory_relevant thy (_, th) =
let
fun do_const (a, T) =
let val (c, cts) = const_with_typ thy (a,T) in
@@ -198,7 +202,7 @@
| do_term (t $ u) = do_term t #> do_term u
| do_term (Abs (_, _, t)) = do_term t
| do_term _ = I
- in axiom |> appropriate_prop_of theory_relevant |> do_term end
+ in th |> theory_const_prop_of theory_relevant |> do_term end
(**** Actual Filtering Code ****)
@@ -239,7 +243,7 @@
Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
- (axiom, axiom |> appropriate_prop_of theory_relevant
+ (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
|> consts_typs_of_term thy)
exception CONST_OR_FREE of unit
@@ -266,7 +270,7 @@
| _ => false
end;
-type annotated_cnf_thm = cnf_thm * ((string * const_typ list) list)
+type annotated_cnf_thm = (string * thm) * (string * const_typ list) list
(*For a reverse sort, putting the largest values first.*)
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
@@ -284,7 +288,7 @@
", exceeds the limit of " ^ Int.toString (max_new)));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
- space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted));
+ space_implode ", " (map (fst o fst o fst) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
end
@@ -314,20 +318,17 @@
(more_rejects @ rejects)
end
| relevant (newrels, rejects)
- ((ax as (clsthm as (_, ((name, n), orig_th)),
- consts_typs)) :: axs) =
+ ((ax as (clsthm as (name, th), consts_typs)) :: axs) =
let
val weight =
- if member Thm.eq_thm add_thms orig_th then 1.0
- else if member Thm.eq_thm del_thms orig_th then 0.0
+ if member Thm.eq_thm add_thms th then 1.0
+ else if member Thm.eq_thm del_thms th then 0.0
else clause_weight const_tab rel_const_tab consts_typs
in
if weight >= threshold orelse
- (defs_relevant andalso
- defines thy (#1 clsthm) rel_const_tab) then
+ (defs_relevant andalso defines thy th rel_const_tab) then
(trace_msg (fn () =>
- name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight
+ name ^ " passes: " ^ Real.toString weight
(* ^ " consts: " ^ commas (map fst consts_typs) *));
relevant ((ax, weight) :: newrels, rejects) axs)
else
@@ -342,7 +343,7 @@
fun relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
- thy (axioms : cnf_thm list) goals =
+ thy axioms goals =
if relevance_threshold > 1.0 then
[]
else if relevance_threshold < 0.0 then
@@ -352,9 +353,7 @@
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
val goal_const_tab = get_consts_typs thy (SOME true) goals
- val relevance_threshold =
- if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
- else relevance_threshold
+ val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
val _ =
trace_msg (fn () => "Initial constants: " ^
commas (goal_const_tab
@@ -388,10 +387,66 @@
String.isSuffix "_def" a orelse String.isSuffix "_defs" a
end;
-fun make_unique xs = Termtab.fold (cons o snd) (make_clause_table xs) []
+fun make_clause_table xs =
+ fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
+
+fun make_unique xs =
+ Termtab.fold (cons o snd) (make_clause_table xs) []
+
+(* FIXME: put other record thms here, or declare as "no_atp" *)
+val multi_base_blacklist =
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"]
+
+val max_lambda_nesting = 3
+
+fun term_has_too_many_lambdas max (t1 $ t2) =
+ exists (term_has_too_many_lambdas max) [t1, t2]
+ | term_has_too_many_lambdas max (Abs (_, _, t)) =
+ max = 0 orelse term_has_too_many_lambdas (max - 1) t
+ | term_has_too_many_lambdas _ _ = false
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
+(* Don't count nested lambdas at the level of formulas, since they are
+ quantifiers. *)
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+ formula_has_too_many_lambdas (T :: Ts) t
+ | formula_has_too_many_lambdas Ts t =
+ if is_formula_type (fastype_of1 (Ts, t)) then
+ exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
+ else
+ term_has_too_many_lambdas max_lambda_nesting t
+
+(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+ was 11. *)
+val max_apply_depth = 15
+
+fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
+ | apply_depth (Abs (_, _, t)) = apply_depth t
+ | apply_depth _ = 0
+
+fun is_formula_too_complex t =
+ apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
+ formula_has_too_many_lambdas [] t
val exists_sledgehammer_const =
- exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+ exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+
+fun is_strange_thm th =
+ case head_of (concl_of th) of
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
+ | _ => false
+
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
+fun is_theorem_bad_for_atps thm =
+ let val t = prop_of thm in
+ is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
+ exists_sledgehammer_const t orelse is_strange_thm thm
+ end
fun all_name_thms_pairs ctxt chained_ths =
let
@@ -415,8 +470,7 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out (is_theorem_bad_for_atps orf
- exists_sledgehammer_const) ths0
+ val ths = filter_out is_theorem_bad_for_atps ths0
in
case find_first check_thms [name1, name2, name] of
NONE => I
@@ -519,18 +573,17 @@
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
(map (name_thms_pair_from_ref ctxt chained_ths) add @
(if only then [] else all_name_thms_pairs ctxt chained_ths))
- |> cnf_rules_pairs thy
|> not has_override ? make_unique
- |> filter (fn (cnf_thm, (_, orig_thm)) =>
- member Thm.eq_thm add_thms orig_thm orelse
- ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso
- not (is_dangerous_term full_types (prop_of cnf_thm))))
+ |> filter (fn (_, th) =>
+ member Thm.eq_thm add_thms th orelse
+ ((* ### FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
+ not (is_dangerous_term full_types (prop_of th))))
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
thy axioms (map prop_of goal_cls)
|> has_override ? make_unique
- |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
+ |> sort_wrt fst
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 29 11:38:51 2010 +0200
@@ -51,11 +51,12 @@
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
filtered_clauses name_thms_pairs =
let
+ val thy = Proof.theory_of state
val num_theorems = length name_thms_pairs
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 = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val axclauses = cnf_rules_pairs thy true name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 29 11:38:51 2010 +0200
@@ -19,6 +19,7 @@
open Clausifier
open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
open ATP_Manager
open ATP_Systems
open Sledgehammer_Fact_Minimizer
@@ -193,8 +194,7 @@
(* Sledgehammer the given subgoal *)
fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | run (params as {atps, timeout, ...}) i relevance_override minimize_command
- state =
+ | run (params as {atps, ...}) i relevance_override minimize_command state =
case subgoal_count state of
0 => priority "No subgoal!"
| n =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 11:38:51 2010 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Metis_Clauses.name_pool
+ type name_pool = Sledgehammer_TPTP_Format.name_pool
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
@@ -30,6 +30,8 @@
open Clausifier
open Metis_Clauses
open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
type minimize_command = string list -> string
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 11:25:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jun 29 11:38:51 2010 +0200
@@ -7,14 +7,11 @@
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
- type name_pool = Metis_Clauses.name_pool
- type type_literal = Metis_Clauses.type_literal
type classrel_clause = Metis_Clauses.classrel_clause
type arity_clause = Metis_Clauses.arity_clause
type hol_clause = Metis_Clauses.hol_clause
+ type name_pool = string Symtab.table * string Symtab.table
- val tptp_of_type_literal :
- bool -> type_literal -> name_pool option -> string * name_pool option
val write_tptp_file :
bool -> bool -> bool -> Path.T
-> hol_clause list * hol_clause list * hol_clause list * hol_clause list
@@ -28,6 +25,65 @@
open Metis_Clauses
open Sledgehammer_Util
+type name_pool = string Symtab.table * string Symtab.table
+
+fun empty_name_pool readable_names =
+ if readable_names then SOME (`I Symtab.empty) else NONE
+
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
+fun pool_map f xs =
+ pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+
+fun translate_first_char f s =
+ String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+fun readable_name full_name s =
+ let
+ val s = s |> Long_Name.base_name |> Name.desymbolize false
+ val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
+ val s' =
+ (s' |> rev
+ |> implode
+ |> String.translate
+ (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c
+ else ""))
+ ^ replicate_string (String.size s - length s') "_"
+ val s' =
+ if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
+ else s'
+ (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
+ ("op &", "op |", etc.). *)
+ val s' = if s' = "equal" orelse s' = "op" then full_name else s'
+ in
+ case (Char.isLower (String.sub (full_name, 0)),
+ Char.isLower (String.sub (s', 0))) of
+ (true, false) => translate_first_char Char.toLower s'
+ | (false, true) => translate_first_char Char.toUpper s'
+ | _ => s'
+ end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+ | nice_name (full_name, desired_name) (SOME the_pool) =
+ case Symtab.lookup (fst the_pool) full_name of
+ SOME nice_name => (nice_name, SOME the_pool)
+ | NONE =>
+ let
+ val nice_prefix = readable_name full_name desired_name
+ fun add j =
+ let
+ val nice_name = nice_prefix ^
+ (if j = 0 then "" else "_" ^ Int.toString j)
+ in
+ case Symtab.lookup (snd the_pool) nice_name of
+ SOME full_name' =>
+ if full_name = full_name' then (nice_name, the_pool)
+ else add (j + 1)
+ | NONE =>
+ (nice_name,
+ (Symtab.update_new (full_name, nice_name) (fst the_pool),
+ Symtab.update_new (nice_name, full_name) (snd the_pool)))
+ end
+ in add 0 |> apsnd SOME end
+
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
val clause_prefix = "cls_"
@@ -190,25 +246,24 @@
(* Find the minimal arity of each function mentioned in the term. Also, note
which uses are not at top level, to see if "hBOOL" is needed. *)
-fun count_constants_term top_level t the_const_tab =
- let
- val (head, args) = strip_combterm_comb t
- val n = length args
- val the_const_tab = the_const_tab |> fold (count_constants_term false) args
- in
- case head of
- CombConst ((a, _), _, ty) =>
- (* Predicate or function version of "equal"? *)
- let val a = if a = "equal" andalso not top_level then "c_fequal" else a in
- the_const_tab
- |> Symtab.map_default
- (a, {min_arity = n, max_arity = n, sub_level = false})
- (fn {min_arity, max_arity, sub_level} =>
- {min_arity = Int.min (n, min_arity),
- max_arity = Int.max (n, max_arity),
- sub_level = sub_level orelse not top_level})
- end
- | _ => the_const_tab
+fun count_constants_term top_level t =
+ let val (head, args) = strip_combterm_comb t in
+ (case head of
+ CombConst ((a, _), _, _) =>
+ let
+ (* Predicate or function version of "equal"? *)
+ val a = if a = "equal" andalso not top_level then "c_fequal" else a
+ val n = length args
+ in
+ Symtab.map_default
+ (a, {min_arity = n, max_arity = 0, sub_level = false})
+ (fn {min_arity, max_arity, sub_level} =>
+ {min_arity = Int.min (n, min_arity),
+ max_arity = Int.max (n, max_arity),
+ sub_level = sub_level orelse not top_level})
+ end
+ | _ => I)
+ #> fold (count_constants_term false) args
end
fun count_constants_literal (Literal (_, t)) = count_constants_term true t
fun count_constants_clause (HOLClause {literals, ...}) =