User Tools
Table of Contents
Attribute Examples
This page contains usage examples for attributes (or directives).
of
Consider rule/theorem mp:
.
Using
mp [of _ "C ∨ D"]
yields the more specific theorem
.
Note that are no longer schematic variables but specific terms.
where
Consider rule/theorem mp:
.
Using
mp [where Q="C ∨ D"]
yields the more specific theorem
.
Note that are no longer schematic variables but specific terms.
THEN
Consider the “composite” theorem
Then,
t [THEN conjunct1]
yields the new theorem
OF
Consider rule subst:
Note that you can use this rule only to substitute from left to right, not the reverse. Using OF together with theorem sym (), i.e.
subst [OF sym]
yields
which allows substitutions from right to left.
simplified
Consider theorem Nat.le_square:
Using
Nat.le_square [simplified]
you get
Wether or not this is actually “simpler” is certainly open to discussion, especially because the original form does say something about while the simplified version does not.
rotated
Consider rule disjE:
.
Then,
disjE [rotated 2]
yields
.
symmetric
Consider the definition of set membership Set.mem_def,
.
Then,
test [symmetric]
yields
.
