Differences

This shows you the differences between two versions of the page.

--- reference:attribute_examples [2011/07/06 12:41] – [of] 131.246.161.187
+++ reference:attribute_examples [2011/07/25 12:32] (current) – [rotated] 131.246.41.159
@@ Line 9: / Line 9: @@
 Using
     mp [of _ "C ∨ D"]
 yields the more specific theorem
@@ Line 18: / Line 16: @@
 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'':
@@ Line 34: / Line 56: @@
 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)$.