如何让伊莎贝尔“计算”归纳谓词的输出

Question

我有一个归纳谓词P，其行为类似于偏函数。换句话说，P x y = P x y' ⟹ y = y'。我想让 Isabelle 在证明具体值的定理时“计算”谓词的输出（例如）。

例如，假设我们有以下谓词div2。

inductive div2 :: "nat ⇒ nat ⇒ bool" where
  Zero: "div2 0 0" |
  SS: "div2 n m ⟹ div2 (Suc (Suc n)) (Suc m)"
code_pred[show_modes] div2 .

如何在不提供输出m 的情况下证明以下引理（实际情况下该术语太大而无法输入）？

lemma "(THE m. div2 8 m) ≠ 5"
  sorry

Answer 1

the 和 some 上的属性几乎总是以相同的方式工作（大锤在它们上效果不佳）。

1. 证明证人的存在；
2. 仅此而已：证明证人的唯一性；
3. 用theI 或someI 推断该属性对值的持有；
4. 证明您真正想要证明的定理。

在您的情况下，这意味着证明 5 不是证人：

inductive_cases div2E: ‹div2 m n›

lemma "(THE m. div2 8 m) ≠ 5"
proof -
  have ex_div2: ‹div2 8 4› (*1: witness*)
    by (auto simp: numeral_eq_Suc div2.intros)
  moreover have ‹div2 8 m ⟹ m = 4› for m (*2: uniqueness*)
    by (force simp: numeral_eq_Suc elim: div2E)
  ultimately have ‹div2 8 (THE x. div2 8 x)› (*3: property holds*)
    by (rule theI)
  (*4 use the property*)
  then show ?thesis
    by (force simp: numeral_eq_Suc elim: div2E)

qed

如果您不需要the，请改用some，这样可以避免每次都非常烦人的唯一性证明。

对于您的用例，我建议将定理写为div2 8 m ⟹ m ≠ 5，这是等效的，但更易于使用和证明。

lemma "div2 8 m ⟹ m ≠ 5"
  by (force simp: numeral_eq_Suc elim: div2E)

为了可重用性：

• 在单独的引理中考虑步骤 3（如果存在倒置时有有意义的表达方式）
• 通过引入定义尽可能隐藏the 谓词，并尽可能避免引用 lambda 定义。