当简化引理时，为什么程序不终止程序？

发布于 2025-02-12 22:06:27 字数 1047 浏览 0 评论 0原文

我正在使用isabelle使用函数apptransfrule（env n）r来简化引理 r是一个大型公式，并带有数百个连词。实际上，当R很小时，可以终止此过程。有人可以告诉我简化的程序做什么吗？是什么原因导致卡住？谢谢！

lemma abs_NI_Remote_GetX_PutX_Home_ref : 
"[|M <= N;dst <= M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
NI_Remote_GetX_PutX_Home_ref M dst"             
"[|M <= N;dst > M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
ABS_NI_Remote_GetX_PutX_Home M"
unfolding NI_Remote_GetX_PutX_Home_ref_def 
NI_Remote_GetX_PutX_Home_ref_def ABS_NI_Remote_GetX_PutX_Home_def  apply(auto simp 
add: Let_def )   
done

这是对问题的附加描述 [1]： https://i.sstatic.net/gdanr.gdanr.png [2]： https://i.sstatic.net/syfoz.png [3]： https://i.sstatic.net/z1qko.png

原文

I'm using Isabelle to simplify a lemma using a functionabsTransfRule (env N) r
and the r is a big formula with conjunctions of hundreds of conjuntals. In fact, when the r is small, this process can be terminated. Can someone tell me what does the simplifying procedure do? What causes the stuck? Thanks!

lemma abs_NI_Remote_GetX_PutX_Home_ref : 
"[|M <= N;dst <= M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
NI_Remote_GetX_PutX_Home_ref M dst"             
"[|M <= N;dst > M|] 
==> absTransfRule (env N) M (NI_Remote_GetX_PutX_Home_ref N dst) = 
ABS_NI_Remote_GetX_PutX_Home M"
unfolding NI_Remote_GetX_PutX_Home_ref_def 
NI_Remote_GetX_PutX_Home_ref_def ABS_NI_Remote_GetX_PutX_Home_def  apply(auto simp 
add: Let_def )   
done

This is an additional description of the problem
[1]: https://i.sstatic.net/GdaNr.png
[2]: https://i.sstatic.net/syfOZ.png
[3]: https://i.sstatic.net/Z1QKO.png

分享到QQ

分享到微博