В доказательствах Изабель в стиле Isar это прекрасно работает:
from `a ∨ b` have foo
proof
assume a
show foo sorry
next
assume b
show foo sorry
qed
Неявное правило, вызываемое здесь proof, называется rule conjE. Но что я должен поместить туда, чтобы заставить его работать более чем для одной дизъюнкции:
from `a ∨ b ∨ c` have foo
proof(?)
assume a
show foo sorry
next
assume b
show foo sorry
next
assume c
show foo sorry
qed
При написании вопроса у меня возникла идея, и получается то, что я хочу:
from `a ∨ b ∨ c` have foo
proof(elim disjE)
assume a
show foo sorry
next
assume b
show foo sorry
next
assume c
show foo sorry
qed
Другой канонический способ проведения подобного рода анализа случая выглядит следующим образом:
{ assume a
have foo sorry }
moreover
{ assume b
have foo sorry }
moreover
{ assume c
have foo sorry }
ultimately
have foo using `a ∨ b ∨ c` by blast
То есть пусть автоматический инструмент «разберется» с деталями в конце. Это особенно хорошо работает при рассмотрении арифметических случаев (с by arith в качестве последнего шага).
Обновление. Используя новый оператор consider, это можно сделать следующим образом:
notepad
begin
fix A B C assume "A ∨ B ∨ C"
then consider A | B | C by blast
then have "something"
proof (cases)
case 1
show ?thesis sorry
next
case 2
show ?thesis sorry
next
case 3
show ?thesis sorry
qed
end
proof, например. настройка дел, ?thesis и тому подобное.
- person Joachim Breitner; 10.04.2013
case в любом случае (что в основном верно для довольно коротких предположений).
- person chris; 10.04.2013
proof не устанавливает ?thesis, lemma (или have) устанавливает. Таким образом, вы можете использовать ?thesis в подходе rule/intro/elim только в том случае, если вы можете использовать его в подходе к тому же.
- person Lars Noschinski; 18.04.2013
В качестве альтернативы, чтобы различать регистры, кажется, что вы можете согнуть более общий метод induct, чтобы выполнить ваши ставки. Для трех случаев это будет работать следующим образом: Докажите лемму disjCases3:
lemma disjCases3[consumes 1, case_names 1 2 3]:
assumes ABC: "A ∨ B ∨ C"
and AP: "A ⟹ P"
and BP: "B ⟹ P"
and CP: "C ⟹ P"
shows "P"
proof -
from ABC AP BP CP show ?thesis by blast
qed
Вы можете использовать эту лемму следующим образом:
from `a ∨ b ∨ c` have foo
proof(induct rule: disjCases3)
case 1 thus ?case
sorry
next
case 2 thus ?case
sorry
next
case 3 thus ?case
sorry
qed
Недостаток в том, что вам нужна куча лемм для покрытия любого количества случаев, disjCases2, disjCases3, disjCases4, disjCases5 и т. д., но в остальном это работает хорошо.
