1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Jun 06 18:47:29 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 07 10:37:30 2010 +0200
1.3 @@ -239,14 +239,14 @@
1.4 fun generic_tptp_prover
1.5 (name, {home_var, executable, arguments, proof_delims, known_failures,
1.6 max_axiom_clauses, prefers_theory_relevant})
1.7 - (params as {debug, overlord, respect_no_atp, relevance_threshold,
1.8 - relevance_convergence, theory_relevant, defs_relevant,
1.9 - isar_proof, ...})
1.10 + (params as {debug, overlord, full_types, respect_no_atp,
1.11 + relevance_threshold, relevance_convergence, theory_relevant,
1.12 + defs_relevant, isar_proof, ...})
1.13 minimize_command timeout =
1.14 generic_prover overlord
1.15 - (get_relevant_facts respect_no_atp relevance_threshold
1.16 - relevance_convergence defs_relevant max_axiom_clauses
1.17 - (the_default prefers_theory_relevant theory_relevant))
1.18 + (relevant_facts full_types respect_no_atp relevance_threshold
1.19 + relevance_convergence defs_relevant max_axiom_clauses
1.20 + (the_default prefers_theory_relevant theory_relevant))
1.21 (prepare_clauses false)
1.22 (write_tptp_file (debug andalso overlord)) home_var
1.23 executable (arguments timeout) proof_delims known_failures name params
1.24 @@ -276,7 +276,7 @@
1.25 known_failures =
1.26 [(Unprovable, "Satisfiability detected"),
1.27 (Unprovable, "UNPROVABLE"),
1.28 - (OutOfResources, "CANNOT PROVE"),
1.29 + (Unprovable, "CANNOT PROVE"),
1.30 (OutOfResources, "Refutation not found")],
1.31 max_axiom_clauses = 60,
1.32 prefers_theory_relevant = false}
1.33 @@ -314,13 +314,13 @@
1.34 fun generic_dfg_prover
1.35 (name, {home_var, executable, arguments, proof_delims, known_failures,
1.36 max_axiom_clauses, prefers_theory_relevant})
1.37 - (params as {overlord, respect_no_atp, relevance_threshold,
1.38 + (params as {overlord, full_types, respect_no_atp, relevance_threshold,
1.39 relevance_convergence, theory_relevant, defs_relevant, ...})
1.40 minimize_command timeout =
1.41 generic_prover overlord
1.42 - (get_relevant_facts respect_no_atp relevance_threshold
1.43 - relevance_convergence defs_relevant max_axiom_clauses
1.44 - (the_default prefers_theory_relevant theory_relevant))
1.45 + (relevant_facts full_types respect_no_atp relevance_threshold
1.46 + relevance_convergence defs_relevant max_axiom_clauses
1.47 + (the_default prefers_theory_relevant theory_relevant))
1.48 (prepare_clauses true) write_dfg_file home_var executable
1.49 (arguments timeout) proof_delims known_failures name params
1.50 minimize_command
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Jun 06 18:47:29 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 07 10:37:30 2010 +0200
2.3 @@ -16,11 +16,13 @@
2.4 del: Facts.ref list,
2.5 only: bool}
2.6
2.7 + val name_thms_pair_from_ref :
2.8 + Proof.context -> thm list -> Facts.ref -> string * thm list
2.9 val tvar_classes_of_terms : term list -> string list
2.10 val tfree_classes_of_terms : term list -> string list
2.11 val type_consts_of_terms : theory -> term list -> string list
2.12 - val get_relevant_facts :
2.13 - bool -> real -> real -> bool -> int -> bool -> relevance_override
2.14 + val relevant_facts :
2.15 + bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
2.16 -> Proof.context * (thm list * 'a) -> thm list
2.17 -> (thm * (string * int)) list
2.18 val prepare_clauses :
2.19 @@ -253,36 +255,41 @@
2.20 end
2.21 end;
2.22
2.23 +fun cnf_for_facts ctxt =
2.24 + let val thy = ProofContext.theory_of ctxt in
2.25 + maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
2.26 + end
2.27 +
2.28 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
2.29 - (relevance_override as {add, del, only}) thy ctab =
2.30 + (relevance_override as {add, del, ...}) ctab =
2.31 let
2.32 - val thms_for_facts =
2.33 - maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
2.34 - val add_thms = thms_for_facts add
2.35 - val del_thms = thms_for_facts del
2.36 - fun iter p rel_consts =
2.37 + val thy = ProofContext.theory_of ctxt
2.38 + val add_thms = cnf_for_facts ctxt add
2.39 + val del_thms = cnf_for_facts ctxt del
2.40 + fun iter threshold rel_consts =
2.41 let
2.42 fun relevant ([], _) [] = [] (* Nothing added this iteration *)
2.43 - | relevant (newpairs,rejects) [] =
2.44 + | relevant (newpairs, rejects) [] =
2.45 let
2.46 val (newrels, more_rejects) = take_best max_new newpairs
2.47 val new_consts = maps #2 newrels
2.48 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
2.49 - val newp = p + (1.0 - p) / relevance_convergence
2.50 + val threshold =
2.51 + threshold + (1.0 - threshold) / relevance_convergence
2.52 in
2.53 trace_msg (fn () => "relevant this iteration: " ^
2.54 Int.toString (length newrels));
2.55 - map #1 newrels @ iter newp rel_consts' (more_rejects @ rejects)
2.56 + map #1 newrels @ iter threshold rel_consts'
2.57 + (more_rejects @ rejects)
2.58 end
2.59 | relevant (newrels, rejects)
2.60 ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
2.61 let
2.62 - val weight = if member Thm.eq_thm del_thms thm then 0.0
2.63 - else if member Thm.eq_thm add_thms thm then 1.0
2.64 - else if only then 0.0
2.65 + val weight = if member Thm.eq_thm add_thms thm then 1.0
2.66 + else if member Thm.eq_thm del_thms thm then 0.0
2.67 else clause_weight ctab rel_consts consts_typs
2.68 in
2.69 - if p <= weight orelse
2.70 + if weight >= threshold orelse
2.71 (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then
2.72 (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
2.73 " passes: " ^ Real.toString weight);
2.74 @@ -291,8 +298,8 @@
2.75 relevant (newrels, ax :: rejects) axs
2.76 end
2.77 in
2.78 - trace_msg (fn () => "relevant_clauses, current pass mark: " ^
2.79 - Real.toString p);
2.80 + trace_msg (fn () => "relevant_clauses, current threshold: " ^
2.81 + Real.toString threshold);
2.82 relevant ([], [])
2.83 end
2.84 in iter end
2.85 @@ -310,7 +317,7 @@
2.86 commas (Symtab.keys goal_const_tab))
2.87 val relevant =
2.88 relevant_clauses ctxt relevance_convergence defs_relevant max_new
2.89 - relevance_override thy const_tab relevance_threshold
2.90 + relevance_override const_tab relevance_threshold
2.91 goal_const_tab
2.92 (map (pair_consts_typs_axiom theory_relevant thy)
2.93 axioms)
2.94 @@ -352,7 +359,7 @@
2.95 fun subtract_cls ax_clauses =
2.96 filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
2.97
2.98 -fun all_valid_thms respect_no_atp ctxt chained_ths =
2.99 +fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
2.100 let
2.101 val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
2.102 val local_facts = ProofContext.facts_of ctxt;
2.103 @@ -369,7 +376,7 @@
2.104
2.105 val name1 = Facts.extern facts name;
2.106 val name2 = Name_Space.extern full_space name;
2.107 - val ths = filter_out bad_for_atp ths0;
2.108 + val ths = filter_out is_theorem_bad_for_atps ths0;
2.109 in
2.110 if Facts.is_concealed facts name orelse
2.111 (respect_no_atp andalso is_package_def name) then
2.112 @@ -398,26 +405,32 @@
2.113
2.114 (* The single-name theorems go after the multiple-name ones, so that single
2.115 names are preferred when both are available. *)
2.116 -fun name_thm_pairs respect_no_atp ctxt chained_ths =
2.117 +fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
2.118 let
2.119 - val (mults, singles) =
2.120 - List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_ths)
2.121 + val (mults, singles) = List.partition is_multi name_thms_pairs
2.122 val ps = [] |> fold add_single_names singles
2.123 |> fold add_multi_names mults
2.124 in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
2.125
2.126 -fun check_named ("", th) =
2.127 - (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
2.128 - | check_named _ = true;
2.129 +fun is_named ("", th) =
2.130 + (warning ("No name for theorem " ^
2.131 + Display.string_of_thm_without_context th); false)
2.132 + | is_named _ = true
2.133 +fun checked_name_thm_pairs respect_no_atp ctxt =
2.134 + name_thm_pairs respect_no_atp ctxt
2.135 + #> tap (fn ps => trace_msg
2.136 + (fn () => ("Considering " ^ Int.toString (length ps) ^
2.137 + " theorems")))
2.138 + #> filter is_named
2.139
2.140 -fun get_all_lemmas respect_no_atp ctxt chained_ths =
2.141 - let val included_thms =
2.142 - tap (fn ths => trace_msg
2.143 - (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
2.144 - (name_thm_pairs respect_no_atp ctxt chained_ths)
2.145 - in
2.146 - filter check_named included_thms
2.147 - end;
2.148 +fun name_thms_pair_from_ref ctxt chained_ths xref =
2.149 + let
2.150 + val ths = ProofContext.get_fact ctxt xref
2.151 + val name = Facts.string_of_ref xref
2.152 + |> forall (member Thm.eq_thm chained_ths) ths
2.153 + ? prefix chained_prefix
2.154 + in (name, ths) end
2.155 +
2.156
2.157 (***************************************************************)
2.158 (* Type Classes Present in the Axiom or Conjecture Clauses *)
2.159 @@ -463,26 +476,29 @@
2.160 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
2.161 | restrict_to_logic thy false cls = cls;
2.162
2.163 -(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
2.164 +(**** Predicates to detect unwanted clauses (prolific or likely to cause
2.165 + unsoundness) ****)
2.166
2.167 (** Too general means, positive equality literal with a variable X as one operand,
2.168 when X does not occur properly in the other operand. This rules out clearly
2.169 inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
2.170
2.171 -fun occurs ix =
2.172 - let fun occ(Var (jx,_)) = (ix=jx)
2.173 - | occ(t1$t2) = occ t1 orelse occ t2
2.174 - | occ(Abs(_,_,t)) = occ t
2.175 - | occ _ = false
2.176 - in occ end;
2.177 +fun var_occurs_in_term ix =
2.178 + let
2.179 + fun aux (Var (jx, _)) = (ix = jx)
2.180 + | aux (t1 $ t2) = aux t1 orelse aux t2
2.181 + | aux (Abs (_, _, t)) = aux t
2.182 + | aux _ = false
2.183 + in aux end
2.184
2.185 -fun is_recordtype T = not (null (Record.dest_recTs T));
2.186 +fun is_record_type T = not (null (Record.dest_recTs T))
2.187
2.188 (*Unwanted equalities include
2.189 (1) those between a variable that does not properly occur in the second operand,
2.190 (2) those between a variable and a record, since these seem to be prolific "cases" thms
2.191 *)
2.192 -fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
2.193 +fun too_general_eqterms (Var (ix,T), t) =
2.194 + not (var_occurs_in_term ix t) orelse is_record_type T
2.195 | too_general_eqterms _ = false;
2.196
2.197 fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
2.198 @@ -492,40 +508,56 @@
2.199 fun has_typed_var tycons = exists_subterm
2.200 (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
2.201
2.202 -(*Clauses are forbidden to contain variables of these types. The typical reason is that
2.203 - they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
2.204 - The resulting clause will have no type constraint, yielding false proofs. Even "bool"
2.205 - leads to many unsound proofs, though (obviously) only for higher-order problems.*)
2.206 -val unwanted_types = [@{type_name unit}, @{type_name bool}];
2.207 +(* Clauses are forbidden to contain variables of these types. The typical reason
2.208 + is that they lead to unsoundness. Note that "unit" satisfies numerous
2.209 + equations like "?x = ()". The resulting clause will have no type constraint,
2.210 + yielding false proofs. Even "bool" leads to many unsound proofs, though only
2.211 + for higher-order problems. *)
2.212 +val dangerous_types = [@{type_name unit}, @{type_name bool}];
2.213
2.214 -fun unwanted t =
2.215 - t = @{prop True} orelse has_typed_var unwanted_types t orelse
2.216 - forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
2.217 +(* Clauses containing variables of type "unit" or "bool" or of the form
2.218 + "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
2.219 + omitted. *)
2.220 +fun is_dangerous_term _ @{prop True} = true
2.221 + | is_dangerous_term full_types t =
2.222 + not full_types andalso
2.223 + (has_typed_var dangerous_types t orelse
2.224 + forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
2.225
2.226 -(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
2.227 - likely to lead to unsound proofs.*)
2.228 -fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
2.229 +fun is_dangerous_theorem full_types add_thms thm =
2.230 + not (member Thm.eq_thm add_thms thm) andalso
2.231 + is_dangerous_term full_types (prop_of thm)
2.232 +
2.233 +fun remove_dangerous_clauses full_types add_thms =
2.234 + filter_out (is_dangerous_theorem full_types add_thms o fst)
2.235
2.236 fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
2.237
2.238 -fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
2.239 - defs_relevant max_new theory_relevant
2.240 - (relevance_override as {add, only, ...})
2.241 - (ctxt, (chained_ths, _)) goal_cls =
2.242 +fun relevant_facts full_types respect_no_atp relevance_threshold
2.243 + relevance_convergence defs_relevant max_new theory_relevant
2.244 + (relevance_override as {add, del, only})
2.245 + (ctxt, (chained_ths, _)) goal_cls =
2.246 if (only andalso null add) orelse relevance_threshold > 1.0 then
2.247 []
2.248 else
2.249 let
2.250 val thy = ProofContext.theory_of ctxt
2.251 + val add_thms = cnf_for_facts ctxt add
2.252 + val has_override = not (null add) orelse not (null del)
2.253 val is_FO = is_first_order thy goal_cls
2.254 - val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths
2.255 - |> cnf_rules_pairs thy |> make_unique
2.256 + val axioms =
2.257 + checked_name_thm_pairs respect_no_atp ctxt
2.258 + (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
2.259 + else all_name_thms_pairs respect_no_atp ctxt chained_ths)
2.260 + |> cnf_rules_pairs thy
2.261 + |> not has_override ? make_unique
2.262 |> restrict_to_logic thy is_FO
2.263 - |> remove_unwanted_clauses
2.264 + |> not only ? remove_dangerous_clauses full_types add_thms
2.265 in
2.266 relevance_filter ctxt relevance_threshold relevance_convergence
2.267 defs_relevant max_new theory_relevant relevance_override
2.268 - thy included_cls (map prop_of goal_cls)
2.269 + thy axioms (map prop_of goal_cls)
2.270 + |> has_override ? make_unique
2.271 end
2.272
2.273 (* prepare for passing to writer,
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Jun 06 18:47:29 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 07 10:37:30 2010 +0200
3.3 @@ -14,11 +14,12 @@
3.4 val skolem_infix: string
3.5 val cnf_axiom: theory -> thm -> thm list
3.6 val multi_base_blacklist: string list
3.7 - val bad_for_atp: thm -> bool
3.8 + val is_theorem_bad_for_atps: thm -> bool
3.9 val type_has_topsort: typ -> bool
3.10 - val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
3.11 - val suppress_endtheory: bool Unsynchronized.ref
3.12 - (*for emergency use where endtheory causes problems*)
3.13 + val cnf_rules_pairs:
3.14 + theory -> (string * thm) list -> (thm * (string * int)) list
3.15 + val use_skolem_cache: bool Unsynchronized.ref
3.16 + (* for emergency use where the Skolem cache causes problems *)
3.17 val strip_subgoal : thm -> int -> (string * typ) list * term list * term
3.18 val neg_clausify: thm -> thm list
3.19 val neg_conjecture_clauses:
3.20 @@ -86,9 +87,9 @@
3.21 val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
3.22 in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
3.23
3.24 -(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
3.25 - prefix for the Skolem constant.*)
3.26 -fun declare_skofuns s th =
3.27 +(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
3.28 + suggested prefix for the Skolem constants. *)
3.29 +fun declare_skolem_funs s th thy =
3.30 let
3.31 val nref = Unsynchronized.ref 0 (* FIXME ??? *)
3.32 fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
3.33 @@ -103,13 +104,13 @@
3.34 val cT = extraTs ---> Ts ---> T
3.35 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
3.36 (*Forms a lambda-abstraction over the formal parameters*)
3.37 - val (c, thy') =
3.38 + val (c, thy) =
3.39 Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
3.40 val cdef = cname ^ "_def"
3.41 - val ((_, ax), thy'') =
3.42 - Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
3.43 + val ((_, ax), thy) =
3.44 + Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
3.45 val ax' = Drule.export_without_context ax
3.46 - in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
3.47 + in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
3.48 | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
3.49 (*Universal quant: insert a free variable into body and continue*)
3.50 let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
3.51 @@ -117,11 +118,11 @@
3.52 | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
3.53 | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
3.54 | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
3.55 - | dec_sko t thx = thx (*Do nothing otherwise*)
3.56 - in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
3.57 + | dec_sko t thx = thx
3.58 + in dec_sko (prop_of th) ([], thy) end
3.59
3.60 (*Traverse a theorem, accumulating Skolem function definitions.*)
3.61 -fun assume_skofuns s th =
3.62 +fun assume_skolem_funs s th =
3.63 let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
3.64 fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
3.65 (*Existential: declare a Skolem function, then insert into body and continue*)
3.66 @@ -135,9 +136,7 @@
3.67 HOLogic.choice_const T $ xtp)
3.68 (*Forms a lambda-abstraction over the formal parameters*)
3.69 val def = Logic.mk_equals (c, rhs)
3.70 - in dec_sko (subst_bound (list_comb(c,args), p))
3.71 - (def :: defs)
3.72 - end
3.73 + in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end
3.74 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
3.75 (*Universal quant: insert a free variable into body and continue*)
3.76 let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
3.77 @@ -219,41 +218,44 @@
3.78 val crator = cterm_of thy rator
3.79 val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
3.80 val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
3.81 - in
3.82 - Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
3.83 - end
3.84 + in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
3.85 else makeK()
3.86 - | _ => error "abstract: Bad term"
3.87 + | _ => raise Fail "abstract: Bad term"
3.88 end;
3.89
3.90 -(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
3.91 - prefix for the constants.*)
3.92 -fun combinators_aux ct =
3.93 - if lambda_free (term_of ct) then Thm.reflexive ct
3.94 +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
3.95 +fun do_introduce_combinators ct =
3.96 + if lambda_free (term_of ct) then
3.97 + Thm.reflexive ct
3.98 + else case term_of ct of
3.99 + Abs _ =>
3.100 + let
3.101 + val (cv, cta) = Thm.dest_abs NONE ct
3.102 + val (v, _) = dest_Free (term_of cv)
3.103 + val u_th = do_introduce_combinators cta
3.104 + val cu = Thm.rhs_of u_th
3.105 + val comb_eq = abstract (Thm.cabs cv cu)
3.106 + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
3.107 + | _ $ _ =>
3.108 + let val (ct1, ct2) = Thm.dest_comb ct in
3.109 + Thm.combination (do_introduce_combinators ct1)
3.110 + (do_introduce_combinators ct2)
3.111 + end
3.112 +
3.113 +fun introduce_combinators th =
3.114 + if lambda_free (prop_of th) then
3.115 + th
3.116 else
3.117 - case term_of ct of
3.118 - Abs _ =>
3.119 - let val (cv, cta) = Thm.dest_abs NONE ct
3.120 - val (v, _) = dest_Free (term_of cv)
3.121 - val u_th = combinators_aux cta
3.122 - val cu = Thm.rhs_of u_th
3.123 - val comb_eq = abstract (Thm.cabs cv cu)
3.124 - in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
3.125 - | _ $ _ =>
3.126 - let val (ct1, ct2) = Thm.dest_comb ct
3.127 - in Thm.combination (combinators_aux ct1) (combinators_aux ct2) end;
3.128 -
3.129 -fun combinators th =
3.130 - if lambda_free (prop_of th) then th
3.131 - else
3.132 - let val th = Drule.eta_contraction_rule th
3.133 - val eqth = combinators_aux (cprop_of th)
3.134 - in Thm.equal_elim eqth th end
3.135 - handle THM (msg,_,_) =>
3.136 - (warning (cat_lines
3.137 - ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
3.138 - " Exception message: " ^ msg]);
3.139 - TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
3.140 + let
3.141 + val th = Drule.eta_contraction_rule th
3.142 + val eqth = do_introduce_combinators (cprop_of th)
3.143 + in Thm.equal_elim eqth th end
3.144 + handle THM (msg, _, _) =>
3.145 + (warning ("Error in the combinator translation of " ^
3.146 + Display.string_of_thm_without_context th ^
3.147 + "\nException message: " ^ msg ^ ".");
3.148 + (* A type variable of sort "{}" will make abstraction fail. *)
3.149 + TrueI)
3.150
3.151 (*cterms are used throughout for efficiency*)
3.152 val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
3.153 @@ -302,37 +304,43 @@
3.154
3.155 (*Generate Skolem functions for a theorem supplied in nnf*)
3.156 fun assume_skolem_of_def s th =
3.157 - map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
3.158 + map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th))
3.159 + (assume_skolem_funs s th)
3.160
3.161
3.162 -(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
3.163 +(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
3.164
3.165 -val max_lambda_nesting = 3;
3.166 +val max_lambda_nesting = 3
3.167
3.168 -fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
3.169 - | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
3.170 - | excessive_lambdas _ = false;
3.171 +fun term_has_too_many_lambdas max (t1 $ t2) =
3.172 + exists (term_has_too_many_lambdas max) [t1, t2]
3.173 + | term_has_too_many_lambdas max (Abs (_, _, t)) =
3.174 + max = 0 orelse term_has_too_many_lambdas (max - 1) t
3.175 + | term_has_too_many_lambdas _ _ = false
3.176
3.177 -fun is_formula_type T = (T = HOLogic.boolT orelse T = propT);
3.178 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
3.179
3.180 -(*Don't count nested lambdas at the level of formulas, as they are quantifiers*)
3.181 -fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t
3.182 - | excessive_lambdas_fm Ts t =
3.183 - if is_formula_type (fastype_of1 (Ts, t))
3.184 - then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t))
3.185 - else excessive_lambdas (t, max_lambda_nesting);
3.186 +(* Don't count nested lambdas at the level of formulas, since they are
3.187 + quantifiers. *)
3.188 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
3.189 + formula_has_too_many_lambdas (T :: Ts) t
3.190 + | formula_has_too_many_lambdas Ts t =
3.191 + if is_formula_type (fastype_of1 (Ts, t)) then
3.192 + exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
3.193 + else
3.194 + term_has_too_many_lambdas max_lambda_nesting t
3.195
3.196 -(*The max apply_depth of any metis call in Metis_Examples (on 31-10-2007) was 11.*)
3.197 -val max_apply_depth = 15;
3.198 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
3.199 + was 11. *)
3.200 +val max_apply_depth = 15
3.201
3.202 -fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1)
3.203 - | apply_depth (Abs(_,_,t)) = apply_depth t
3.204 - | apply_depth _ = 0;
3.205 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
3.206 + | apply_depth (Abs (_, _, t)) = apply_depth t
3.207 + | apply_depth _ = 0
3.208
3.209 -fun too_complex t =
3.210 - apply_depth t > max_apply_depth orelse
3.211 - Meson.too_many_clauses NONE t orelse
3.212 - excessive_lambdas_fm [] t;
3.213 +fun is_formula_too_complex t =
3.214 + apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
3.215 + formula_has_too_many_lambdas [] t
3.216
3.217 fun is_strange_thm th =
3.218 case head_of (concl_of th) of
3.219 @@ -340,10 +348,11 @@
3.220 a <> @{const_name "=="})
3.221 | _ => false;
3.222
3.223 -fun bad_for_atp th =
3.224 - too_complex (prop_of th)
3.225 - orelse exists_type type_has_topsort (prop_of th)
3.226 - orelse is_strange_thm th;
3.227 +fun is_theorem_bad_for_atps thm =
3.228 + let val t = prop_of thm in
3.229 + is_formula_too_complex t orelse exists_type type_has_topsort t orelse
3.230 + is_strange_thm thm
3.231 + end
3.232
3.233 (* FIXME: put other record thms here, or declare as "no_atp" *)
3.234 val multi_base_blacklist =
3.235 @@ -356,14 +365,21 @@
3.236
3.237 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
3.238 fun skolem_thm (s, th) =
3.239 - if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
3.240 + if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
3.241 + is_theorem_bad_for_atps th then
3.242 + []
3.243 else
3.244 let
3.245 val ctxt0 = Variable.global_thm_context th
3.246 - val (nnfth, ctxt1) = to_nnf th ctxt0
3.247 - val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
3.248 - in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
3.249 - handle THM _ => [];
3.250 + val (nnfth, ctxt) = to_nnf th ctxt0
3.251 + val defs = assume_skolem_of_def s nnfth
3.252 + val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
3.253 + in
3.254 + cnfs |> map introduce_combinators
3.255 + |> Variable.export ctxt ctxt0
3.256 + |> Meson.finish_cnf
3.257 + end
3.258 + handle THM _ => []
3.259
3.260 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
3.261 Skolem functions.*)
3.262 @@ -413,19 +429,19 @@
3.263
3.264 fun skolem_def (name, th) thy =
3.265 let val ctxt0 = Variable.global_thm_context th in
3.266 - (case try (to_nnf th) ctxt0 of
3.267 + case try (to_nnf th) ctxt0 of
3.268 NONE => (NONE, thy)
3.269 - | SOME (nnfth, ctxt1) =>
3.270 - let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy
3.271 - in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end)
3.272 + | SOME (nnfth, ctxt) =>
3.273 + let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy
3.274 + in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end
3.275 end;
3.276
3.277 -fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) =
3.278 +fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
3.279 let
3.280 - val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1;
3.281 + val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt;
3.282 val cnfs' = cnfs
3.283 - |> map combinators
3.284 - |> Variable.export ctxt2 ctxt0
3.285 + |> map introduce_combinators
3.286 + |> Variable.export ctxt ctxt0
3.287 |> Meson.finish_cnf
3.288 |> map Thm.close_derivation;
3.289 in (th, cnfs') end;
3.290 @@ -441,8 +457,10 @@
3.291 val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
3.292 if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
3.293 else fold_index (fn (i, th) =>
3.294 - if bad_for_atp th orelse is_some (lookup_cache thy th) then I
3.295 - else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
3.296 + if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
3.297 + I
3.298 + else
3.299 + cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
3.300 in
3.301 if null new_facts then NONE
3.302 else
3.303 @@ -457,11 +475,10 @@
3.304
3.305 end;
3.306
3.307 -val suppress_endtheory = Unsynchronized.ref false
3.308 +val use_skolem_cache = Unsynchronized.ref true
3.309
3.310 fun clause_cache_endtheory thy =
3.311 - if ! suppress_endtheory then NONE
3.312 - else saturate_skolem_cache thy;
3.313 + if !use_skolem_cache then saturate_skolem_cache thy else NONE
3.314
3.315
3.316 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
3.317 @@ -481,7 +498,10 @@
3.318 EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
3.319
3.320 val neg_clausify =
3.321 - single #> Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf
3.322 + single
3.323 + #> Meson.make_clauses_unsorted
3.324 + #> map introduce_combinators
3.325 + #> Meson.finish_cnf
3.326
3.327 fun neg_conjecture_clauses ctxt st0 n =
3.328 let
3.329 @@ -509,7 +529,7 @@
3.330 (** setup **)
3.331
3.332 val setup =
3.333 - perhaps saturate_skolem_cache #>
3.334 - Theory.at_end clause_cache_endtheory;
3.335 + perhaps saturate_skolem_cache
3.336 + #> Theory.at_end clause_cache_endtheory
3.337
3.338 end;
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Jun 06 18:47:29 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 07 10:37:30 2010 +0200
4.3 @@ -19,6 +19,7 @@
4.4 struct
4.5
4.6 open Sledgehammer_Util
4.7 +open Sledgehammer_Fact_Filter
4.8 open Sledgehammer_Fact_Preprocessor
4.9 open ATP_Manager
4.10 open ATP_Systems
4.11 @@ -238,19 +239,12 @@
4.12 state) atps
4.13 in () end
4.14
4.15 -fun minimize override_params i frefs state =
4.16 +fun minimize override_params i refs state =
4.17 let
4.18 val thy = Proof.theory_of state
4.19 val ctxt = Proof.context_of state
4.20 val chained_ths = #facts (Proof.goal state)
4.21 - fun theorems_from_ref ctxt fref =
4.22 - let
4.23 - val ths = ProofContext.get_fact ctxt fref
4.24 - val name = Facts.string_of_ref fref
4.25 - |> forall (member Thm.eq_thm chained_ths) ths
4.26 - ? prefix chained_prefix
4.27 - in (name, ths) end
4.28 - val name_thms_pairs = map (theorems_from_ref ctxt) frefs
4.29 + val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
4.30 in
4.31 case subgoal_count state of
4.32 0 => priority "No subgoal!"