# 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:27]131.246.161.187 [Example] 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 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$. ==== Example ==== ==== Example ==== + Assume we have a goal + + $\quad[|\ A |] \Longrightarrow A \vee B$ + + Applying ''​apply (rule disjI1)''​ yields the new subgoal + + $\quad [|\ A\ |] \Longrightarrow A$ + + which can obviously be solved by one application of ''​[[assumption]]''​. Note that ''​apply (rule(1) disjI)''​ is a shortcut for this and immediately solves the goal. + ==== Non-Example ==== ==== Non-Example ==== Line 23: Line 33: 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 ====