Theory Name

theory Name
imports Basis
(*  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