Theory Name

Up to index of Isabelle/HOL/Bali

theory Name
imports Basis
begin

(*  Title:      HOL/Bali/Name.thy
    ID:         $Id: Name.thy,v 1.9 2005/08/28 14:04:44 wenzelm Exp $
    Author:     David von Oheimb
*)
header {* 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
syntax   
  VName  :: "vname => lname"
  Result :: lname

translations
  "VName n" == "EName (VNam n)"
  "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

axclass has_pname < "type"
consts pname::"'a::has_pname => pname"

instance pname::has_pname ..

defs (overloaded)
pname_pname_def: "pname (p::pname) ≡ p"

axclass has_tname < "type"
consts tname::"'a::has_tname => tname"

instance tname::has_tname ..

defs (overloaded)
tname_tname_def: "tname (t::tname) ≡ t"

axclass has_qtname < type
consts qtname:: "'a::has_qtname => qtname"

instance qtname_ext_type :: (type) has_qtname ..

defs (overloaded)
qtname_qtname_def: "qtname (q::qtname) ≡ q"

translations
  "mname"  <= "Name.mname"
  "xname"  <= "Name.xname"
  "tname"  <= "Name.tname"
  "ename"  <= "Name.ename"
  "qtname" <= (type) "(|pid::pname,tid::tname|)),"
  (type) "'a qtname_scheme" <= (type) "(|pid::pname,tid::tname,…::'a|)),"


consts java_lang::pname --{* package java.lang *}

consts 
  Object :: qtname
  SXcpt  :: "xname => qtname"
defs
  Object_def: "Object  ≡ (|pid = java_lang, tid = Object_|)),"
  SXcpt_def:  "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

lemma xn_cases:

  xn = Throwable ∨
  xn = NullPointer ∨
  xn = OutOfMemory ∨
  xn = ClassCast ∨ xn = NegArrSize ∨ xn = IndOutBound ∨ xn = ArrStore

lemma Object_neq_SXcpt:

  Object ≠ SXcpt xn

lemma SXcpt_inject:

  (SXcpt xn = SXcpt xm) = (xn = xm)