This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
reference:attribute_examples [2011/07/06 13:07] 131.246.161.187 [THEN] |
reference:attribute_examples [2011/07/25 12:32] (current) 131.246.41.159 [rotated] |
||
---|---|---|---|
Line 9: | Line 9: | ||
Using | Using | ||
- | | ||
mp [of _ "C ∨ D"] | mp [of _ "C ∨ D"] | ||
- | | ||
yields the more specific theorem | yields the more specific theorem | ||
Line 24: | Line 22: | ||
Using | Using | ||
- | | ||
mp [where Q="C ∨ D"] | mp [where Q="C ∨ D"] | ||
- | | ||
yields the more specific theorem | yields the more specific theorem | ||
Line 60: | Line 56: | ||
which allows substitutions from right to left. | which allows substitutions from right to left. | ||
==== simplified ==== | ==== 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 ==== | ==== rotated ==== | ||
Consider rule ''disjE'': | Consider rule ''disjE'': | ||
- | $\quad [|\ ?P \vee ?Q; ?P \Longrightarrow ?R; ?Q \Longrightarrow ?R\ |] \Longrightarrow ?R$. | + | $\quad [|\ ?P\;\vee\; ?Q; ?P \Longrightarrow ?R; ?Q \Longrightarrow ?R\ |] \Longrightarrow ?R$. |
Then, | Then, | ||
disjE [rotated 2] | disjE [rotated 2] | ||
- | | ||
yields | yields | ||
- | $\quad [\ ?Q \Longrightarrow ?R; ?P \vee ?Q; ?P \Longrightarrow ?R\ |] \Longrightarrow ?R$. | + | $\quad [|\ ?Q \Longrightarrow ?R; ?P\;\vee\; ?Q; ?P \Longrightarrow ?R\ |] \Longrightarrow ?R$. |
==== symmetric ===== | ==== symmetric ===== | ||
Consider the definition of set membership ''Set.mem_def'', | Consider the definition of set membership ''Set.mem_def'', | ||
Line 79: | Line 86: | ||
Then, | Then, | ||
- | test [symmetric] | + | test [symmetric] |
- | + | ||
yields | yields | ||
$\quad ?X ?x = (?x \in ?X)$. | $\quad ?X ?x = (?x \in ?X)$. |