时间戳

首页 > 解决方案 > How to fix "partially applied constant on left hand side of code equation"?

isabelle - How to fix "partially applied constant on left hand side of code equation"?

问题描述

I'm trying to define the code equation:

datatype t = A | B | C

inductive less_t :: "t ⇒ t ⇒ bool" where
  "less_t A B"
| "less_t B C"

code_pred [show_modes] less_t .

fun less_t_fun :: "t ⇒ t ⇒ bool" where
  "less_t_fun A A = False"
| "less_t_fun A B = True"
| "less_t_fun A C = True"
| "less_t_fun B C = True"
| "less_t_fun B _ = False"
| "less_t_fun C _ = False"

lemma tancl_less_t_code [code]:
  "less_t⇧+⇧+ x y ⟷ less_t_fun x y"
  apply (rule iffI)
  apply (erule tranclp_trans_induct)
  apply (erule less_t.cases; simp)
  apply (metis less_t_fun.elims(2) less_t_fun.simps(3) t.simps(4))
  apply (induct rule: less_t_fun.induct; simp)
  using less_t.intros apply auto
  done

value "less_t A B"
value "less_t_fun A C"
value "less_t⇧+⇧+ A C"

And get the following warning:

Partially applied constant "less_t" on left hand side of equation, in theorem:
less_t⇧+⇧+ ?x ?y ≡ less_t_fun ?x ?y

This question is unrelated to transitive closures. I already received such a warning for different theorems:

I just need to understand the meaning of this warning and how to fix it. Maybe I should define a different lemma?

标签： isabelle

解决方案

问题是你的引理的结构tancl_less_t_code确实不适合作为代码方程。请注意，等式左侧的最外层常数是传递闭包谓词tranclp。因此，这告诉代码生成器使用引理来实现tranclp. 但是，使用您的引理只知道如何tranclp为一个特定谓词实现，即less_t. 因此，您收到 Isabelle 的抱怨，即您的实施过于具体。

至少有两种解决方法。

首先，[code]您可以使用[code unfold]. 然后在代码生成期间，每次出现的tranclp less_t x y都将被替换。less_t_fun为了使这条规则更加适用，我会将引理重新表述为tranclp less = less_t_fun，这样即使 tranclp less_t没有完全应用，展开也可以发生。

其次，您可以获取引理的对称版本并将其声明为 [simp]. 然后在您的实现中，您只需调用less_t_fun而不是 tranclp less_t在证明中，简化器将切换到后一个。

有关更多信息[code]并[code_unfold]查看代码生成器的文档。

推荐阅读