equal
deleted
inserted
replaced
461 (*** Converting a subgoal into negated conjecture clauses. ***) |
461 (*** Converting a subgoal into negated conjecture clauses. ***) |
462 |
462 |
463 fun neg_skolemize_tac ctxt = |
463 fun neg_skolemize_tac ctxt = |
464 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]; |
465 |
465 |
466 val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf; |
466 val neg_clausify = |
|
467 Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf; |
467 |
468 |
468 fun neg_conjecture_clauses ctxt st0 n = |
469 fun neg_conjecture_clauses ctxt st0 n = |
469 let |
470 let |
470 val st = Seq.hd (neg_skolemize_tac ctxt n st0) |
471 val st = Seq.hd (neg_skolemize_tac ctxt n st0) |
471 val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st |
472 val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st |