User Tools
reference:frule
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
reference:frule [2011/06/22 12:33] 131.246.161.187 created |
reference:frule [2011/06/22 12:37] (current) 131.246.161.187 [Relatives] |
||
|---|---|---|---|
| Line 26: | Line 26: | ||
| Applying ''apply (drule mp)'' yields new goals | Applying ''apply (drule mp)'' yields new goals | ||
| - | $\quad A \Longrightarrow A$ | + | $\quad [|\ A \longrightarrow B; A\ |] \Longrightarrow A$ |
| - | $\quad[|\ A; B\ |] \Longrightarrow B$ | + | $\quad[|\ A \longrightarrow B; A; B\ |] \Longrightarrow B$ |
| - | which can both be solved by ''[[assumption]]''. Note that ''apply (drule(2) mp)'' is a shortcut for this and immediately solves the goal. | + | which can both be solved by ''[[assumption]]''. Note that ''apply (frule(2) mp)'' is a shortcut for this and immediately solves the goal. |
| ==== Non-Example ==== | ==== Non-Example ==== | ||
| ==== Variants ==== | ==== Variants ==== | ||
| - | === drule_tac === | + | === frule_tac === |
| - | With ''drule_tac'', you can force [[schematic variable|schematic variables]] in the used rule to take specific values. The extended syntax is: | + | With ''frule_tac'', you can force [[schematic variable|schematic variables]] in the used rule to take specific values. The extended syntax is: |
| - | apply (drule_tac ident1="expr1" and ident2="expr1" and ... in rule) | + | apply (frule_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 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''. | ||
| - | === drule(k) === | + | === frule(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 ''drule(k)'' which forces Isabelle to apply ''assumption'' $k$ times after the rule application. | + | 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 ''frule(k)'' which forces Isabelle to apply ''assumption'' $k$ times after the rule application. |
| ==== Relatives ==== | ==== Relatives ==== | ||
| * ''[[rule]]'' | * ''[[rule]]'' | ||
| + | * ''[[drule]]'' | ||
| * ''[[erule]]'' | * ''[[erule]]'' | ||
| - | * ''[[frule]]'' | ||
reference/frule.1308738801.txt.gz · Last modified: 2011/06/22 12:33 by 131.246.161.187
Page Tools
