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

如何解决归纳谓词，可传递闭包和代码生成

我正在将子类和子类型关系定义为类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 .

在此，如果is_subclass1 P C C'是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表示。

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

解决方法

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