src/HOL/Bali/Name.thy
author haftmann
Tue, 23 Feb 2010 10:11:12 +0100
changeset 35315 fbdc860d87a3
parent 35069 09154b995ed8
child 35431 8758fe1fc9f8
permissions -rw-r--r--
dropped axclass
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
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
header {* Java names *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     6
theory Name imports Basis begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
(* cf. 6.5 *) 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
     9
typedecl tnam   --{* ordinary type name, i.e. class or interface name *}
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 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
    11
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
    12
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
    13
typedecl label  --{* label as destination of break or continue *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
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
    15
datatype ename        --{* expression name *} 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
        = 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
    17
        | Res         --{* special name to model the return value of methods *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
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
    19
datatype lname        --{* names for local variables and the This pointer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
        = EName ename 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
        | This
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    22
abbreviation VName   :: "vname \<Rightarrow> lname"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    23
      where "VName n == EName (VNam n)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    25
abbreviation Result :: lname
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    26
      where "Result == EName Res"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    28
datatype xname          --{* names of standard exceptions *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    29
        = Throwable
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    30
        | NullPointer | OutOfMemory | ClassCast   
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    31
        | NegArrSize  | IndOutBound | ArrStore
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
lemma xn_cases: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
  "xn = Throwable   \<or> xn = NullPointer \<or>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
         xn = OutOfMemory \<or> xn = ClassCast \<or> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
apply (induct xn)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    42
datatype tname  --{* type names for standard classes and other type names *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    43
        = Object'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    44
        | SXcpt'   xname
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
    45
        | TName   tnam
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
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
    47
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
    48
          pid :: pname  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
          tid :: tname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    51
class has_pname =
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    52
  fixes pname :: "'a \<Rightarrow> pname"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    54
instantiation pname :: has_pname
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    55
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    57
definition
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    58
  pname_pname_def: "pname (p::pname) \<equiv> p"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    60
instance ..
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    61
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    62
end
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    64
class has_tname =
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    65
  fixes tname :: "'a \<Rightarrow> tname"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    67
instantiation tname :: has_tname
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    68
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    70
definition
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    71
  tname_tname_def: "tname (t::tname) \<equiv> t"
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    72
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    73
instance ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    75
end
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    77
definition
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
    78
  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
  "mname"  <= "Name.mname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  "xname"  <= "Name.xname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
  "tname"  <= "Name.tname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
  "ename"  <= "Name.ename"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
  "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
19726
df95778b4c2f axiomatization java_lang;
wenzelm
parents: 17160
diff changeset
    89
axiomatization java_lang::pname --{* package java.lang *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
consts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
  Object :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
  SXcpt  :: "xname \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
defs
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 19726
diff changeset
    95
  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
5a3e336a2e37 avoid internal names;
wenzelm
parents: 19726
diff changeset
    96
  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
by (simp add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
by (simp add: SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
end