Как я обращаюсь к текущей подцели в Изаре?

Question

Я пытаюсь решить упражнение 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

Предложение после последнего show скопировано из контрольного состояния в Изабель / Джедит. Тем не менее, Изабель сообщает об ошибке (на последнем 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появляется ошибка для последнего show из 0 случай, но больше не для Suc дело.

Может кто-нибудь объяснить, почему Изабель не примет здесь ни одной из этих, казалось бы, правильных целей? И как я могу сформулировать подцель так, как Изабель примет? Существует ли общий способ обращения к текущей подцели? Я думал, что учитывая конструкции, которые я использую, ?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