539 |
539 |
540 fun skolemize_prems_tac prems = |
540 fun skolemize_prems_tac prems = |
541 cut_facts_tac (map (skolemize o make_nnf) prems) THEN' |
541 cut_facts_tac (map (skolemize o make_nnf) prems) THEN' |
542 REPEAT o (etac exE); |
542 REPEAT o (etac exE); |
543 |
543 |
544 (*Expand all definitions (presumably of Skolem functions) in a proof state.*) |
|
545 fun expand_defs_tac st = |
|
546 let val defs = filter (can dest_equals) (#hyps (crep_thm st)) |
|
547 in PRIMITIVE (LocalDefs.expand defs) st end; |
|
548 |
|
549 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. |
544 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. |
550 Function mkcl converts theorems to clauses.*) |
545 Function mkcl converts theorems to clauses.*) |
551 fun MESON mkcl cltac i st = |
546 fun MESON mkcl cltac i st = |
552 SELECT_GOAL |
547 SELECT_GOAL |
553 (EVERY [rtac ccontr 1, |
548 (EVERY [rtac ccontr 1, |
554 METAHYPS (fn negs => |
549 METAHYPS (fn negs => |
555 EVERY1 [skolemize_prems_tac negs, |
550 EVERY1 [skolemize_prems_tac negs, |
556 METAHYPS (cltac o mkcl)]) 1, |
551 METAHYPS (cltac o mkcl)]) 1]) i st |
557 expand_defs_tac]) i st |
552 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) |
558 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) |
|
559 |
553 |
560 (** Best-first search versions **) |
554 (** Best-first search versions **) |
561 |
555 |
562 (*ths is a list of additional clauses (HOL disjunctions) to use.*) |
556 (*ths is a list of additional clauses (HOL disjunctions) to use.*) |
563 fun best_meson_tac sizef = |
557 fun best_meson_tac sizef = |