DECIDE
bossLib.DECIDE : term -> thm
Invoke decision procedure(s).
An application DECIDE M, where M is a boolean term, attempts to
prove M using a propositional tautology checker and a linear
arithmetic decision procedure.
Failure
The invocation fails if M is not of boolean type. It also fails if M
is not a tautology or an instance of a theorem of linear arithmetic.
Example
> DECIDE (Term `p /\ p /\ r ==> r`);
val it = ⊢ p ∧ p ∧ r ⇒ r: thm
> DECIDE (Term `x < 17 /\ y < 26 ==> x + y < 17 + 26`);
val it = ⊢ x < 17 ∧ y < 26 ⇒ x + y < 17 + 26: thm
Comments
DECIDE is currently somewhat underpowered. Formerly it was implemented
by a cooperating decision procedure mechanism. However, most proofs
seemed to go somewhat smoother with simplification using the arith_ss
simpset, so we have adopted a simpler implementation. That should not be
taken as final, since cooperating decision procedures are an important
component in highly automated proof systems.