計算傳遞閉

我有以下定義：計算傳遞閉

definition someRel :: "nat rel" 
where 
    "someRel = {(1, 2), (2, 3), (3, 4), (4, 5)}"

我要證明以下引理：

lemma "someRel^*``{1}={1, 2, 3, 4, 5}"

我設計了以下證明：

proof 
    show "someRel^*``{1} ⊆ {1, 2, 3, 4, 5}" 
    proof 
    fix x 
    assume "x ∈ someRel⇧* `` {1}" 
    then show "x ∈ {1, 2, 3, 4, 5}" 
     using assms someRel_def by (auto elim: rtranclE) 
    qed 
next 
    show "{1, 2, 3, 4, 5} ⊆ someRel^*``{1}" 
    proof 
    fix x 
    assume "x ∈ {1::nat, 2, 3, 4, 5}" 
    then show "x ∈ someRel⇧* `` {1}" 
     using assms someRel_def Image_singleton by (induction) blast+ 
    qed 
qed

這個證明有以下問題：

使用規則 rtranclE證明了第一部分（show "someRel^*``{1} ⊆ {1, 2, 3, 4, 5}"）。如果我向someRel關係中添加一對（如對(6, 7)）
第二部分的證明（show "{1, 2, 3, 4, 5} ⊆ someRel^*``{1}"）不會終止。

任何人都可以提出更好的證據嗎？（a）允許someRel關係中的更多對和（b）終止。

來源

2014-09-02 Nuno Amálio

小意見：只要涉及非終止方法/策略，我不會談論「證明」。 – chris 2014-09-03 08:08:09

在你的證明嘗試的第二部分中，「使用assms」並不是真正有意義的（'assms'指的是你的引理的全部假設，根本沒有）。而不是'使用someRel_def'，你可能想通過'展開someRel_def'展開'someRel'的定義。 – chris 2014-09-03 08:18:44

事實證明，針對您的具體實例（和一些稍大一點的人我試過），以下就足夠了（通過首先將auto，然後運行在剩餘的目標sledgehammer識別有用的事實，像converse_rtrancl_into_rtrancl這裏找到）：

by (auto simp: someRel_def converse_rtrancl_into_rtrancl elim: rtranclE)

然而，在總體上可能是一個更好的主意，做下列操作之一：

設備的策略，以證明這些目標（按實際計算所涉及的傳遞閉包）
計算Isabelle/HOL內部的傳遞封閉（通過simp--可能會很慢 - 或通過eval--據我所知，它是一種預言）。

對於後者，法新社項目 Executable Transitive Closures可能是感興趣的。

更新：我添加了一個simproc的例子，它通過評估AFP的開發版本來計算有限集上的有限傳遞閉包的圖像。而不是可執行傳遞閉包但是，我基於 Executable Transitive Closures of Finite Relations上的示例。您的示例可在理論最後找到 Finite_Transitive_Closure_Simprocs（只要法新社網站與底層的mercurial存儲庫同步）。

更新：注意的是，上述simproc是專門針對形式r^* `` x的圖案，其中套r和x是有限的意義上，它們是在有限集合符號{x1, x2, ..., xN}給出。因此，爲了觸發一個特定的目標，你可能必須添加額外的事實/ simp規則/ simprocs/...，以便將表達規範化爲這種形式。

例如：如果你有目標

"(converse someRel)^* `` {1} = {1}"

你就必須補充一點，實際上是在給定的有限集合「應用」的converse操作規則。下面會做：

lemma [simp]: 
    "converse (insert (x, y) A) = insert (y, x) (converse A)" 
    by auto

現在的目標可以通過

by (auto simp: someRel_def)

來源

2014-09-03 08:35:06 chris

我認爲在這種情況下，應用證明看起來更好。我得到以下幾點：引理「someRel^*''{1} = {1,2,3,4,5}」 apply（rule equalityI） apply（simp add：someRel_def Image_singleton） apply（rule subsetI ，簡體）申請（erule rtranclE，BLAST）申請（自動琳：Image_singleton converse_rtrancl_into_rtrancl琳：rtranclE）由（自動SIMP someRel_def 展開rtranclE） – 2014-09-04 13:46:02

我無法訪問的理論，您所提供。有什麼不對的嗎？或者我應該等待？ – 2014-09-05 14:38:31

原則上等待......同時您可以直接訪問mercurial repository [here]（http://sourceforge.net/p/afp/code/ci/default/tree/thys/Transitive-Closure/Finite_Transitive_Closure_Simprocs。你）。 – chris 2014-09-05 18:37:23

添加到克里斯的回答解決了，這裏是它使用AFP-條目傳遞閉完整版，並確實使用code-simp而不是eval。 code-simp比eval慢一些，但不依賴於oracles。

theory Test 
imports "$AFP/Transitive-Closure/Transitive_Closure_List_Impl" 
begin 

lemma to_memo_list: "(set xs)^* `` {a} = set (memo_list_rtrancl xs a)" 
    unfolding memo_list_rtrancl Image_def by auto 

definition someRel :: "nat rel" 
where 
    "someRel = {(1, 2), (2, 3), (3, 4), (4, 5), (5,3)}" 

definition someRel_list :: "(nat × nat)list" 
where 
    "someRel_list = [(1, 2), (2, 3), (3, 4), (4, 5), (5,3)]" 

lemma someRel_list: "someRel = set someRel_list" by code_simp 

lemma "someRel^*``{4}={3, 4, 5}" 
    unfolding someRel_list to_memo_list by code_simp 

end

來源

2016-01-11 15:51:24

回答

相關問題