src/HOL/Bali/Name.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Bali/Name.thy	Mon Jan 28 17:00:19 2002 +0100
@@ -0,0 +1,123 @@
+(*  Title:      isabelle/Bali/Name.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1997 Technische Universitaet Muenchen
+*)
+header {* Java names *}
+
+theory Name = Basis:
+
+(* 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 *)
+
+arities
+  tnam  :: "type"
+  pname :: "type"
+  vname :: "type"
+  mname :: "type"
+  label :: "type"
+
+
+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 \<Rightarrow> 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   \<or> xn = NullPointer \<or>  
+         xn = OutOfMemory \<or> xn = ClassCast \<or> 
+         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
+apply (induct xn)
+apply auto
+done
+
+lemma xn_cases_old:   (* FIXME cf. Example.thy *)
+  "ALL 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
+
+record   qtname = (* qualified tname cf. 6.5.3, 6.5.4*)
+          pid :: pname 
+          tid :: tname
+
+axclass has_pname < "type"
+consts pname::"'a::has_pname \<Rightarrow> pname"
+
+instance pname::has_pname
+by (intro_classes)
+
+defs (overloaded)
+pname_pname_def: "pname (p::pname) \<equiv> p"
+
+axclass has_tname < "type"
+consts tname::"'a::has_tname \<Rightarrow> tname"
+
+instance tname::has_tname
+by (intro_classes)
+
+defs (overloaded)
+tname_tname_def: "tname (t::tname) \<equiv> t"
+
+axclass has_qtname < "type"
+consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
+
+(* Declare qtname as instance of has_qtname *)
+instance pid_field_type::(has_pname,"type") has_qtname
+by intro_classes 
+
+defs (overloaded)
+qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
+
+translations
+  "mname"  <= "Name.mname"
+  "xname"  <= "Name.xname"
+  "tname"  <= "Name.tname"
+  "ename"  <= "Name.ename"
+  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
+
+
+consts java_lang::pname (* package java.lang *)
+
+consts 
+  Object :: qtname
+  SXcpt  :: "xname \<Rightarrow> qtname"
+defs
+  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
+  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
+
+lemma Object_neq_SXcpt [simp]: "Object \<noteq> 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
+