Theory Name

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/Name.thy
    ID:         $Id: Name.thy,v 1.5 2000/06/29 19:35:31 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java names

simplifications:
no packages, thus no internal structure of names
*)

Name = Basis +

(* cf. 6.5 *)
types   tnam            (* ordinary type name, i.e. class or interface name *)
        ename           (* expression name, i.e. variable or field name *)
        mname           (* method name *)
arities tnam, ename, mname :: term

types    lname           (* names for local variables and the This pointer *)
        = "ename + unit"
syntax   EName, This :: lname
translations
  "lname" <= (type) "ename + unit"
  "EName" => "Inl"
  "This"  => "Inr ()"

datatype xname          (* names of standard exceptions *)
        = Throwable
        | NullPointer | OutOfMemory | ClassCast   
        | NegArrSize  | IndOutBound | ArrStore

datatype tname          (* type names for standard classes and other type names *)
        = Object
        | SXcpt   xname
        | TName   tnam

translations
  "mname" <= (type) "Name.mname"
  "xname" <= (type) "Name.xname"
  "tname" <= (type) "Name.tname"
  "ename" <= (type) "Name.ename"

end

theorem xn_cases:

  ALL xn.
     xn = Throwable |
     xn = NullPointer |
     xn = OutOfMemory |
     xn = ClassCast | xn = NegArrSize | xn = IndOutBound | xn = ArrStore
    [!]