theorem-proving - 有限有界量词的消除规则

Question

我有以下目标：

∀x ∈ {0,1,2,3,4,5}. P x

我想将此目标分解为六个子目标P 0，P 1，P 2，P 3和。这很容易做到。但是用于执行此操作的相关规则是什么？我问是因为我的实际目标看起来更像这样：P 4P 5apply autoauto

∀x ∈ {0..<6}. P x

并且apply auto不会以同样的方式打破这个目标（它给了我

⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x

反而）。

Answer 1

正在使用的规则auto是ballI（限制所有介绍）。这转变∀x ∈ S. P x为x ∈ S ==> P x.

转化x ∈ {0,1,2,3,4,5}为 6 个独立子目标的问题是一个独立的子目标。基本上，auto将显式枚举转换为析取，然后将其拆分。

Answer 2

您可以使用如下引理来拆分单个目标：

lemma expand_ballI: "⟦ (n :: nat) > 0; ∀x ∈ {0..< (n - 1)}. P x; P (n - 1) ⟧ ⟹ ∀x ∈ {0..< n}. P x"
  by (induct n, auto simp: less_Suc_eq)

然后可以将其重复应用于您的规则，如下所示：

lemma "∀x ∈ {0..< 6 :: nat}. P x"
  apply (rule expand_ballI, fastforce)+
  apply simp_all

导致目标拆分如下：

goal (6 subgoals):
 1. P 0
 2. P (Suc 0)
 3. P 2
 4. P 3
 5. P 4
 6. P 5

Answer 3

使用[simp]引理将集合转换为更方便的集合版本非常方便。例如{0..<6} = {0,1,2,3,4,5}