equal
deleted
inserted
replaced
486 fun TRACE ctxt rl tac i st = |
486 fun TRACE ctxt rl tac i st = |
487 (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st); |
487 (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st); |
488 |
488 |
489 (*Resolution/matching tactics: if upd then the proof state may be updated. |
489 (*Resolution/matching tactics: if upd then the proof state may be updated. |
490 Matching makes the tactics more deterministic in the presence of Vars.*) |
490 Matching makes the tactics more deterministic in the presence of Vars.*) |
491 fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]); |
491 fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac ctxt [rl]); |
492 fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]); |
492 fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac ctxt [rl]); |
493 |
493 |
494 (*Tableau rule from elimination rule. |
494 (*Tableau rule from elimination rule. |
495 Flag "upd" says that the inference updated the branch. |
495 Flag "upd" says that the inference updated the branch. |
496 Flag "dup" requests duplication of the affected formula.*) |
496 Flag "dup" requests duplication of the affected formula.*) |
497 fun fromRule (state as State {ctxt, ...}) vars rl = |
497 fun fromRule (state as State {ctxt, ...}) vars rl = |
779 exception NEWBRANCHES and CLOSEF; |
779 exception NEWBRANCHES and CLOSEF; |
780 |
780 |
781 exception PROVE; |
781 exception PROVE; |
782 |
782 |
783 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) |
783 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) |
784 val contr_tac = ematch_tac [Data.notE] THEN' |
784 fun contr_tac ctxt = |
785 (eq_assume_tac ORELSE' assume_tac); |
785 ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac); |
786 |
786 |
787 (*Try to unify complementary literals and return the corresponding tactic. *) |
787 (*Try to unify complementary literals and return the corresponding tactic. *) |
788 fun tryClose state (G, L) = |
788 fun tryClose state (G, L) = |
789 let |
789 let |
790 val State {ctxt, ...} = state; |
790 val State {ctxt, ...} = state; |
793 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; |
793 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; |
794 fun arg (_ $ t) = t; |
794 fun arg (_ $ t) = t; |
795 in |
795 in |
796 if isGoal G then close (arg G) L eAssume_tac |
796 if isGoal G then close (arg G) L eAssume_tac |
797 else if isGoal L then close G (arg L) eAssume_tac |
797 else if isGoal L then close G (arg L) eAssume_tac |
798 else if isNot G then close (arg G) L eContr_tac |
798 else if isNot G then close (arg G) L (eContr_tac ctxt) |
799 else if isNot L then close G (arg L) eContr_tac |
799 else if isNot L then close G (arg L) (eContr_tac ctxt) |
800 else NONE |
800 else NONE |
801 end; |
801 end; |
802 |
802 |
803 (*Were there Skolem terms in the premise? Must NOT chase Vars*) |
803 (*Were there Skolem terms in the premise? Must NOT chase Vars*) |
804 fun hasSkolem (Skolem _) = true |
804 fun hasSkolem (Skolem _) = true |