Isabelle не смог завершить доказательство, хотя это точно так же, как цель

Question

Мой код выглядит следующим образом. Я ожидал, что он будет работать отлично, и действительно к концу финальной линии «отсюда» (которая была найдена Кувалдом) Изабель утверждает, что - ∀y. ∃x. P x y, и что его цель имеет только один подцель, который равен ∀y. ∃x. P x y. Эти два выражения идентичны, поэтому я бы подумал, что Изабель примет доказательство как законченное.

lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" 
proof - 
fix y 
assume "EX x. ALL f. P x f" 
then obtain x where "ALL f. P x f" by blast 
hence "P x y" by blast 
hence "ALL y. EX x. P x y" using `∀f. P x f` by blast 
qed 

Что я пропустил? Я новичок в Изабель, как это очевидно.

Answer 1

Команды have и hence содержат только промежуточные данные о состоянии, которые вы хотите доказать. Вы должны прямо заявить, что утверждение должно выполнять задачу. Для этого вам необходимо использовать show или thus вместо have или hence. Поэтому, если вы замените свой последний hence на thus, доказательство должно быть успешным (по модулю замечания ниже). Вы также можете увидеть в Output буфера (или при наведении с помощью мыши над thus, что вы получите сообщение о том, Successful attempt to solve goal by exported rule .... Это свидетельствует о том, что цель была действительно разряжается.

Кстати, доказательство не будет работать, как ожидалось. Во-первых, на начальном этапе, когда вы пишете proof -, вы действительно хотите сделать введение для универсального квантификатора (по мере того как вы исправите y на следующем шаге, поэтому - следует заменить соответствующим приложением правила, а именно (rule allI). Следовательно, ваша заявка на шоу должна быть EX x. P x y, а не ALL y. EX x. P x y.

Во-вторых, assumes в заявлении леммы уже добавляет предположение к контексту. Поэтому нет необходимости принимать его еще раз в доказательстве. В случае если Isabelle пожалован на show или thus, это не может решить цель. Поэтому вы должны удалить часть assume ... и заменить ее ссылкой на предположение, например, используя предопределенное имя assms.