доказательство (правило disjE) для вложенного дизъюнкции

В Изар стиле Isabelle доказательств, это прекрасно работает:доказательство (правило disjE) для вложенного дизъюнкции

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

источник

2013-04-09 Joachim Breitner

При написании вопроса, у меня была идея, и она оказывается то, что я хочу:

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

источник

2013-04-09 12:12:26

Другой канонический способ сделать этот вид анализа случая выглядит следующим образом:

{ 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 в качестве последнего шага).

Update: Используя новый 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

источник

2013-04-10 09:26:30 chris

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

@JoachimBreitner: True. Он лучше всего работает, когда доказательство становится более читаемым, явно указывая предположение вместо использования 'case' в любом случае (что в основном верно для довольно коротких предположений). – chris

@JoachimBreitner: 'proof' не настраивается'? Thesis', 'lemma' (или' have'). Таким образом, вы можете использовать '? Thesis' в правиле/вступлении/исключении, только если вы можете использовать его в более подходящем подходе. –

В качестве альтернативы делать случай различия, это, кажется, вы можете согнуть более общий 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 и т. д., но в остальном он работает хорошо.

источник

2016-05-04 08:14:52

доказательство (правило disjE) для вложенного дизъюнкции

ответ

Смежные вопросы