专注于一个子目标

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无法实例化原理图变量。

Answer 2

Mathias 和 Manuel 提到 Isar 风格是关注子目标的首选方式。这是一个看起来像这样的例子：

theorem add_0: "n+0 = (n::nat)"
proof (induction n)
  case 0 ― ‹Focus on induction base subgoal here›
  show "0 + 0 = (0::nat)" 
    by (rule plus_nat.add_0)
next
  case (Suc n) ― ‹Focus on induction step subgoal here›
  show "Suc n + 0 = Suc n"
  proof (subst plus_nat.add_Suc)
    show "Suc (n + 0) = Suc n"
      by (subst Suc.IH) (rule refl)
  qed
qed

或隐含地，不命名案例：

theorem add_0: "n+0 = (n::nat)"
proof (induction n)
  show "0 + 0 = (0::nat)" 
    by (rule plus_nat.add_0)
next
  fix n :: nat
  assume IH: "n + 0 = n"
  show "Suc n + 0 = Suc n"
  proof (subst plus_nat.add_Suc)
    show "Suc (n + 0) = Suc n"
      by (subst IH) (rule refl)
  qed
qed

专注于一个子目标

Focusing on a subgoal

isabelle