User Tools

Site Tools


reference:rule_method

Differences

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

Link to this comparison view

Next revision Both sides next revision
reference:rule_method [2011/06/13 22:01]
178.26.109.100 created
reference:rule_method [2011/06/22 11:59]
131.246.161.187
Line 12: Line 12:
  
 Then, ''​rule''​ does the following: Then, ''​rule''​ does the following:
-  * [[unification|Unify]] $C$ and $Q$. The application fails if there is no unifiert; otherwise, let $U$ be this unifier.+  * [[unification|Unify]] $C$ and $Q$. The application fails if there is no unifier; otherwise, let $U$ be this unifier.
   * Remove the old subgoal and create one new subgoal \\ \\ $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ \\ for each $k = 1, \dots, n$.   * Remove the old subgoal and create one new subgoal \\ \\ $\quad\bigwedge x_1 \dots x_k : [|\ U(A_1); \dots ; U(A_m)\ |] \Longrightarrow U(P_k)$ \\ \\ for each $k = 1, \dots, n$.
  
Line 23: Line 23:
 With ''​rule_tac'',​ you can force [[schematic variable|schematic variables]] in the used rule to take specific values. The extended syntax is: With ''​rule_tac'',​ you can force [[schematic variable|schematic variables]] in the used rule to take specific values. The extended syntax is:
   apply (rule_tac ident1="​expr1"​ and ident2="​expr1"​ and ... in rule)   apply (rule_tac ident1="​expr1"​ and ident2="​expr1"​ and ... in rule)
-This means that the variables ​''?​ident1''​ is replaced by expression ''​expr1''​ and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''​thm rule''​.+This means that the variable ​''?​ident1''​ is replaced by expression ''​expr1''​ and similarly for the others. Note that you have to leave out the question mark marking schematic variables. Find out which variables a rule uses with ''​thm rule''​.
  
 ==== Relatives ==== ==== Relatives ====
reference/rule_method.txt ยท Last modified: 2011/06/22 12:27 by 131.246.161.187