User Tools

Site Tools


reference:attribute_examples

Differences

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

Link to this comparison view

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)$.
reference/attribute_examples.1309950468.txt.gz · Last modified: 2011/07/06 13:07 by 131.246.161.187