एक विधि को लागू करें यदि और केवल यदि यह

Question

कभी कभी वर्तमान लक्ष्य को हल करती है, जब मैं लागू शैली सबूत लिख रहा हूँ, मैं

के लिए एक सबूत विधि foo संशोधित करने के लिए पहले पर foo प्रयास करें एक तरह से चाहते थे लक्ष्य। यदि यह लक्ष्य हल करता है, अच्छा; अगर यह इसे हल नहीं करता है, तो मूल स्थिति पर वापस लौटें और असफल हो जाएं। कुछ परिवर्तन के बाद

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+ 

आगे, simp करने के लिए कॉल पूरी तरह से एक लक्ष्य किसी भी अधिक का समाधान नहीं होगा, और फिर यह पाश होगा:

यह निम्न कोड में आया। (Synatx विकल्प का सुझाव दिया) मैं

qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+ 

या की तरह कुछ निर्दिष्ट किया जा सकता था, तो

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+ 

या (शायद भी अच्छे वाक्य रचना)

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+ 

यह पहला लक्ष्य पर रोका होगा कि इस लिपि द्वारा हल नहीं किया जा सका।

Answer 1

Eisbach proof script language के आगमन के बाद, यह अब समर्थित है । "~~/src/HOL/Eisbach/Eisbach" आयात करने के बाद, एक

apply (solves ‹foo›) 

साथ

apply foo 

जगह ले सकता है और लाइन असफल हो जायेगी अगर solves किसी भी नए लक्ष्यों को पैदा करता है। यह

apply (solves ‹(auto)[1]›) 

अगर वांछित के रूप [1] के साथ जोड़ा जा सकता है।

solves की परिभाषा वास्तव में काफी सरल है:

method solves methods m = (m; fail) 

Answer 2

इसाबेल जो कुछ मैं याद आती है, भी है ऐसी कोई Combinator है। अक्सर, मैं इस तरह के एक Combinator के लिए की जरूरत है, तो मैं द्वारा auto या simp कॉल की जगह से बच सकते हैं fastforce या force (जो हल या असफल व्यवहार है)।

तो, अपने उदाहरण में simp (पाशन के बिना) लक्ष्य हल करने के लिए,

qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+ 

एक और अधिक मजबूत संस्करण हो सकता है माना जाता है अगर।

Answer 3

इसाबेल की इस्सार भाषा उस सुविधा को प्रदान नहीं करती है; इस जानबूझकर और नहीं एक बग है, के रूप में समझाया on the isabelle developer list:

Isar सबूत विधि भाषा एक निश्चित तरीके से डिजाइन किया गया था, पर पहुंचने के लिए सबूत टेक्स्ट में "stilized" कुछ परिचालन पहलुओं के विनिर्देशों। इस उद्देश्य पर किसी भी प्रकार के प्रोग्रामिंग या परिष्कृत नियंत्रण संरचनाओं को बाहर रखा गया है।

Answer 4

जबकि वहाँ है कोई अंतर्निहित रणनीति या Combinator उपलब्ध है, तो आप एक अपने आप को लागू कर सकते हैं इस प्रकार है:

ML {* 
fun solved_tac thm = 
    if nprems_of thm = 0 then Seq.single thm else Seq.empty 
*} 

method_setup solved = {* 
    Scan.succeed (K (SIMPLE_METHOD solved_tac)) 
*} 

यह एक नई विधि solved है कि अगर वर्तमान लक्ष्य पूरी तरह से हल किया गया है सफल होगा बनाता है , या विफल रहता है अगर एक या अधिक सबगोल्स अभी भी शेष हैं।

यह उदाहरण के लिए, प्रयोग किया जा सकता, इस प्रकार है:

lemma "a ∨ ¬ a " 
    apply ((rule disjI1, solved) | (simp, solved)) 
    done 

solved खंड के बिना, इसाबेल apply कदम की rule disjI1 पक्ष का चयन करेंगे, एक न सुलझा हुआ लक्ष्य के साथ छोड़।प्रत्येक पक्ष में solved खंड के साथ, इसाबेल rule disjI1 का उपयोग करने का प्रयास करता है, और जब यह लक्ष्य को हल करने में विफल रहता है, तो simp पर स्विच करता है जो तब सफल होता है।

इसका उपयोग इसाबेल के (...)[1] सिंटैक्स का उपयोग कर व्यक्तिगत लक्ष्यों को हल करने के लिए किया जा सकता है। उदाहरण के लिए, निम्न कथन simp का उपयोग कर यथासंभव अधिक से अधिक subgoals का समाधान करने का प्रयास करेंगे, लेकिन एक subgoal अपरिवर्तित छोड़ देंगे अगर simp पूरी तरह से इसे हल करने में विफल रहता है:

apply ((simp, solved)[1])+