證明（排除disjE）嵌套脫節

在伊薩爾式伊莎貝爾證明，這很好地工作：這裏證明（排除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作爲最後一步）。

更新：使用新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

我也這樣做過。一個問題是它缺乏「證明」的自動性，例如設立案件，「論文」等。 – 2013-04-10 10:42:20

@JoachimBreitner：的確如此。無論如何，通過明確地寫出一個假設而不是使用'case'來證明它更具可讀性（對於相當短的假設而言，這種說法大部分是正確的），它的效果最好。 – chris 2013-04-10 11:19:55

@JoachimBreitner：'proof'不會設置'？thesis'，'lemma'（或'have'）。因此，只有在另一種方法中可以使用規則/ intro/elim方法中的'？thesis'時。 – 2013-04-18 06:39:45

或者做區分的情況下，似乎可以彎曲的更一般induct方法聽從你的命令。對於三種情況下，這會工作是這樣的：證明引理disjCases3：

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

缺點是，你需要一堆引理覆蓋任何號碼：

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

如下您可以使用此引理的情況下，disjCases2，disjCases3,disjCases4,disjCases5等，但否則它似乎很好地工作。

來源

2016-05-04 08:14:52

證明（排除disjE）嵌套脫節

回答

相關問題