Как с помощью основных пропозициональных правил Isar доказать `A ⟶ A ∨ B`?

У вас несколько проблем.

Рассмотрим пример:

have "A ⟹ A" by (rule disjI1)

Это не удается, так что сначала какова на самом деле теорема disjI1?

thm disjI1
(* ?P ⟹ ?P ∨ ?Q *)

Из-за того, как работают правила, он пытается сопоставить цель «A» с «? P ∨? Q», что терпит неудачу. Теперь, если ваша цель имеет правильную форму:

have "A ⟹ A ∨ B" by (rule disjI1)

оно работает!

Вторая проблема:

 proof

по умолчанию эквивалентен «стандарту доказательства» и по умолчанию применяет некоторую теорему. Обычно вы используете «доказательство -», чтобы не применять теоремы.

Напоследок давайте рассмотрим ваш пример

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)

В режиме просмотра состояний вы видите:

proof (state)
goal (1 subgoal):
 1. A ⟹ A ∨ B

Это значит, что Isar должен выглядеть как

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  show ‹A ∨ B›
    sorry
qed

Тот факт, что выставка работает, указывает на то, что пробный блок имеет правильную форму.

Осторожно: это важный шаг, особенно в начале. ВСЕГДА начинайте с предположения и шоу. Больше ничего не пиши. Если шоу не работает, структура, наведенная доказательством Isar (принять и показать), не соответствует ожидаемому доказательству (которое можно увидеть на панели состояния).

Оттуда вы можете делать все, что захотите (включая запуск нового блока проверки), но вы не можете изменить эту структуру, не изменив применяемое правило.

Закончим доказательство. Мы хотим использовать предположение (поэтому мы добавляем then) и правило, чтобы доказать цель.

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  then show ‹A ∨ B›
    by (rule disjI1)
qed

В целом, я думаю, вам следует прочитать часть Isar в Конкретной семантике.

РЕДАКТИРОВАТЬ: Самая важная проблема заключается в том, что вы неправильно понимаете, что такое Isar: Isar здесь не для того, чтобы помочь вам с различными шагами доказательства (например, доказательством tha "A ==> A"). Здесь делается прямое доказательство: вы начинаете с предположения (здесь А) и переходите к заключению. Таким образом, доказательство Isar будет выглядеть так:

  assume A
  show "A \/ B"

Вам никогда не придется повторять предположение A в доказательстве!