Inductive predicates, transitive closure, and code generation

Question

I am defining subclass and subtype relations as inductive predicates for a Java-like language and would like to generate code for these relations. Defining and generating code for the subtype relation was no problem:

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 .

Here, is_subclass1 P C C' is true if C' is the name of the direct superclass of C. Then is_subclass is defined to be the transitive closure of is_subclass1.

For code generation to work, it is crucial that is_subclass1 has the mode i ⇒ i ⇒ o ⇒ bool, because otherwise the transitive closure cannot be computed. In the case of is_subclass1 this is easy, as a class has at most a single direct superclass, and the name of the superclass can thus be uniquely determined from the inputs.

However, for the subtype relation I also need to consider the interfaces that a class might implement:

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'"

The problem is that there are multiple possible values for C' and that it cannot be marked as an output.

Intuitively, I think this should not be a problem for the code generator, as the generated code could just iterate over all the interfaces of a class. However, I don't know if this can be expressed in Isabelle/HOL.

Thus, the question is: Is there a way to generate code for is_subtype1 with mode i ⇒ i ⇒ o ⇒ bool?

Answer 1

You can solve your problem by importing HOL-Library.Predicate_Compile_Alternative_Defs and then using List.member _ _ instead of _ ∈ set _.