(*  Title:      HOL/Bali/Name.thy
    Author:     David von Oheimb
*)
subsection ‹Java names›

theory Name imports Basis begin

(* cf. 6.5 *) 
typedecl tnam   ― ‹ordinary type name, i.e. class or interface name›
typedecl pname  ― ‹package name›
typedecl mname  ― ‹method name›
typedecl vname  ― ‹variable or field name›
typedecl label  ― ‹label as destination of break or continue›

datatype ename        ― ‹expression name›
        = VNam vname 
        | Res         ― ‹special name to model the return value of methods›

datatype lname        ― ‹names for local variables and the This pointer›
        = EName ename 
        | This
abbreviation VName   :: "vname → lname"
      where "VName n == EName (VNam n)"

abbreviation Result :: lname
      where "Result == EName Res"

datatype xname          ― ‹names of standard exceptions›
        = Throwable
        | NullPointer | OutOfMemory | ClassCast   
        | NegArrSize  | IndOutBound | ArrStore

lemma xn_cases: 
  "xn = Throwable ∨ xn = NullPointer ∨
         xn = OutOfMemory ∨ xn = ClassCast ∨
         xn = NegArrSize ∨ xn = IndOutBound ∨ xn = ArrStore"
apply (induct xn)
apply auto
done


datatype tname  ― ‹type names for standard classes and other type names›
        = Object'
        | SXcpt'   xname
        | TName   tnam

record   qtname = ― ‹qualified tname cf. 6.5.3, 6.5.4›
          pid :: pname  
          tid :: tname

class has_pname =
  fixes pname :: "'a → pname"

instantiation pname :: has_pname
begin

definition
  pname_pname_def: "pname (p::pname) ≡ p"

instance ..

end

class has_tname =
  fixes tname :: "'a → tname"

instantiation tname :: has_tname
begin

definition
  tname_tname_def: "tname (t::tname) = t"

instance ..

end

definition
  qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"

translations
  (type) "qtname" <= (type) "(pid::pname,tid::tname)"
  (type) "'a qtname_scheme" <= (type) "(pid::pname,tid::tname,…::'a)"


axiomatization java_lang::pname ― ‹package java.lang›

definition
  Object :: qtname
  where "Object = (pid = java_lang, tid = Object')"

definition SXcpt :: "xname → qtname"
  where "SXcpt = (λx. (pid = java_lang, tid = SXcpt' x))"

lemma Object_neq_SXcpt [simp]: "Object ≠ SXcpt xn"
by (simp add: Object_def SXcpt_def)

lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
by (simp add: SXcpt_def)

end