∀x∈S (Isabelle) 的介绍规则
Intro rule for ∀x∈S (Isabelle)
通常当你有一个目标开始时∀x你可以写这样的东西
show "∀x. Px"
proof (rule allI)
但是当你有一些开始时这似乎不起作用 ∀x∈S。例如，我试过
show "∀x∈S. P x"
proof (rule allI)
给出消息
Failed to apply initial proof method
这让我感到惊讶，因为我认为 ∀x∈S. P x 可能是 ∀x. x∈S --> P x 的语法糖，在这种情况下它应该起作用。
这与我之前问过的一个问题类似
但我觉得这次的答案可能会有所不同
这不仅仅是语法；是它自己的常量叫Ball，引入规则叫ballI.
如果您按住 Ctrl 键并单击“∀x∈A”，它应该会直接带您到定义处，在那里您可以看到它的名称。此外，您可以使用 Isabelle 中的“查找定理”面板来找到与之相关的引理。
通常当你有一个目标开始时∀x你可以写这样的东西
show "∀x. Px"
proof (rule allI)
但是当你有一些开始时这似乎不起作用 ∀x∈S。例如，我试过
show "∀x∈S. P x"
proof (rule allI)
给出消息
Failed to apply initial proof method
这让我感到惊讶，因为我认为 ∀x∈S. P x 可能是 ∀x. x∈S --> P x 的语法糖，在这种情况下它应该起作用。
这与我之前问过的一个问题类似
但我觉得这次的答案可能会有所不同
这不仅仅是语法；是它自己的常量叫Ball，引入规则叫ballI.
如果您按住 Ctrl 键并单击“∀x∈A”，它应该会直接带您到定义处，在那里您可以看到它的名称。此外，您可以使用 Isabelle 中的“查找定理”面板来找到与之相关的引理。