done first attempts to close the goal using contradiction. If this fails, it creates an SMT state and will repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas ps) and congruence closure.
safe_core s ps cfg opt negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas s), and then tries contradiction.
If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas ps) and congruence closure.
safe_core is complete for propositional logic. Depending on the form of opt it will:
clarify is safe_core, but with the (opt : case_option) parameter fixed at case_option.at_most_one.
safe is safe_core, but with the (opt : case_option) parameter fixed at case_option.accept.
finish is safe_core, but with the (opt : case_option) parameter fixed at case_option.force.
iclarify is like clarify, but only uses intuitionistic logic.
isafe is like safe, but only uses intuitionistic logic.
ifinish is like finish, but only uses intuitionistic logic.
clarify [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.
If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.
clarify is complete for propositional logic.
Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
clarify will fail if it produces more than one goal.
safe [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.
If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.
safe is complete for propositional logic.
Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
safe ignores the number of goals it produces, and should never fail.
finish [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.
If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.
finish is complete for propositional logic.
Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
finish will fail if it does not close the goal.
iclarify is like clarify, but only uses intuitionistic logic.
isafe is like safe, but only uses intuitionistic logic.
ifinish is like finish, but only uses intuitionistic logic.