src/HOL/BCV/JType.thy

ignore quick_and_dirty for coind;

(*  Title:      HOL/BCV/JType.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

The type system of the JVM
*)

JType = Err +

types cname
arities cname :: term

types subclass = "(cname*cname)set"

datatype ty = Void | Integer | NullT | Class cname

constdefs
 is_Class :: ty => bool
"is_Class T == case T of Void => False | Integer => False | NullT => False
               | Class C => True"

 is_ref :: ty => bool
"is_ref T == T=NullT | is_Class T"

 subtype :: subclass => ty ord
"subtype S T1 T2 ==
 (T1=T2) | T1=NullT & is_Class T2 |
 (? C D. T1 = Class C & T2 = Class D & (C,D) : S^*)"

 sup :: "subclass => ty => ty => ty err"
"sup S T1 T2 ==
 case T1 of Void => (case T2 of Void    => OK Void
                              | Integer => Err
                              | NullT   => Err
                              | Class D => Err)
          | Integer => (case T2 of Void    => Err
                                 | Integer => OK Integer
                                 | NullT   => Err
                                 | Class D => Err)
          | NullT => (case T2 of Void    => Err
                               | Integer => Err
                               | NullT   => OK NullT
                               | Class D => OK(Class D))
          | Class C => (case T2 of Void    => Err
                                 | Integer => Err
                                 | NullT   => OK(Class C)
                                 | Class D => OK(Class(some_lub (S^*) C D)))"

 Object :: cname
"Object == arbitrary"

 is_type :: subclass => ty => bool
"is_type S T == case T of Void => True | Integer => True | NullT => True
                | Class C => (C,Object):S^*"

syntax
 "types" :: subclass => ty set
 "@subty" :: ty => subclass => ty => bool  ("(_ /[='__ _)" [50, 1000, 51] 50)
translations
 "types S" == "Collect(is_type S)"
 "x [=_S y"  == "x <=_(subtype S) y"

constdefs
 esl :: "subclass => ty esl"
"esl S == (types S, subtype S, sup S)"

end