# Isabelle/HOL Support Wiki

### Site Tools

reference:rule_method

# Differences

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

 reference:rule_method [2011/06/13 22:01]178.26.109.100 created reference:rule_method [2011/06/22 12:19]131.246.161.187 2011/06/22 12:27 [Example] 2011/06/22 12:19 2011/06/22 11:59 2011/06/13 22:01 created Next revision Previous revision 2011/06/22 12:27 [Example] 2011/06/22 12:19 2011/06/22 11:59 2011/06/13 22:01 created Last revision Both sides next revision 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''​. + + === rule(k) === + Oftentimes, a rule application results in several subgoals that can directly be solved by ''​[[assumption]]'';​ see [[#​Example|above]] for an example. Instead of applying ''​assumption''​ by hand, you can apply ''​rule(k)''​ which forces Isabelle to apply ''​assumption''​ $k$ times after the rule application. ==== Relatives ==== ==== Relatives ====