User Tools
reference:attribute_examples
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
reference:attribute_examples [2011/07/06 12:29] 131.246.161.187 created |
reference:attribute_examples [2011/07/25 12:32] (current) 131.246.41.159 [rotated] |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| ==== of ==== | ==== 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 ==== | ==== 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 ==== | ==== 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 ==== | ==== 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 ==== | ==== 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'': | ||
| + | |||
| + | $\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 ===== | ==== 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)$. | ||
reference/attribute_examples.1309948175.txt.gz · Last modified: 2011/07/06 12:29 by 131.246.161.187
Page Tools
