This is an old revision of the document!
Table of Contents
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)$.