'नियम (नियम)' या 'सबूत' उपयोग किस नियम पर है?

Question

जब मैं लागू-स्क्रिप्ट में apply (rule) का उपयोग करता हूं, आमतौर पर एक उचित नियम चुना जाता है। संरचित सबूत में proof के लिए भी यही है। इस्तेमाल किए गए नियम के नाम को मैं कहां/सीख सकता हूं?

Answer 1

आप इस प्रकार rule_trace उपयोग करने का प्रयास कर सकते हैं:

lemma "a ∧ b" 
    using [[rule_trace]] 
    apply rule 

जो उत्पादन में प्रदर्शित होगा:

rules: 
    ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
    ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
proof (prove): step 2 

goal (2 subgoals): 
1. a 
2. b 

हैं नियमों के नाम की आवश्यकता है, तो आप find_theorems का उपयोग करने का प्रयास कर सकते हैं; मुझे यकीन नहीं है कि क्या उन्हें सीधे निर्धारित किया जा सकता है।

Answer 2

सब कुछ है कि के रूप में Pure.intro/intro/iff (या इसके ? या ! वेरिएंट में से एक) घोषित किया जाता है डिफ़ॉल्ट परिचय नियम के रूप में माना जाता है (यानी, कोई वर्तमान तथ्यों में श्रृंखलित रहे हैं)। इसी प्रकार, Pure.elim/elim/iff के रूप में घोषित किया गया सब कुछ डिफ़ॉल्ट उन्मूलन नियम (यानी, यदि वर्तमान तथ्यों में शामिल है) के रूप में माना जाता है। आम तौर पर बाद में घोषणाएं पहले की तुलना में प्राथमिकता लेती हैं (कम से कम अगर समान प्रकार की घोषणा का उपयोग किया जाता है ... मिश्रण, उदाहरण के लिए, Pure.intro?intro आदि के साथ, अलग-अलग हो सकता है)।

हालांकि, यह सिर्फ उत्तर देता है कि सिद्धांत में किस प्रकार के नियमों पर विचार किया जाता है। मुझे सीधे यह पता लगाने का कोई तरीका नहीं पता कि कौन सा नियम लागू किया गया था। लेकिन यह उस रेखा से ऊपर find_theorems intro द्वारा सही नियम खोजने के लिए अपेक्षाकृत सीधे आगे है, जिसके बारे में आप सोच रहे थे। जैसे,

lemma "A & B" 
find_theorems intro 
proof 

आप सभी नियमों का उस लक्ष्य को A & B का परिचय नियम के रूप में लागू किया जा सकता दिखाएगा। उनमें से एक डिफ़ॉल्ट नियम है जिसे proof द्वारा लागू किया गया है (आप इसे प्राप्त उपगोर्गों द्वारा पहचान लेंगे)।

उन्मूलन नियम आप उपयोग कर सकते हैं, उदाहरण के लिए,

lemma assumes "A | B" shows "P" 
using assms 
find_theorems elim 
proof 

Answer 3

अन्य उत्तरों पहले से ही आपको यह निर्धारित करने के लिए बताते हैं कि rule द्वारा कौन से लेमा लागू किए जाते हैं। ध्यान दें कि proofrule पर कॉल नहीं करता है, लेकिन विधि default। अधिकांश समय, defaultrule जैसा ही है, लेकिन उदा। एक लोकेल भविष्यवाणी करने के लिए यह unfold_locales पर कॉल करता है।

मुझे यह देखने के लिए किसी विधि की जानकारी नहीं है कि वास्तव में वहां क्या होता है।