User Tools
reference:rule_method
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
reference:rule_method [2011/06/13 22:01] 178.26.109.100 created |
reference:rule_method [2011/06/22 12:27] (current) 131.246.161.187 [Example] |
||
|---|---|---|---|
| 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 ==== | ||
reference/rule_method.1307995264.txt.gz · Last modified: 2011/06/13 22:01 by 178.26.109.100
Page Tools
