如何让 Isabelle "compute" 归纳谓词的输出

Question

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

例如，假设我们有以下谓词 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 上的属性几乎总是以相同的方式工作（大锤在它们上效果不佳）。

证明证人的存在；
For the only：证明见证人的唯一性；
用 theI 或 someI 推导出属性的值；
证明你真正想证明的定理。

在你的案例中，这转化为证明 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-definition。

如何让 Isabelle "compute" 归纳谓词的输出

How to let Isabelle "compute" THE output of an inductive predicate

isabelle