क्या इसाबेल में कोई सिद्धांत आयात करना संभव नहीं है?

Question

मैं List नामक सिद्धांत में अपनी खुद की सूची प्रकार को परिभाषित करना चाहता हूं, लेकिन उस नाम के साथ पहले से ही एक सिद्धांत है। क्या Main से अधिक हल्का सिद्धांत है?

Answer 1

आप इसाबेल में कुछ भी आयात नहीं कर सकते (क्योंकि आयात मूल तर्क के लिए भी आवश्यक है)। इसाबेल में एचओएल के कार्यान्वयन में तीन समर्थित प्रवेश बिंदु हैं: Main, Complex_Main (जो Main प्लस कुछ विश्लेषण है) और Plain, लेकिन केवल पहले दो नियमित उपयोग के लिए इच्छुक हैं।

सादा में पहले से ही मूल तर्क शामिल है, लेकिन मानक पुस्तकालय (उदा। कोई सूचियां) के संदर्भ में लगभग कुछ भी नहीं है। लेकिन क्विक चेक, स्लेजहैमर और कोड जनरेटर जैसे महत्वपूर्ण टूल भी गायब हैं। इसके अलावा, यदि आप अपनी खुद की सिद्धांत सूची का नाम देने में सक्षम होने के लिए सादा से शुरू करते हैं, तो ध्यान रखें कि आपका सिद्धांत मुख्य पर किसी भी कार्य भवन के साथ असंगत होगा (जो लगभग सबकुछ है)।

इसलिए, जब तक आपके पास ऐसा करने के लिए वास्तव में अच्छे कारण नहीं हैं, तो मैं राफेल की टिप्पणी के बाद सुझाव दूंगा और अपनी सूची सिद्धांत का दूसरा नाम दूंगा।

Answer 2

आप केवल HOL आयात कर सकते हैं, के रूप में

theory Test_Theory 
imports HOL 
begin 
    … 
end 

में मैं अक्सर परीक्षण और इसाबेल के बारे में जांच के लिए करते हैं।

हालांकि, अगर आप डेटा प्रकार परिभाषाओं की कमी होगी, और शायद Datatype आयात करने के लिए की आवश्यकता होगी (और यहां तक ​​Record हो सकता है) के लिए अपने List सिद्धांत लिखने के लिए सक्षम होने के लिए के साथ-साथ,।

theory Test_Theory 
imports HOL Datatype Record 
begin 
    … 
end 

दोनों Datatype और Record आयात HOL के रूप में, आप बस हो सकता है:

theory Test_Theory 
imports Datatype Record 
begin 
    … 
end 

सिद्धांत Main के बिना ऐसा करने के लिए आसान है, लेकिन असंभव नहीं नहीं है यही कारण है कि। बस जागरूक रहें कि आपको कई व्यापक रूप से प्रयुक्त प्रमेय के बिना करना होगा, और आपको खुद को लिखना और साबित करना पड़ सकता है।

Answer 3

ध्यान दें कि $ISABELLE_HOME/src/HOL/ex/Seq.thy अपने Main प्रविष्टि बिंदु से नीचे सिस्टम के साथ काम करने के नाज़ुक प्रश्न को शुरू किए बिना, अपनी खुद की सूची डेटाटाइप को परिभाषित करने का एक न्यूनतम उदाहरण देता है। (शुरुआती भ्रमित हो और विशेषज्ञों यह मत करो।)

सैद्धांतिक रूप से, सबसे आदिम सिद्धांत आप आयात कर सकता है Pure है, लेकिन यह अभी तक सिर्फ नंगे हड्डियों तार्किक रूपरेखा है, HOL की तरह किसी भी वस्तु-तर्क के बिना। जिज्ञासा के लिए, आप $ISABELLE_HOME/src/HOL/ex/Higher_Order_Logic.thy देख सकते हैं जो Pure से शुरू होता है और एचओएल के न्यूनतम संस्करण को परिभाषित करता है। इसके शीर्ष पर, किसी भी उन्नत सिद्धांत और उपकरण के बिना आप पूरी इसाबेल/एचओएल से अपेक्षा करेंगे।