Theory Name

Up to index of Isabelle/Bali5

(*  Title:      isabelle/Bali/Name.thy
    ID:         $Id: Name.thy,v 1.6 2001/05/11 14:41:58 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java names

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

theory Name = Basis:

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

arities
  tnam :: "term"
  ename :: "term"
  mname :: "term"

types    lname           (* names for local variables and the This pointer *)
        = "ename + unit"
syntax   
  EName :: lname
  This :: lname

translations
  "lname" <= (type) "ename + unit"
  "EName" => "Inl"
  "This"  => "Inr ()"

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

lemma xn_cases: 
  "\<forall> xn. xn = Throwable   \<or> xn = NullPointer \<or>  
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
apply (rule allI)
apply (induct_tac "xn")
apply auto
done

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

lemma xn_cases:

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