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

.