src/HOL/Bali/Name.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 14700 2f885b7e5ba7
child 16417 9bc16273c2d4
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Name.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Java names *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
theory Name = Basis:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
(* cf. 6.5 *) 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    10
typedecl tnam	--{* ordinary type name, i.e. class or interface name *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    11
typedecl pname  --{* package name *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    12
typedecl mname  --{* method name *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    13
typedecl vname  --{* variable or field name *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    14
typedecl label  --{* label as destination of break or continue *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
arities
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
  tnam  :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  pname :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  vname :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
  mname :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
  label :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    24
datatype ename        --{* expression name *} 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
        = VNam vname 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    26
        | Res         --{* special name to model the return value of methods *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    28
datatype lname        --{* names for local variables and the This pointer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
        = EName ename 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
        | This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
syntax   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
  VName  :: "vname \<Rightarrow> lname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
  Result :: lname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  "VName n" == "EName (VNam n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  "Result"  == "EName Res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    39
datatype xname		--{* names of standard exceptions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
	= Throwable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
	| NullPointer | OutOfMemory | ClassCast   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
	| NegArrSize  | IndOutBound | ArrStore
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
lemma xn_cases: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
  "xn = Throwable   \<or> xn = NullPointer \<or>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
apply (induct xn)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    53
datatype tname	--{* type names for standard classes and other type names *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
	= Object_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
	| SXcpt_   xname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
	| TName   tnam
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    58
record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    59
          pid :: pname  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
          tid :: tname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
axclass has_pname < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
consts pname::"'a::has_pname \<Rightarrow> pname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
12859
wenzelm
parents: 12858
diff changeset
    65
instance pname::has_pname ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
pname_pname_def: "pname (p::pname) \<equiv> p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
axclass has_tname < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
consts tname::"'a::has_tname \<Rightarrow> tname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
12859
wenzelm
parents: 12858
diff changeset
    73
instance tname::has_tname ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
tname_tname_def: "tname (t::tname) \<equiv> t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
axclass has_qtname < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
(* Declare qtname as instance of has_qtname *)
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 13688
diff changeset
    82
instance qtname_ext_type::("type") has_qtname ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
  "mname"  <= "Name.mname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  "xname"  <= "Name.xname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
  "tname"  <= "Name.tname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
  "ename"  <= "Name.ename"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12859
diff changeset
    96
consts java_lang::pname --{* package java.lang *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
consts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
  Object :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
  SXcpt  :: "xname \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
by (simp add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
by (simp add: SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
end
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111