270 cutL_tac : string -> int -> tactic |
270 cutL_tac : string -> int -> tactic |
271 \end{ttbox} |
271 \end{ttbox} |
272 These tactics refine a subgoal into two by applying the cut rule. The cut |
272 These tactics refine a subgoal into two by applying the cut rule. The cut |
273 formula is given as a string, and replaces some other formula in the sequent. |
273 formula is given as a string, and replaces some other formula in the sequent. |
274 \begin{description} |
274 \begin{description} |
275 \item[\ttindexbold{cutR_tac} {\it formula} {\it i}] |
275 \item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] |
276 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It |
276 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It |
277 then deletes some formula from the right side of subgoal~$i$, replacing |
277 then deletes some formula from the right side of subgoal~$i$, replacing |
278 that formula by~$P$. |
278 that formula by~$P$. |
279 |
279 |
280 \item[\ttindexbold{cutL_tac} {\it formula} {\it i}] |
280 \item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] |
281 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It |
281 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It |
282 then deletes some formula from the let side of the new subgoal $i+1$, |
282 then deletes some formula from the let side of the new subgoal $i+1$, |
283 replacing that formula by~$P$. |
283 replacing that formula by~$P$. |
284 \end{description} |
284 \end{description} |
285 All the structural rules --- cut, contraction, and thinning --- can be |
285 All the structural rules --- cut, contraction, and thinning --- can be |