1

当我有像"∀x. P x"伊莎贝尔这样的目标时，我知道我可以写作

show "∀x. P x"
proof (rule allI)

但是，当目标是 时"∀x>0. P x"，我不能那样做。proof为了简化我的目标，我可以使用类似的规则/方法吗？对于您有表单目标的情况，我也会感兴趣"∃x>0. P x"。

proof (rule something)我正在寻找使用该样式的 Isar 证明。

4

2 回答 2

3

通用量词

扩展拉斯的答案：∀x>0. P x只是∀x. x > 0 ⟶ P x. 因此，如果你想证明这样的陈述，你首先必须用 去掉全称量词，allI然后用 去掉蕴涵impI。你可以这样做：

lemma "∀x>0. P x"
proof (rule allI, rule impI)

或使用intro，这或多或少与应用相同，rule直到不再可能：

lemma "∀x>0. P x"
proof (intro allI impI)

或者您可以使用safe，它急切地应用所有声明为“安全”的引入规则，例如allIand impI：

lemma "∀x>0. P x"
proof safe

无论如何，您的新证明状态是

proof (state)
goal (1 subgoal):
 1. ⋀x. 0 < x ⟹ P x

你可以这样进行：

lemma "∀x>0. P (x :: nat)"
proof safe
  fix x :: nat assume "x > 0"
  show "P x"

请注意，我添加了注释；我不知道你的类型是什么P，所以我只使用了nat. 当您在 Isar 中修复一个变量并且从假设中不清楚类型时，您将收到一个警告，指出引入了一个新的自由类型变量，这不是您想要的。当您收到该警告时，您应该fix像我上面所做的那样添加类型注释。

存在量词

对于存在量词，safe将不起作用，因为exI由于技术原因，介绍规则并不总是安全的。an 的典型证明模式∃x>0. P x类似于：

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > (0 :: nat)" by simp
  moreover have "P 42" sorry
  ultimately show ?thesis by blast
qed

或者更明确一点：

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > 0 ∧ P 42" sorry
  thus ?thesis by (rule exI)
qed

如果存在见证（即本例中的 42）不依赖于您从obtain命令中获得的任何变量，您也可以更直接地执行此操作：

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)

这给你留下了目标?x > 0和P ?x。请注意，这?x是一个示意图变量，您可以为其放置任何内容。所以你可以像这样完成证明：

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)
  show "42 > (0::nat)" by simp
  show "P 42" sorry
qed

正如我所说，如果您的存在证人依赖于您因技术限制而获得的某些变量，则这不起作用。obtain在这种情况下，您必须退回到我提到的其他解决方案。

于 2016-11-24T07:27:53.343 回答
1

Isabelle2016-1-RC2 中的以下作品：

lemma "∀ x>0. P x"
  apply (rule allI)

一般来说，您也可以只使用apply rule，它将选择默认的引入规则。存在量词也是如此。

于 2016-11-22T16:42:13.070 回答