Theory Type

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/Type.thy
    ID:         $Id: Type.thy,v 1.20 2001/05/11 14:41:59 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
*)

theory 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" (** primrec not possible here **)
 
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)

end

lemma the_Class_eq:

  the_Class (Class C) = C