归纳谓词、传递闭包和代码生成

Question

我将子类和子类型关系定义为类Java语言的归纳谓词，并希望为这些关系生成代码。为子类型关系定义和生成代码没有问题：

type_synonym class_name = string
record class_def =
cname :: class_name
super :: "class_name option"
interfaces :: "class_name list"
type_synonym program = "class_def list"
(* Look up a class by its name *)
definition lookup_class :: "program ⇒ class_name ⇒ class_def option" where
"lookup_class P C ≡ find (λcl. (class_def.cname cl) = C) P"
(* Direct subclass relation *)
inductive is_subclass1 :: "program ⇒ class_name ⇒ class_name ⇒ bool" where
"⟦
Some cl = lookup_class P C;
(class_def.super cl) = Some C'
⟧ ⟹ is_subclass1 P C C'"
(* Reflexive transitive closure of `is_subclass1` *)
definition is_subclass :: "program ⇒ class_name ⇒ class_name ⇒ bool" where
"is_subclass P C C' ≡ (is_subclass1 P)⇧*⇧* C C'"

code_pred(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool) is_subclass1 .
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
[inductify]
is_subclass .

在这里，如果C'是C的直接超类的名称，则is_subclass1 P C C'为真。然后is_subclass定义为is_subclass1的传递闭包。

为了使代码生成工作，is_subclass1具有模式i ⇒ i ⇒ o ⇒ bool是至关重要的，因为否则无法计算传递闭包。在is_subclass1的情况下，这很容易，因为一个类最多只有一个直接超类，因此可以从输入中唯一地确定超类的名称。

但是，对于子类型关系，我还需要考虑类可能实现的接口：

inductive is_subtype1 :: "program ⇒ class_name ⇒ class_name ⇒ bool" for P :: program where
― ‹Same as subclass relation, no problem›
"⟦
Ok cl = lookup_class P C;
Some C' = (class_def.super cl)
⟧ ⟹ is_subtype1 P C C'" |
"⟦
Ok cl = lookup_class P C;
― ‹HERE IS THE PROBLEM: C' cannot be uniquely derived from the inputs and can thus not be marked as an output›
C' ∈ set (class_def.interfaces cl)
⟧ ⟹ is_subtype1 P C C'"

问题是C'有多个可能的值，并且无法将其标记为输出。

直观地说，我认为这对代码生成器来说应该不是问题，因为生成的代码可以遍历一个类的所有接口。但是，我不知道这是否可以用Isabelle/HOL来表达。

因此，问题是：有没有办法使用模式i ⇒ i ⇒ o ⇒ bool生成is_subtype1代码？

Answer 1

您可以通过导入HOL-Library.Predicate_Compile_Alternative_Defs然后使用List.member _ _而不是_ ∈ set _来解决问题。