如何让Isabelle“计算”归纳谓词的输出

编程问答 2022-06-11

问题描述

我有一个归纳谓词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

解决方法

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定义。
isabelle