DECIDE : term -> thm
STRUCTURE
SYNOPSIS
Invoke decision procedure(s).
DESCRIPTION
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.
SEEALSO
HOL  Kananaskis-14