src/HOL/Bali/Name.thy
author wenzelm
Sun, 28 Aug 2005 16:04:44 +0200
changeset 17160 fb65eda72fc7
parent 16417 9bc16273c2d4
child 19726 df95778b4c2f
permissions -rw-r--r--
removed obsolete arities;
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
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Name imports Basis begin
12854
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
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
    16
datatype ename        --{* expression name *} 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
        = 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
    18
        | Res         --{* special name to model the return value of methods *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
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
    20
datatype lname        --{* names for local variables and the This pointer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
        = EName ename 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
        | This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
syntax   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
  VName  :: "vname \<Rightarrow> lname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
  Result :: lname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
  "VName n" == "EName (VNam n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  "Result"  == "EName Res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
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
    31
datatype xname		--{* names of standard exceptions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
	= Throwable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
	| NullPointer | OutOfMemory | ClassCast   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
	| NegArrSize  | IndOutBound | ArrStore
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
lemma xn_cases: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  "xn = Throwable   \<or> xn = NullPointer \<or>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
apply (induct xn)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
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
    45
datatype tname	--{* type names for standard classes and other type names *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
	= Object_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
	| SXcpt_   xname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
	| TName   tnam
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
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
    50
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
    51
          pid :: pname  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
          tid :: tname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
axclass has_pname < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
consts pname::"'a::has_pname \<Rightarrow> pname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
12859
wenzelm
parents: 12858
diff changeset
    57
instance pname::has_pname ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
pname_pname_def: "pname (p::pname) \<equiv> p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
axclass has_tname < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
consts tname::"'a::has_tname \<Rightarrow> tname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
12859
wenzelm
parents: 12858
diff changeset
    65
instance tname::has_tname ..
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
tname_tname_def: "tname (t::tname) \<equiv> t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
17160
fb65eda72fc7 removed obsolete arities;
wenzelm
parents: 16417
diff changeset
    70
axclass has_qtname < type
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
17160
fb65eda72fc7 removed obsolete arities;
wenzelm
parents: 16417
diff changeset
    73
instance qtname_ext_type :: (type) has_qtname ..
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
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
  "mname"  <= "Name.mname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
  "xname"  <= "Name.xname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
  "tname"  <= "Name.tname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  "ename"  <= "Name.ename"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
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
    87
consts java_lang::pname --{* package java.lang *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
consts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
  Object :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
  SXcpt  :: "xname \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
by (simp add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
by (simp add: SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
end