我如何参考ISAR中的当前子目标

Question

我试图从编程和证明Isabelle中解决练习4.7。我遇到了我证明是错误的情况，因此我无法结束案件，因为我不知道如何参考我的证明义务。

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

从Isabelle/Jedit中的证明状态复制了最后一个show之后的命题。但是，Isabelle报告了错误（在最后一个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)

现在评论的证明目标导致了同样的错误。如果我将案例交换为0和Suc，则出现0案例的最后一个show的错误，但不再为Suc案例。

有人可以解释为什么Isabelle在这里不接受这些看似正确的进球？我该如何以伊莎贝尔接受的方式陈述子目标？是否有一种通用的方式来指代当前的子目标？我认为鉴于我使用的结构，?case应该做这份工作，但显然不是。

我发现了一个提到相同错误的堆栈溢出问题，但是存在不同的问题（定理存在等效性，应通过 rule的隐式应用将其分为方向子目标）并应用所提供的解决方案引线在我的情况下，要实现错误和无法证明的目标。

Answer 1

您只是在内部感应证明中缺少next。

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