Ответ можно найти в «Главе 6: Доказательства» документа Isar-ref. В идеале вы должны sh прочитать введение к главе, а также разделы 6.1 и 6.2, чтобы полностью решить ваши проблемы. Ниже я представляю наиболее подходящие отрывки:
Логический контекст доказательства состоит из фиксированных переменных и предположений.
...
Аналогично, введение некоторого предположения χ имеет два эффекта. С одной стороны, создается локальная теорема, которую можно использовать как факт на последующих этапах доказательства. С другой стороны, любой результат χ ⊢ φ, экспортированный из контекста, становится условным. предположение: ⊢ χ ==> φ. Таким образом, решение закрывающей цели с использованием такого результата в основном вводит новую подцель, вытекающую из предположения. Как эта ситуация обрабатывается, зависит от версии используемой команды предположения: в то время как предположение настаивает на решении подцели путем объединения с некоторой предпосылкой цели , предположение оставляет подцель без изменений, чтобы пользователь мог позже подтвердить .
Давайте посмотрим на ваш первый пример:
lemma
assumes "A"
shows "A"
proof -
assume "A"
from this show "A" by (simp)
qed
Есть только одна подцель без предпосылок: A. При отсутствии посылок «объединение с посылками» неприменимо.
Во втором примере
lemma
shows "A⟹A"
proof -
assume "A"
from this show "A" by simp
qed
подцель A⟹A с посылкой A. Таким образом, вы можете использовать assume: объединение может быть выполнено.
Наконец,
lemma
assumes "A"
shows "A"
proof -
have "A" by (simp add: assms)
from this show "A" by (simp)
qed
отличается от предыдущих случаев, потому что вы не вводите никаких предположений. Следовательно, вы можете использовать show для выполнения подцели. Следует отметить, что from this show "A" by (simp) идентично from assms show "A" by simp или, что еще лучше, from this show "A".:
lemma
assumes "A"
shows "A"
proof -
from assms show "A".
qed