我正在尝试解决Isabelle 中的 Programming and Proving 中的练习 4.7 。我遇到了一个案例，我证明了 False 并因此证明了所有内容，但我无法结案，因为我不知道如何提及我的证明义务。
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
最后一个命题show是从 Isabelle/jedit 中的证明状态复制而来的。但是，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)
现在被注释掉的证明目标导致了同样的错误。如果我将案例交换为0and Suc，则错误出现在最后一个show案例0中，但不再出现在Suc案例中。
有人可以解释为什么伊莎贝尔不会在这里接受这些看似正确的目标吗？我如何以 Isabelle 接受的方式陈述子目标？是否有指代当前子目标的一般方式？我认为考虑到我使用的构造，?case应该完成这项工作，但显然它没有。
我发现这个Stack Overflow question 提到了相同的错误，但是问题不同（定理存在一个等价性，应该通过隐式应用将其拆分为方向子目标rule）并且应用所提供的解决方案会导致不正确且无法证明就我而言，目标。