Theory Type

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/Type.thy
    ID:         $Id: Type.thy,v 1.19 2000/05/02 09:40:54 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java types

simplifications:
* only the most important primitive types
* the null type is regarded as reference type
*)

Type = Name +

datatype prim_ty        (* primitive type, cf. 4.2 *)
        = Void          (* 'result type' of void methods *)
        | Boolean
        | Integer


datatype ref_ty         (* reference type, cf. 4.3 *)
        = NullT         (* null type, cf. 4.1 *)
        | IfaceT tname  (* interface type *)
        | ClassT tname  (* class type *)
        | ArrayT ty     (* array type *)

and ty                  (* any type, cf. 4.1 *)
        = PrimT prim_ty (* primitive type *)
        | RefT  ref_ty  (* reference type *)

translations
  "prim_ty" <= (type) "Type.prim_ty"
  "ref_ty"  <= (type) "Type.ref_ty"
  "ty"      <= (type) "Type.ty"

syntax
         NT     :: "          ty"
         Iface  :: "tname  \<Rightarrow> ty"
         Class  :: "tname  \<Rightarrow> ty"
         Array  :: "ty     \<Rightarrow> ty"   ("_.[]" [90] 90)

translations
        "NT"      == "RefT   NullT"
        "Iface I" == "RefT (IfaceT I)"
        "Class C" == "RefT (ClassT C)"
        "T.[]"    == "RefT (ArrayT T)"

constdefs
  the_Class :: "ty \<Rightarrow> tname"
 "the_Class T \<equiv> \<epsilon>C. T = Class C"
 
end

theorem ty_exhaust:

  (EX pt. T = PrimT pt) | (EX rt. T = RefT rt)

theorem tyE:

  [| !!pt. T = PrimT pt ==> P; !!rt. T = RefT rt ==> P |] ==> P

theorem non_PrimT:

  (ALL pt. T ~= PrimT pt) = (EX t. T = RefT t)

theorem the_Class_eq:

  the_Class (Class C) = C