src/HOL/Bali/Name.thy
author wenzelm
Mon, 26 Jul 2010 17:41:26 +0200
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 38540 8c08631cb4b6
permissions -rw-r--r--
modernized/unified some specifications;
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
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    71
  tname_tname_def: "tname (t::tname) = t"
35315
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
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    78
  qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35315
diff changeset
    81
  (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
19726
df95778b4c2f axiomatization java_lang;
wenzelm
parents: 17160
diff changeset
    85
axiomatization java_lang::pname --{* package java.lang *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    87
definition
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
  Object :: qtname
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    89
  where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    90
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    91
definition SXcpt :: "xname \<Rightarrow> qtname"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    92
  where "SXcpt = (\<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
by (simp add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
by (simp add: SXcpt_def)
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35431
diff changeset
    99
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
end