7 |
7 |
8 signature RES_AXIOMS = |
8 signature RES_AXIOMS = |
9 sig |
9 sig |
10 val cnf_axiom: theory -> thm -> thm list |
10 val cnf_axiom: theory -> thm -> thm list |
11 val pairname: thm -> string * thm |
11 val pairname: thm -> string * thm |
12 val multi_base_blacklist: string list |
12 val multi_base_blacklist: string list |
13 val bad_for_atp: thm -> bool |
13 val bad_for_atp: thm -> bool |
14 val type_has_empty_sort: typ -> bool |
14 val type_has_empty_sort: typ -> bool |
15 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
15 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
16 val neg_clausify: thm list -> thm list |
16 val neg_clausify: thm list -> thm list |
17 val expand_defs_tac: thm -> tactic |
17 val expand_defs_tac: thm -> tactic |
18 val combinators: thm -> thm |
18 val combinators: thm -> thm |
19 val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list |
19 val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list |
20 val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
20 val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
21 val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
21 val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
22 val atpset_rules_of: Proof.context -> (string * thm) list |
22 val atpset_rules_of: Proof.context -> (string * thm) list |
23 val meson_method_setup: theory -> theory |
|
24 val clause_cache_endtheory: theory -> theory option |
|
25 val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) |
23 val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) |
26 val setup: theory -> theory |
24 val setup: theory -> theory |
27 end; |
25 end; |
28 |
26 |
29 structure ResAxioms: RES_AXIOMS = |
27 structure ResAxioms: RES_AXIOMS = |
159 |
157 |
160 val lambda_free = not o Term.has_abs; |
158 val lambda_free = not o Term.has_abs; |
161 |
159 |
162 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); |
160 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); |
163 |
161 |
164 val abs_S = @{thm"abs_S"}; |
162 val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B})); |
165 val abs_K = @{thm"abs_K"}; |
163 val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C})); |
166 val abs_I = @{thm"abs_I"}; |
164 val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S})); |
167 val abs_B = @{thm"abs_B"}; |
|
168 val abs_C = @{thm"abs_C"}; |
|
169 |
|
170 val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B)); |
|
171 val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C)); |
|
172 val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S)); |
|
173 |
165 |
174 (*FIXME: requires more use of cterm constructors*) |
166 (*FIXME: requires more use of cterm constructors*) |
175 fun abstract ct = |
167 fun abstract ct = |
176 let val _ = Output.debug (fn()=>" abstraction: " ^ Display.string_of_cterm ct) |
168 let val _ = Output.debug (fn()=>" abstraction: " ^ Display.string_of_cterm ct) |
177 val Abs(x,_,body) = term_of ct |
169 val Abs(x,_,body) = term_of ct |
178 val thy = theory_of_cterm ct |
170 val thy = theory_of_cterm ct |
179 val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) |
171 val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) |
180 val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
172 val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
181 fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K |
173 fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} |
182 in |
174 in |
183 case body of |
175 case body of |
184 Const _ => makeK() |
176 Const _ => makeK() |
185 | Free _ => makeK() |
177 | Free _ => makeK() |
186 | Var _ => makeK() (*though Var isn't expected*) |
178 | Var _ => makeK() (*though Var isn't expected*) |
187 | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*) |
179 | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) |
188 | rator$rand => |
180 | rator$rand => |
189 if loose_bvar1 (rator,0) then (*C or S*) |
181 if loose_bvar1 (rator,0) then (*C or S*) |
190 if loose_bvar1 (rand,0) then (*S*) |
182 if loose_bvar1 (rand,0) then (*S*) |
191 let val crator = cterm_of thy (Abs(x,xT,rator)) |
183 let val crator = cterm_of thy (Abs(x,xT,rator)) |
192 val crand = cterm_of thy (Abs(x,xT,rand)) |
184 val crand = cterm_of thy (Abs(x,xT,rand)) |
193 val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S |
185 val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} |
194 val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
186 val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
195 in |
187 in |
196 Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
188 Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
197 end |
189 end |
198 else (*C*) |
190 else (*C*) |
199 let val crator = cterm_of thy (Abs(x,xT,rator)) |
191 let val crator = cterm_of thy (Abs(x,xT,rator)) |
200 val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C |
192 val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} |
201 val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
193 val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
202 in |
194 in |
203 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
195 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
204 end |
196 end |
205 else if loose_bvar1 (rand,0) then (*B or eta*) |
197 else if loose_bvar1 (rand,0) then (*B or eta*) |
206 if rand = Bound 0 then eta_conversion ct |
198 if rand = Bound 0 then eta_conversion ct |
207 else (*B*) |
199 else (*B*) |
208 let val crand = cterm_of thy (Abs(x,xT,rand)) |
200 let val crand = cterm_of thy (Abs(x,xT,rand)) |
209 val crator = cterm_of thy rator |
201 val crator = cterm_of thy rator |
210 val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B |
202 val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} |
211 val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
203 val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
212 in |
204 in |
213 Thm.transitive abs_B' (Conv.arg_conv abstract rhs) |
205 Thm.transitive abs_B' (Conv.arg_conv abstract rhs) |
214 end |
206 end |
215 else makeK() |
207 else makeK() |
216 | _ => error "abstract: Bad term" |
208 | _ => error "abstract: Bad term" |
233 in Output.debug (fn()=>" abstraction result: " ^ Display.string_of_thm comb_eq); |
225 in Output.debug (fn()=>" abstraction result: " ^ Display.string_of_thm comb_eq); |
234 (transitive (abstract_rule v cv u_th) comb_eq) end |
226 (transitive (abstract_rule v cv u_th) comb_eq) end |
235 | t1 $ t2 => |
227 | t1 $ t2 => |
236 let val (ct1,ct2) = Thm.dest_comb ct |
228 let val (ct1,ct2) = Thm.dest_comb ct |
237 in combination (combinators_aux ct1) (combinators_aux ct2) end; |
229 in combination (combinators_aux ct1) (combinators_aux ct2) end; |
238 |
230 |
239 fun combinators th = |
231 fun combinators th = |
240 if lambda_free (prop_of th) then th |
232 if lambda_free (prop_of th) then th |
241 else |
233 else |
242 let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); |
234 let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); |
243 val th = Drule.eta_contraction_rule th |
235 val th = Drule.eta_contraction_rule th |
244 val eqth = combinators_aux (cprop_of th) |
236 val eqth = combinators_aux (cprop_of th) |
245 val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); |
237 val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); |
246 in equal_elim eqth th end |
238 in equal_elim eqth th end |
247 handle THM (msg,_,_) => |
239 handle THM (msg,_,_) => |
248 (warning ("Error in the combinator translation of " ^ Display.string_of_thm th); |
240 (warning ("Error in the combinator translation of " ^ Display.string_of_thm th); |
249 warning (" Exception message: " ^ msg); |
241 warning (" Exception message: " ^ msg); |
250 TrueI); (*A type variable of sort {} will cause make abstraction fail.*) |
242 TrueI); (*A type variable of sort {} will cause make abstraction fail.*) |
251 |
243 |
252 (*cterms are used throughout for efficiency*) |
244 (*cterms are used throughout for efficiency*) |
318 then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) |
310 then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) |
319 else excessive_lambdas (t, max_lambda_nesting); |
311 else excessive_lambdas (t, max_lambda_nesting); |
320 |
312 |
321 (*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*) |
313 (*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*) |
322 val max_apply_depth = 15; |
314 val max_apply_depth = 15; |
323 |
315 |
324 fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1) |
316 fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1) |
325 | apply_depth (Abs(_,_,t)) = apply_depth t |
317 | apply_depth (Abs(_,_,t)) = apply_depth t |
326 | apply_depth _ = 0; |
318 | apply_depth _ = 0; |
327 |
319 |
328 fun too_complex t = |
320 fun too_complex t = |
329 apply_depth t > max_apply_depth orelse |
321 apply_depth t > max_apply_depth orelse |
330 Meson.too_many_clauses NONE t orelse |
322 Meson.too_many_clauses NONE t orelse |
331 excessive_lambdas_fm [] t; |
323 excessive_lambdas_fm [] t; |
332 |
324 |
333 fun is_strange_thm th = |
325 fun is_strange_thm th = |
334 case head_of (concl_of th) of |
326 case head_of (concl_of th) of |
335 Const (a,_) => (a <> "Trueprop" andalso a <> "==") |
327 Const (a,_) => (a <> "Trueprop" andalso a <> "==") |
336 | _ => false; |
328 | _ => false; |
337 |
329 |
338 fun bad_for_atp th = |
330 fun bad_for_atp th = |
339 PureThy.is_internal th |
331 PureThy.is_internal th |
340 orelse too_complex (prop_of th) |
332 orelse too_complex (prop_of th) |
341 orelse exists_type type_has_empty_sort (prop_of th) |
333 orelse exists_type type_has_empty_sort (prop_of th) |
342 orelse is_strange_thm th; |
334 orelse is_strange_thm th; |
343 |
335 |
344 val multi_base_blacklist = |
336 val multi_base_blacklist = |
345 ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm", |
337 ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm", |
346 "cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*) |
338 "cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*) |
354 |
346 |
355 fun name_or_string th = |
347 fun name_or_string th = |
356 if PureThy.has_name_hint th then PureThy.get_name_hint th |
348 if PureThy.has_name_hint th then PureThy.get_name_hint th |
357 else Display.string_of_thm th; |
349 else Display.string_of_thm th; |
358 |
350 |
|
351 (*Skolemize a named theorem, with Skolem functions as additional premises.*) |
|
352 fun skolem_thm (s, th) = |
|
353 if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then [] |
|
354 else |
|
355 let |
|
356 val ctxt0 = Variable.thm_context th |
|
357 val (nnfth, ctxt1) = to_nnf th ctxt0 |
|
358 val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 |
|
359 in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end |
|
360 handle THM _ => []; |
|
361 |
359 (*Declare Skolem functions for a theorem, supplied in nnf and with its name. |
362 (*Declare Skolem functions for a theorem, supplied in nnf and with its name. |
360 It returns a modified theory, unless skolemization fails.*) |
363 It returns a modified theory, unless skolemization fails.*) |
361 fun skolem th0 thy = |
364 fun skolem (name, th0) thy = |
362 let |
365 let |
363 val th = Thm.transfer thy th0 |
366 val th = Thm.transfer thy th0 |
364 val ctxt0 = Variable.thm_context th |
367 val ctxt0 = Variable.thm_context th |
365 val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th) |
|
366 in |
368 in |
367 Option.map |
369 try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) => |
368 (fn (nnfth,ctxt1) => |
370 let |
369 let |
371 val s = flatten_name name |
370 val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth) |
372 val (defs, thy') = declare_skofuns s nnfth thy |
371 val s = fake_name th |
373 val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 |
372 val (defs,thy') = declare_skofuns s nnfth thy |
374 val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |
373 val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 |
375 |> Meson.finish_cnf |> map Thm.close_derivation |
374 val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") |
376 in (cnfs', thy') end |
375 val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |
377 handle Clausify_failure thy_e => ([], thy_e)) (* FIXME !? *) |
376 |> Meson.finish_cnf |> map Thm.close_derivation |
|
377 in (cnfs', thy') end |
|
378 handle Clausify_failure thy_e => ([],thy_e) |
|
379 ) |
|
380 (try (to_nnf th) ctxt0) |
|
381 end; |
378 end; |
382 |
379 |
383 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of |
380 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of |
384 Skolem functions.*) |
381 Skolem functions.*) |
385 structure ThmCache = TheoryDataFun |
382 structure ThmCache = TheoryDataFun |
386 ( |
383 ( |
387 type T = thm list Thmtab.table; |
384 type T = thm list Thmtab.table * unit Symtab.table |
388 val empty = Thmtab.empty; |
385 val empty = (Thmtab.empty, Symtab.empty) |
389 val copy = I; |
386 val copy = I; |
390 val extend = I; |
387 val extend = I; |
391 fun merge _ tabs : T = Thmtab.merge (K true) tabs; |
388 fun merge _ ((cache1, seen1), (cache2, seen2)) : T = |
|
389 (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); |
392 ); |
390 ); |
393 |
391 |
394 (*Populate the clause cache using the supplied theorem. Return the clausal form |
392 val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; |
395 and modified theory.*) |
393 val already_seen = Symtab.defined o #2 o ThmCache.get; |
396 fun skolem_cache_thm th thy = |
394 |
397 case Thmtab.lookup (ThmCache.get thy) th of |
395 val update_cache = ThmCache.map o apfst o Thmtab.update; |
398 NONE => |
396 fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); |
399 (case skolem th thy of |
|
400 NONE => ([th],thy) |
|
401 | SOME (cls,thy') => |
|
402 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ |
|
403 " clauses inserted into cache: " ^ name_or_string th); |
|
404 (cls, ThmCache.map (Thmtab.update (th,cls)) thy'))) |
|
405 | SOME cls => (cls,thy); |
|
406 |
|
407 (*Skolemize a named theorem, with Skolem functions as additional premises.*) |
|
408 fun skolem_thm (s,th) = |
|
409 if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then [] |
|
410 else |
|
411 let val ctxt0 = Variable.thm_context th |
|
412 val (nnfth,ctxt1) = to_nnf th ctxt0 |
|
413 val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 |
|
414 in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end |
|
415 handle THM _ => []; |
|
416 |
397 |
417 (*Exported function to convert Isabelle theorems into axiom clauses*) |
398 (*Exported function to convert Isabelle theorems into axiom clauses*) |
418 fun cnf_axiom thy th0 = |
399 fun cnf_axiom thy th0 = |
419 let val th = Thm.transfer thy th0 |
400 let val th = Thm.transfer thy th0 in |
420 in |
401 case lookup_cache thy th of |
421 case Thmtab.lookup (ThmCache.get thy) th of |
402 NONE => map Thm.close_derivation (skolem_thm (fake_name th, th)) |
422 NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); |
403 | SOME cls => cls |
423 map Thm.close_derivation (skolem_thm (fake_name th, th))) |
404 end; |
424 | SOME cls => cls |
405 |
425 end; |
406 |
|
407 (**** Extract and Clausify theorems from a theory's claset and simpset ****) |
426 |
408 |
427 fun pairname th = (PureThy.get_name_hint th, th); |
409 fun pairname th = (PureThy.get_name_hint th, th); |
428 |
|
429 (**** Extract and Clausify theorems from a theory's claset and simpset ****) |
|
430 |
410 |
431 fun rules_of_claset cs = |
411 fun rules_of_claset cs = |
432 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs |
412 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs |
433 val intros = safeIs @ hazIs |
413 val intros = safeIs @ hazIs |
434 val elims = map Classical.classical_rule (safeEs @ hazEs) |
414 val elims = map Classical.classical_rule (safeEs @ hazEs) |
465 |
445 |
466 (*The combination of rev and tail recursion preserves the original order*) |
446 (*The combination of rev and tail recursion preserves the original order*) |
467 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); |
447 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); |
468 |
448 |
469 |
449 |
470 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) |
450 (**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****) |
471 |
451 |
472 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*) |
452 (*Populate the clause cache using the supplied theorem. Return the clausal form |
473 |
453 and modified theory.*) |
474 val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; |
454 fun skolem_cache_thm (name, th) thy = |
475 |
455 if bad_for_atp th then thy |
476 fun skolem_cache th thy = |
456 else |
477 if bad_for_atp th then thy else #2 (skolem_cache_thm th thy); |
457 (case lookup_cache thy th of |
478 |
458 SOME _ => thy |
479 fun skolem_cache_list (a,ths) thy = |
459 | NONE => |
480 if (Sign.base_name a) mem_string multi_base_blacklist then thy |
460 (case skolem (name, th) thy of |
481 else fold skolem_cache ths thy; |
461 NONE => thy |
482 |
462 | SOME (cls, thy') => update_cache (th, cls) thy')); |
483 val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of; |
463 |
484 fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; |
464 fun skolem_cache_fact (name, ths) (changed, thy) = |
485 fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; |
465 if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name |
|
466 then (changed, thy) |
|
467 else (true, thy |> mark_seen name |> fold skolem_cache_thm (PureThy.name_multi name ths)); |
|
468 |
|
469 fun saturate_skolem_cache thy = |
|
470 (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of |
|
471 (false, _) => NONE |
|
472 | (true, thy') => SOME thy'); |
|
473 |
|
474 |
|
475 val suppress_endtheory = ref false; |
|
476 |
|
477 fun clause_cache_endtheory thy = |
|
478 if ! suppress_endtheory then NONE |
|
479 else saturate_skolem_cache thy; |
|
480 |
486 |
481 |
487 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
482 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
488 lambda_free, but then the individual theory caches become much bigger.*) |
483 lambda_free, but then the individual theory caches become much bigger.*) |
489 |
|
490 val suppress_endtheory = ref false; |
|
491 |
|
492 (*The new constant is a hack to prevent multiple execution*) |
|
493 fun clause_cache_endtheory thy = |
|
494 if !suppress_endtheory then NONE |
|
495 else |
|
496 (Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy); |
|
497 Option.map skolem_cache_node (try mark_skolemized thy) ); |
|
498 |
484 |
499 |
485 |
500 (*** meson proof methods ***) |
486 (*** meson proof methods ***) |
501 |
487 |
502 (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) |
488 (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) |
571 (Method.insert_tac |
550 (Method.insert_tac |
572 (map forall_intr_vars (neg_clausify hyps)) 1)), |
551 (map forall_intr_vars (neg_clausify hyps)) 1)), |
573 REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
552 REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
574 end); |
553 end); |
575 |
554 |
576 |
|
577 (** The Skolemization attribute **) |
|
578 |
|
579 fun conj2_rule (th1,th2) = conjI OF [th1,th2]; |
|
580 |
|
581 (*Conjoin a list of theorems to form a single theorem*) |
|
582 fun conj_rule [] = TrueI |
|
583 | conj_rule ths = foldr1 conj2_rule ths; |
|
584 |
|
585 fun skolem_attr (Context.Theory thy, th) = |
|
586 let val (cls, thy') = skolem_cache_thm th thy |
|
587 in (Context.Theory thy', conj_rule cls) end |
|
588 | skolem_attr (context, th) = (context, th) |
|
589 |
|
590 val setup_attrs = Attrib.add_attributes |
|
591 [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), |
|
592 ("clausify", clausify, "conversion of theorem to clauses")]; |
|
593 |
|
594 val setup_methods = Method.add_methods |
555 val setup_methods = Method.add_methods |
595 [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), |
556 [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), |
596 "conversion of goal to conjecture clauses")]; |
557 "conversion of goal to conjecture clauses")]; |
597 |
558 |
598 val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods; |
559 |
|
560 (** Attribute for converting a theorem into clauses **) |
|
561 |
|
562 val clausify = Attrib.syntax (Scan.lift Args.nat |
|
563 >> (fn i => Thm.rule_attribute (fn context => fn th => |
|
564 Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))); |
|
565 |
|
566 val setup_attrs = Attrib.add_attributes |
|
567 [("clausify", clausify, "conversion of theorem to clauses")]; |
|
568 |
|
569 |
|
570 |
|
571 (** setup **) |
|
572 |
|
573 val setup = |
|
574 meson_method_setup #> |
|
575 setup_methods #> |
|
576 setup_attrs #> |
|
577 perhaps saturate_skolem_cache #> |
|
578 Theory.at_end clause_cache_endtheory; |
599 |
579 |
600 end; |
580 end; |
|
581 |