我正在尝试定义代码方程式：
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"
并得到以下警告：
Partially applied constant "less_t" on left hand side of equation, in theorem:
less_t⇧+⇧+ ?x ?y ≡ less_t_fun ?x ?y
这个问题与传递闭包无关。对于不同的定理，我已经收到这样的警告：
我只需要了解此警告的含义以及如何解决它。也许我应该定义一个不同的引理？
问题在于引理的结构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]看看到代码生成的文档。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句