Filter
Top Products
9.5. OTHER RULES 79
9.5 Other rules
As well as these handy general-purpose rules, there are some special ones for par-
ticular theories, described later. For example, ARITH RULE is useful for disposing of
trivial facts of linear arithmetic over the natural numbers:
#ARITH_RULE ‘x < y ==> 4 * x + 3 < 4 * y‘;;
it : thm = |- x < y ==> 4 * x + 3 < 4 * y
Another easy rule, TAUT, proves propositional tautologies automatically, e.g.
#TAUT ‘p /\ q ==> p‘;;
it : thm = |- p /\ q ==> p
#TAUT ‘(p ==> q) \/ (q ==> p)‘;;
it : thm = |- (p ==> q) \/ (q ==> p)