在不使用 Isar 的情况下证明蕴涵存在于前提中
Proof implication with exist in the premises without using Isar
我从我必须证明的定理之一中提取了以下目标：
∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ P [] [x] ∨ P [x] []
这里我想应用存在消除规则，但它产生了两个奇怪的子目标：
1. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ∃x. ?P25 x
2. ⋀xa. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ?P25 xa ⟹ P [] [x] ∨ P [x] []
我的想法是，如果我可以删除量词，那么证明确实很容易。如果 [x]= ys @ zs 那么有两种可能性。 ys = [x], zs = [] 或相反。因此，我们将 P [x] [] 或 P [] [x]。
如何在不使用 Isar 的情况下仅使用应用命令来证明这一点？
我不知道为什么 exists 消除策略在你的情况下失败了，但下面一行成功了。
by (elim exE, rename_tac ys zs, case_tac ys, auto)
这里，rename_tac将新获得的列表重命名为用户选择的名称ys和zs，以便随后对ys进行案例分析（是否为空）是可能的。
我从我必须证明的定理之一中提取了以下目标：
∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ P [] [x] ∨ P [x] []
这里我想应用存在消除规则，但它产生了两个奇怪的子目标：
1. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ∃x. ?P25 x
2. ⋀xa. ∃ys zs. [x] = ys @ zs ∧ P ys zs ⟹ ?P25 xa ⟹ P [] [x] ∨ P [x] []
我的想法是，如果我可以删除量词，那么证明确实很容易。如果 [x]= ys @ zs 那么有两种可能性。 ys = [x], zs = [] 或相反。因此，我们将 P [x] [] 或 P [] [x]。
如何在不使用 Isar 的情况下仅使用应用命令来证明这一点？
我不知道为什么 exists 消除策略在你的情况下失败了，但下面一行成功了。
by (elim exE, rename_tac ys zs, case_tac ys, auto)
这里，rename_tac将新获得的列表重命名为用户选择的名称ys和zs，以便随后对ys进行案例分析（是否为空）是可能的。