=====Attribute Examples=====

This page contains usage examples for attributes (or directives).

==== of ====
Consider rule/theorem ''mp'':

$\quad [|\ ?P \longrightarrow ?Q; ?P\ |] \Longrightarrow ?Q$.

Using
    mp [of _ "C ∨ D"]
yields the more specific theorem

$\quad [|\ ?P \longrightarrow C \vee D; ?P\ |] \Longrightarrow C \vee D$.

Note that $C, D$ are no longer schematic variables but specific terms.
==== where ====

Consider rule/theorem ''mp'':

$\quad [|\ ?P \longrightarrow ?Q; ?P\ |] \Longrightarrow ?Q$.

Using
    mp [where Q="C ∨ D"]
yields the more specific theorem

$\quad [|\ ?P \longrightarrow C \vee D; ?P\ |] \Longrightarrow C \vee D$.

Note that $C, D$ are no longer schematic variables but specific terms.
==== THEN ====

Consider the "composite" theorem

$\quad t :  (?A \vee \neg ?A) \wedge (\text{False} \longrightarrow ?A)$

Then,

    t [THEN conjunct1]

yields the new theorem

$\quad ?A \vee \neg ?A$
==== OF ====
Consider rule ''subst'':

$\quad [|\ ?s = ?t; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

Note that you can use this rule only to substitute from left to right, not the reverse. Using ''OF'' together with theorem ''sym'' ($?s = ?t\ \Longrightarrow\ ?t = ?s$), i.e.

    subst [OF sym]

yields

$\quad [|\ ?t = ?s; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

which allows substitutions from right to left.
==== simplified ====
Consider theorem ''Nat.le_square'':

$\quad ?m \leq\ ?m\ \cdot\ ?m$

Using

     Nat.le_square [simplified]
you get

$\quad 0 <\ ?m \longrightarrow Suc\ 0 \leq\ ?m$

Wether or not this is actually "simpler" is certainly open to discussion, especially because the original form does say something about $?m=0$ while the ''simplified'' version does not.
==== rotated ====
Consider rule ''disjE'':

$\quad [|\ ?P\;\vee\; ?Q; ?P \Longrightarrow ?R; ?Q \Longrightarrow ?R\ |] \Longrightarrow ?R$.

Then, 

    disjE [rotated 2]
yields

$\quad [|\ ?Q \Longrightarrow ?R; ?P\;\vee\; ?Q; ?P \Longrightarrow ?R\ |] \Longrightarrow ?R$.
==== symmetric =====
Consider the definition of set membership ''Set.mem_def'',

$\quad (?x \in ?A) = ?A ?x$.

Then,

     test [symmetric]   
yields

$\quad ?X ?x = (?x \in ?X)$.