src/HOL/Bali/Name.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Name.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,123 @@
     1.4 +(*  Title:      isabelle/Bali/Name.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* Java names *}
    1.10 +
    1.11 +theory Name = Basis:
    1.12 +
    1.13 +(* cf. 6.5 *) 
    1.14 +typedecl tnam		(* ordinary type name, i.e. class or interface name *)
    1.15 +typedecl pname          (* package name *)
    1.16 +typedecl mname		(* method name *)
    1.17 +typedecl vname          (* variable or field name *)
    1.18 +typedecl label          (* label as destination of break or continue *)
    1.19 +
    1.20 +arities
    1.21 +  tnam  :: "type"
    1.22 +  pname :: "type"
    1.23 +  vname :: "type"
    1.24 +  mname :: "type"
    1.25 +  label :: "type"
    1.26 +
    1.27 +
    1.28 +datatype ename        (* expression name *) 
    1.29 +        = VNam vname 
    1.30 +        | Res         (* special name to model the return value of methods *)
    1.31 +
    1.32 +datatype lname        (* names for local variables and the This pointer *)
    1.33 +        = EName ename 
    1.34 +        | This
    1.35 +syntax   
    1.36 +  VName  :: "vname \<Rightarrow> lname"
    1.37 +  Result :: lname
    1.38 +
    1.39 +translations
    1.40 +  "VName n" == "EName (VNam n)"
    1.41 +  "Result"  == "EName Res"
    1.42 +
    1.43 +datatype xname		(* names of standard exceptions *)
    1.44 +	= Throwable
    1.45 +	| NullPointer | OutOfMemory | ClassCast   
    1.46 +	| NegArrSize  | IndOutBound | ArrStore
    1.47 +
    1.48 +lemma xn_cases: 
    1.49 +  "xn = Throwable   \<or> xn = NullPointer \<or>  
    1.50 +         xn = OutOfMemory \<or> xn = ClassCast \<or> 
    1.51 +         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
    1.52 +apply (induct xn)
    1.53 +apply auto
    1.54 +done
    1.55 +
    1.56 +lemma xn_cases_old:   (* FIXME cf. Example.thy *)
    1.57 +  "ALL xn. xn = Throwable   \<or> xn = NullPointer \<or>  
    1.58 +         xn = OutOfMemory \<or> xn = ClassCast \<or> 
    1.59 +         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
    1.60 +apply (rule allI)
    1.61 +apply (induct_tac xn)
    1.62 +apply auto
    1.63 +done
    1.64 +
    1.65 +datatype tname	(* type names for standard classes and other type names *)
    1.66 +	= Object_
    1.67 +	| SXcpt_   xname
    1.68 +	| TName   tnam
    1.69 +
    1.70 +record   qtname = (* qualified tname cf. 6.5.3, 6.5.4*)
    1.71 +          pid :: pname 
    1.72 +          tid :: tname
    1.73 +
    1.74 +axclass has_pname < "type"
    1.75 +consts pname::"'a::has_pname \<Rightarrow> pname"
    1.76 +
    1.77 +instance pname::has_pname
    1.78 +by (intro_classes)
    1.79 +
    1.80 +defs (overloaded)
    1.81 +pname_pname_def: "pname (p::pname) \<equiv> p"
    1.82 +
    1.83 +axclass has_tname < "type"
    1.84 +consts tname::"'a::has_tname \<Rightarrow> tname"
    1.85 +
    1.86 +instance tname::has_tname
    1.87 +by (intro_classes)
    1.88 +
    1.89 +defs (overloaded)
    1.90 +tname_tname_def: "tname (t::tname) \<equiv> t"
    1.91 +
    1.92 +axclass has_qtname < "type"
    1.93 +consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    1.94 +
    1.95 +(* Declare qtname as instance of has_qtname *)
    1.96 +instance pid_field_type::(has_pname,"type") has_qtname
    1.97 +by intro_classes 
    1.98 +
    1.99 +defs (overloaded)
   1.100 +qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
   1.101 +
   1.102 +translations
   1.103 +  "mname"  <= "Name.mname"
   1.104 +  "xname"  <= "Name.xname"
   1.105 +  "tname"  <= "Name.tname"
   1.106 +  "ename"  <= "Name.ename"
   1.107 +  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
   1.108 +  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
   1.109 +
   1.110 +
   1.111 +consts java_lang::pname (* package java.lang *)
   1.112 +
   1.113 +consts 
   1.114 +  Object :: qtname
   1.115 +  SXcpt  :: "xname \<Rightarrow> qtname"
   1.116 +defs
   1.117 +  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
   1.118 +  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
   1.119 +
   1.120 +lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
   1.121 +by (simp add: Object_def SXcpt_def)
   1.122 +
   1.123 +lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
   1.124 +by (simp add: SXcpt_def)
   1.125 +end
   1.126 +