應用的方法當且僅當它解決了當前的目標

有時，當我在寫申請風格的證明，我就想辦法修改論證方法foo到應用的方法當且僅當它解決了當前的目標

在第一次嘗試foo目標。如果它解決了這個目標，好的;如果沒有解決問題，則恢復到原始狀態並失敗。

這在下面的代碼上來：

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

一些變化後進一步上漲，調用simp就不能完全解決一個目標多提了，那麼這將循環。如果我可以指定類似

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

或（替代建議synatx）

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!])+

它會停在第一個目標是這個劇本無法解決。

來源

2013-03-08 Joachim Breitner

我想你'fibs.simps'或'fib.simps'觸發循環行爲（可能是由於一般的左側和如果在右側）？通常可以用條件規則來替換它們。 – 2013-03-08 09:42:57

我提交了一個[補丁實現這個]（https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-March/003911.html），讓我們看看會發生什麼。 – 2013-03-08 12:48:58

@Joachim Breitner：就我個人而言，我並不認爲在一個結構化證明（如你的例子）中這樣的怪物屬於「qed」;）。我總是希望在相應的「證明」/「qed」中明確地設置另一個子證明。但是，你正在談論'應用'腳本，對他們我完全同意。（也許你可以把你的例子中的qed變成'apply'？） – chris 2013-03-15 05:58:22

由於Eisbach proof script language的到來，這是現在支持。進口"~~/src/HOL/Eisbach/Eisbach"後，可以用

apply (solves ‹foo›)

更換

apply foo

，如果solves產生任何新的目標線將失敗。這可以與[1]相結合，如

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

如果需要的話。

的solves的定義其實很簡單：

method solves methods m = (m; fail)

來源

2016-05-20 08:12:32

伊莎貝爾沒有這樣的combinator，這也是我想念的東西。通常，如果我用fastforce或force（它們具有解決或失敗行爲）替換auto或simp調用，我可以避免使用這種組合器。

所以，如果在你的榜樣的simp應該解決的目標（不循環），

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

可能是一個更強大的變種。

來源

2013-03-08 09:40:47

啊，最後是使用'fastforce'或'force'的原因 - 我從來沒有覺得需要它們，只使用'auto'和'simp'。然而，是否有可能使用'ML {* .. *}'實現這樣一個組合器，還是那個部分不可擴展？ – 2013-03-08 10:11:07

Isabelle/Isar方法子語言可以通過'method_setup'擴展，但少數方法組合子是固定的。所以你可以根據任意複雜的戰術和策略來定義你自己的證明方法，但它不會改變證明方法表達式的風格化方式。 – Makarius 2013-03-08 11:39:23

伊莎貝爾伊薩爾語不提供該功能;這是故意的，而不是一個錯誤，因爲解釋on the isabelle developer list：

伊薩爾證明方法的語言被設計以某種方式，在到達的證明文本「stilized」的一些操作方面的規格。它已經排除了任何形式的編程或複雜的控制結構。

來源

2013-03-15 22:25:18

雖然沒有內置的策略或組合子可用，你可以自己實現一個如下：

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，然後成功。

這可以用於通過使用Isabelle的(...)[1]語法來解決個人目標。例如，下面的語句將嘗試使用simp解決儘可能多的子目標的可能，但會留下一個子目標不變，如果simp不能完全解決這個問題：

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

來源

2013-04-10 00:17:14 davidg

好極了，這使得我有'方法[1！]'（如果'方法'解決了第一個目標，即使還有其他目標，那麼這個方法就成功了]'（方法，解決）[1]'。 – 2013-04-10 09:11:26

我想我也開始了一些類似的代碼，這會產生一個'assert_goals n'方法，如果開放目標的數量是n，就會成功... – 2013-04-10 09:14:49

@JoachimBreitner：謝謝。我的意思是要提到這一點，但是它讓我放鬆了下來。我在最後添加了一個例子，希望可以幫助未來的搜索者。 – davidg 2013-04-10 23:51:04

應用的方法當且僅當它解決了當前的目標

回答

相關問題