|
1 (* Title: HOL/Tools/Sledgehammer/clausifier.ML |
|
2 Author: Jia Meng, Cambridge University Computer Laboratory |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Transformation of axiom rules (elim/intro/etc) into CNF forms. |
|
6 *) |
|
7 |
|
8 signature CLAUSIFIER = |
|
9 sig |
|
10 type cnf_thm = thm * ((string * int) * thm) |
|
11 |
|
12 val sledgehammer_prefix: string |
|
13 val chained_prefix: string |
|
14 val trace: bool Unsynchronized.ref |
|
15 val trace_msg: (unit -> string) -> unit |
|
16 val name_thms_pair_from_ref : |
|
17 Proof.context -> thm list -> Facts.ref -> string * thm list |
|
18 val skolem_theory_name: string |
|
19 val skolem_prefix: string |
|
20 val skolem_infix: string |
|
21 val is_skolem_const_name: string -> bool |
|
22 val num_type_args: theory -> string -> int |
|
23 val cnf_axiom: theory -> thm -> thm list |
|
24 val multi_base_blacklist: string list |
|
25 val is_theorem_bad_for_atps: thm -> bool |
|
26 val type_has_topsort: typ -> bool |
|
27 val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list |
|
28 val saturate_skolem_cache: theory -> theory option |
|
29 val auto_saturate_skolem_cache: bool Unsynchronized.ref |
|
30 val neg_clausify: thm -> thm list |
|
31 val neg_conjecture_clauses: |
|
32 Proof.context -> thm -> int -> thm list list * (string * typ) list |
|
33 val setup: theory -> theory |
|
34 end; |
|
35 |
|
36 structure Clausifier : CLAUSIFIER = |
|
37 struct |
|
38 |
|
39 type cnf_thm = thm * ((string * int) * thm) |
|
40 |
|
41 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
|
42 |
|
43 (* Used to label theorems chained into the goal. *) |
|
44 val chained_prefix = sledgehammer_prefix ^ "chained_" |
|
45 |
|
46 val trace = Unsynchronized.ref false; |
|
47 fun trace_msg msg = if !trace then tracing (msg ()) else (); |
|
48 |
|
49 fun name_thms_pair_from_ref ctxt chained_ths xref = |
|
50 let |
|
51 val ths = ProofContext.get_fact ctxt xref |
|
52 val name = Facts.string_of_ref xref |
|
53 |> forall (member Thm.eq_thm chained_ths) ths |
|
54 ? prefix chained_prefix |
|
55 in (name, ths) end |
|
56 |
|
57 val skolem_theory_name = sledgehammer_prefix ^ "Sko" |
|
58 val skolem_prefix = "sko_" |
|
59 val skolem_infix = "$" |
|
60 |
|
61 val type_has_topsort = Term.exists_subtype |
|
62 (fn TFree (_, []) => true |
|
63 | TVar (_, []) => true |
|
64 | _ => false); |
|
65 |
|
66 |
|
67 (**** Transformation of Elimination Rules into First-Order Formulas****) |
|
68 |
|
69 val cfalse = cterm_of @{theory HOL} HOLogic.false_const; |
|
70 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); |
|
71 |
|
72 (*Converts an elim-rule into an equivalent theorem that does not have the |
|
73 predicate variable. Leaves other theorems unchanged. We simply instantiate the |
|
74 conclusion variable to False.*) |
|
75 fun transform_elim th = |
|
76 case concl_of th of (*conclusion variable*) |
|
77 @{const Trueprop} $ (v as Var (_, @{typ bool})) => |
|
78 Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th |
|
79 | v as Var(_, @{typ prop}) => |
|
80 Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th |
|
81 | _ => th; |
|
82 |
|
83 (*To enforce single-threading*) |
|
84 exception Clausify_failure of theory; |
|
85 |
|
86 |
|
87 (**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
|
88 |
|
89 (*Keep the full complexity of the original name*) |
|
90 fun flatten_name s = space_implode "_X" (Long_Name.explode s); |
|
91 |
|
92 fun skolem_name thm_name j var_name = |
|
93 skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^ |
|
94 skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name) |
|
95 |
|
96 (* Hack: Could return false positives (e.g., a user happens to declare a |
|
97 constant called "SomeTheory.sko_means_shoe_in_$wedish". *) |
|
98 val is_skolem_const_name = |
|
99 Long_Name.base_name |
|
100 #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix |
|
101 |
|
102 (* The number of type arguments of a constant, zero if it's monomorphic. For |
|
103 (instances of) Skolem pseudoconstants, this information is encoded in the |
|
104 constant name. *) |
|
105 fun num_type_args thy s = |
|
106 if String.isPrefix skolem_theory_name s then |
|
107 s |> unprefix skolem_theory_name |
|
108 |> space_explode skolem_infix |> hd |
|
109 |> space_explode "_" |> List.last |> Int.fromString |> the |
|
110 else |
|
111 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
|
112 |
|
113 fun rhs_extra_types lhsT rhs = |
|
114 let val lhs_vars = Term.add_tfreesT lhsT [] |
|
115 fun add_new_TFrees (TFree v) = |
|
116 if member (op =) lhs_vars v then I else insert (op =) (TFree v) |
|
117 | add_new_TFrees _ = I |
|
118 val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] |
|
119 in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; |
|
120 |
|
121 fun skolem_type_and_args bound_T body = |
|
122 let |
|
123 val args1 = OldTerm.term_frees body |
|
124 val Ts1 = map type_of args1 |
|
125 val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body |
|
126 val args2 = map (fn T => Free (gensym "vsk", T)) Ts2 |
|
127 in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end |
|
128 |
|
129 (* Traverse a theorem, declaring Skolem function definitions. String "s" is the |
|
130 suggested prefix for the Skolem constants. *) |
|
131 fun declare_skolem_funs s th thy = |
|
132 let |
|
133 val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) |
|
134 fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) |
|
135 (axs, thy) = |
|
136 (*Existential: declare a Skolem function, then insert into body and continue*) |
|
137 let |
|
138 val id = skolem_name s (Unsynchronized.inc skolem_count) s' |
|
139 val (cT, args) = skolem_type_and_args T body |
|
140 val rhs = list_abs_free (map dest_Free args, |
|
141 HOLogic.choice_const T $ body) |
|
142 (*Forms a lambda-abstraction over the formal parameters*) |
|
143 val (c, thy) = |
|
144 Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy |
|
145 val cdef = id ^ "_def" |
|
146 val ((_, ax), thy) = |
|
147 Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy |
|
148 val ax' = Drule.export_without_context ax |
|
149 in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end |
|
150 | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = |
|
151 (*Universal quant: insert a free variable into body and continue*) |
|
152 let val fname = Name.variant (OldTerm.add_term_names (p, [])) a |
|
153 in dec_sko (subst_bound (Free (fname, T), p)) thx end |
|
154 | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) |
|
155 | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) |
|
156 | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx |
|
157 | dec_sko _ thx = thx |
|
158 in dec_sko (prop_of th) ([], thy) end |
|
159 |
|
160 fun mk_skolem_id t = |
|
161 let val T = fastype_of t in |
|
162 Const (@{const_name skolem_id}, T --> T) $ t |
|
163 end |
|
164 |
|
165 fun quasi_beta_eta_contract (Abs (s, T, t')) = |
|
166 Abs (s, T, quasi_beta_eta_contract t') |
|
167 | quasi_beta_eta_contract t = Envir.beta_eta_contract t |
|
168 |
|
169 (*Traverse a theorem, accumulating Skolem function definitions.*) |
|
170 fun assume_skolem_funs s th = |
|
171 let |
|
172 val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) |
|
173 fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs = |
|
174 (*Existential: declare a Skolem function, then insert into body and continue*) |
|
175 let |
|
176 val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) |
|
177 val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*) |
|
178 val Ts = map type_of args |
|
179 val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) |
|
180 val id = skolem_name s (Unsynchronized.inc skolem_count) s' |
|
181 val c = Free (id, cT) (* FIXME: needed? ### *) |
|
182 (* Forms a lambda-abstraction over the formal parameters *) |
|
183 val rhs = |
|
184 list_abs_free (map dest_Free args, |
|
185 HOLogic.choice_const T |
|
186 $ quasi_beta_eta_contract body) |
|
187 |> mk_skolem_id |
|
188 val def = Logic.mk_equals (c, rhs) |
|
189 val comb = list_comb (rhs, args) |
|
190 in dec_sko (subst_bound (comb, p)) (def :: defs) end |
|
191 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = |
|
192 (*Universal quant: insert a free variable into body and continue*) |
|
193 let val fname = Name.variant (OldTerm.add_term_names (p,[])) a |
|
194 in dec_sko (subst_bound (Free(fname,T), p)) defs end |
|
195 | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) |
|
196 | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) |
|
197 | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs |
|
198 | dec_sko _ defs = defs |
|
199 in dec_sko (prop_of th) [] end; |
|
200 |
|
201 |
|
202 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) |
|
203 |
|
204 (*Returns the vars of a theorem*) |
|
205 fun vars_of_thm th = |
|
206 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
|
207 |
|
208 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} |
|
209 |
|
210 (* Removes the lambdas from an equation of the form t = (%x. u). *) |
|
211 fun extensionalize th = |
|
212 case prop_of th of |
|
213 _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) |
|
214 $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) |
|
215 | _ => th |
|
216 |
|
217 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
|
218 | is_quasi_lambda_free (t1 $ t2) = |
|
219 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
|
220 | is_quasi_lambda_free (Abs _) = false |
|
221 | is_quasi_lambda_free _ = true |
|
222 |
|
223 val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); |
|
224 val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); |
|
225 val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); |
|
226 |
|
227 (*FIXME: requires more use of cterm constructors*) |
|
228 fun abstract ct = |
|
229 let |
|
230 val thy = theory_of_cterm ct |
|
231 val Abs(x,_,body) = term_of ct |
|
232 val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) |
|
233 val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
|
234 fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} |
|
235 in |
|
236 case body of |
|
237 Const _ => makeK() |
|
238 | Free _ => makeK() |
|
239 | Var _ => makeK() (*though Var isn't expected*) |
|
240 | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) |
|
241 | rator$rand => |
|
242 if loose_bvar1 (rator,0) then (*C or S*) |
|
243 if loose_bvar1 (rand,0) then (*S*) |
|
244 let val crator = cterm_of thy (Abs(x,xT,rator)) |
|
245 val crand = cterm_of thy (Abs(x,xT,rand)) |
|
246 val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} |
|
247 val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
|
248 in |
|
249 Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
|
250 end |
|
251 else (*C*) |
|
252 let val crator = cterm_of thy (Abs(x,xT,rator)) |
|
253 val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} |
|
254 val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
|
255 in |
|
256 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
|
257 end |
|
258 else if loose_bvar1 (rand,0) then (*B or eta*) |
|
259 if rand = Bound 0 then Thm.eta_conversion ct |
|
260 else (*B*) |
|
261 let val crand = cterm_of thy (Abs(x,xT,rand)) |
|
262 val crator = cterm_of thy rator |
|
263 val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} |
|
264 val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
|
265 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end |
|
266 else makeK() |
|
267 | _ => raise Fail "abstract: Bad term" |
|
268 end; |
|
269 |
|
270 (* Traverse a theorem, remplacing lambda-abstractions with combinators. *) |
|
271 fun do_introduce_combinators ct = |
|
272 if is_quasi_lambda_free (term_of ct) then |
|
273 Thm.reflexive ct |
|
274 else case term_of ct of |
|
275 Abs _ => |
|
276 let |
|
277 val (cv, cta) = Thm.dest_abs NONE ct |
|
278 val (v, _) = dest_Free (term_of cv) |
|
279 val u_th = do_introduce_combinators cta |
|
280 val cu = Thm.rhs_of u_th |
|
281 val comb_eq = abstract (Thm.cabs cv cu) |
|
282 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
|
283 | _ $ _ => |
|
284 let val (ct1, ct2) = Thm.dest_comb ct in |
|
285 Thm.combination (do_introduce_combinators ct1) |
|
286 (do_introduce_combinators ct2) |
|
287 end |
|
288 |
|
289 fun introduce_combinators th = |
|
290 if is_quasi_lambda_free (prop_of th) then |
|
291 th |
|
292 else |
|
293 let |
|
294 val th = Drule.eta_contraction_rule th |
|
295 val eqth = do_introduce_combinators (cprop_of th) |
|
296 in Thm.equal_elim eqth th end |
|
297 handle THM (msg, _, _) => |
|
298 (warning ("Error in the combinator translation of " ^ |
|
299 Display.string_of_thm_without_context th ^ |
|
300 "\nException message: " ^ msg ^ "."); |
|
301 (* A type variable of sort "{}" will make abstraction fail. *) |
|
302 TrueI) |
|
303 |
|
304 (*cterms are used throughout for efficiency*) |
|
305 val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; |
|
306 |
|
307 (*cterm version of mk_cTrueprop*) |
|
308 fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
309 |
|
310 (*Given an abstraction over n variables, replace the bound variables by free |
|
311 ones. Return the body, along with the list of free variables.*) |
|
312 fun c_variant_abs_multi (ct0, vars) = |
|
313 let val (cv,ct) = Thm.dest_abs NONE ct0 |
|
314 in c_variant_abs_multi (ct, cv::vars) end |
|
315 handle CTERM _ => (ct0, rev vars); |
|
316 |
|
317 (*Given the definition of a Skolem function, return a theorem to replace |
|
318 an existential formula by a use of that function. |
|
319 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
|
320 fun skolem_theorem_of_def inline def = |
|
321 let |
|
322 val (c, rhs) = def |> Drule.legacy_freeze_thaw |> #1 |> cprop_of |
|
323 |> Thm.dest_equals |
|
324 val rhs' = rhs |> inline ? (snd o Thm.dest_comb) |
|
325 val (ch, frees) = c_variant_abs_multi (rhs', []) |
|
326 val (chilbert, cabs) = ch |> Thm.dest_comb |
|
327 val thy = Thm.theory_of_cterm chilbert |
|
328 val t = Thm.term_of chilbert |
|
329 val T = |
|
330 case t of |
|
331 Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T |
|
332 | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t]) |
|
333 val cex = Thm.cterm_of thy (HOLogic.exists_const T) |
|
334 val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
|
335 and conc = |
|
336 Drule.list_comb (if inline then rhs else c, frees) |
|
337 |> Drule.beta_conv cabs |> c_mkTrueprop |
|
338 fun tacf [prem] = |
|
339 (if inline then rewrite_goals_tac @{thms skolem_id_def_raw} |
|
340 else rewrite_goals_tac [def]) |
|
341 THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw}) |
|
342 RS @{thm someI_ex}) 1 |
|
343 in Goal.prove_internal [ex_tm] conc tacf |
|
344 |> forall_intr_list frees |
|
345 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
|
346 |> Thm.varifyT_global |
|
347 end; |
|
348 |
|
349 |
|
350 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) |
|
351 fun to_nnf th ctxt0 = |
|
352 let val th1 = th |> transform_elim |> zero_var_indexes |
|
353 val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
|
354 val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize |
|
355 |> extensionalize |
|
356 |> Meson.make_nnf ctxt |
|
357 in (th3, ctxt) end; |
|
358 |
|
359 (*Generate Skolem functions for a theorem supplied in nnf*) |
|
360 fun skolem_theorems_of_assume s th = |
|
361 map (skolem_theorem_of_def true o Thm.assume o cterm_of (theory_of_thm th)) |
|
362 (assume_skolem_funs s th) |
|
363 |
|
364 |
|
365 (*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) |
|
366 |
|
367 val max_lambda_nesting = 3 |
|
368 |
|
369 fun term_has_too_many_lambdas max (t1 $ t2) = |
|
370 exists (term_has_too_many_lambdas max) [t1, t2] |
|
371 | term_has_too_many_lambdas max (Abs (_, _, t)) = |
|
372 max = 0 orelse term_has_too_many_lambdas (max - 1) t |
|
373 | term_has_too_many_lambdas _ _ = false |
|
374 |
|
375 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) |
|
376 |
|
377 (* Don't count nested lambdas at the level of formulas, since they are |
|
378 quantifiers. *) |
|
379 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = |
|
380 formula_has_too_many_lambdas (T :: Ts) t |
|
381 | formula_has_too_many_lambdas Ts t = |
|
382 if is_formula_type (fastype_of1 (Ts, t)) then |
|
383 exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) |
|
384 else |
|
385 term_has_too_many_lambdas max_lambda_nesting t |
|
386 |
|
387 (* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007) |
|
388 was 11. *) |
|
389 val max_apply_depth = 15 |
|
390 |
|
391 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) |
|
392 | apply_depth (Abs (_, _, t)) = apply_depth t |
|
393 | apply_depth _ = 0 |
|
394 |
|
395 fun is_formula_too_complex t = |
|
396 apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse |
|
397 formula_has_too_many_lambdas [] t |
|
398 |
|
399 fun is_strange_thm th = |
|
400 case head_of (concl_of th) of |
|
401 Const (a, _) => (a <> @{const_name Trueprop} andalso |
|
402 a <> @{const_name "=="}) |
|
403 | _ => false; |
|
404 |
|
405 fun is_theorem_bad_for_atps thm = |
|
406 let val t = prop_of thm in |
|
407 is_formula_too_complex t orelse exists_type type_has_topsort t orelse |
|
408 is_strange_thm thm |
|
409 end |
|
410 |
|
411 (* FIXME: put other record thms here, or declare as "no_atp" *) |
|
412 val multi_base_blacklist = |
|
413 ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", |
|
414 "split_asm", "cases", "ext_cases"]; |
|
415 |
|
416 fun fake_name th = |
|
417 if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) |
|
418 else gensym "unknown_thm_"; |
|
419 |
|
420 (*Skolemize a named theorem, with Skolem functions as additional premises.*) |
|
421 fun skolemize_theorem s th = |
|
422 if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse |
|
423 is_theorem_bad_for_atps th then |
|
424 [] |
|
425 else |
|
426 let |
|
427 val ctxt0 = Variable.global_thm_context th |
|
428 val (nnfth, ctxt) = to_nnf th ctxt0 |
|
429 val defs = skolem_theorems_of_assume s nnfth |
|
430 val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt |
|
431 in |
|
432 cnfs |> map introduce_combinators |
|
433 |> Variable.export ctxt ctxt0 |
|
434 |> Meson.finish_cnf |
|
435 end |
|
436 handle THM _ => [] |
|
437 |
|
438 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of |
|
439 Skolem functions.*) |
|
440 structure ThmCache = Theory_Data |
|
441 ( |
|
442 type T = thm list Thmtab.table * unit Symtab.table; |
|
443 val empty = (Thmtab.empty, Symtab.empty); |
|
444 val extend = I; |
|
445 fun merge ((cache1, seen1), (cache2, seen2)) : T = |
|
446 (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); |
|
447 ); |
|
448 |
|
449 val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; |
|
450 val already_seen = Symtab.defined o #2 o ThmCache.get; |
|
451 |
|
452 val update_cache = ThmCache.map o apfst o Thmtab.update; |
|
453 fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); |
|
454 |
|
455 (* Convert Isabelle theorems into axiom clauses. *) |
|
456 fun cnf_axiom thy th0 = |
|
457 let val th = Thm.transfer thy th0 in |
|
458 case lookup_cache thy th of |
|
459 SOME cls => cls |
|
460 | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th) |
|
461 end; |
|
462 |
|
463 |
|
464 (**** Translate a set of theorems into CNF ****) |
|
465 |
|
466 (*The combination of rev and tail recursion preserves the original order*) |
|
467 fun cnf_rules_pairs thy = |
|
468 let |
|
469 fun do_one _ [] = [] |
|
470 | do_one ((name, k), th) (cls :: clss) = |
|
471 (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss |
|
472 fun do_all pairs [] = pairs |
|
473 | do_all pairs ((name, th) :: ths) = |
|
474 let |
|
475 val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) |
|
476 handle THM _ => [] |
|
477 in do_all (new_pairs @ pairs) ths end |
|
478 in do_all [] o rev end |
|
479 |
|
480 |
|
481 (**** Convert all facts of the theory into FOL or HOL clauses ****) |
|
482 |
|
483 local |
|
484 |
|
485 fun skolem_def (name, th) thy = |
|
486 let val ctxt0 = Variable.global_thm_context th in |
|
487 case try (to_nnf th) ctxt0 of |
|
488 NONE => (NONE, thy) |
|
489 | SOME (nnfth, ctxt) => |
|
490 let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy |
|
491 in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end |
|
492 end; |
|
493 |
|
494 fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) = |
|
495 let |
|
496 val (cnfs, ctxt) = |
|
497 Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt |
|
498 val cnfs' = cnfs |
|
499 |> map introduce_combinators |
|
500 |> Variable.export ctxt ctxt0 |
|
501 |> Meson.finish_cnf |
|
502 |> map Thm.close_derivation; |
|
503 in (th, cnfs') end; |
|
504 |
|
505 in |
|
506 |
|
507 fun saturate_skolem_cache thy = |
|
508 let |
|
509 val facts = PureThy.facts_of thy; |
|
510 val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) => |
|
511 if Facts.is_concealed facts name orelse already_seen thy name then I |
|
512 else cons (name, ths)); |
|
513 val new_thms = (new_facts, []) |-> fold (fn (name, ths) => |
|
514 if member (op =) multi_base_blacklist (Long_Name.base_name name) then |
|
515 I |
|
516 else |
|
517 fold_index (fn (i, th) => |
|
518 if is_theorem_bad_for_atps th orelse |
|
519 is_some (lookup_cache thy th) then |
|
520 I |
|
521 else |
|
522 cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) |
|
523 in |
|
524 if null new_facts then |
|
525 NONE |
|
526 else |
|
527 let |
|
528 val (defs, thy') = thy |
|
529 |> fold (mark_seen o #1) new_facts |
|
530 |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms) |
|
531 |>> map_filter I; |
|
532 val cache_entries = Par_List.map skolem_cnfs defs; |
|
533 in SOME (fold update_cache cache_entries thy') end |
|
534 end; |
|
535 |
|
536 end; |
|
537 |
|
538 (* For emergency use where the Skolem cache causes problems. *) |
|
539 val auto_saturate_skolem_cache = Unsynchronized.ref true |
|
540 |
|
541 fun conditionally_saturate_skolem_cache thy = |
|
542 if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE |
|
543 |
|
544 |
|
545 (*** Converting a subgoal into negated conjecture clauses. ***) |
|
546 |
|
547 fun neg_skolemize_tac ctxt = |
|
548 EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt] |
|
549 |
|
550 val neg_clausify = |
|
551 single |
|
552 #> Meson.make_clauses_unsorted |
|
553 #> map introduce_combinators |
|
554 #> Meson.finish_cnf |
|
555 |
|
556 fun neg_conjecture_clauses ctxt st0 n = |
|
557 let |
|
558 (* "Option" is thrown if the assumptions contain schematic variables. *) |
|
559 val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0 |
|
560 val ({params, prems, ...}, _) = |
|
561 Subgoal.focus (Variable.set_body false ctxt) n st |
|
562 in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end |
|
563 |
|
564 |
|
565 (** setup **) |
|
566 |
|
567 val setup = |
|
568 perhaps conditionally_saturate_skolem_cache |
|
569 #> Theory.at_end conditionally_saturate_skolem_cache |
|
570 |
|
571 end; |