Как использовать get, чтобы упростить чтение доказательств прямого исключения?

Эта модификация вашего доказательства работает:

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then show ‹B› using ‹A› ..
qed

Проблема двоякая:

1. При открытии блока доказательства автоматически применяется «стандартное» правило введения, основанное на форме цели, которую вы пытаетесь доказать. В вашем случае это было введение импликации, то есть теорема impI. Проблема в том, что вы применяете это только один раз, что оставляет вам предположение A -> A -> B и оставшуюся цель A -> B. В результате у вас еще нет предположения A, которое, как вы предполагаете, у вас есть, поскольку для его получения требуется второе использование impI. Вместо этого, используя proof(intros impI), я говорю Изабель воздержаться от использования своего стандартного набора правил введения и исключения в качестве первого шага в доказательстве и вместо этого применять правило введения impI как можно чаще (т. Е. Дважды). В качестве альтернативы, proof(rule impI, rule impI) также будет работать здесь с тем же эффектом.
2. Во-вторых, ваша последняя строка then obtain и далее не завершает доказательство: вы ничего show не делаете! Используя явное show, вы сигнализируете Изабель, что хотите «уточнить» открытую цель и фактически сделать вывод о том, что вы намеревались доказать в начале блока.

Обратите внимание, что ваше использование obtain здесь для продвижения вперед на основе фактов A -> B и A не было неправильным, если ваша единственная цель - получить B. Проблема в том, что вы пытаетесь отталкиваться от фактов, чтобы вывести новые, одновременно уточняя открытую цель. Например, это тоже работает:

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
  then show ‹B› .
qed

где факт B получен в первой строке, а вторая строка тривиально использует этот факт для уточнения открытой цели B.