计算传递闭

我有以下定义：计算传递闭

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

回答

相关问题