इसाबेल में विरोधाभास द्वारा बेवकूफ सबूत?

Question

अब तक मैं इसाबेल में निम्नलिखित शैली में विरोधाभास द्वारा सबूत लिखा था (Jeremy Siek द्वारा एक पैटर्न का उपयोग कर): { ... } ब्लॉक एक तरीका है कि नेस्टेड कच्चे सबूत के बिना काम करता

lemma "<expression>" 
proof - 
    { 
    assume "¬ <expression>" 
    then have False sorry 
    } 
    then show ?thesis by blast 
qed 

वहाँ है?

have "<expression>" 
proof (rule ccontr) 
    assume "¬ <expression>" 
    then show False sorry 
qed 

यह कभी कभी by contradiction उपयोग करने के लिए अंतिम कदम साबित करने के लिए मदद कर सकते हैं:

Answer 1

शास्त्रीय सबूत के लिए नियम ccontr विरोधाभास से नहीं है।

have "<expression>" 
proof (rule classical) 
    assume "¬ <expression>" 
    then show "<expression>" sorry 
qed 

classical का उपयोग कर आगे उदाहरणों के लिए, $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

नियम classical की बेहतर समझ के लिए यह संरचित Isar शैली में मुद्रित किया जा सकता:

वहाँ भी नियम classical (जो कम सहज दिखता है) है इस तरह:

print_statement classical 

आउटपुट:

theorem classical: 
    obtains "¬ thesis" 

इस प्रकार intuitionists को शुद्ध बुराई थोड़ा अधिक सहज ज्ञान युक्त प्रकट होता है: आदेश कुछ मनमाने ढंग से शोध साबित करने के लिए, हम मान सकते हैं कि उसका निषेध रखती है।

notepad 
begin 
    have A 
    proof (rule classical) 
    assume "¬ ?thesis" 
    then show ?thesis sorry 
    qed 
end 

यहाँ ?thesisA के ऊपर दावा है, जो एक मनमाने ढंग से जटिल बयान हो सकता है की ठोस थीसिस है:

इसी विहित सबूत पैटर्न यह है। संक्षिप्त नाम ?thesis के माध्यम से यह अर्ध अमूर्तता तर्कसंगत इस्सार के लिए सामान्य है, तर्क की संरचना पर जोर देने के लिए।