क्या स्वचालित रूप से संयोजन को विभाजित करने का कोई तरीका है?

Question

मैं इसाबेल में A /\ B /\ C /\ D /\ E /\ F साबित करना चाहता हूं। proof(rule ...) में मैं subgoal को 6 अलग-अलग सबगोल्स में कैसे विभाजित कर सकता हूं, तो फिर मैं उन्हें अलग-अलग साबित कर सकता हूं?

बेशक, मैं proof(rule conjI) 5 बार लिख सकता हूं, लेकिन हो सकता है कि एक चरण में विभाजन करने का एक और शानदार तरीका हो? सबूत के लिए इस तरह के लक्ष्यों को proof (intro conjI)

Answer 1

intro विधि का उपयोग करें। जैसे, के रूप में

lemma "A & B & C & D & E & F" 
proof - 
    { have "A" ... } 
    moreover 
    { have "B" ... } 
    moreover 
    { have "C" ... } 
    moreover 
    { have "D" ... } 
    moreover 
    { have "E" ... } 
    moreover 
    { have "F" ... } 
    ultimately 
    show ?thesis by blast 
qed 

इस प्रकार अंतर यहाँ है कि आप एक अधिक आगे सबूत (जो मैं कभी कभी अधिक पठनीय लगता है) करते हैं। आप बस जो कुछ जानते हैं उससे शुरू करें, आपको किसी भी बिंदु पर सबूत देना होगा और अंत में कुछ स्वचालित विधि (यहां blast) को "तुच्छ" चरणों को समझने दें।

Answer 2

एक और तरीका है कच्चे सबूत ब्लॉक का उपयोग करना है: