enrich javatype , 
       intnat
 , 
       predefined with
   functions 
       . .jtclass : javatype → classname;
      comment: select classname from a class- or 
                      arraytype (the innermost type of the array should be a class type, 
                      i.e. has_classtype should be true.;
       
       . .jtelemtype : javatype → javatype;
      comment: select innermost element type from an
                      array type.;
       
       . .jtdims : javatype → int;
      mktype_from_dims : javatype × int → javatype;
   predicates 
      type∃ : string × javatype;
      comment: true if class in tdname+.;
       
      tdname∃ : string × classname;
      comment: user defined class or interface.
                                                   Derived from class∃/interface∃.;
       
      tdname+∃ : string × classname;
      comment: derived from class∃/interface∃.;
       
      class+∃ : string × classname;
      comment: user defined or predefined class.
                                                   Derived from class∃/interface∃.;
       
      class∃ : string × classname;
      comment: user defined class.
                                                   no axioms, added by Java classes.;
       
      interface∃ : string × classname;
      comment: user defined interface.
                                                   no axioms, added by Java classes.;
       
      is_abstract : classname;
      comment: true if classname is an abstract class.
                                          No axioms, added by Java classes.;
       
      has_classtype : javatype;
      comment: true if class or array(...class);
       
      is_reftype : javatype;
      comment: true if class or array;
       
      is_primtype : javatype;
      comment: true if primitive type;
       
       . ≤ . : javatype × javatype;
      comment: check if ty1 ≤ t2 (using ≤ on classes if necessary);
       
      is_subtype : string × javatype × javatype;
      comment: true if classes exist and ty1 ≤ t2, string is level.;
       
      is_subtype : javatype × javatype × classnameset;
      comment: check if ty1 ≤ ty2. classes are all subclasses of ty2.;
       
      is_subtype : javatype × classnames × javatype;
      comment: check if ty1 ≤ ty2. classes are all superclasses of ty1.;
       
      is_subclass : classname × classnames × classname;
      comment: check if c1 ≤ c2. classes are all superclasses of c1.;
       
   
   axioms 
      classex-notpredef :  ⊦ class∃(str, class) → ¬ is_predefined_class(class);
      comment: for some generic theorems, can be derived for every concrete level.;
      used for : s, ls;
       
      classex-nointerface :  ⊦ class∃(str, class) → ¬ interface∃(str, class);
      comment: for some generic theorems, can be derived for every concrete level.;
      used for : s, ls;
       
      interfaceex-notpredef :  ⊦ interface∃(str, class) → ¬ is_predefined_class(class);
      comment: for some generic theorems, can be derived for every concrete level.;
      used for : s, ls;
       
      is_abstract-predef :  ⊦ is_predefined_class(class) → ¬ is_abstract(class);
      comment: This axiom is needed!;
      used for : s, ls;
       
      classex-object :  ⊦ class∃(str, class) → class ≤ `java.lang.Object' .class;
      comment: no longer needed, every class is ≤ Object.;
      used for : s, ls;
       
      interfaceex-object :  ⊦ interface∃(str, class) → class ≤ `java.lang.Object' .class;
      comment: no longer needed, every interface is ≤ Object.;
      used for : s, ls;
       
      tdnameex-def :  ⊦ tdname∃(str, class) ↔ class∃(str, class) ∨ interface∃(str, class);
      tdname+ex-def :  ⊦ tdname+∃(str, class) ↔ tdname∃(str, class) ∨ is_predefined_class(class);
      classex-def :  ⊦ class+∃(str, class) ↔ class∃(str, class) ∨ is_predefined_class(class);
      typeex-def :  ⊦ type∃(str, ty) ↔ ¬ has_classtype(ty) ∨ tdname+∃(str, ty .jtclass);
      mktype_base :  ⊦ i ≤ 0 → mktype_from_dims(ty, i) = ty;
      used for : s, ls;
       
      mktype_rec :  ⊦ 0 < i → mktype_from_dims(ty, i) = mkarraytype(mktype_from_dims(ty, i - 1));
      dims-base :  ⊦ ¬ is_arraytype(ty) → ty .jtdims = 0;
      used for : s, ls;
       
      dims-rec :  ⊦ is_arraytype(ty) → ty .jtdims = ty .type .jtdims + 1;
      used for : s, ls;
       
      is-reftype :  ⊦ is_reftype(ty) ↔ is_classtype(ty) ∨ is_arraytype(ty);
      is_primtype
      : ⊦ 
          is_primtype(ty)
        ↔ ty = boolean_type ∨ ty = int_type ∨ ty = short_type ∨ ty = byte_type ∨ ty = long_type ∨ ty = float_type ∨ ty = double_type ∨ ty = char_type;
      elemtype-base :  ⊦ ¬ is_arraytype(ty) → ty .jtelemtype = ty;
      used for : s, ls;
       
      elemtype-rec :  ⊦ is_arraytype(ty) → ty .jtelemtype = ty .type .jtelemtype;
      used for : s, ls;
       
      has-classtype :  ⊦ has_classtype(ty) ↔ is_classtype(ty .jtelemtype);
      used for : ls;
       
      jtclass :  ⊦ ty .jtclass = ty .jtelemtype .class;
      used for : s, ls;
       
      subclass :  ⊦ mkclasstype(class1) ≤ mkclasstype(class2) ↔ class1 ≤ class2;
      used for : s, ls;
       
      subarray1 :  ⊦ mkarraytype(ty) ≤ mkarraytype(ty0) ↔ ty ≤ ty0;
      used for : s, ls;
       
      subarray2 :  ⊦ mkarraytype(ty) ≤ mkclasstype(class1) ↔ class1 = `java.lang.Object' .class;
      used for : s, ls;
       
      subarray3 :  ⊦ ¬ mkclasstype(class1) ≤ mkarraytype(ty);
      used for : s, ls;
       
      subbasic1 :  ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (ty ≤ ty0 ↔ ty = ty0);
      used for : s, ls;
       
      subbasic2 :  ⊦ ¬ is_classtype(ty0) ∧ ¬ is_arraytype(ty0) → (ty ≤ ty0 ↔ ty = ty0);
      used for : s, ls;
       
      subtype-arr :  ⊦ is_subtype(ty1, mkarraytype(ty2), claset) ↔ is_arraytype(ty1) ∧ is_subtype(ty1 .type, ty2, claset);
      used for : s, ls;
       
      subtype-obj :  ⊦ is_subtype(ty1, mkclasstype(`java.lang.Object' .class), claset) ↔ is_reftype(ty1);
      used for : s, ls;
       
      subtype-cla :  ⊦ class ≠ `java.lang.Object' .class → (is_subtype(ty1, mkclasstype(class), claset) ↔ is_classtype(ty1) ∧ ty1 .class ∈ claset);
      used for : s, ls;
       
      subtype-other :  ⊦ ¬ is_reftype(ty2) → (is_subtype(ty1, ty2, claset) ↔ ty1 = ty2);
      used for : s, ls;
       
      subsups-arr
      : ⊦ 
          is_subtype(mkarraytype(ty1), classes, ty2)
        ↔ ty2 = mkclasstype(`java.lang.Object' .class) ∨ is_arraytype(ty2) ∧ is_subtype(ty1, classes, ty2 .type);
      used for : s, ls;
       
      subsups-cla :  ⊦ is_subtype(mkclasstype(class), classes, ty2) ↔ is_classtype(ty2) ∧ is_subclass(class, classes, ty2 .class);
      used for : s, ls;
       
      subsups-other :  ⊦ ¬ is_reftype(ty1) → (is_subtype(ty1, classes, ty2) ↔ ty1 = ty2);
      used for : s, ls;
       
      subclass-pre :  ⊦ is_predefined_class(class1) → (is_subclass(class1, classes, class2) ↔ class2 ∈ predef_supers(class1));
      used for : s, ls;
       
      subclass-other
      :  ⊦ ¬ is_predefined_class(class1) → (is_subclass(class1, classes, class2) ↔ class2 = `java.lang.Object' .class ∨ class2 ∈ classes);
      used for : s, ls;
       
      is_subtype-level
      : ⊦ 
          is_subtype(str, ty1, ty2)
        ↔ ty1 ≤ ty2 ∧ (has_classtype(ty1) → tdname+∃(str, ty1 .jtclass)) ∧ (has_classtype(ty2) → tdname+∃(str, ty2 .jtclass));
end enrich