設定メンバーシップの否定、等価

Question

私は、Isabelleが自動的に¬ (a ∈ (- A))と¬ (x = y)からa ∉ Aとx ≠ yを簡素化することに気付きました。

ここでは、自然な控除では単純なペンとペーパーの証明ですが、Isabelleでは失敗します。 2行目の¬ (a ∈ (- A))はa ∉ - Aに簡略化されています。後者からComplDを適用することはできませんが、なぜですか？

lemma "- (- A) ⊆ (A::'a set)" 
proof 
    fix a assume "a ∈ - (- A)" 
    hence "¬ (a ∈ (- A))" by (rule ComplD) 
    hence "¬ (¬ (a ∈ A))" by (rule ComplD) (* fail! *) 
    thus "a ∈ A" by (rule notnotD) 
qed 

単純化されていない表現に戻る方法はありますか？

もちろん、補題はsimpで1行で証明できます。しかし、私の目的は、自然控除ルールを（教授のために）明示的に使用することです。

Answer 1

これらは単純化ではありません。 Isabelleのa ≠ bとx ∉ Aの定義を見ると（記号をクリックするなどして）、¬(a = b)と¬(x ∈ A)の略語であることがわかります。これらのステートメントは、内部的には上に書いたとおりに表現されていますが、読みやすさを高めるために別の方法で印刷されています。

ルールComplDを適用できないのは、単純に一致しないためです。 ComplDは、それが?c ∈ - ?A ⟹ ?c ∉ ?Aと言います。しかし、失敗したステップでは、あなたの前提はa ∉ -Aであり、前提として?c ∈ -?AがComplDに統一されないため、ruleが失敗します。

あなたの声明が直感的に理解できないため、この証拠のために古典的な推論が必要であることは比較的確信しています。これは、あなたが矛盾で証明する必要があることを意味します。

lemma "- (- A) ⊆ (A::'a set)" 
proof 
    fix a assume a: "a ∈ - (- A)" 
    show "a ∈ A" 
    proof (rule ccontr) 
    assume "a ∉ A" 
    have "a ∈ -A" 
    proof (rule ComplI) 
     assume "a ∈ A" 
     with ‹a ∉ A› show False by contradiction 
    qed 
    moreover from a have "a ∉ -A" by (rule ComplD) 
    ultimately show False by contradiction 
    qed 
qed 

そこのrule ccontrは、矛盾して証明を開始します。証明方法contradictionは、事実とその否定が証明されたときに、何かを派生させるための単なる良い方法です。