在Eisbach中，我可以使用;将方法应用于由方法创建的所有新子目标。
但是，我经常知道创建了多少个子目标，并且想对新的子目标应用不同的方法。
有没有办法说类似“将方法X应用于第一个新子目标并将方法Y应用于第二个新子目标”的说法？
这是一个简单的用例：
我想开发一种方法，该方法适用于任意长度的2个并列，但结构相同。
该方法应可用于通过显示每个分量的含义成立来表明连词1暗含连词2。
应该可以这样使用：
lemma example:
assumes c: "a 0 ∧ a 1 ∧ a 2 ∧ a 3"
and imp: "⋀i. a i ⟹ a' i"
shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
proof (conj_one_by_one pre: c)
show "a 0 ⟹ a' 0" by (rule imp)
show "a 1 ⟹ a' 1" by (rule imp)
show "a 2 ⟹ a' 2" by (rule imp)
show "a 3 ⟹ a' 3" by (rule imp)
qed
在Eisbach中实现此方法时，使用
rule conjI后出现问题。我得到了两个要递归处理的子目标，但是我想在两种情况下使用不同的事实。
我想出了以下解决方法，该方法对这两个子目标使用了人工标记，并且有点丑陋：
definition "marker_L x ≡ x"
definition "marker_R x ≡ x"
lemma conjI_marked:
assumes "marker_L P" and "marker_R Q"
shows "P ∧ Q"
using assms unfolding marker_L_def marker_R_def by simp
method conj_one_by_one uses pre = (
match pre in
p: "?P ∧ ?Q" ⇒ ‹
(unfold marker_L_def marker_R_def)?,
rule conjI_marked;(
(match conclusion in "marker_L _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct1])?›)
| (match conclusion in "marker_R _" ⇒ ‹(conj_one_by_one pre: p[THEN conjunct2])?›))›)
| ((unfold marker_L_def marker_R_def)?, insert pre)
最佳答案
这不是一个完整的答案，但是您可能可以从此处说明的内容中得出一些有用的信息。
在艾斯巴赫我可以用;将方法应用于创建的所有新子目标
通过一种方法。但是，我经常知道创建了多少个子目标，
希望对新的子目标应用不同的方法。有没有
这样说：“将方法X应用于第一个新的子目标，
方法Y到第二个新子目标”？
您可以使用标准战术RANGE定义自己的战术，以应用于连续的子目标。我在下面提供了一个非常专业且大大简化的用例：
ML‹
fun mytac ctxt thms = thms
|> map (fn thm => resolve_tac ctxt (single thm))
|> RANGE
›
lemma
assumes A: A and B: B and C: C
shows "A ∧ B ∧ C"
apply(intro conjI)
apply(tactic‹mytac @{context} [@{thm A}, @{thm B}, @{thm C}] 1›)
done
希望将它扩展到更复杂的用例应该是相当容易的（同时要比我对子目标索引更谨慎：您可能还需要
SELECT_GOAL以确保实现是安全的）。虽然在上面的示例中，mytac接受了一个定理列表，但应该很容易看到如何用策略替换这些定理，并且通过进一步的工作，可以将该策略包装为高阶方法。我想开发一种适用于任意2个连接的方法
长度，但结构相同。该方法应适用于
通过显示连词1暗示连词2
含义适用于每个组件。应该可以这样使用：
更新
从另一个角度看问题，似乎存在着一种更为自然的解决方案。该解决方案遵循原始答案的概述，但是元含义被HOL的对象逻辑含义替代（可以使用
atomize (full)和intro impI实现“往返”转换）：lemma arg_imp2: "(a ⟶ b) ⟹ (c ⟶ d) ⟹ ((a ∧ c) ⟶ (b ∧ d))" by auto
lemma example:
assumes "a 0 ∧ a 1 ∧ a 2 ∧ a 3"
and imp: "⋀i. a i ⟹ a' i"
shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
apply(insert assms(1), atomize (full))
apply(intro arg_imp2; intro impI; intro imp; assumption)
done
旧版（这是原始答案的一部分，但是由于上面建议的UPDATE几乎无关紧要）
如果这是您唯一想到的应用程序，也许有一个基于以下迭代过程的合理自然的解决方案：
lemma arg_imp2: "(a ⟹ b) ⟹ (c ⟹ d) ⟹ ((a ∧ c) ⟹ (b ∧ d))" by auto
lemma example:
assumes c: "a 0 ∧ a 1 ∧ a 2 ∧ a 3"
and imp: "⋀i. a i ⟹ a' i"
shows "a' 0 ∧ a' 1 ∧ a' 2 ∧ a' 3"
using c
apply(intro arg_imp2[of ‹a 0› ‹a' 0› ‹a 1 ∧ a 2 ∧ a 3› ‹a' 1 ∧ a' 2 ∧ a' 3›])
apply(rule imp)
apply(assumption)
apply(intro arg_imp2[of ‹a 1› ‹a' 1› ‹a 2 ∧ a 3› ‹a' 2 ∧ a' 3›])
apply(rule imp)
apply(assumption)
apply(intro arg_imp2[of ‹a 2› ‹a' 2› ‹a 3› ‹a' 3›])
apply(rule imp)
apply(assumption)
apply(rule imp)
apply(assumption+)
done
我不确定在Eisbach中表达它会多么容易，但是在
Isabelle/ML中表达它应该很容易。