代码之家 › 专栏 › 技术社区 › user1868607

过渡系统上的有限运行

isabelle

0

user1868607 · 技术社区 · 7 年前

我想写一个谓词,声明一个转换系统不能从一个状态s无限运行。所以考虑到转换系统是由r给出的,那么我得出的定义是:

inductive finite_runs for R where         
"(â s'. R s s' â¶ finite_runs R s') â¹ finite_runs R s"

这是我在伊莎贝尔陈述这一事实最简单的方式吗?特别是,我浏览了形式证明的档案(重写和标记的转换理论),但没有得到更简单的解决方案。

2 回复 | 直到 7 年前

1

Manuel Eberl 7 年前

有 Wellfounded.termip 在标准库中。我认为它应该做你想做的。

它基本上是一个缩写,使用 Wellfounded.accp 做同样的事情,但要向后移动。

2

0

René Thiemann 7 年前

如果您的意思是有限次运行意味着没有无限次运行,那么可以使用强规范化谓词 SN_on AFP条目摘要重写。但是你的定义也允许

A->A->A->…

这是不允许的 SNON .