equal
deleted
inserted
replaced
485 fun meson_general_tac ths i st0 = |
485 fun meson_general_tac ths i st0 = |
486 let |
486 let |
487 val thy = Thm.theory_of_thm st0 |
487 val thy = Thm.theory_of_thm st0 |
488 in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end; |
488 in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end; |
489 |
489 |
490 val meson_method_setup = Method.add_methods |
490 val meson_method_setup = |
491 [("meson", Method.thms_args (fn ths => |
491 Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ => |
492 SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), |
492 SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths))) |
493 "MESON resolution proof procedure")]; |
493 "MESON resolution proof procedure"; |
494 |
494 |
495 |
495 |
496 (*** Converting a subgoal into negated conjecture clauses. ***) |
496 (*** Converting a subgoal into negated conjecture clauses. ***) |
497 |
497 |
498 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; |
498 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; |
519 (Method.insert_tac |
519 (Method.insert_tac |
520 (map forall_intr_vars (neg_clausify hyps)) 1)), |
520 (map forall_intr_vars (neg_clausify hyps)) 1)), |
521 REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
521 REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
522 end); |
522 end); |
523 |
523 |
524 val setup_methods = Method.add_methods |
524 val setup_methods = |
525 [("neg_clausify", Method.no_args (SIMPLE_METHOD' neg_clausify_tac), |
525 Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac))) |
526 "conversion of goal to conjecture clauses")]; |
526 "conversion of goal to conjecture clauses"; |
527 |
527 |
528 |
528 |
529 (** Attribute for converting a theorem into clauses **) |
529 (** Attribute for converting a theorem into clauses **) |
530 |
530 |
531 val clausify = Attrib.syntax (Scan.lift OuterParse.nat |
531 val clausify = Attrib.syntax (Scan.lift OuterParse.nat |