Focusing on a subgoal

user_14656198 0
Viewed 137

Having worked with Coq before, I'm used to its system of "focusing" and "unfocusing" goals, so you can work with one goal at a time.

Does a similar system exists in Isabelle?

As an example, this code:

theory Scratch
  imports Main
begin

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

Generates a proof state with 2 subgoals:

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

If I use apply(auto), both of them are solved. Let's suppose however that I want to work only on goal 1, is it possible to "focus" on it? If not, how may I apply auto to only one (or some) of the subgoals?

isabelle
2 Answers

If you don't want to use Isar (which probably is better for readability), you can use subgoal to focus on the goal:

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

or the brackets:

apply auto[]

to focus auto on the first goal only.

The main difference is that subgoal makes it impossible to instantiate schematic variables.

user_128242070

Mathias and Manuel mentioned the Isar style as the preferred way to focus on subgoals. Here is an example of how that could look like:

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

Or implicitly, without naming cases:

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
user_3036370
Related