6 |
6 |
7 signature SLEDGEHAMMER_FACT_PREPROCESSOR = |
7 signature SLEDGEHAMMER_FACT_PREPROCESSOR = |
8 sig |
8 sig |
9 val trace: bool Unsynchronized.ref |
9 val trace: bool Unsynchronized.ref |
10 val trace_msg: (unit -> string) -> unit |
10 val trace_msg: (unit -> string) -> unit |
|
11 val skolem_prefix: string |
11 val cnf_axiom: theory -> thm -> thm list |
12 val cnf_axiom: theory -> thm -> thm list |
12 val pairname: thm -> string * thm |
13 val pairname: thm -> string * thm |
13 val multi_base_blacklist: string list |
14 val multi_base_blacklist: string list |
14 val bad_for_atp: thm -> bool |
15 val bad_for_atp: thm -> bool |
15 val type_has_topsort: typ -> bool |
16 val type_has_topsort: typ -> bool |
16 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
17 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list |
17 val neg_clausify: thm list -> thm list |
18 val neg_clausify: thm list -> thm list |
18 val expand_defs_tac: thm -> tactic |
|
19 val combinators: thm -> thm |
19 val combinators: thm -> thm |
20 val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list |
20 val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list |
21 val suppress_endtheory: bool Unsynchronized.ref |
21 val suppress_endtheory: bool Unsynchronized.ref |
22 (*for emergency use where endtheory causes problems*) |
22 (*for emergency use where endtheory causes problems*) |
23 val setup: theory -> theory |
23 val setup: theory -> theory |
24 end; |
24 end; |
25 |
25 |
26 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR = |
26 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR = |
27 struct |
27 struct |
28 |
28 |
|
29 open Sledgehammer_FOL_Clause |
|
30 |
29 val trace = Unsynchronized.ref false; |
31 val trace = Unsynchronized.ref false; |
30 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
32 fun trace_msg msg = if !trace then tracing (msg ()) else (); |
|
33 |
|
34 val skolem_prefix = "sko_" |
31 |
35 |
32 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th); |
36 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th); |
33 |
37 |
34 val type_has_topsort = Term.exists_subtype |
38 val type_has_topsort = Term.exists_subtype |
35 (fn TFree (_, []) => true |
39 (fn TFree (_, []) => true |
73 let |
77 let |
74 val nref = Unsynchronized.ref 0 (* FIXME ??? *) |
78 val nref = Unsynchronized.ref 0 (* FIXME ??? *) |
75 fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = |
79 fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = |
76 (*Existential: declare a Skolem function, then insert into body and continue*) |
80 (*Existential: declare a Skolem function, then insert into body and continue*) |
77 let |
81 let |
78 val cname = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) |
82 val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) |
79 val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) |
83 val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) |
80 val Ts = map type_of args0 |
84 val Ts = map type_of args0 |
81 val extraTs = rhs_extra_types (Ts ---> T) xtp |
85 val extraTs = rhs_extra_types (Ts ---> T) xtp |
82 val argsx = map (fn T => Free (gensym "vsk", T)) extraTs |
86 val argsx = map (fn T => Free (gensym "vsk", T)) extraTs |
83 val args = argsx @ args0 |
87 val args = argsx @ args0 |
108 (*Existential: declare a Skolem function, then insert into body and continue*) |
112 (*Existential: declare a Skolem function, then insert into body and continue*) |
109 let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) |
113 let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) |
110 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*) |
114 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*) |
111 val Ts = map type_of args |
115 val Ts = map type_of args |
112 val cT = Ts ---> T |
116 val cT = Ts ---> T |
113 val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count) |
117 val id = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count) |
114 val c = Free (id, cT) |
118 val c = Free (id, cT) |
115 val rhs = list_abs_free (map dest_Free args, |
119 val rhs = list_abs_free (map dest_Free args, |
116 HOLogic.choice_const T $ xtp) |
120 HOLogic.choice_const T $ xtp) |
117 (*Forms a lambda-abstraction over the formal parameters*) |
121 (*Forms a lambda-abstraction over the formal parameters*) |
118 val def = Logic.mk_equals (c, rhs) |
122 val def = Logic.mk_equals (c, rhs) |
384 |
388 |
385 fun cnf_rules_pairs_aux _ pairs [] = pairs |
389 fun cnf_rules_pairs_aux _ pairs [] = pairs |
386 | cnf_rules_pairs_aux thy pairs ((name,th)::ths) = |
390 | cnf_rules_pairs_aux thy pairs ((name,th)::ths) = |
387 let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs |
391 let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs |
388 handle THM _ => pairs | |
392 handle THM _ => pairs | |
389 Sledgehammer_FOL_Clause.CLAUSE _ => pairs |
393 CLAUSE _ => pairs |
390 in cnf_rules_pairs_aux thy pairs' ths end; |
394 in cnf_rules_pairs_aux thy pairs' ths end; |
391 |
395 |
392 (*The combination of rev and tail recursion preserves the original order*) |
396 (*The combination of rev and tail recursion preserves the original order*) |
393 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); |
397 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); |
394 |
398 |
395 |
399 |
396 (**** Convert all facts of the theory into clauses |
400 (**** Convert all facts of the theory into FOL or HOL clauses ****) |
397 (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****) |
|
398 |
401 |
399 local |
402 local |
400 |
403 |
401 fun skolem_def (name, th) thy = |
404 fun skolem_def (name, th) thy = |
402 let val ctxt0 = Variable.thm_context th in |
405 let val ctxt0 = Variable.thm_context th in |
453 |
456 |
454 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
457 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
455 lambda_free, but then the individual theory caches become much bigger.*) |
458 lambda_free, but then the individual theory caches become much bigger.*) |
456 |
459 |
457 |
460 |
458 (*** meson proof methods ***) |
|
459 |
|
460 (*Expand all new definitions of abstraction or Skolem functions in a proof state.*) |
|
461 fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a |
|
462 | is_absko _ = false; |
|
463 |
|
464 fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*) |
|
465 is_Free t andalso not (member (op aconv) xs t) |
|
466 | is_okdef _ _ = false |
|
467 |
|
468 (*This function tries to cope with open locales, which introduce hypotheses of the form |
|
469 Free == t, conjecture clauses, which introduce various hypotheses, and also definitions |
|
470 of sko_ functions. *) |
|
471 fun expand_defs_tac st0 st = |
|
472 let val hyps0 = #hyps (rep_thm st0) |
|
473 val hyps = #hyps (crep_thm st) |
|
474 val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps |
|
475 val defs = filter (is_absko o Thm.term_of) newhyps |
|
476 val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) |
|
477 (map Thm.term_of hyps) |
|
478 val fixed = OldTerm.term_frees (concl_of st) @ |
|
479 fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) [] |
|
480 in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; |
|
481 |
|
482 |
|
483 fun meson_general_tac ctxt ths i st0 = |
|
484 let |
|
485 val thy = ProofContext.theory_of ctxt |
|
486 val ctxt0 = Classical.put_claset HOL_cs ctxt |
|
487 in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end; |
|
488 |
|
489 val meson_method_setup = |
|
490 Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => |
|
491 SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) |
|
492 "MESON resolution proof procedure"; |
|
493 |
|
494 |
|
495 (*** Converting a subgoal into negated conjecture clauses. ***) |
461 (*** Converting a subgoal into negated conjecture clauses. ***) |
496 |
462 |
497 fun neg_skolemize_tac ctxt = |
463 fun neg_skolemize_tac ctxt = |
498 EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]; |
464 EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]; |
499 |
465 |
532 (fn i => Thm.rule_attribute (fn context => fn th => |
498 (fn i => Thm.rule_attribute (fn context => fn th => |
533 Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))) |
499 Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))) |
534 "conversion of theorem to clauses"; |
500 "conversion of theorem to clauses"; |
535 |
501 |
536 |
502 |
537 |
|
538 (** setup **) |
503 (** setup **) |
539 |
504 |
540 val setup = |
505 val setup = |
541 meson_method_setup #> |
|
542 neg_clausify_setup #> |
506 neg_clausify_setup #> |
543 clausify_setup #> |
507 clausify_setup #> |
544 perhaps saturate_skolem_cache #> |
508 perhaps saturate_skolem_cache #> |
545 Theory.at_end clause_cache_endtheory; |
509 Theory.at_end clause_cache_endtheory; |
546 |
510 |