伊莎贝尔中“∀r>0”的介绍规则
Intro rule for "∀r>0" in Isabelle
当我有一个像伊莎贝尔"∀x. P x"这样的目标时，我知道我可以写
show "∀x. P x"
proof (rule allI)
但是，当目标是 "∀x>0. P x" 时，我不能那样做。我可以在 proof 之后使用类似的 rule/method 来简化我的目标吗？如果您有 "∃x>0. P x".
形式的目标，我也会对其中一个感兴趣
我正在寻找使用 proof (rule something) 样式的 Isar 证明。
Isabelle2016-1-RC2以下作品：
lemma "∀ x>0. P x"
apply (rule allI)
一般情况下，您也可以只使用apply rule，这将select默认引入规则。存在量词也是如此。
全称量词
扩展 Lars 的回答：∀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，它会急切地应用所有声明为“安全”的引入规则，例如 allI 和 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 由于技术原因并不总是安全的。 ∃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 获得的某些变量，这 不会 起作用。在那种情况下，您必须退回到我提到的其他解决方案。
当我有一个像伊莎贝尔"∀x. P x"这样的目标时，我知道我可以写
show "∀x. P x"
proof (rule allI)
但是，当目标是 "∀x>0. P x" 时，我不能那样做。我可以在 proof 之后使用类似的 rule/method 来简化我的目标吗？如果您有 "∃x>0. P x".
我正在寻找使用 proof (rule something) 样式的 Isar 证明。
Isabelle2016-1-RC2以下作品：
lemma "∀ x>0. P x"
apply (rule allI)
一般情况下，您也可以只使用apply rule，这将select默认引入规则。存在量词也是如此。
全称量词
扩展 Lars 的回答：∀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，它会急切地应用所有声明为“安全”的引入规则，例如 allI 和 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 由于技术原因并不总是安全的。 ∃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 获得的某些变量，这 不会 起作用。在那种情况下，您必须退回到我提到的其他解决方案。