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?

What are the theory imports? The predicate compiler by default doesn't handle _ ∈ set _, but it should if you import HOL-Library.Predicate_Compile_Alternative_Defs. I cannot test this though as the above code is missing the definitions for Program, get_class, etc. — Andreas Lochbihler
Ah, sorry, I did some copy/paste errors. The definition of is_subtype1 now also uses lookup_class etc like the first snippet. I do not think it's because of _ ∈ set _ because code generation works for the mode i ⇒ i ⇒ i ⇒ bool (I just tried HOL-Library.Predicate_Compile_Alternative_Defs but it does not seem to make a difference). I also tried replacing _ ∈ set _ with a function contains :: 'a ⇒ 'a list ⇒ bool, but this also didn't work. — DaviD.
Yes, thank you! Totally overlooked List.member, now it's working! (If you post an answer I will accept it) — DaviD.
Also, since something like values "{c. is_subtype <program> <class> c}" will loop forever, you might need to add alternative introduction rules for rtranclp along the lines of Section 4.2 from Code generation from Isabelle/HOL theories in the Isabelle documentation. — Javier Díaz

Javier Díaz Javier Díaz · Accepted Answer · 2020-11-09T20:36:00

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

Inductive predicates, transitive closure, and code generation

1 Answers