Не удалось уточнить любую ожидающую цель

Question

Я пытаюсь доказать теорему в Изабель, и я застрял в этом шаге:

theorem exists_prime_factor: " (n > Suc 0) ⟶ (∃xs::nat list. prod_list xs = n ∧ all_prime xs)"
proof (induct n rule: less_induct)
    case (less k)
    assume HI: "⋀y::nat. (y < k ⟹ Suc 0 < y ⟶ (∃xs. prod_list xs = y ∧ all_prime xs))"
    then show ?case
    proof -
      show "(Suc 0 < k) ⟶ (∃xs. prod_list xs = k ∧ all_prime xs)"
        proof -     
          assume "Suc 0 < k" then show "(∃xs. prod_list xs = k ∧ all_prime xs)" sorry

В последней цели мне нужно доказать подтекст. Как обычно, я принимаю помещение и пытаюсь показать заключение. Однако, когда я пишу последнюю строку, я получаю "Не удалось уточнить любую ожидающую цель". Это из-за принципа индукции, который я применял раньше? Потому что без этой индукции я могу, как обычно, использовать правило введения импликации (предположим посылку, а затем покажем заключение).

Кто-нибудь имеет представление о том, что может происходить?

Большое спасибо.

Answer 1

"Проблема" действительно имеет отношение к proof -, Утверждение открывает новое подчинение без применения каких-либо методов доказательства к цели. Если ты пишешь proof без -метод доказательства rule будет применяться неявно, что делает свое дело в этой ситуации.

proof rule выбирает самое простое правило, применимое к вашей цели. В этом случае это будет эквивалентно proof (rule impI)потому что утверждение уровня объекта, которое вы хотите доказать, имеет форму "a --> b", impI является правилом введения для импликации. Это позволяет поднять уровень объекта на уровне формы "a --> b" к мета-логическому "a" ==> "b",

Ваши цели должны быть в форме "a" ==> "b" продолжить с подпунктами формы assume "a" [...] show "b",