How do I refer to the current subgoal in Isar?

Question

I am trying to solve Exercise 4.7 from Programming and Proving in Isabelle. I run into a case where I have proved False and therefore everything, but I cannot close the case because I do not know how to refer to my proof obligation.

theory ProgProveEx47
  imports Main
begin

datatype alpha = a | b | c

inductive S :: "alpha list ⇒ bool" where
  Nil: "S []" |
  Grow: "S xs ⟹ S ([a]@xs@[b])" |
  Append: "S xs ⟹ S ys ⟹ S (xs@ys)"

fun balanced :: "nat ⇒ alpha list ⇒ bool" where
  "balanced 0 [] = True" |
  "balanced (Suc n) (b#xs) = balanced n xs" |
  "balanced n (a#xs) = balanced (Suc n) xs" |
  "balanced _ _ = False"

lemma
  fixes n xs
  assumes b: "balanced n xs"
  shows "S (replicate n a @ xs)"
proof -
  from b show ?thesis
  proof (induction xs)
    case Nil
    hence "S (replicate n a)"
    proof (induction n)
      case 0
      show ?case using S.Nil by simp
      case (Suc n)
      value ?case
      from `balanced (Suc n) []` have False by simp
      (* thus "S (replicate (Suc n) a)" by simp *)
      (* thus ?case by simp *)
      then show "⋀n. (balanced n [] ⟹ S (replicate n a)) ⟹ balanced (Suc n) [] ⟹ S (replicate (Suc n) a)" by simp

The proposition after the last show is copied from the proof state in Isabelle/jedit. However, Isabelle reports the error (at the last show):

   Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (balanced 0 []) ⟹
  (balanced ?na3 [] ⟹ S (replicate ?na3 a)) ⟹
  (balanced (Suc ?na3) []) ⟹
  (balanced ?n [] ⟹ S (replicate ?n a)) ⟹
  (balanced (Suc ?n) []) ⟹ S (replicate (Suc ?n) a)

The proof goals that are commented out now resulted in the same kind of error. If I swap the cases for 0 and Suc, the error appears for the last show of the 0 case, but no longer for the Suc case.

Can someone explain why Isabelle will accept none of these seemingly correct goalsg here? And how can I state the subgoal in a way that Isabelle will accept? Is there a general way of referring to the current subgoal? I thought that given the constructs I use, ?case should do that job, but apparently it does not.

I found this Stack Overflow question which mentions the same error, but the problem there is different (the theorem there is an equivalence which should be split into the to directional subgoals by an implicit application of rule) and applying the offered solution leads to incorrect and unprovable goals in my case.

Answer 1

You're simply missing a next in the inner induction proof.

lemma
  fixes n xs
  assumes b: "balanced n xs"
  shows "S (replicate n a @ xs)"
proof -
  from b show ?thesis
  proof (induction xs)
    case Nil
    hence "S (replicate n a)"
    proof (induction n)
      case 0
      show ?case using S.Nil by simp
    next (* this next was missing *)
      case (Suc n)
      show ?case sorry
    qed
    show ?case sorry
  next
    case (Cons a xs)
    then show ?case sorry
  qed