isabelle - 专注于子目标

Question

之前使用过 Coq，我习惯了它的“聚焦”和“不聚焦”目标系统，因此您可以一次只处理一个目标。

伊莎贝尔是否存在类似的系统？

作为示例，此代码:

theory Scratch
  imports Main
begin

theorem add_0: "n+0 = (n::nat)"
  apply(induction n)

生成具有 2 个子目标的证明状态:

proof (prove)
goal (2 subgoals):
 1. 0 + 0 = 0
 2. ⋀n. n + 0 = n ⟹
         Suc n + 0 = Suc n

如果我使用apply(auto)，两个问题都解决了。然而，假设我只想致力于目标 1，是否可以“专注”它？如果不是，我如何才能将 auto 仅应用于一个(或部分)子目标？

Answer 1

如果您不想使用 Isar(这可能更有利于可读性)，您可以使用 subgoal 来专注于目标:

theorem add_0: "n+0 = (n::nat)"
  apply(induction n)
  subgoal by auto
  subgoal by auto

或括号:

apply auto[]

仅将auto聚焦于第一个目标。

主要区别在于subgoal使得无法实例化原理图变量。