src/HOL/Bali/DeclConcepts.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13585 db4005b40cc6
child 14025 d9b155757dc8
permissions -rw-r--r--
"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@12925
     1
(*  Title:      HOL/Bali/DeclConcepts.thy
schirmer@12925
     2
    ID:         $Id$
schirmer@12925
     3
    Author:     Norbert Schirmer
schirmer@12925
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12925
     5
*)
schirmer@12854
     6
header {* Advanced concepts on Java declarations like overriding, inheritance,
schirmer@12854
     7
dynamic method lookup*}
schirmer@12854
     8
schirmer@12854
     9
theory DeclConcepts = TypeRel:
schirmer@12854
    10
schirmer@12854
    11
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
schirmer@12854
    12
schirmer@12854
    13
constdefs
schirmer@12854
    14
is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
    15
"is_public G qn \<equiv> (case class G qn of
schirmer@12854
    16
                     None       \<Rightarrow> (case iface G qn of
schirmer@12854
    17
                                      None       \<Rightarrow> False
schirmer@12854
    18
                                    | Some iface \<Rightarrow> access iface = Public)
schirmer@12854
    19
                   | Some class \<Rightarrow> access class = Public)"
schirmer@12854
    20
schirmer@12854
    21
subsection "accessibility of types (cf. 6.6.1)"
schirmer@12854
    22
text {* 
schirmer@12854
    23
Primitive types are always accessible, interfaces and classes are accessible
schirmer@12854
    24
in their package or if they are defined public, an array type is accessible if
schirmer@12854
    25
its element type is accessible *}
schirmer@12854
    26
 
schirmer@12854
    27
consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
schirmer@12854
    28
                                      ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
schirmer@12854
    29
       rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
schirmer@12854
    30
                                      ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
schirmer@12854
    31
primrec
schirmer@12854
    32
"G\<turnstile>(PrimT p)   accessible_in pack  = True"
schirmer@12854
    33
accessible_in_RefT_simp: 
schirmer@12854
    34
"G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
schirmer@12854
    35
schirmer@12854
    36
"G\<turnstile>(NullT)     accessible_in' pack = True"
schirmer@12854
    37
"G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
schirmer@12854
    38
"G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
schirmer@12854
    39
"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
schirmer@12854
    40
schirmer@12854
    41
declare accessible_in_RefT_simp [simp del]
schirmer@12854
    42
schirmer@12854
    43
constdefs
schirmer@12854
    44
  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
    45
    "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
schirmer@12854
    46
  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
    47
    "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
schirmer@12854
    48
  is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool"
schirmer@12854
    49
    "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
schirmer@12854
    50
  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
schirmer@12854
    51
  "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
schirmer@12854
    52
schirmer@12854
    53
lemma is_acc_classD:
schirmer@12854
    54
 "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
schirmer@12854
    55
by (simp add: is_acc_class_def)
schirmer@12854
    56
schirmer@12854
    57
lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C"
schirmer@12854
    58
by (auto simp add: is_acc_class_def)
schirmer@12854
    59
schirmer@12854
    60
lemma is_acc_ifaceD:
schirmer@12854
    61
  "is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
schirmer@12854
    62
by (simp add: is_acc_iface_def)
schirmer@12854
    63
schirmer@12854
    64
lemma is_acc_typeD:
schirmer@12925
    65
 "is_acc_type  G P T \<Longrightarrow> is_type G T  \<and> G\<turnstile>T accessible_in P"
schirmer@12854
    66
by (simp add: is_acc_type_def)
schirmer@12854
    67
schirmer@12854
    68
lemma is_acc_reftypeD:
schirmer@12854
    69
"is_acc_reftype  G P T \<Longrightarrow> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
schirmer@12854
    70
by (simp add: is_acc_reftype_def)
schirmer@12854
    71
schirmer@12854
    72
subsection "accessibility of members"
schirmer@12854
    73
text {*
schirmer@12854
    74
The accessibility of members is more involved as the accessibility of types.
schirmer@12854
    75
We have to distinguish several cases to model the different effects of 
schirmer@12854
    76
accessibility during inheritance, overriding and ordinary member access 
schirmer@12854
    77
*}
schirmer@12854
    78
schirmer@12854
    79
subsubsection {* Various technical conversion and selection functions *}
schirmer@12854
    80
schirmer@12854
    81
text {* overloaded selector @{text accmodi} to select the access modifier 
schirmer@12854
    82
out of various HOL types *}
schirmer@12854
    83
schirmer@12854
    84
axclass has_accmodi < "type"
schirmer@12854
    85
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
schirmer@12854
    86
wenzelm@12859
    87
instance acc_modi::has_accmodi ..
schirmer@12854
    88
schirmer@12854
    89
defs (overloaded)
schirmer@12854
    90
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
schirmer@12854
    91
schirmer@12854
    92
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
schirmer@12854
    93
by (simp add: acc_modi_accmodi_def)
schirmer@12854
    94
wenzelm@12859
    95
instance access_field_type:: ("type","type") has_accmodi ..
schirmer@12854
    96
schirmer@12854
    97
defs (overloaded)
schirmer@12854
    98
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
schirmer@12854
    99
schirmer@12854
   100
schirmer@12854
   101
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
schirmer@12854
   102
by (simp add: decl_acc_modi_def)
schirmer@12854
   103
wenzelm@12859
   104
instance * :: ("type",has_accmodi) has_accmodi ..
schirmer@12854
   105
schirmer@12854
   106
defs (overloaded)
schirmer@12854
   107
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
schirmer@12854
   108
schirmer@12854
   109
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
schirmer@12854
   110
by (simp add: pair_acc_modi_def)
schirmer@12854
   111
wenzelm@12859
   112
instance memberdecl :: has_accmodi ..
schirmer@12854
   113
schirmer@12854
   114
defs (overloaded)
schirmer@12854
   115
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
schirmer@12854
   116
                                          fdecl f \<Rightarrow> accmodi f
schirmer@12854
   117
                                        | mdecl m \<Rightarrow> accmodi m)"
schirmer@12854
   118
schirmer@12854
   119
lemma memberdecl_fdecl_acc_modi_simp[simp]:
schirmer@12854
   120
 "accmodi (fdecl m) = accmodi m"
schirmer@12854
   121
by (simp add: memberdecl_acc_modi_def)
schirmer@12854
   122
schirmer@12854
   123
lemma memberdecl_mdecl_acc_modi_simp[simp]:
schirmer@12854
   124
 "accmodi (mdecl m) = accmodi m"
schirmer@12854
   125
by (simp add: memberdecl_acc_modi_def)
schirmer@12854
   126
schirmer@12854
   127
text {* overloaded selector @{text declclass} to select the declaring class 
schirmer@12854
   128
out of various HOL types *}
schirmer@12854
   129
schirmer@12854
   130
axclass has_declclass < "type"
schirmer@12854
   131
consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
schirmer@12854
   132
wenzelm@12859
   133
instance pid_field_type::("type","type") has_declclass ..
schirmer@12854
   134
schirmer@12854
   135
defs (overloaded)
schirmer@12854
   136
qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
schirmer@12854
   137
schirmer@12854
   138
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
schirmer@12854
   139
by (simp add: qtname_declclass_def)
schirmer@12854
   140
wenzelm@12859
   141
instance * :: ("has_declclass","type") has_declclass ..
schirmer@12854
   142
schirmer@12854
   143
defs (overloaded)
schirmer@12854
   144
pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
schirmer@12854
   145
schirmer@12854
   146
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
schirmer@12854
   147
by (simp add: pair_declclass_def)
schirmer@12854
   148
schirmer@12854
   149
text {* overloaded selector @{text is_static} to select the static modifier 
schirmer@12854
   150
out of various HOL types *}
schirmer@12854
   151
schirmer@12854
   152
schirmer@12854
   153
axclass has_static < "type"
schirmer@12854
   154
consts is_static :: "'a::has_static \<Rightarrow> bool"
schirmer@12854
   155
wenzelm@12859
   156
instance access_field_type :: ("type","has_static") has_static ..
schirmer@12854
   157
schirmer@12854
   158
defs (overloaded)
schirmer@12854
   159
decl_is_static_def: 
schirmer@12854
   160
 "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
schirmer@12854
   161
wenzelm@12859
   162
instance static_field_type :: ("type","type") has_static ..
schirmer@12854
   163
schirmer@12854
   164
defs (overloaded)
schirmer@12854
   165
static_field_type_is_static_def: 
schirmer@12854
   166
 "is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m"
schirmer@12854
   167
schirmer@12854
   168
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
schirmer@12854
   169
apply (cases m)
schirmer@12854
   170
apply (simp add: static_field_type_is_static_def 
schirmer@12854
   171
                 decl_is_static_def Decl.member.dest_convs)
schirmer@12854
   172
done
schirmer@12854
   173
wenzelm@12859
   174
instance * :: ("type","has_static") has_static ..
schirmer@12854
   175
schirmer@12854
   176
defs (overloaded)
schirmer@12854
   177
pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
schirmer@12854
   178
schirmer@12854
   179
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
schirmer@12854
   180
by (simp add: pair_is_static_def)
schirmer@12854
   181
schirmer@12854
   182
lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
schirmer@12854
   183
by (simp add: pair_is_static_def)
schirmer@12854
   184
wenzelm@12859
   185
instance memberdecl:: has_static ..
schirmer@12854
   186
schirmer@12854
   187
defs (overloaded)
schirmer@12854
   188
memberdecl_is_static_def: 
schirmer@12854
   189
 "is_static m \<equiv> (case m of
schirmer@12854
   190
                    fdecl f \<Rightarrow> is_static f
schirmer@12854
   191
                  | mdecl m \<Rightarrow> is_static m)"
schirmer@12854
   192
schirmer@12854
   193
lemma memberdecl_is_static_fdecl_simp[simp]:
schirmer@12854
   194
 "is_static (fdecl f) = is_static f"
schirmer@12854
   195
by (simp add: memberdecl_is_static_def)
schirmer@12854
   196
schirmer@12854
   197
lemma memberdecl_is_static_mdecl_simp[simp]:
schirmer@12854
   198
 "is_static (mdecl m) = is_static m"
schirmer@12854
   199
by (simp add: memberdecl_is_static_def)
schirmer@12854
   200
schirmer@12854
   201
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
schirmer@12854
   202
by (cases m) (simp add: mhead_def member_is_static_simp)
schirmer@12854
   203
schirmer@13688
   204
constdefs  --{* some mnemotic selectors for various pairs *} 
schirmer@13688
   205
           
schirmer@12854
   206
 "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
schirmer@13688
   207
 "decliface \<equiv> fst"          --{* get the interface component *}
schirmer@12854
   208
schirmer@12854
   209
 "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
schirmer@13688
   210
 "mbr \<equiv> snd"            --{* get the memberdecl component *}
schirmer@12854
   211
schirmer@12854
   212
 "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
schirmer@13688
   213
                           --{* also used for mdecl, mhead *}
schirmer@13688
   214
 "mthd \<equiv> snd"              --{* get the method component *}
schirmer@12854
   215
schirmer@12854
   216
 "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
schirmer@13688
   217
              --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
schirmer@13688
   218
 "fld \<equiv> snd"               --{* get the field component *}
schirmer@12854
   219
schirmer@12854
   220
schirmer@13688
   221
constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
schirmer@13688
   222
 fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
schirmer@12854
   223
 "fname \<equiv> fst"
schirmer@12854
   224
  
schirmer@12854
   225
  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
schirmer@12854
   226
 "declclassf \<equiv> snd"
schirmer@12854
   227
schirmer@13688
   228
schirmer@12854
   229
schirmer@12854
   230
lemma decliface_simp[simp]: "decliface (I,m) = I"
schirmer@12854
   231
by (simp add: decliface_def) 
schirmer@12854
   232
schirmer@12854
   233
lemma mbr_simp[simp]: "mbr (C,m) = m"
schirmer@12854
   234
by (simp add: mbr_def)
schirmer@12854
   235
schirmer@12854
   236
lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m"
schirmer@12854
   237
by (cases m) (simp add:  mbr_def) 
schirmer@12854
   238
schirmer@12854
   239
lemma mthd_simp[simp]: "mthd (C,m) = m"
schirmer@12854
   240
by (simp add: mthd_def)
schirmer@12854
   241
schirmer@12854
   242
lemma fld_simp[simp]: "fld (C,f) = f"
schirmer@12854
   243
by (simp add: fld_def)
schirmer@12854
   244
schirmer@12854
   245
lemma accmodi_simp[simp]: "accmodi (C,m) = access m"
schirmer@12854
   246
by (simp )
schirmer@12854
   247
schirmer@12854
   248
lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m"
schirmer@12854
   249
by (cases m) (simp add: mthd_def) 
schirmer@12854
   250
schirmer@12854
   251
lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
schirmer@12854
   252
by (cases f) (simp add:  fld_def) 
schirmer@12854
   253
schirmer@12854
   254
lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
schirmer@12854
   255
by (cases m) (simp add:  mthd_def member_is_static_simp)
schirmer@12854
   256
schirmer@12854
   257
lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m"
schirmer@12854
   258
by (cases m) simp
schirmer@12854
   259
schirmer@12854
   260
lemma static_fld_simp[simp]: "static (fld f) = is_static f"
schirmer@12854
   261
by (cases f) (simp add:  fld_def member_is_static_simp)
schirmer@12854
   262
schirmer@12854
   263
lemma ext_field_simp [simp]: "(declclass f,fld f) = f"
schirmer@12854
   264
by (cases f) (simp add:  fld_def)
schirmer@12854
   265
schirmer@12854
   266
lemma ext_method_simp [simp]: "(declclass m,mthd m) = m"
schirmer@12854
   267
by (cases m) (simp add:  mthd_def)
schirmer@12854
   268
schirmer@12854
   269
lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m"
schirmer@12854
   270
by (cases m) (simp add: mbr_def)
schirmer@12854
   271
schirmer@12854
   272
lemma fname_simp[simp]:"fname (n,c) = n"
schirmer@12854
   273
by (simp add: fname_def)
schirmer@12854
   274
schirmer@12854
   275
lemma declclassf_simp[simp]:"declclassf (n,c) = c"
schirmer@12854
   276
by (simp add: declclassf_def)
schirmer@12854
   277
schirmer@13688
   278
constdefs  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
schirmer@12854
   279
  "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
schirmer@12854
   280
  "fldname \<equiv> fst"
schirmer@12854
   281
schirmer@12854
   282
  "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
schirmer@12854
   283
  "fldclass \<equiv> snd"
schirmer@12854
   284
schirmer@12854
   285
lemma fldname_simp[simp]: "fldname (n,c) = n"
schirmer@12854
   286
by (simp add: fldname_def)
schirmer@12854
   287
schirmer@12854
   288
lemma fldclass_simp[simp]: "fldclass (n,c) = c"
schirmer@12854
   289
by (simp add: fldclass_def)
schirmer@12854
   290
schirmer@12854
   291
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
schirmer@12854
   292
by (simp add: fldname_def fldclass_def)
schirmer@12854
   293
schirmer@12854
   294
text {* Convert a qualified method declaration (qualified with its declaring 
schirmer@12854
   295
class) to a qualified member declaration:  @{text methdMembr}  *}
schirmer@12854
   296
schirmer@12854
   297
constdefs
schirmer@12854
   298
methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)"
schirmer@12854
   299
 "methdMembr m \<equiv> (fst m,mdecl (snd m))"
schirmer@12854
   300
schirmer@12854
   301
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
schirmer@12854
   302
by (simp add: methdMembr_def)
schirmer@12854
   303
schirmer@12854
   304
lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m"
schirmer@12854
   305
by (cases m) (simp add: methdMembr_def)
schirmer@12854
   306
schirmer@12854
   307
lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m"
schirmer@12854
   308
by (cases m) (simp add: methdMembr_def)
schirmer@12854
   309
schirmer@12854
   310
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
schirmer@12854
   311
by (cases m) (simp add: methdMembr_def)
schirmer@12854
   312
schirmer@12854
   313
text {* Convert a qualified method (qualified with its declaring 
schirmer@12854
   314
class) to a qualified member declaration:  @{text method}  *}
schirmer@12854
   315
schirmer@12854
   316
constdefs
schirmer@12854
   317
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 
schirmer@12854
   318
"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
schirmer@12854
   319
schirmer@12854
   320
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
schirmer@12854
   321
by (simp add: method_def)
schirmer@12854
   322
schirmer@12854
   323
lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m"
schirmer@12854
   324
by (simp add: method_def)
schirmer@12854
   325
schirmer@12854
   326
lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m"
schirmer@12854
   327
by (simp add: method_def)
schirmer@12854
   328
schirmer@12854
   329
lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m"
schirmer@12854
   330
by (cases m) (simp add: method_def)
schirmer@12854
   331
schirmer@12854
   332
lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)"
schirmer@12854
   333
by (simp add: mbr_def method_def)
schirmer@12854
   334
schirmer@12854
   335
lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
schirmer@12854
   336
  by (simp add: method_def) 
schirmer@12854
   337
schirmer@12854
   338
constdefs
schirmer@12854
   339
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 
schirmer@12854
   340
"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
schirmer@12854
   341
schirmer@12854
   342
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
schirmer@12854
   343
by (simp add: fieldm_def)
schirmer@12854
   344
schirmer@12854
   345
lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f"
schirmer@12854
   346
by (simp add: fieldm_def)
schirmer@12854
   347
schirmer@12854
   348
lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f"
schirmer@12854
   349
by (simp add: fieldm_def)
schirmer@12854
   350
schirmer@12854
   351
lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f"
schirmer@12854
   352
by (cases f) (simp add: fieldm_def)
schirmer@12854
   353
schirmer@12854
   354
lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)"
schirmer@12854
   355
by (simp add: mbr_def fieldm_def)
schirmer@12854
   356
schirmer@12854
   357
lemma memberid_fieldm_simp[simp]:  "memberid (fieldm n f) = fid n"
schirmer@12854
   358
by (simp add: fieldm_def) 
schirmer@12854
   359
schirmer@12854
   360
text {* Select the signature out of a qualified method declaration:
schirmer@12854
   361
 @{text msig} *}
schirmer@12854
   362
schirmer@12854
   363
constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig"
schirmer@12854
   364
"msig m \<equiv> fst (snd m)"
schirmer@12854
   365
schirmer@12854
   366
lemma msig_simp[simp]: "msig (c,(s,m)) = s"
schirmer@12854
   367
by (simp add: msig_def)
schirmer@12854
   368
schirmer@12854
   369
text {* Convert a qualified method (qualified with its declaring 
schirmer@12854
   370
class) to a qualified method declaration:  @{text qmdecl}  *}
schirmer@12854
   371
schirmer@12854
   372
constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
schirmer@12854
   373
"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
schirmer@12854
   374
schirmer@12854
   375
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
schirmer@12854
   376
by (simp add: qmdecl_def)
schirmer@12854
   377
schirmer@12854
   378
lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m"
schirmer@12854
   379
by (simp add: qmdecl_def)
schirmer@12854
   380
schirmer@12854
   381
lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m"
schirmer@12854
   382
by (simp add: qmdecl_def)
schirmer@12854
   383
schirmer@12854
   384
lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m"
schirmer@12854
   385
by (cases m) (simp add: qmdecl_def)
schirmer@12854
   386
schirmer@12854
   387
lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig"
schirmer@12854
   388
by (simp add: qmdecl_def)
schirmer@12854
   389
schirmer@12854
   390
lemma mdecl_qmdecl_simp[simp]:  
schirmer@12854
   391
 "mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 
schirmer@12854
   392
by (simp add: qmdecl_def) 
schirmer@12854
   393
schirmer@12854
   394
lemma methdMembr_qmdecl_simp [simp]: 
schirmer@12854
   395
 "methdMembr (qmdecl sig old) = method sig old"
schirmer@12854
   396
by (simp add: methdMembr_def qmdecl_def method_def)
schirmer@12854
   397
schirmer@12854
   398
text {* overloaded selector @{text resTy} to select the result type 
schirmer@12854
   399
out of various HOL types *}
schirmer@12854
   400
schirmer@12854
   401
axclass has_resTy < "type"
schirmer@12854
   402
consts resTy:: "'a::has_resTy \<Rightarrow> ty"
schirmer@12854
   403
wenzelm@12859
   404
instance access_field_type :: ("type","has_resTy") has_resTy ..
schirmer@12854
   405
schirmer@12854
   406
defs (overloaded)
schirmer@12854
   407
decl_resTy_def: 
schirmer@12854
   408
 "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
schirmer@12854
   409
wenzelm@12859
   410
instance static_field_type :: ("type","has_resTy") has_resTy ..
schirmer@12854
   411
schirmer@12854
   412
defs (overloaded)
schirmer@12854
   413
static_field_type_resTy_def: 
schirmer@12854
   414
 "resTy (m::(bool,'b::has_resTy) static_field_type) 
schirmer@12854
   415
  \<equiv> resTy (static_more m)" 
schirmer@12854
   416
wenzelm@12859
   417
instance pars_field_type :: ("type","has_resTy") has_resTy ..
schirmer@12854
   418
schirmer@12854
   419
defs (overloaded)
schirmer@12854
   420
pars_field_type_resTy_def: 
schirmer@12854
   421
 "resTy (m::(vname list,'b::has_resTy) pars_field_type) 
schirmer@12854
   422
  \<equiv> resTy (pars_more m)" 
schirmer@12854
   423
wenzelm@12859
   424
instance resT_field_type :: ("type","type") has_resTy ..
schirmer@12854
   425
schirmer@12854
   426
defs (overloaded)
schirmer@12854
   427
resT_field_type_resTy_def: 
schirmer@12854
   428
 "resTy (m::(ty,'b::type) resT_field_type) 
schirmer@12854
   429
  \<equiv> resT_val m" 
schirmer@12854
   430
schirmer@12854
   431
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
schirmer@12854
   432
apply (cases m)
schirmer@12854
   433
apply (simp add: decl_resTy_def static_field_type_resTy_def 
schirmer@12854
   434
                 pars_field_type_resTy_def resT_field_type_resTy_def
schirmer@12854
   435
                 member.dest_convs mhead.dest_convs)
schirmer@12854
   436
done
schirmer@12854
   437
schirmer@12854
   438
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
schirmer@12854
   439
by (simp add: mhead_def mhead_resTy_simp)
schirmer@12854
   440
wenzelm@12859
   441
instance * :: ("type","has_resTy") has_resTy ..
schirmer@12854
   442
schirmer@12854
   443
defs (overloaded)
schirmer@12854
   444
pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
schirmer@12854
   445
schirmer@12854
   446
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
schirmer@12854
   447
by (simp add: pair_resTy_def)
schirmer@12854
   448
schirmer@12854
   449
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m"
schirmer@12854
   450
by (cases m) (simp)
schirmer@12854
   451
schirmer@12854
   452
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m"
schirmer@12854
   453
by (cases m) (simp add: mthd_def )
schirmer@12854
   454
schirmer@12854
   455
subsubsection "inheritable-in"
schirmer@12854
   456
text {*
schirmer@12854
   457
@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by
schirmer@12854
   458
classes in package P if:
schirmer@12854
   459
\begin{itemize} 
schirmer@12854
   460
\item the declaration class of m is accessible in P and
schirmer@12854
   461
\item the member m is declared with protected or public access or if it is
schirmer@12854
   462
      declared with default (package) access, the package of the declaration 
schirmer@12854
   463
      class of m is also P. If the member m is declared with private access
schirmer@12854
   464
      it is not accessible for inheritance at all.
schirmer@12854
   465
\end{itemize}
schirmer@12854
   466
*}
schirmer@12854
   467
constdefs
schirmer@12854
   468
inheritable_in:: 
schirmer@12854
   469
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool"
schirmer@12854
   470
                  ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
schirmer@12854
   471
"G\<turnstile>membr inheritable_in pack 
schirmer@12854
   472
  \<equiv> (case (accmodi membr) of
schirmer@12854
   473
       Private   \<Rightarrow> False
schirmer@12854
   474
     | Package   \<Rightarrow> (pid (declclass membr)) = pack
schirmer@12854
   475
     | Protected \<Rightarrow> True
schirmer@12854
   476
     | Public    \<Rightarrow> True)"
schirmer@12854
   477
schirmer@12854
   478
syntax
schirmer@12854
   479
Method_inheritable_in::
schirmer@12854
   480
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
schirmer@12854
   481
                ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
schirmer@12854
   482
schirmer@12854
   483
translations
schirmer@12854
   484
"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
schirmer@12854
   485
schirmer@12854
   486
syntax
schirmer@12854
   487
Methd_inheritable_in::
schirmer@12854
   488
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
schirmer@12854
   489
                ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
schirmer@12854
   490
schirmer@12854
   491
translations
schirmer@12854
   492
"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
schirmer@12854
   493
schirmer@12854
   494
subsubsection "declared-in/undeclared-in"
schirmer@12854
   495
schirmer@12854
   496
constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table"
schirmer@12854
   497
"cdeclaredmethd G C 
schirmer@12854
   498
  \<equiv> (case class G C of
schirmer@12854
   499
       None \<Rightarrow> \<lambda> sig. None
schirmer@12854
   500
     | Some c \<Rightarrow> table_of (methods c)
schirmer@12854
   501
    )"
schirmer@12854
   502
schirmer@12854
   503
constdefs
schirmer@12854
   504
cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table"
schirmer@12854
   505
"cdeclaredfield G C 
schirmer@12854
   506
  \<equiv> (case class G C of
schirmer@12854
   507
       None \<Rightarrow> \<lambda> sig. None
schirmer@12854
   508
     | Some c \<Rightarrow> table_of (cfields c)
schirmer@12854
   509
    )"
schirmer@12854
   510
schirmer@12854
   511
schirmer@12854
   512
constdefs
schirmer@12854
   513
declared_in:: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   514
                                 ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
schirmer@12854
   515
"G\<turnstile>m declared_in C \<equiv> (case m of
schirmer@12854
   516
                        fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
schirmer@12854
   517
                      | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
schirmer@12854
   518
schirmer@12854
   519
syntax
schirmer@12854
   520
method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   521
                                 ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
schirmer@12854
   522
translations
schirmer@12854
   523
"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
schirmer@12854
   524
schirmer@12854
   525
syntax
schirmer@12854
   526
methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   527
                               ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
schirmer@12854
   528
translations
schirmer@12854
   529
"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
schirmer@12854
   530
schirmer@12854
   531
lemma declared_in_classD:
schirmer@12854
   532
 "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
schirmer@12854
   533
by (cases m) 
schirmer@12854
   534
   (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
schirmer@12854
   535
schirmer@12854
   536
constdefs
schirmer@12854
   537
undeclared_in:: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   538
                                 ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
schirmer@12854
   539
schirmer@12854
   540
"G\<turnstile>m undeclared_in C \<equiv> (case m of
schirmer@12854
   541
                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
schirmer@12854
   542
                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
schirmer@12854
   543
schirmer@12854
   544
schirmer@12854
   545
subsubsection "members"
schirmer@12854
   546
schirmer@12854
   547
consts
schirmer@12854
   548
members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set"
schirmer@12854
   549
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because
schirmer@12854
   550
   the class qtname changes to the superclass in the inductive definition
schirmer@12854
   551
   below
schirmer@12854
   552
*)
schirmer@12854
   553
schirmer@12854
   554
syntax
schirmer@12854
   555
member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   556
                           ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
schirmer@12854
   557
schirmer@12854
   558
translations
schirmer@12854
   559
 "G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G"
schirmer@12854
   560
schirmer@12854
   561
inductive "members G"  intros
schirmer@12854
   562
schirmer@12854
   563
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
schirmer@12854
   564
Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
schirmer@12854
   565
             G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
schirmer@12854
   566
            \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
schirmer@12854
   567
text {* Note that in the case of an inherited member only the members of the
schirmer@12854
   568
direct superclass are concerned. If a member of a superclass of the direct
schirmer@12854
   569
superclass isn't inherited in the direct superclass (not member of the
schirmer@12854
   570
direct superclass) than it can't be a member of the class. E.g. If a
schirmer@12854
   571
member of a class A is defined with package access it isn't member of a 
schirmer@12854
   572
subclass S if S isn't in the same package as A. Any further subclasses 
schirmer@12854
   573
of S will not inherit the member, regardless if they are in the same
schirmer@12854
   574
package as A or not.*}
schirmer@12854
   575
schirmer@12854
   576
syntax
schirmer@12854
   577
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   578
                           ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
schirmer@12854
   579
schirmer@12854
   580
translations
schirmer@12854
   581
 "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
schirmer@12854
   582
schirmer@12854
   583
syntax
schirmer@12854
   584
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   585
                           ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
schirmer@12854
   586
schirmer@12854
   587
translations
schirmer@12854
   588
 "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
schirmer@12854
   589
schirmer@12854
   590
syntax
schirmer@12854
   591
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   592
                           ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
schirmer@12854
   593
schirmer@12854
   594
translations
schirmer@12854
   595
 "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
schirmer@12854
   596
schirmer@12854
   597
constdefs
schirmer@12854
   598
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
schirmer@12854
   599
                           ("_ \<turnstile> _ inherits _" [61,61,61] 60)
schirmer@12854
   600
"G\<turnstile>C inherits m 
schirmer@12854
   601
  \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
schirmer@12854
   602
    (\<exists> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
schirmer@12854
   603
schirmer@12854
   604
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
schirmer@12854
   605
by (auto simp add: inherits_def intro: members.Inherited)
schirmer@12854
   606
schirmer@12854
   607
schirmer@12854
   608
constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   609
                           ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
schirmer@12854
   610
"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
schirmer@12854
   611
text {* A member is in a class if it is member of the class or a superclass.
schirmer@12854
   612
If a member is in a class we can select this member. This additional notion
schirmer@12854
   613
is necessary since not all members are inherited to subclasses. So such
schirmer@12854
   614
members are not member-of the subclass but member-in the subclass.*}
schirmer@12854
   615
schirmer@12854
   616
syntax
schirmer@12854
   617
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   618
                           ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
schirmer@12854
   619
schirmer@12854
   620
translations
schirmer@12854
   621
 "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
schirmer@12854
   622
schirmer@12854
   623
syntax
schirmer@12854
   624
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   625
                           ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
schirmer@12854
   626
schirmer@12854
   627
translations
schirmer@12854
   628
 "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
schirmer@12854
   629
schirmer@12854
   630
consts stat_overridesR::
schirmer@12854
   631
  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
schirmer@12854
   632
schirmer@12854
   633
lemma member_inD: "G\<turnstile>m member_in C 
schirmer@12854
   634
 \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
schirmer@12854
   635
by (auto simp add: member_in_def)
schirmer@12854
   636
schirmer@12854
   637
lemma member_inI: "\<lbrakk>G \<turnstile> m member_of provC;G\<turnstile> C \<preceq>\<^sub>C provC\<rbrakk> \<Longrightarrow>  G\<turnstile>m member_in C"
schirmer@12854
   638
by (auto simp add: member_in_def)
schirmer@12854
   639
schirmer@12854
   640
lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C"
schirmer@12854
   641
by (auto intro: member_inI)
schirmer@12854
   642
schirmer@12854
   643
schirmer@12854
   644
subsubsection "overriding"
schirmer@12854
   645
schirmer@12854
   646
text {* Unfortunately the static notion of overriding (used during the
schirmer@12854
   647
typecheck of the compiler) and the dynamic notion of overriding (used during
schirmer@12854
   648
execution in the JVM) are not exactly the same. 
schirmer@12854
   649
*}
schirmer@12854
   650
schirmer@12854
   651
text {* Static overriding (used during the typecheck of the compiler) *}
schirmer@12854
   652
syntax
schirmer@12854
   653
stat_overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
schirmer@12854
   654
                                  ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
schirmer@12854
   655
translations
schirmer@12854
   656
 "G\<turnstile>new overrides\<^sub>S  old" == "(new,old) \<in> stat_overridesR G "
schirmer@12854
   657
schirmer@12854
   658
inductive "stat_overridesR G" intros
schirmer@12854
   659
schirmer@12854
   660
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
schirmer@12854
   661
         G\<turnstile>Method new declared_in (declclass new);  
schirmer@12854
   662
         G\<turnstile>Method old declared_in (declclass old); 
schirmer@12854
   663
         G\<turnstile>Method old inheritable_in pid (declclass new);
schirmer@12854
   664
         G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
schirmer@12854
   665
         G \<turnstile>Method old member_of superNew
schirmer@12854
   666
         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
schirmer@12854
   667
schirmer@12854
   668
Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
schirmer@12854
   669
           \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
schirmer@12854
   670
schirmer@12854
   671
text {* Dynamic overriding (used during the typecheck of the compiler) *}
schirmer@12854
   672
consts overridesR::
schirmer@12854
   673
  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
schirmer@12854
   674
schirmer@12854
   675
schirmer@12854
   676
overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
schirmer@12854
   677
                                  ("_ \<turnstile> _ overrides _" [61,61,61] 60)
schirmer@12854
   678
translations
schirmer@12854
   679
 "G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G "
schirmer@12854
   680
schirmer@12854
   681
inductive "overridesR G" intros
schirmer@12854
   682
schirmer@12854
   683
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;
schirmer@12854
   684
         msig new = msig old; 
schirmer@12854
   685
         G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
schirmer@12854
   686
         G\<turnstile>Method new declared_in (declclass new);  
schirmer@12854
   687
         G\<turnstile>Method old declared_in (declclass old);    
schirmer@12854
   688
         G\<turnstile>Method old inheritable_in pid (declclass new);
schirmer@12854
   689
         G\<turnstile>resTy new \<preceq> resTy old
schirmer@12854
   690
         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
schirmer@12854
   691
schirmer@12854
   692
Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
schirmer@12854
   693
           \<Longrightarrow> G\<turnstile>new overrides old"
schirmer@12854
   694
schirmer@12854
   695
syntax
schirmer@12854
   696
sig_stat_overrides:: 
schirmer@12854
   697
 "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
schirmer@12854
   698
                                  ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
schirmer@12854
   699
translations
schirmer@12854
   700
 "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
schirmer@12854
   701
schirmer@12854
   702
syntax
schirmer@12854
   703
sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
schirmer@12854
   704
                                  ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
schirmer@12854
   705
translations
schirmer@12854
   706
 "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
schirmer@12854
   707
schirmer@12854
   708
subsubsection "Hiding"
schirmer@12854
   709
schirmer@12854
   710
constdefs hides::
schirmer@12854
   711
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
schirmer@12854
   712
                                ("_\<turnstile> _ hides _" [61,61,61] 60)
schirmer@12854
   713
"G\<turnstile>new hides old
schirmer@12854
   714
  \<equiv> is_static new \<and> msig new = msig old \<and>
schirmer@12854
   715
    G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
schirmer@12854
   716
    G\<turnstile>Method new declared_in (declclass new) \<and>
schirmer@12854
   717
    G\<turnstile>Method old declared_in (declclass old) \<and> 
schirmer@12854
   718
    G\<turnstile>Method old inheritable_in pid (declclass new)"
schirmer@12854
   719
schirmer@12854
   720
syntax
schirmer@12854
   721
sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
schirmer@12854
   722
                                  ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
schirmer@12854
   723
translations
schirmer@12854
   724
 "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
schirmer@12854
   725
schirmer@12854
   726
lemma hidesI:
schirmer@12854
   727
"\<lbrakk>is_static new; msig new = msig old;
schirmer@12854
   728
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
schirmer@12854
   729
  G\<turnstile>Method new declared_in (declclass new);
schirmer@12854
   730
  G\<turnstile>Method old declared_in (declclass old);
schirmer@12854
   731
  G\<turnstile>Method old inheritable_in pid (declclass new)
schirmer@12854
   732
 \<rbrakk> \<Longrightarrow> G\<turnstile>new hides old"
schirmer@12854
   733
by (auto simp add: hides_def)
schirmer@12854
   734
schirmer@12854
   735
lemma hidesD:
schirmer@12854
   736
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow>  
schirmer@12854
   737
  declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 
schirmer@12854
   738
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
schirmer@12854
   739
  G\<turnstile>Method new declared_in (declclass new) \<and>   
schirmer@12854
   740
  G\<turnstile>Method old declared_in (declclass old)"
schirmer@12854
   741
by (auto simp add: hides_def)
schirmer@12854
   742
schirmer@12854
   743
lemma overrides_commonD:
schirmer@12854
   744
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow>  
schirmer@12854
   745
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
schirmer@12854
   746
  accmodi new \<noteq> Private \<and> 
schirmer@12854
   747
  msig new = msig old  \<and>
schirmer@12854
   748
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
schirmer@12854
   749
  G\<turnstile>Method new declared_in (declclass new) \<and>   
schirmer@12854
   750
  G\<turnstile>Method old declared_in (declclass old)"
schirmer@12854
   751
by (induct set: overridesR) (auto intro: trancl_trans)
schirmer@12854
   752
schirmer@12854
   753
lemma ws_overrides_commonD:
schirmer@12854
   754
"\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
   755
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
schirmer@12854
   756
  accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and>
schirmer@12854
   757
  msig new = msig old  \<and>
schirmer@12854
   758
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
schirmer@12854
   759
  G\<turnstile>Method new declared_in (declclass new) \<and>   
schirmer@12854
   760
  G\<turnstile>Method old declared_in (declclass old)"
schirmer@12854
   761
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)
schirmer@12854
   762
schirmer@12854
   763
lemma overrides_eq_sigD: 
schirmer@12854
   764
 "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new"
schirmer@12854
   765
by (auto dest: overrides_commonD)
schirmer@12854
   766
schirmer@12854
   767
lemma hides_eq_sigD: 
schirmer@12854
   768
 "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new"
schirmer@12854
   769
by (auto simp add: hides_def)
schirmer@12854
   770
schirmer@12854
   771
subsubsection "permits access" 
schirmer@12854
   772
constdefs 
schirmer@12854
   773
permits_acc:: 
schirmer@12854
   774
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   775
                   ("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60)
schirmer@12854
   776
schirmer@12854
   777
"G\<turnstile>membr in class permits_acc_to accclass 
schirmer@12854
   778
  \<equiv> (case (accmodi membr) of
schirmer@12854
   779
       Private   \<Rightarrow> (declclass membr = accclass)
schirmer@12854
   780
     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
schirmer@12854
   781
     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
schirmer@12854
   782
                    \<or>
schirmer@12925
   783
                    (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
schirmer@12925
   784
                     \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
schirmer@12854
   785
     | Public    \<Rightarrow> True)"
schirmer@12854
   786
text {*
schirmer@12854
   787
The subcondition of the @{term "Protected"} case: 
schirmer@12854
   788
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
schirmer@12854
   789
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the
schirmer@12854
   790
same the other condition @{term "(pid (declclass membr) = pid accclass)"}
schirmer@12854
   791
holds anyway.
schirmer@12854
   792
*} 
schirmer@12854
   793
schirmer@12854
   794
text {* Like in case of overriding, the static and dynamic accessibility 
schirmer@12854
   795
of members is not uniform.
schirmer@12854
   796
\begin{itemize}
schirmer@12854
   797
\item Statically the class/interface of the member must be accessible for the
schirmer@12854
   798
      member to be accessible. During runtime this is not necessary. For
schirmer@12854
   799
      Example, if a class is accessible and we are allowed to access a member
schirmer@12854
   800
      of this class (statically) we expect that we can access this member in 
schirmer@12854
   801
      an arbitrary subclass (during runtime). It's not intended to restrict
schirmer@12854
   802
      the access to accessible subclasses during runtime.
schirmer@12854
   803
\item Statically the member we want to access must be "member of" the class.
schirmer@12854
   804
      Dynamically it must only be "member in" the class.
schirmer@12854
   805
\end{itemize} 
schirmer@12854
   806
*} 
schirmer@12854
   807
schirmer@12854
   808
schirmer@12854
   809
consts
schirmer@12854
   810
accessible_fromR:: 
schirmer@12854
   811
 "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
schirmer@12854
   812
schirmer@12854
   813
syntax 
schirmer@12854
   814
accessible_from:: 
schirmer@12854
   815
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   816
                   ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
schirmer@12854
   817
schirmer@12854
   818
translations
schirmer@12854
   819
"G\<turnstile>membr of cls accessible_from accclass"  
schirmer@12854
   820
 \<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass"
schirmer@12854
   821
schirmer@12854
   822
syntax 
schirmer@12854
   823
method_accessible_from:: 
schirmer@12854
   824
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   825
                   ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
schirmer@12854
   826
schirmer@12854
   827
translations
schirmer@12854
   828
"G\<turnstile>Method m of cls accessible_from accclass"  
schirmer@12854
   829
 \<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass"  
schirmer@12854
   830
schirmer@12854
   831
syntax 
schirmer@12854
   832
methd_accessible_from:: 
schirmer@12854
   833
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   834
                 ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
schirmer@12854
   835
schirmer@12854
   836
translations
schirmer@12854
   837
"G\<turnstile>Methd s m of cls accessible_from accclass"  
schirmer@12854
   838
 \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
schirmer@12854
   839
schirmer@12854
   840
syntax 
schirmer@12854
   841
field_accessible_from:: 
schirmer@12854
   842
 "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   843
                 ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
schirmer@12854
   844
schirmer@12854
   845
translations
schirmer@12854
   846
"G\<turnstile>Field fn f of C accessible_from accclass"  
schirmer@12854
   847
 \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
schirmer@12854
   848
schirmer@12854
   849
inductive "accessible_fromR G accclass" intros
schirmer@12925
   850
Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
schirmer@12854
   851
              G\<turnstile>(Class class) accessible_in (pid accclass);
schirmer@12854
   852
              G\<turnstile>membr in class permits_acc_to accclass 
schirmer@12854
   853
             \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
schirmer@12854
   854
schirmer@12925
   855
Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
schirmer@12854
   856
              G\<turnstile>(Class class) accessible_in (pid accclass);
schirmer@12854
   857
              membr=(C,mdecl new);
schirmer@12854
   858
              G\<turnstile>(C,new) overrides\<^sub>S old; 
schirmer@12854
   859
              G\<turnstile>class \<prec>\<^sub>C sup;
schirmer@12854
   860
              G\<turnstile>Method old of sup accessible_from accclass
schirmer@12854
   861
             \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
schirmer@12854
   862
schirmer@12854
   863
consts
schirmer@12854
   864
dyn_accessible_fromR:: 
schirmer@12854
   865
 "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
schirmer@12854
   866
schirmer@12854
   867
syntax 
schirmer@12854
   868
dyn_accessible_from:: 
schirmer@12854
   869
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   870
                   ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
schirmer@12854
   871
schirmer@12854
   872
translations
schirmer@12854
   873
"G\<turnstile>membr in C dyn_accessible_from accC"  
schirmer@12854
   874
 \<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC"
schirmer@12854
   875
schirmer@12854
   876
syntax 
schirmer@12854
   877
method_dyn_accessible_from:: 
schirmer@12854
   878
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   879
                 ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
schirmer@12854
   880
schirmer@12854
   881
translations
schirmer@12854
   882
"G\<turnstile>Method m in C dyn_accessible_from accC"  
schirmer@12854
   883
 \<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC"  
schirmer@12854
   884
schirmer@12854
   885
syntax 
schirmer@12854
   886
methd_dyn_accessible_from:: 
schirmer@12854
   887
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   888
             ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
schirmer@12854
   889
schirmer@12854
   890
translations
schirmer@12854
   891
"G\<turnstile>Methd s m in C dyn_accessible_from accC"  
schirmer@12854
   892
 \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
schirmer@12854
   893
schirmer@12854
   894
syntax 
schirmer@12854
   895
field_dyn_accessible_from:: 
schirmer@12854
   896
 "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
schirmer@12854
   897
         ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
schirmer@12854
   898
schirmer@12854
   899
translations
schirmer@12854
   900
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
schirmer@12854
   901
 \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
schirmer@12854
   902
  
schirmer@12854
   903
inductive "dyn_accessible_fromR G accclass" intros
schirmer@12925
   904
Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
schirmer@12854
   905
              G\<turnstile>membr in class permits_acc_to accclass 
schirmer@12854
   906
             \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
schirmer@12854
   907
schirmer@12925
   908
Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
schirmer@12854
   909
              membr=(C,mdecl new);
schirmer@12854
   910
              G\<turnstile>(C,new) overrides old; 
schirmer@12854
   911
              G\<turnstile>class \<prec>\<^sub>C sup;
schirmer@12854
   912
              G\<turnstile>Method old in sup dyn_accessible_from accclass
schirmer@12854
   913
             \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
schirmer@12854
   914
schirmer@12854
   915
schirmer@12854
   916
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
schirmer@12854
   917
 \<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)"
schirmer@12854
   918
by (auto elim: accessible_fromR.induct)
schirmer@12854
   919
schirmer@12925
   920
lemma unique_declaration: 
schirmer@12925
   921
 "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
schirmer@12925
   922
  \<Longrightarrow> m = n"
schirmer@12925
   923
apply (cases m)
schirmer@12925
   924
apply (cases n,
schirmer@12925
   925
        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
schirmer@12925
   926
done
schirmer@12925
   927
schirmer@12854
   928
lemma declared_not_undeclared:
schirmer@12854
   929
  "G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C"
schirmer@12854
   930
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
schirmer@12854
   931
schirmer@12925
   932
lemma undeclared_not_declared:
schirmer@12925
   933
 "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
schirmer@12925
   934
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
schirmer@12925
   935
schirmer@12854
   936
lemma not_undeclared_declared:
schirmer@12854
   937
  "\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 
schirmer@12854
   938
                                           membr_id = memberid m)"
schirmer@12854
   939
proof -
schirmer@12854
   940
  assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C"
schirmer@12854
   941
  show ?thesis (is "?P membr_id")
schirmer@12854
   942
  proof (cases membr_id)
schirmer@12854
   943
    case (fid vname)
schirmer@12854
   944
    with not_undecl
schirmer@12854
   945
    obtain fld where
schirmer@12854
   946
      "G\<turnstile>fdecl (vname,fld) declared_in C" 
schirmer@12854
   947
      by (auto simp add: undeclared_in_def declared_in_def
schirmer@12854
   948
                         cdeclaredfield_def)
schirmer@12854
   949
    with fid show ?thesis 
schirmer@12854
   950
      by auto
schirmer@12854
   951
  next
schirmer@12854
   952
    case (mid sig)
schirmer@12854
   953
    with not_undecl
schirmer@12854
   954
    obtain mthd where
schirmer@12854
   955
      "G\<turnstile>mdecl (sig,mthd) declared_in C" 
schirmer@12854
   956
      by (auto simp add: undeclared_in_def declared_in_def
schirmer@12854
   957
                         cdeclaredmethd_def)
schirmer@12854
   958
    with mid show ?thesis 
schirmer@12854
   959
      by auto
schirmer@12854
   960
  qed
schirmer@12854
   961
qed
schirmer@12854
   962
schirmer@12854
   963
lemma unique_declared_in:
schirmer@12854
   964
 "\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk>
schirmer@12854
   965
 \<Longrightarrow> m = n"
schirmer@12854
   966
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
schirmer@12854
   967
            split: memberdecl.splits)
schirmer@12854
   968
schirmer@12854
   969
lemma unique_member_of: 
wenzelm@12937
   970
  assumes n: "G\<turnstile>n member_of C" and  
schirmer@12854
   971
          m: "G\<turnstile>m member_of C" and
schirmer@12854
   972
       eqid: "memberid n = memberid m"
wenzelm@12937
   973
  shows "n=m"
schirmer@12854
   974
proof -
schirmer@12854
   975
  from n m eqid  
schirmer@12854
   976
  show "n=m"
schirmer@12854
   977
  proof (induct)
schirmer@12854
   978
    case (Immediate C n)
schirmer@12854
   979
    assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C"
schirmer@12854
   980
    assume eqid: "memberid n = memberid m"
schirmer@12854
   981
    assume "G \<turnstile> m member_of C"
schirmer@12854
   982
    then show "n=m"
schirmer@12854
   983
    proof (cases)
schirmer@12854
   984
      case (Immediate _ m')
schirmer@12854
   985
      with eqid 
schirmer@12854
   986
      have "m=m'"
schirmer@12854
   987
           "memberid n = memberid m" 
schirmer@12854
   988
           "G\<turnstile> mbr m declared_in C" 
schirmer@12854
   989
           "declclass m = C"
schirmer@12854
   990
	by auto
schirmer@12854
   991
      with member_n   
schirmer@12854
   992
      show ?thesis
schirmer@12854
   993
	by (cases n, cases m) 
schirmer@12854
   994
           (auto simp add: declared_in_def 
schirmer@12854
   995
                           cdeclaredmethd_def cdeclaredfield_def
schirmer@12854
   996
                    split: memberdecl.splits)
schirmer@12854
   997
    next
schirmer@12854
   998
      case (Inherited _ _ m')
schirmer@12854
   999
      then have "G\<turnstile> memberid m undeclared_in C"
schirmer@12854
  1000
	by simp
schirmer@12854
  1001
      with eqid member_n
schirmer@12854
  1002
      show ?thesis
schirmer@12854
  1003
	by (cases n) (auto dest: declared_not_undeclared)
schirmer@12854
  1004
    qed
schirmer@12854
  1005
  next
schirmer@12854
  1006
    case (Inherited C S n)
schirmer@12854
  1007
    assume undecl: "G\<turnstile> memberid n undeclared_in C"
schirmer@12854
  1008
    assume  super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"
schirmer@12854
  1009
    assume    hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"
schirmer@12854
  1010
    assume   eqid: "memberid n = memberid m"
schirmer@12854
  1011
    assume "G \<turnstile> m member_of C"
schirmer@12854
  1012
    then show "n=m"
schirmer@12854
  1013
    proof (cases)
schirmer@12854
  1014
      case Immediate
schirmer@12854
  1015
      then have "G\<turnstile> mbr m declared_in C" by simp
schirmer@12854
  1016
      with eqid undecl
schirmer@12854
  1017
      show ?thesis
schirmer@12854
  1018
	by (cases m) (auto dest: declared_not_undeclared)
schirmer@12854
  1019
    next
schirmer@12854
  1020
      case Inherited 
schirmer@12854
  1021
      with super have "G \<turnstile> m member_of S"
schirmer@12854
  1022
	by (auto dest!: subcls1D)
schirmer@12854
  1023
      with eqid hyp
schirmer@12854
  1024
      show ?thesis 
schirmer@12854
  1025
	by blast
schirmer@12854
  1026
    qed
schirmer@12854
  1027
  qed
schirmer@12854
  1028
qed
schirmer@12854
  1029
schirmer@12854
  1030
lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C"
schirmer@12854
  1031
proof (induct set: members)
schirmer@12854
  1032
  case (Immediate C m)
schirmer@12854
  1033
  assume "G\<turnstile> mbr m declared_in C"
schirmer@12854
  1034
  then show "is_class G C"
schirmer@12854
  1035
    by (cases "mbr m")
schirmer@12854
  1036
       (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
schirmer@12854
  1037
next
schirmer@12854
  1038
  case (Inherited C S m)  
schirmer@12854
  1039
  assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"
schirmer@12854
  1040
  then show "is_class G C"
schirmer@12854
  1041
    by - (rule subcls_is_class2,auto)
schirmer@12854
  1042
qed
schirmer@12854
  1043
schirmer@12854
  1044
lemma member_of_declC: 
schirmer@12854
  1045
 "G\<turnstile>m member_of C 
schirmer@12854
  1046
  \<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)"
schirmer@12854
  1047
by (induct set: members) auto
schirmer@12854
  1048
schirmer@12854
  1049
lemma member_of_member_of_declC:
schirmer@12854
  1050
 "G\<turnstile>m member_of C 
schirmer@12854
  1051
  \<Longrightarrow> G\<turnstile>m member_of (declclass m)"
schirmer@12854
  1052
by (auto dest: member_of_declC intro: members.Immediate)
schirmer@12854
  1053
schirmer@12854
  1054
lemma member_of_class_relation:
schirmer@12854
  1055
  "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
schirmer@12854
  1056
proof (induct set: members)
schirmer@12854
  1057
  case (Immediate C m)
schirmer@12854
  1058
  then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp
schirmer@12854
  1059
next
schirmer@12854
  1060
  case (Inherited C S m)
schirmer@12854
  1061
  then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
schirmer@12854
  1062
    by (auto dest: r_into_rtrancl intro: rtrancl_trans)
schirmer@12854
  1063
qed
schirmer@12854
  1064
schirmer@12854
  1065
lemma member_in_class_relation:
schirmer@12854
  1066
  "G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
schirmer@12854
  1067
by (auto dest: member_inD member_of_class_relation
schirmer@12854
  1068
        intro: rtrancl_trans)
schirmer@12854
  1069
schirmer@12962
  1070
lemma stat_override_declclasses_relation: 
schirmer@12962
  1071
"\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk>
schirmer@12962
  1072
\<Longrightarrow> G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old)"
schirmer@12962
  1073
apply (rule trancl_rtrancl_trancl)
schirmer@12962
  1074
apply (erule r_into_trancl)
schirmer@12962
  1075
apply (cases old)
schirmer@12962
  1076
apply (auto dest: member_of_class_relation)
schirmer@12962
  1077
done
schirmer@12962
  1078
schirmer@12962
  1079
lemma stat_overrides_commonD:
schirmer@12962
  1080
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>  
schirmer@12962
  1081
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
schirmer@12962
  1082
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
schirmer@12962
  1083
  G\<turnstile>Method new declared_in (declclass new) \<and>   
schirmer@12962
  1084
  G\<turnstile>Method old declared_in (declclass old)"
schirmer@12962
  1085
apply (induct set: stat_overridesR) 
schirmer@12962
  1086
apply (frule (1) stat_override_declclasses_relation) 
schirmer@12962
  1087
apply (auto intro: trancl_trans)
schirmer@12962
  1088
done
schirmer@12962
  1089
schirmer@12854
  1090
lemma member_of_Package: 
schirmer@12854
  1091
 "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
schirmer@12854
  1092
  \<Longrightarrow> pid (declclass m) = pid C" 
schirmer@12854
  1093
proof -
schirmer@12854
  1094
  assume   member: "G\<turnstile>m member_of C"
schirmer@12854
  1095
  then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
schirmer@12854
  1096
  proof (induct rule: members.induct)
schirmer@12854
  1097
    fix C m
schirmer@12854
  1098
    assume     C: "declclass m = C"
schirmer@12854
  1099
    then show "pid (declclass m) = pid C"
schirmer@12854
  1100
      by simp
schirmer@12854
  1101
  next
schirmer@12854
  1102
    fix C S m  
schirmer@12854
  1103
    assume inheritable: "G \<turnstile> m inheritable_in pid C"
schirmer@12854
  1104
    assume         hyp: "PROP ?P m S" and
schirmer@12854
  1105
           package_acc: "accmodi m = Package" 
schirmer@12854
  1106
    with inheritable package_acc hyp
schirmer@12854
  1107
    show "pid (declclass m) = pid C" 
schirmer@12854
  1108
      by (auto simp add: inheritable_in_def)
schirmer@12854
  1109
  qed
schirmer@12854
  1110
qed
schirmer@12854
  1111
schirmer@12925
  1112
lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
schirmer@12925
  1113
proof -
schirmer@12925
  1114
  assume member_in_C:  "G\<turnstile>m member_in C"
schirmer@12925
  1115
  from member_in_C
schirmer@12925
  1116
  obtain provC where
schirmer@12925
  1117
    subclseq_C_provC: "G\<turnstile> C \<preceq>\<^sub>C provC" and
schirmer@12925
  1118
     member_of_provC: "G \<turnstile> m member_of provC"
schirmer@12925
  1119
    by (auto simp add: member_in_def)
schirmer@12925
  1120
  from member_of_provC
schirmer@12925
  1121
  have "G \<turnstile> m member_of declclass m"
schirmer@12925
  1122
    by (rule member_of_member_of_declC)
schirmer@12925
  1123
  moreover
schirmer@12925
  1124
  from member_in_C
schirmer@12925
  1125
  have "G\<turnstile>C \<preceq>\<^sub>C declclass m"
schirmer@12925
  1126
    by (rule member_in_class_relation)
schirmer@12925
  1127
  ultimately
schirmer@12925
  1128
  show ?thesis
schirmer@12925
  1129
    by (auto simp add: member_in_def)
schirmer@12925
  1130
qed
schirmer@12925
  1131
schirmer@12854
  1132
lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S
schirmer@12854
  1133
 \<Longrightarrow> G\<turnstile>m member_in C"
schirmer@12854
  1134
by (auto elim: dyn_accessible_fromR.induct)
schirmer@12854
  1135
schirmer@12854
  1136
lemma no_Private_stat_override: 
schirmer@12854
  1137
 "\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
schirmer@12854
  1138
by (induct set:  stat_overridesR) (auto simp add: inheritable_in_def)
schirmer@12854
  1139
schirmer@12854
  1140
lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
schirmer@12854
  1141
by (induct set: overridesR) (auto simp add: inheritable_in_def)
schirmer@12854
  1142
schirmer@12854
  1143
lemma permits_acc_inheritance:
schirmer@12854
  1144
 "\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
schirmer@12854
  1145
  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC"
schirmer@12854
  1146
by (cases "accmodi m")
schirmer@12854
  1147
   (auto simp add: permits_acc_def
schirmer@12854
  1148
            intro: subclseq_trans) 
schirmer@12854
  1149
schirmer@12925
  1150
lemma permits_acc_static_declC:
schirmer@12925
  1151
 "\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m
schirmer@12925
  1152
  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC"
schirmer@12925
  1153
by (cases "accmodi m") (auto simp add: permits_acc_def)
schirmer@12925
  1154
schirmer@12925
  1155
lemma dyn_accessible_from_static_declC: 
wenzelm@12937
  1156
  assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
schirmer@12925
  1157
           static: "is_static m"
wenzelm@12937
  1158
  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
schirmer@12925
  1159
proof -
schirmer@12925
  1160
  from acc_C static
schirmer@12925
  1161
  show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
schirmer@12925
  1162
  proof (induct)
schirmer@12925
  1163
    case (Immediate C m)
schirmer@12925
  1164
    then show ?case 
schirmer@12925
  1165
      by (auto intro!: dyn_accessible_fromR.Immediate
schirmer@12925
  1166
                 dest: member_in_declC permits_acc_static_declC) 
schirmer@12925
  1167
  next 
schirmer@12925
  1168
    case (Overriding declCNew C m new old sup)
schirmer@12925
  1169
    then have "\<not> is_static m"
schirmer@12925
  1170
      by (auto dest: overrides_commonD)
schirmer@12925
  1171
    moreover
schirmer@12925
  1172
    assume "is_static m"
schirmer@12925
  1173
    ultimately show ?case 
schirmer@12925
  1174
      by contradiction
schirmer@12925
  1175
  qed
schirmer@12925
  1176
qed
schirmer@12925
  1177
schirmer@12854
  1178
lemma field_accessible_fromD:
schirmer@12854
  1179
 "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
schirmer@12854
  1180
  \<Longrightarrow> G\<turnstile>membr member_of C \<and>
schirmer@12854
  1181
      G\<turnstile>(Class C) accessible_in (pid accC) \<and>
schirmer@12854
  1182
      G\<turnstile>membr in C permits_acc_to accC"
schirmer@12854
  1183
by (cases set: accessible_fromR)
schirmer@12854
  1184
   (auto simp add: is_field_def split: memberdecl.splits) 
schirmer@12854
  1185
schirmer@12854
  1186
lemma field_accessible_from_permits_acc_inheritance:
schirmer@12854
  1187
"\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
schirmer@12854
  1188
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC"
schirmer@12854
  1189
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
schirmer@12854
  1190
schirmer@12854
  1191
schirmer@12854
  1192
(*
schirmer@12854
  1193
lemma accessible_Package:
schirmer@12854
  1194
 "\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package;
schirmer@12854
  1195
   \<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk>
schirmer@12854
  1196
  \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
schirmer@12854
  1197
proof -
schirmer@12854
  1198
  assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new"
schirmer@12854
  1199
  assume "G \<turnstile> m of C accessible_from S"
schirmer@12854
  1200
  then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
schirmer@12854
  1201
    (is "?Pack m \<Longrightarrow> ?P C m")
schirmer@12854
  1202
  proof (induct rule: accessible_fromR.induct)
schirmer@12854
  1203
    fix C m
schirmer@12854
  1204
    assume "G\<turnstile>m member_of C"
schirmer@12854
  1205
           "G \<turnstile> m in C permits_acc_to S"
schirmer@12854
  1206
           "accmodi m = Package"      
schirmer@12854
  1207
    then show "?P C m"
schirmer@12854
  1208
      by (auto dest: member_of_Package simp add: permits_acc_def)
schirmer@12854
  1209
  next
schirmer@12854
  1210
    fix declC C new newm old Sup
schirmer@12854
  1211
    assume member_new: "G \<turnstile> new member_of C" and 
schirmer@12854
  1212
                acc_C: "G \<turnstile> Class C accessible_in pid S" and
schirmer@12854
  1213
                  new: "new = (declC, mdecl newm)" and
schirmer@12854
  1214
             override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and
schirmer@12854
  1215
         subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
schirmer@12854
  1216
              acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and
schirmer@12854
  1217
                  hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and
schirmer@12854
  1218
          accmodi_new: "accmodi new = Package"
schirmer@12854
  1219
    from override wf 
schirmer@12854
  1220
    have accmodi_weaken: "accmodi old \<le> accmodi newm"
schirmer@12854
  1221
      by (cases old,cases newm) auto
schirmer@12854
  1222
    from override new
schirmer@12854
  1223
    have "accmodi old \<noteq> Private"
schirmer@12854
  1224
      by (simp add: no_Private_stat_override)
schirmer@12854
  1225
    with accmodi_weaken accmodi_new new
schirmer@12854
  1226
    have accmodi_old: "accmodi old = Package"
schirmer@12854
  1227
      by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 
schirmer@12854
  1228
    with hyp 
schirmer@12854
  1229
    have P_sup: "?P Sup (methdMembr old)"
schirmer@12854
  1230
      by (simp)
schirmer@12854
  1231
    from wf override new accmodi_old accmodi_new
schirmer@12854
  1232
    have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
schirmer@12854
  1233
      by (auto dest: stat_override_Package) 
schirmer@12854
  1234
    from member_new accmodi_new
schirmer@12854
  1235
    have "pid (declclass new) = pid C"
schirmer@12854
  1236
      by (auto dest: member_of_Package)
schirmer@12854
  1237
    with eq_pid_new_old P_sup show "?P C new"
schirmer@12854
  1238
      by auto
schirmer@12854
  1239
  qed
schirmer@12854
  1240
qed
schirmer@12854
  1241
*)
schirmer@13688
  1242
schirmer@12854
  1243
lemma accessible_fieldD: 
schirmer@12854
  1244
 "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
schirmer@12854
  1245
 \<Longrightarrow> G\<turnstile>membr member_of C \<and>
schirmer@12854
  1246
     G\<turnstile>(Class C) accessible_in (pid accC) \<and>
schirmer@12854
  1247
     G\<turnstile>membr in C permits_acc_to accC"
schirmer@12854
  1248
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
schirmer@12854
  1249
      
schirmer@12854
  1250
schirmer@12854
  1251
schirmer@12854
  1252
lemma member_of_Private:
schirmer@12854
  1253
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C"
schirmer@12854
  1254
by (induct set: members) (auto simp add: inheritable_in_def)
schirmer@12854
  1255
schirmer@12854
  1256
lemma member_of_subclseq_declC:
schirmer@12854
  1257
  "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
schirmer@12854
  1258
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
schirmer@12854
  1259
schirmer@12854
  1260
lemma member_of_inheritance:
wenzelm@12937
  1261
  assumes       m: "G\<turnstile>m member_of D" and
schirmer@12854
  1262
     subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
schirmer@12854
  1263
     subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
schirmer@12854
  1264
               ws: "ws_prog G" 
wenzelm@12937
  1265
  shows "G\<turnstile>m member_of C"
schirmer@12854
  1266
proof -
schirmer@12854
  1267
  from m subclseq_D_C subclseq_C_m
schirmer@12854
  1268
  show ?thesis
schirmer@12854
  1269
  proof (induct)
schirmer@12854
  1270
    case (Immediate D m)
schirmer@12854
  1271
    assume "declclass m = D" and
schirmer@12854
  1272
           "G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m"
schirmer@12854
  1273
    with ws have "D=C" 
schirmer@12854
  1274
      by (auto intro: subclseq_acyclic)
schirmer@12854
  1275
    with Immediate 
schirmer@12854
  1276
    show "G\<turnstile>m member_of C"
schirmer@12854
  1277
      by (auto intro: members.Immediate)
schirmer@12854
  1278
  next
schirmer@12854
  1279
    case (Inherited D S m)
schirmer@12854
  1280
    assume member_of_D_props: 
schirmer@12854
  1281
            "G \<turnstile> m inheritable_in pid D" 
schirmer@12854
  1282
            "G\<turnstile> memberid m undeclared_in D"  
schirmer@12854
  1283
            "G \<turnstile> Class S accessible_in pid D" 
schirmer@12854
  1284
            "G \<turnstile> m member_of S"
schirmer@12854
  1285
    assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S"
schirmer@12854
  1286
    assume hyp: "\<lbrakk>G\<turnstile>S\<preceq>\<^sub>C C; G\<turnstile>C\<preceq>\<^sub>C declclass m\<rbrakk> \<Longrightarrow> G \<turnstile> m member_of C"
schirmer@12854
  1287
    assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m"
schirmer@12854
  1288
    assume "G\<turnstile>D\<preceq>\<^sub>C C"
schirmer@12854
  1289
    then show "G\<turnstile>m member_of C"
schirmer@12854
  1290
    proof (cases rule: subclseq_cases)
schirmer@12854
  1291
      case Eq
schirmer@12854
  1292
      assume "D=C" 
schirmer@12854
  1293
      with super member_of_D_props 
schirmer@12854
  1294
      show ?thesis
schirmer@12854
  1295
	by (auto intro: members.Inherited)
schirmer@12854
  1296
    next
schirmer@12854
  1297
      case Subcls
schirmer@12854
  1298
      assume "G\<turnstile>D\<prec>\<^sub>C C"
schirmer@12854
  1299
      with super 
schirmer@12854
  1300
      have "G\<turnstile>S\<preceq>\<^sub>C C"
schirmer@12854
  1301
	by (auto dest: subcls1D subcls_superD)
schirmer@12854
  1302
      with subclseq_C_m hyp show ?thesis
schirmer@12854
  1303
	by blast
schirmer@12854
  1304
    qed
schirmer@12854
  1305
  qed
schirmer@12854
  1306
qed
schirmer@12854
  1307
schirmer@12854
  1308
lemma member_of_subcls:
wenzelm@12937
  1309
  assumes     old: "G\<turnstile>old member_of C" and 
schirmer@12854
  1310
              new: "G\<turnstile>new member_of D" and
schirmer@12854
  1311
             eqid: "memberid new = memberid old" and
schirmer@12854
  1312
     subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
schirmer@12854
  1313
   subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
schirmer@12854
  1314
               ws: "ws_prog G"
wenzelm@12937
  1315
  shows "G\<turnstile>D \<prec>\<^sub>C C"
schirmer@12854
  1316
proof -
schirmer@12854
  1317
  from old 
schirmer@12854
  1318
  have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
schirmer@12854
  1319
    by (auto dest: member_of_subclseq_declC)
schirmer@12854
  1320
  from new 
schirmer@12854
  1321
  have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new"
schirmer@12854
  1322
    by (auto dest: member_of_subclseq_declC)
schirmer@12854
  1323
  from subcls_new_old ws
schirmer@12854
  1324
  have neq_new_old: "new\<noteq>old"
schirmer@12854
  1325
    by (cases new,cases old) (auto dest: subcls_irrefl)
schirmer@12854
  1326
  from subclseq_D_new subclseq_D_C
schirmer@12854
  1327
  have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 
schirmer@12854
  1328
    by (rule subcls_compareable)
schirmer@12854
  1329
  then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C"
schirmer@12854
  1330
  proof
schirmer@12854
  1331
    assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis .
schirmer@12854
  1332
  next
schirmer@12854
  1333
    assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)"
schirmer@12854
  1334
    with new subclseq_D_C ws 
schirmer@12854
  1335
    have "G\<turnstile>new member_of C"
schirmer@12854
  1336
      by (blast intro: member_of_inheritance)
schirmer@12854
  1337
    with eqid old 
schirmer@12854
  1338
    have "new=old"
schirmer@12854
  1339
      by (blast intro: unique_member_of)
schirmer@12854
  1340
    with neq_new_old 
schirmer@12854
  1341
    show ?thesis
schirmer@12854
  1342
      by contradiction
schirmer@12854
  1343
  qed
schirmer@12854
  1344
  then show ?thesis
schirmer@12854
  1345
  proof (cases rule: subclseq_cases)
schirmer@12854
  1346
    case Eq
schirmer@12854
  1347
    assume "declclass new = C"
schirmer@12854
  1348
    with new have "G\<turnstile>new member_of C"
schirmer@12854
  1349
      by (auto dest: member_of_member_of_declC)
schirmer@12854
  1350
    with eqid old 
schirmer@12854
  1351
    have "new=old"
schirmer@12854
  1352
      by (blast intro: unique_member_of)
schirmer@12854
  1353
    with neq_new_old 
schirmer@12854
  1354
    show ?thesis
schirmer@12854
  1355
      by contradiction
schirmer@12854
  1356
  next
schirmer@12854
  1357
    case Subcls
schirmer@12854
  1358
    assume "G\<turnstile>declclass new\<prec>\<^sub>C C"
schirmer@12854
  1359
    with subclseq_D_new
schirmer@12854
  1360
    show "G\<turnstile>D\<prec>\<^sub>C C"
schirmer@12854
  1361
      by (rule rtrancl_trancl_trancl)
schirmer@12854
  1362
  qed
schirmer@12854
  1363
qed
schirmer@12854
  1364
schirmer@12854
  1365
corollary member_of_overrides_subcls:
schirmer@12854
  1366
 "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
schirmer@12854
  1367
   G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk>
schirmer@12854
  1368
 \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
schirmer@12854
  1369
by (drule overrides_commonD) (auto intro: member_of_subcls)    
schirmer@12854
  1370
schirmer@12854
  1371
corollary member_of_stat_overrides_subcls:
schirmer@12854
  1372
 "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
schirmer@12854
  1373
   G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk>
schirmer@12854
  1374
 \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
schirmer@12854
  1375
by (drule stat_overrides_commonD) (auto intro: member_of_subcls)    
schirmer@12854
  1376
schirmer@12854
  1377
schirmer@12854
  1378
schirmer@12854
  1379
lemma inherited_field_access: 
wenzelm@12937
  1380
  assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
schirmer@12854
  1381
          is_field: "is_field membr" and 
schirmer@12854
  1382
          subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
wenzelm@12937
  1383
  shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
schirmer@12854
  1384
proof -
schirmer@12854
  1385
  from stat_acc is_field subclseq 
schirmer@12854
  1386
  show ?thesis
schirmer@12854
  1387
    by (auto dest: accessible_fieldD 
schirmer@12925
  1388
            intro: dyn_accessible_fromR.Immediate 
schirmer@12854
  1389
                   member_inI 
schirmer@12854
  1390
                   permits_acc_inheritance)
schirmer@12854
  1391
qed
schirmer@12854
  1392
schirmer@12854
  1393
lemma accessible_inheritance:
wenzelm@12937
  1394
  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
schirmer@12854
  1395
          subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
schirmer@12854
  1396
       member_dynC: "G\<turnstile>m member_of dynC" and
schirmer@12854
  1397
          dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
wenzelm@12937
  1398
  shows "G\<turnstile>m of dynC accessible_from accC"
schirmer@12854
  1399
proof -
schirmer@12854
  1400
  from stat_acc
schirmer@12854
  1401
  have member_statC: "G\<turnstile>m member_of statC" 
schirmer@12854
  1402
    by (auto dest: accessible_from_commonD)
schirmer@12854
  1403
  from stat_acc
schirmer@12854
  1404
  show ?thesis
schirmer@12854
  1405
  proof (cases)
schirmer@12925
  1406
    case Immediate
schirmer@12854
  1407
    with member_dynC member_statC subclseq dynC_acc
schirmer@12854
  1408
    show ?thesis
schirmer@12925
  1409
      by (auto intro: accessible_fromR.Immediate permits_acc_inheritance)
schirmer@12854
  1410
  next
schirmer@12925
  1411
    case Overriding
schirmer@12854
  1412
    with member_dynC subclseq dynC_acc
schirmer@12854
  1413
    show ?thesis
schirmer@12925
  1414
      by (auto intro: accessible_fromR.Overriding rtrancl_trancl_trancl)
schirmer@12854
  1415
  qed
schirmer@12854
  1416
qed
schirmer@12854
  1417
schirmer@12854
  1418
section "fields and methods"
schirmer@12854
  1419
schirmer@12854
  1420
schirmer@12854
  1421
types
schirmer@12854
  1422
  fspec = "vname \<times> qtname"
schirmer@12854
  1423
schirmer@12854
  1424
translations 
schirmer@12854
  1425
  "fspec" <= (type) "vname \<times> qtname" 
schirmer@12854
  1426
schirmer@12854
  1427
constdefs
schirmer@12854
  1428
imethds:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
schirmer@12854
  1429
"imethds G I 
schirmer@12854
  1430
  \<equiv> iface_rec (G,I)  
schirmer@12854
  1431
              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
schirmer@12854
  1432
                        (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
schirmer@12854
  1433
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
schirmer@12854
  1434
schirmer@12854
  1435
constdefs
schirmer@12854
  1436
accimethds:: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
schirmer@12854
  1437
"accimethds G pack I
schirmer@12854
  1438
  \<equiv> if G\<turnstile>Iface I accessible_in pack 
schirmer@12854
  1439
       then imethds G I
schirmer@12854
  1440
       else \<lambda> k. {}"
schirmer@12854
  1441
text {* only returns imethds if the interface is accessible *}
schirmer@12854
  1442
schirmer@12854
  1443
constdefs
schirmer@12854
  1444
methd:: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
schirmer@12854
  1445
schirmer@12854
  1446
"methd G C 
schirmer@12854
  1447
 \<equiv> class_rec (G,C) empty
schirmer@12854
  1448
             (\<lambda>C c subcls_mthds. 
schirmer@12854
  1449
               filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
schirmer@12854
  1450
                          subcls_mthds 
schirmer@12854
  1451
               ++ 
schirmer@12854
  1452
               table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))"
schirmer@12854
  1453
text {* @{term "methd G C"}: methods of a class C (statically visible from C), 
schirmer@12854
  1454
     with inheritance and hiding cf. 8.4.6;
schirmer@12854
  1455
     Overriding is captured by @{text dynmethd}.
schirmer@12854
  1456
     Every new method with the same signature coalesces the
schirmer@12854
  1457
     method of a superclass. *}
schirmer@12854
  1458
schirmer@12854
  1459
constdefs                      
schirmer@12854
  1460
accmethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
schirmer@12854
  1461
"accmethd G S C 
schirmer@12854
  1462
 \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
schirmer@12854
  1463
              (methd G C)"
schirmer@12854
  1464
text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
schirmer@12854
  1465
        accessible from S *}
schirmer@12854
  1466
schirmer@12854
  1467
text {* Note the class component in the accessibility filter. The class where
schirmer@12854
  1468
    method @{term m} is declared (@{term declC}) isn't necessarily accessible 
schirmer@12854
  1469
    from the current scope @{term S}. The method can be made accessible 
schirmer@12854
  1470
    through inheritance, too.
schirmer@12854
  1471
    So we must test accessibility of method @{term m} of class @{term C} 
schirmer@12854
  1472
    (not @{term "declclass m"}) *}
schirmer@12854
  1473
schirmer@12854
  1474
constdefs 
schirmer@12854
  1475
dynmethd:: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
schirmer@12854
  1476
"dynmethd G statC dynC  
schirmer@12854
  1477
  \<equiv> \<lambda> sig. 
schirmer@12854
  1478
     (if G\<turnstile>dynC \<preceq>\<^sub>C statC
schirmer@12854
  1479
        then (case methd G statC sig of
schirmer@12854
  1480
                None \<Rightarrow> None
schirmer@12854
  1481
              | Some statM 
schirmer@12854
  1482
                  \<Rightarrow> (class_rec (G,dynC) empty
schirmer@12854
  1483
                       (\<lambda>C c subcls_mthds. 
schirmer@12854
  1484
                          subcls_mthds
schirmer@12854
  1485
                          ++
schirmer@12854
  1486
                          (filter_tab 
schirmer@12854
  1487
                            (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
schirmer@12854
  1488
                            (methd G C) ))
schirmer@12854
  1489
                      ) sig
schirmer@12854
  1490
              )
schirmer@12854
  1491
        else None)"
schirmer@13688
  1492
schirmer@12854
  1493
text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
schirmer@12854
  1494
        with dynamic class @{term dynC} and static class @{term statC} *}
schirmer@12854
  1495
text {* Note some kind of duality between @{term methd} and @{term dynmethd} 
schirmer@12854
  1496
        in the @{term class_rec} arguments. Whereas @{term methd} filters the 
schirmer@12854
  1497
        subclass methods (to get only the inherited ones), @{term dynmethd} 
schirmer@12854
  1498
        filters the new methods (to get only those methods which actually
schirmer@12854
  1499
        override the methods of the static class) *}
schirmer@12854
  1500
schirmer@12854
  1501
constdefs 
schirmer@12854
  1502
dynimethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
schirmer@12854
  1503
"dynimethd G I dynC 
schirmer@12854
  1504
  \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
schirmer@12854
  1505
               then methd G dynC sig
schirmer@12854
  1506
               else dynmethd G Object dynC sig"
schirmer@12854
  1507
text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
schirmer@12854
  1508
        dynamic class dynC and static interface type I *}
schirmer@12854
  1509
text {* 
schirmer@12854
  1510
   When calling an interface method, we must distinguish if the method signature
schirmer@12854
  1511
   was defined in the interface or if it must be an Object method in the other
schirmer@12854
  1512
   case. If it was an interface method we search the class hierarchy
schirmer@12854
  1513
   starting at the dynamic class of the object up to Object to find the 
schirmer@12854
  1514
   first matching method (@{term methd}). Since all interface methods have 
schirmer@12854
  1515
   public access the method can't be coalesced due to some odd visibility 
schirmer@12854
  1516
   effects like in case of dynmethd. The method will be inherited or 
schirmer@12854
  1517
   overridden in all classes from the first class implementing the interface 
schirmer@12854
  1518
   down to the actual dynamic class.
schirmer@12854
  1519
 *}
schirmer@12854
  1520
schirmer@12854
  1521
constdefs
schirmer@12854
  1522
dynlookup::"prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
schirmer@12854
  1523
"dynlookup G statT dynC
schirmer@12854
  1524
  \<equiv> (case statT of
schirmer@12854
  1525
       NullT        \<Rightarrow> empty
schirmer@12854
  1526
     | IfaceT I     \<Rightarrow> dynimethd G I      dynC
schirmer@12854
  1527
     | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
schirmer@12854
  1528
     | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
schirmer@12854
  1529
text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the 
schirmer@12854
  1530
    static reference type statT and the dynamic class dynC. 
schirmer@12854
  1531
    In a wellformd context statT will not be NullT and in case
schirmer@12854
  1532
    statT is an array type, dynC=Object *}
schirmer@12854
  1533
schirmer@12854
  1534
constdefs
schirmer@12854
  1535
fields:: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list"
schirmer@12854
  1536
"fields G C 
schirmer@12854
  1537
  \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
schirmer@12854
  1538
text {* @{term "fields G C"} 
schirmer@12854
  1539
     list of fields of a class, including all the fields of the superclasses
schirmer@12854
  1540
     (private, inherited and hidden ones) not only the accessible ones
schirmer@12854
  1541
     (an instance of a object allocates all these fields *}
schirmer@12854
  1542
schirmer@12854
  1543
constdefs
schirmer@12854
  1544
accfield:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table"
schirmer@12854
  1545
"accfield G S C
schirmer@12854
  1546
  \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
schirmer@12854
  1547
    in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
schirmer@12854
  1548
                  field_tab"
schirmer@12854
  1549
text  {* @{term "accfield G C S"}: fields of a class @{term C} which are 
schirmer@12854
  1550
         accessible from scope of class
schirmer@12854
  1551
         @{term S} with inheritance and hiding, cf. 8.3 *}
schirmer@12854
  1552
text {* note the class component in the accessibility filter (see also 
schirmer@12854
  1553
        @{term methd}).
schirmer@12854
  1554
   The class declaring field @{term f} (@{term declC}) isn't necessarily 
schirmer@12854
  1555
   accessible from scope @{term S}. The field can be made visible through 
schirmer@12854
  1556
   inheritance, too. So we must test accessibility of field @{term f} of class 
schirmer@12854
  1557
   @{term C} (not @{term "declclass f"}) *} 
schirmer@12854
  1558
schirmer@12854
  1559
constdefs
schirmer@12854
  1560
schirmer@12854
  1561
  is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
schirmer@12854
  1562
 "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
schirmer@12854
  1563
schirmer@12854
  1564
constdefs efname:: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
schirmer@12854
  1565
"efname \<equiv> fst"
schirmer@12854
  1566
schirmer@12854
  1567
lemma efname_simp[simp]:"efname (n,f) = n"
schirmer@12854
  1568
by (simp add: efname_def) 
schirmer@12854
  1569
schirmer@12854
  1570
schirmer@12854
  1571
subsection "imethds"
schirmer@12854
  1572
schirmer@12854
  1573
lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1574
  imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
schirmer@12854
  1575
                      (o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
schirmer@12854
  1576
apply (unfold imethds_def)
schirmer@12854
  1577
apply (rule iface_rec [THEN trans])
schirmer@12854
  1578
apply auto
schirmer@12854
  1579
done
schirmer@12854
  1580
schirmer@12854
  1581
schirmer@12854
  1582
(* local lemma *)
schirmer@12854
  1583
lemma imethds_norec:
schirmer@12854
  1584
  "\<lbrakk>iface G md = Some i; ws_prog G; table_of (imethods i) sig = Some mh\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1585
  (md, mh) \<in> imethds G md sig"
schirmer@12854
  1586
apply (subst imethds_rec)
schirmer@12854
  1587
apply assumption+
schirmer@12854
  1588
apply (rule iffD2)
schirmer@12854
  1589
apply (rule overrides_t_Some_iff)
schirmer@12854
  1590
apply (rule disjI1)
schirmer@12854
  1591
apply (auto elim: table_of_map_SomeI)
schirmer@12854
  1592
done
schirmer@12854
  1593
schirmer@12854
  1594
lemma imethds_declI: "\<lbrakk>m \<in> imethds G I sig; ws_prog G; is_iface G I\<rbrakk> \<Longrightarrow> 
schirmer@12854
  1595
  (\<exists>i. iface G (decliface m) = Some i \<and> 
schirmer@12854
  1596
  table_of (imethods i) sig = Some (mthd m)) \<and>  
schirmer@12854
  1597
  (I,decliface m) \<in> (subint1 G)^* \<and> m \<in> imethds G (decliface m) sig"
schirmer@12854
  1598
apply (erule make_imp)
schirmer@12854
  1599
apply (rule ws_subint1_induct, assumption, assumption)
schirmer@12854
  1600
apply (subst imethds_rec, erule conjunct1, assumption)
schirmer@12854
  1601
apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
schirmer@12854
  1602
done
schirmer@12854
  1603
schirmer@12854
  1604
lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
wenzelm@12937
  1605
  assumes im: "im \<in> imethds G I sig" and  
schirmer@12854
  1606
         ifI: "iface G I = Some i" and
schirmer@12854
  1607
          ws: "ws_prog G" and
schirmer@12854
  1608
     hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
schirmer@12854
  1609
                = Some im \<Longrightarrow> P" and
schirmer@12854
  1610
     hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
wenzelm@12937
  1611
  shows P
schirmer@12854
  1612
proof -
schirmer@12854
  1613
  from ifI ws im hyp_new hyp_inh
schirmer@12854
  1614
  show "P"
schirmer@12854
  1615
    by (auto simp add: imethds_rec)
schirmer@12854
  1616
qed
schirmer@12854
  1617
schirmer@12854
  1618
subsection "accimethd"
schirmer@12854
  1619
schirmer@12854
  1620
lemma accimethds_simp [simp]: 
schirmer@12854
  1621
"G\<turnstile>Iface I accessible_in pack \<Longrightarrow> accimethds G pack I = imethds G I"
schirmer@12854
  1622
by (simp add: accimethds_def)
schirmer@12854
  1623
schirmer@12854
  1624
lemma accimethdsD:
schirmer@12854
  1625
 "im \<in> accimethds G pack I sig 
schirmer@12854
  1626
  \<Longrightarrow> im \<in> imethds G I sig \<and> G\<turnstile>Iface I accessible_in pack"
schirmer@12854
  1627
by (auto simp add: accimethds_def)
schirmer@12854
  1628
schirmer@12854
  1629
lemma accimethdsI: 
schirmer@12854
  1630
"\<lbrakk>im \<in> imethds G I sig;G\<turnstile>Iface I accessible_in pack\<rbrakk>
schirmer@12854
  1631
 \<Longrightarrow> im \<in> accimethds G pack I sig"
schirmer@12854
  1632
by simp
schirmer@12854
  1633
schirmer@12854
  1634
subsection "methd"
schirmer@12854
  1635
schirmer@12854
  1636
lemma methd_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1637
  methd G C 
schirmer@12854
  1638
    = (if C = Object 
schirmer@12854
  1639
          then empty 
schirmer@12854
  1640
          else filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
schirmer@12854
  1641
                          (methd G (super c))) 
schirmer@12854
  1642
      ++ table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))"
schirmer@12854
  1643
apply (unfold methd_def)
schirmer@12854
  1644
apply (erule class_rec [THEN trans], assumption)
schirmer@12854
  1645
apply (simp)
schirmer@12854
  1646
done
schirmer@12854
  1647
schirmer@12854
  1648
(* local lemma *)
schirmer@12854
  1649
lemma methd_norec: 
schirmer@12854
  1650
 "\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> 
schirmer@12854
  1651
  \<Longrightarrow> methd G declC sig = Some (declC, m)"
schirmer@12854
  1652
apply (simp only: methd_rec)
schirmer@12854
  1653
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
schirmer@12854
  1654
apply (auto elim: table_of_map_SomeI)
schirmer@12854
  1655
done
schirmer@12854
  1656
schirmer@12854
  1657
schirmer@12854
  1658
lemma methd_declC: 
schirmer@12854
  1659
"\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> \<Longrightarrow>
schirmer@12854
  1660
 (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> 
schirmer@12854
  1661
 G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"   
schirmer@12854
  1662
apply (erule make_imp)
schirmer@12854
  1663
apply (rule ws_subcls1_induct, assumption, assumption)
schirmer@12854
  1664
apply (subst methd_rec, assumption)
schirmer@12854
  1665
apply (case_tac "Ca=Object")
schirmer@12854
  1666
apply   (force elim: methd_norec )
schirmer@12854
  1667
schirmer@12854
  1668
apply   simp
schirmer@12854
  1669
apply   (case_tac "table_of (map (\<lambda>(s, m). (s, Ca, m)) (methods c)) sig")
schirmer@12854
  1670
apply     (force intro: rtrancl_into_rtrancl2)
schirmer@12854
  1671
schirmer@12854
  1672
apply     (auto intro: methd_norec)
schirmer@12854
  1673
done
schirmer@12854
  1674
schirmer@12854
  1675
lemma methd_inheritedD:
schirmer@12854
  1676
  "\<lbrakk>class G C = Some c; ws_prog G;methd G C sig = Some m\<rbrakk>
schirmer@12854
  1677
  \<Longrightarrow>  (declclass m \<noteq> C \<longrightarrow> G \<turnstile>C inherits method sig m)"
schirmer@12854
  1678
by (auto simp add: methd_rec)
schirmer@12854
  1679
schirmer@12854
  1680
lemma methd_diff_cls:
schirmer@12854
  1681
"\<lbrakk>ws_prog G; is_class G C; is_class G D;
schirmer@12854
  1682
 methd G C sig = m; methd G D sig = n; m\<noteq>n
schirmer@12854
  1683
\<rbrakk> \<Longrightarrow> C\<noteq>D"
schirmer@12854
  1684
by (auto simp add: methd_rec)
schirmer@12854
  1685
schirmer@12854
  1686
lemma method_declared_inI: 
schirmer@12854
  1687
 "\<lbrakk>table_of (methods c) sig = Some m; class G C = Some c\<rbrakk>
schirmer@12854
  1688
  \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
schirmer@12854
  1689
by (auto simp add: cdeclaredmethd_def declared_in_def)
schirmer@12854
  1690
schirmer@12854
  1691
lemma methd_declared_in_declclass: 
schirmer@12854
  1692
 "\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> 
schirmer@12854
  1693
 \<Longrightarrow> G\<turnstile>Methd sig m declared_in (declclass m)"
schirmer@12854
  1694
by (auto dest: methd_declC method_declared_inI)
schirmer@12854
  1695
schirmer@12854
  1696
lemma member_methd:
wenzelm@12937
  1697
  assumes member_of: "G\<turnstile>Methd sig m member_of C" and
schirmer@12854
  1698
                 ws: "ws_prog G"
wenzelm@12937
  1699
  shows "methd G C sig = Some m"
schirmer@12854
  1700
proof -
schirmer@12854
  1701
  from member_of 
schirmer@12854
  1702
  have iscls_C: "is_class G C" 
schirmer@12854
  1703
    by (rule member_of_is_classD)
schirmer@12854
  1704
  from iscls_C ws member_of
schirmer@12854
  1705
  show ?thesis (is "?Methd C")
schirmer@12854
  1706
  proof (induct rule: ws_class_induct')
schirmer@12854
  1707
    case (Object co)
schirmer@12854
  1708
    assume "G \<turnstile>Methd sig m member_of Object"
schirmer@12854
  1709
    then have "G\<turnstile>Methd sig m declared_in Object \<and> declclass m = Object"
schirmer@12854
  1710
      by (cases set: members) (cases m, auto dest: subcls1D)
schirmer@12854
  1711
    with ws Object 
schirmer@12854
  1712
    show "?Methd Object"
schirmer@12854
  1713
      by (cases m)
schirmer@12854
  1714
         (auto simp add: declared_in_def cdeclaredmethd_def methd_rec
schirmer@12854
  1715
                  intro:  table_of_mapconst_SomeI)
schirmer@12854
  1716
  next
schirmer@12854
  1717
    case (Subcls C c)
schirmer@12854
  1718
    assume clsC: "class G C = Some c" and
schirmer@12854
  1719
      neq_C_Obj: "C \<noteq> Object" and
schirmer@12854
  1720
            hyp: "G \<turnstile>Methd sig m member_of super c \<Longrightarrow> ?Methd (super c)" and
schirmer@12854
  1721
      member_of: "G \<turnstile>Methd sig m member_of C"
schirmer@12854
  1722
    from member_of
schirmer@12854
  1723
    show "?Methd C"
schirmer@12854
  1724
    proof (cases)
schirmer@12854
  1725
      case (Immediate Ca membr)
schirmer@12854
  1726
      then have "Ca=C" "membr = method sig m" and 
schirmer@12854
  1727
                "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
schirmer@12854
  1728
	by (cases m,auto)
schirmer@12854
  1729
      with clsC 
schirmer@12854
  1730
      have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
schirmer@12854
  1731
	by (cases m)
schirmer@12854
  1732
	   (auto simp add: declared_in_def cdeclaredmethd_def
schirmer@12854
  1733
	            intro: table_of_mapconst_SomeI)
schirmer@12854
  1734
      with clsC neq_C_Obj ws 
schirmer@12854
  1735
      show ?thesis
schirmer@12854
  1736
	by (simp add: methd_rec)
schirmer@12854
  1737
    next
schirmer@12854
  1738
      case (Inherited Ca S membr)
schirmer@12854
  1739
      with clsC
schirmer@12854
  1740
      have eq_Ca_C: "Ca=C" and
schirmer@12854
  1741
            undecl: "G\<turnstile>mid sig undeclared_in C" and
schirmer@12854
  1742
             super: "G \<turnstile>Methd sig m member_of (super c)"
schirmer@12854
  1743
	by (auto dest: subcls1D)
schirmer@12854
  1744
      from eq_Ca_C clsC undecl 
schirmer@12854
  1745
      have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
schirmer@12854
  1746
	by (auto simp add: undeclared_in_def cdeclaredmethd_def
schirmer@12854
  1747
	            intro: table_of_mapconst_NoneI)
schirmer@12854
  1748
      moreover
schirmer@12854
  1749
      from Inherited have "G \<turnstile> C inherits (method sig m)"
schirmer@12854
  1750
	by (auto simp add: inherits_def)
schirmer@12854
  1751
      moreover
schirmer@12854
  1752
      note clsC neq_C_Obj ws super hyp 
schirmer@12854
  1753
      ultimately
schirmer@12854
  1754
      show ?thesis
schirmer@12854
  1755
	by (auto simp add: methd_rec intro: filter_tab_SomeI)
schirmer@12854
  1756
    qed
schirmer@12854
  1757
  qed
schirmer@12854
  1758
qed
schirmer@12854
  1759
schirmer@12854
  1760
(*unused*)
schirmer@12854
  1761
lemma finite_methd:"ws_prog G \<Longrightarrow> finite {methd G C sig |sig C. is_class G C}"
schirmer@12854
  1762
apply (rule finite_is_class [THEN finite_SetCompr2])
schirmer@12854
  1763
apply (intro strip)
schirmer@12854
  1764
apply (erule_tac ws_subcls1_induct, assumption)
schirmer@12854
  1765
apply (subst methd_rec)
schirmer@12854
  1766
apply (assumption)
schirmer@12854
  1767
apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_override)
schirmer@12854
  1768
done
schirmer@12854
  1769
schirmer@12854
  1770
lemma finite_dom_methd:
schirmer@12854
  1771
 "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (methd G C))"
schirmer@12854
  1772
apply (erule_tac ws_subcls1_induct)
schirmer@12854
  1773
apply assumption
schirmer@12854
  1774
apply (subst methd_rec)
schirmer@12854
  1775
apply (assumption)
schirmer@12854
  1776
apply (auto intro!: finite_dom_map_of finite_dom_filter_tab)
schirmer@12854
  1777
done
schirmer@12854
  1778
schirmer@12854
  1779
schirmer@12854
  1780
subsection "accmethd"
schirmer@12854
  1781
schirmer@12854
  1782
lemma accmethd_SomeD:
schirmer@12854
  1783
"accmethd G S C sig = Some m
schirmer@12854
  1784
 \<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S"
schirmer@12854
  1785
by (auto simp add: accmethd_def dest: filter_tab_SomeD)
schirmer@12854
  1786
schirmer@12854
  1787
lemma accmethd_SomeI:
schirmer@12854
  1788
"\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk> 
schirmer@12854
  1789
 \<Longrightarrow> accmethd G S C sig = Some m"
schirmer@12854
  1790
by (auto simp add: accmethd_def intro: filter_tab_SomeI)
schirmer@12854
  1791
schirmer@12854
  1792
lemma accmethd_declC: 
schirmer@12854
  1793
"\<lbrakk>accmethd G S C sig = Some m; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>
schirmer@12854
  1794
 (\<exists>d. class G (declclass m)=Some d \<and> 
schirmer@12854
  1795
  table_of (methods d) sig=Some (mthd m)) \<and> 
schirmer@12854
  1796
 G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m \<and> 
schirmer@12854
  1797
 G\<turnstile>method sig m of C accessible_from S"
schirmer@12854
  1798
by (auto dest: accmethd_SomeD methd_declC accmethd_SomeI)
schirmer@12854
  1799
schirmer@12854
  1800
schirmer@12854
  1801
lemma finite_dom_accmethd:
schirmer@12854
  1802
 "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (accmethd G S C))"
schirmer@12854
  1803
by (auto simp add: accmethd_def intro: finite_dom_filter_tab finite_dom_methd)
schirmer@12854
  1804
schirmer@12854
  1805
schirmer@12854
  1806
subsection "dynmethd"
schirmer@12854
  1807
schirmer@12854
  1808
lemma dynmethd_rec:
schirmer@12854
  1809
"\<lbrakk>class G dynC = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1810
 dynmethd G statC dynC sig
schirmer@12854
  1811
   = (if G\<turnstile>dynC \<preceq>\<^sub>C statC
schirmer@12854
  1812
        then (case methd G statC sig of
schirmer@12854
  1813
                None \<Rightarrow> None
schirmer@12854
  1814
              | Some statM 
schirmer@12854
  1815
                  \<Rightarrow> (case methd G dynC sig of
schirmer@12854
  1816
                        None \<Rightarrow> dynmethd G statC (super c) sig
schirmer@12854
  1817
                      | Some dynM \<Rightarrow> 
schirmer@12854
  1818
                          (if G,sig\<turnstile> dynM overrides statM \<or> dynM = statM 
schirmer@12854
  1819
                              then Some dynM
schirmer@12854
  1820
                              else (dynmethd G statC (super c) sig)
schirmer@12854
  1821
                      )))
schirmer@12854
  1822
         else None)" 
schirmer@12854
  1823
   (is "_ \<Longrightarrow> _ \<Longrightarrow> ?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig") 
schirmer@12854
  1824
proof -
schirmer@12854
  1825
  assume clsDynC: "class G dynC = Some c" and 
schirmer@12854
  1826
              ws: "ws_prog G"
schirmer@12854
  1827
  then show "?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig" 
schirmer@12854
  1828
  proof (induct rule: ws_class_induct'')
schirmer@12854
  1829
    case (Object co)
schirmer@12854
  1830
    show "?Dynmethd_def Object sig = ?Dynmethd_rec Object co sig"
schirmer@12854
  1831
    proof (cases "G\<turnstile>Object \<preceq>\<^sub>C statC") 
schirmer@12854
  1832
      case False
schirmer@12854
  1833
      then show ?thesis by (simp add: dynmethd_def)
schirmer@12854
  1834
    next
schirmer@12854
  1835
      case True
schirmer@12854
  1836
      then have eq_statC_Obj: "statC = Object" ..
schirmer@12854
  1837
      show ?thesis 
schirmer@12854
  1838
      proof (cases "methd G statC sig")
schirmer@12854
  1839
	case None then show ?thesis by (simp add: dynmethd_def)
schirmer@12854
  1840
      next
schirmer@12854
  1841
	case Some
schirmer@12854
  1842
	with True Object ws eq_statC_Obj 
schirmer@12854
  1843
	show ?thesis
schirmer@12854
  1844
	  by (auto simp add: dynmethd_def class_rec
schirmer@12854
  1845
                      intro: filter_tab_SomeI)
schirmer@12854
  1846
      qed
schirmer@12854
  1847
    qed
schirmer@12854
  1848
  next  
schirmer@12854
  1849
    case (Subcls dynC c sc)
schirmer@12854
  1850
    show "?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig"
schirmer@12854
  1851
    proof (cases "G\<turnstile>dynC \<preceq>\<^sub>C statC") 
schirmer@12854
  1852
      case False
schirmer@12854
  1853
      then show ?thesis by (simp add: dynmethd_def)
schirmer@12854
  1854
    next
schirmer@12854
  1855
      case True
schirmer@12854
  1856
      note subclseq_dynC_statC = True
schirmer@12854
  1857
      show ?thesis
schirmer@12854
  1858
      proof (cases "methd G statC sig")
schirmer@12854
  1859
	case None then show ?thesis by (simp add: dynmethd_def)
schirmer@12854
  1860
      next
schirmer@12854
  1861
	case (Some statM)
schirmer@12854
  1862
	note statM = Some
schirmer@12854
  1863
	let "?filter C" = 
schirmer@12854
  1864
              "filter_tab
schirmer@12854
  1865
                (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
schirmer@12854
  1866
                (methd G C)"
schirmer@12854
  1867
        let "?class_rec C" =
schirmer@12854
  1868
              "(class_rec (G, C) empty
schirmer@12854
  1869
                           (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
schirmer@12854
  1870
	from statM Subcls ws subclseq_dynC_statC
schirmer@12854
  1871
	have dynmethd_dynC_def:
schirmer@12854
  1872
             "?Dynmethd_def dynC sig =
schirmer@12854
  1873
                ((?class_rec (super c)) 
schirmer@12854
  1874
                 ++
schirmer@12854
  1875
                (?filter dynC)) sig"
schirmer@12854
  1876
         by (simp (no_asm_simp) only: dynmethd_def class_rec)
schirmer@12854
  1877
	    auto
schirmer@12854
  1878
       show ?thesis
schirmer@12854
  1879
       proof (cases "dynC = statC")
schirmer@12854
  1880
	 case True
schirmer@12854
  1881
	 with subclseq_dynC_statC statM dynmethd_dynC_def
schirmer@12854
  1882
	 have "?Dynmethd_def dynC sig = Some statM"
schirmer@12854
  1883
	   by (auto intro: override_find_right filter_tab_SomeI)
schirmer@12854
  1884
	 with subclseq_dynC_statC True Some 
schirmer@12854
  1885
	 show ?thesis
schirmer@12854
  1886
	   by auto
schirmer@12854
  1887
       next
schirmer@12854
  1888
	 case False
schirmer@12854
  1889
	 with subclseq_dynC_statC Subcls 
schirmer@12854
  1890
	 have subclseq_super_statC: "G\<turnstile>(super c) \<preceq>\<^sub>C statC"
schirmer@12854
  1891
	   by (blast dest: subclseq_superD)
schirmer@12854
  1892
	 show ?thesis
schirmer@12854
  1893
	 proof (cases "methd G dynC sig") 
schirmer@12854
  1894
	   case None
schirmer@12854
  1895
	   then have "?filter dynC sig = None"
schirmer@12854
  1896
	     by (rule filter_tab_None)
schirmer@12854
  1897
           then have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
schirmer@12854
  1898
	     by (simp add: dynmethd_dynC_def)
schirmer@12854
  1899
	   with  subclseq_super_statC statM None
schirmer@12854
  1900
	   have "?Dynmethd_def dynC sig = ?Dynmethd_def (super c) sig"
schirmer@12854
  1901
	     by (auto simp add: empty_def dynmethd_def)
schirmer@12854
  1902
           with None subclseq_dynC_statC statM
schirmer@12854
  1903
	   show ?thesis 
schirmer@12854
  1904
	     by simp
schirmer@12854
  1905
	 next
schirmer@12854
  1906
	   case (Some dynM)
schirmer@12854
  1907
	   note dynM = Some
schirmer@12854
  1908
	   let ?Termination = "G \<turnstile> qmdecl sig dynM overrides qmdecl sig statM \<or>
schirmer@12854
  1909
                               dynM = statM"
schirmer@12854
  1910
	   show ?thesis
schirmer@12854
  1911
	   proof (cases "?filter dynC sig")
schirmer@12854
  1912
	     case None
schirmer@12854
  1913
	     with dynM 
schirmer@12854
  1914
	     have no_termination: "\<not> ?Termination"
schirmer@12854
  1915
	       by (simp add: filter_tab_def)
schirmer@12854
  1916
	     from None 
schirmer@12854
  1917
	     have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
schirmer@12854
  1918
	       by (simp add: dynmethd_dynC_def)
schirmer@12854
  1919
	     with subclseq_super_statC statM dynM no_termination
schirmer@12854
  1920
	     show ?thesis
schirmer@12854
  1921
	       by (auto simp add: empty_def dynmethd_def)
schirmer@12854
  1922
	   next
schirmer@12854
  1923
	     case Some
schirmer@12854
  1924
	     with dynM
schirmer@12854
  1925
	     have termination: "?Termination"
schirmer@12854
  1926
	       by (auto)
schirmer@12854
  1927
	     with Some dynM
schirmer@12854
  1928
	     have "?Dynmethd_def dynC sig=Some dynM"
schirmer@12854
  1929
	      by (auto simp add: dynmethd_dynC_def)
schirmer@12854
  1930
	     with subclseq_super_statC statM dynM termination
schirmer@12854
  1931
	     show ?thesis
schirmer@12854
  1932
	       by (auto simp add: dynmethd_def)
schirmer@12854
  1933
	   qed
schirmer@12854
  1934
	 qed
schirmer@12854
  1935
       qed
schirmer@12854
  1936
     qed
schirmer@12854
  1937
   qed
schirmer@12854
  1938
 qed
schirmer@12854
  1939
qed
schirmer@12854
  1940
	       
schirmer@12854
  1941
lemma dynmethd_C_C:"\<lbrakk>is_class G C; ws_prog G\<rbrakk> 
schirmer@12854
  1942
\<Longrightarrow> dynmethd G C C sig = methd G C sig"          
schirmer@12854
  1943
apply (auto simp add: dynmethd_rec)
schirmer@12854
  1944
done
schirmer@12854
  1945
 
schirmer@12854
  1946
lemma dynmethdSomeD: 
schirmer@12854
  1947
 "\<lbrakk>dynmethd G statC dynC sig = Some dynM; is_class G dynC; ws_prog G\<rbrakk> 
schirmer@12854
  1948
  \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
schirmer@12854
  1949
by (auto simp add: dynmethd_rec)
schirmer@12854
  1950
 
schirmer@12854
  1951
lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
wenzelm@12937
  1952
  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
schirmer@12854
  1953
        is_cls_dynC: "is_class G dynC" and
schirmer@12854
  1954
                 ws: "ws_prog G" and
schirmer@12854
  1955
         hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
schirmer@12854
  1956
       hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
schirmer@12854
  1957
                       G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
wenzelm@12937
  1958
  shows P
schirmer@12854
  1959
proof -
schirmer@12854
  1960
  from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
schirmer@12854
  1961
  from clsDynC ws dynM hyp_static hyp_override
schirmer@12854
  1962
  show "P"
schirmer@12854
  1963
  proof (induct rule: ws_class_induct)
schirmer@12854
  1964
    case (Object co)
schirmer@12854
  1965
    with ws  have "statC = Object" 
schirmer@12854
  1966
      by (auto simp add: dynmethd_rec)
schirmer@12854
  1967
    with ws Object show ?thesis by (auto simp add: dynmethd_C_C)
schirmer@12854
  1968
  next
schirmer@12854
  1969
    case (Subcls C c)
schirmer@12854
  1970
    with ws show ?thesis
schirmer@12854
  1971
      by (auto simp add: dynmethd_rec)
schirmer@12854
  1972
  qed
schirmer@12854
  1973
qed
schirmer@12854
  1974
schirmer@12854
  1975
lemma no_override_in_Object:
wenzelm@12937
  1976
  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
schirmer@12854
  1977
            is_cls_dynC: "is_class G dynC" and
schirmer@12854
  1978
                     ws: "ws_prog G" and
schirmer@12854
  1979
                  statM: "methd G statC sig = Some statM" and
schirmer@12854
  1980
         neq_dynM_statM: "dynM\<noteq>statM"
wenzelm@12937
  1981
  shows "dynC \<noteq> Object"
schirmer@12854
  1982
proof -
schirmer@12854
  1983
  from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
schirmer@12854
  1984
  from clsDynC ws dynM statM neq_dynM_statM 
schirmer@12854
  1985
  show ?thesis (is "?P dynC")
schirmer@12854
  1986
  proof (induct rule: ws_class_induct)
schirmer@12854
  1987
    case (Object co)
schirmer@12854
  1988
    with ws  have "statC = Object" 
schirmer@12854
  1989
      by (auto simp add: dynmethd_rec)
schirmer@12854
  1990
    with ws Object show "?P Object" by (auto simp add: dynmethd_C_C)
schirmer@12854
  1991
  next
schirmer@12854
  1992
    case (Subcls dynC c)
schirmer@12854
  1993
    with ws show "?P dynC"
schirmer@12854
  1994
      by (auto simp add: dynmethd_rec)
schirmer@12854
  1995
  qed
schirmer@12854
  1996
qed
schirmer@12854
  1997
schirmer@12854
  1998
schirmer@12854
  1999
lemma dynmethd_Some_rec_cases [consumes 3, 
schirmer@12854
  2000
                               case_names Static Override  Recursion]:
wenzelm@12937
  2001
  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
schirmer@12854
  2002
                clsDynC: "class G dynC = Some c" and
schirmer@12854
  2003
                     ws: "ws_prog G" and
schirmer@12854
  2004
             hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
schirmer@12854
  2005
           hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;
schirmer@12854
  2006
                                     methd G dynC sig = Some dynM; statM\<noteq>dynM;
schirmer@12854
  2007
                                     G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
schirmer@12854
  2008
schirmer@12854
  2009
          hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
wenzelm@12937
  2010
                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
wenzelm@12937
  2011
  shows P
schirmer@12854
  2012
proof -
schirmer@12854
  2013
  from clsDynC have "is_class G dynC" by simp
schirmer@12854
  2014
  note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
schirmer@12854
  2015
  from ws clsDynC dynM hyp_static hyp_override hyp_recursion
schirmer@12854
  2016
  show ?thesis
schirmer@12854
  2017
    by (auto simp add: dynmethd_rec dest: no_override_in_Object')
schirmer@12854
  2018
qed
schirmer@12854
  2019
schirmer@12854
  2020
lemma dynmethd_declC: 
schirmer@12854
  2021
"\<lbrakk>dynmethd G statC dynC sig = Some m;
schirmer@12854
  2022
  is_class G statC;ws_prog G
schirmer@12854
  2023
 \<rbrakk> \<Longrightarrow>
schirmer@12854
  2024
  (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and>
schirmer@12854
  2025
  G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"
schirmer@12854
  2026
proof - 
schirmer@12854
  2027
  assume  is_cls_statC: "is_class G statC" 
schirmer@12854
  2028
  assume            ws: "ws_prog G"  
schirmer@12854
  2029
  assume             m: "dynmethd G statC dynC sig = Some m"
schirmer@12854
  2030
  from m 
schirmer@12854
  2031
  have "G\<turnstile>dynC \<preceq>\<^sub>C statC" by (auto simp add: dynmethd_def)
schirmer@12854
  2032
  from this is_cls_statC 
schirmer@12854
  2033
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
schirmer@12854
  2034
  from is_cls_dynC ws m  
schirmer@12854
  2035
  show ?thesis (is "?P dynC") 
schirmer@12854
  2036
  proof (induct rule: ws_class_induct')
schirmer@12854
  2037
    case (Object co)
schirmer@12854
  2038
    with ws have "statC=Object" by (auto simp add: dynmethd_rec)
schirmer@12854
  2039
    with ws Object  
schirmer@12854
  2040
    show "?P Object" 
schirmer@12854
  2041
      by (auto simp add: dynmethd_C_C dest: methd_declC)
schirmer@12854
  2042
  next
schirmer@12854
  2043
    case (Subcls dynC c)
schirmer@12854
  2044
    assume   hyp: "dynmethd G statC (super c) sig = Some m \<Longrightarrow> ?P (super c)" and
schirmer@12854
  2045
         clsDynC: "class G dynC = Some c"  and
schirmer@12854
  2046
              m': "dynmethd G statC dynC sig = Some m" and
schirmer@12854
  2047
    neq_dynC_Obj: "dynC \<noteq> Object"
schirmer@12854
  2048
    from ws this obtain statM where
schirmer@12854
  2049
      subclseq_dynC_statC: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and 
schirmer@12854
  2050
                     statM: "methd G statC sig = Some statM"
schirmer@12854
  2051
      by (blast dest: dynmethdSomeD)
schirmer@12854
  2052
    from clsDynC neq_dynC_Obj 
schirmer@12854
  2053
    have subclseq_dynC_super: "G\<turnstile>dynC \<preceq>\<^sub>C (super c)" 
schirmer@12854
  2054
      by (auto intro: subcls1I) 
schirmer@12854
  2055
    from m' clsDynC ws 
schirmer@12854
  2056
    show "?P dynC"
schirmer@12854
  2057
    proof (cases rule: dynmethd_Some_rec_cases) 
schirmer@12854
  2058
      case Static
schirmer@12854
  2059
      with is_cls_statC ws subclseq_dynC_statC 
schirmer@12854
  2060
      show ?thesis 
schirmer@12854
  2061
	by (auto intro: rtrancl_trans dest: methd_declC)
schirmer@12854
  2062
    next
schirmer@12854
  2063
      case Override
schirmer@12854
  2064
      with clsDynC ws 
schirmer@12854
  2065
      show ?thesis 
schirmer@12854
  2066
	by (auto dest: methd_declC)
schirmer@12854
  2067
    next
schirmer@12854
  2068
      case Recursion
schirmer@12854
  2069
      with hyp subclseq_dynC_super 
schirmer@12854
  2070
      show ?thesis 
schirmer@12854
  2071
	by (auto intro: rtrancl_trans) 
schirmer@12854
  2072
    qed
schirmer@12854
  2073
  qed
schirmer@12854
  2074
qed
schirmer@12854
  2075
schirmer@12854
  2076
lemma methd_Some_dynmethd_Some:
wenzelm@12937
  2077
  assumes     statM: "methd G statC sig = Some statM" and
schirmer@12854
  2078
           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
schirmer@12854
  2079
       is_cls_statC: "is_class G statC" and
schirmer@12854
  2080
                 ws: "ws_prog G"
wenzelm@12937
  2081
  shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
wenzelm@12937
  2082
    (is "?P dynC")
schirmer@12854
  2083
proof -
schirmer@12854
  2084
  from subclseq is_cls_statC 
schirmer@12854
  2085
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
schirmer@12854
  2086
  then obtain dc where
schirmer@12854
  2087
    clsDynC: "class G dynC = Some dc" by blast
schirmer@12854
  2088
  from clsDynC ws subclseq 
schirmer@12854
  2089
  show "?thesis"
schirmer@12854
  2090
  proof (induct rule: ws_class_induct)
schirmer@12854
  2091
    case (Object co)
schirmer@12854
  2092
    with ws  have "statC = Object" 
schirmer@12854
  2093
      by (auto)
schirmer@12854
  2094
    with ws Object statM
schirmer@12854
  2095
    show "?P Object"  
schirmer@12854
  2096
      by (auto simp add: dynmethd_C_C)
schirmer@12854
  2097
  next
schirmer@12854
  2098
    case (Subcls dynC dc)
schirmer@12854
  2099
    assume clsDynC': "class G dynC = Some dc"
schirmer@12854
  2100
    assume neq_dynC_Obj: "dynC \<noteq> Object"
schirmer@12854
  2101
    assume hyp: "G\<turnstile>super dc\<preceq>\<^sub>C statC \<Longrightarrow> ?P (super dc)"
schirmer@12854
  2102
    assume subclseq': "G\<turnstile>dynC\<preceq>\<^sub>C statC"
schirmer@12854
  2103
    then
schirmer@12854
  2104
    show "?P dynC"
schirmer@12854
  2105
    proof (cases rule: subclseq_cases)
schirmer@12854
  2106
      case Eq
schirmer@12854
  2107
      with ws statM clsDynC' 
schirmer@12854
  2108
      show ?thesis
schirmer@12854
  2109
	by (auto simp add: dynmethd_rec)
schirmer@12854
  2110
    next
schirmer@12854
  2111
      case Subcls
schirmer@12854
  2112
      assume "G\<turnstile>dynC\<prec>\<^sub>C statC"
schirmer@12854
  2113
      from this clsDynC' 
schirmer@12854
  2114
      have "G\<turnstile>super dc\<preceq>\<^sub>C statC" by (rule subcls_superD)
schirmer@12854
  2115
      with hyp ws clsDynC' subclseq' statM
schirmer@12854
  2116
      show ?thesis
schirmer@12854
  2117
	by (auto simp add: dynmethd_rec)
schirmer@12854
  2118
    qed
schirmer@12854
  2119
  qed
schirmer@12854
  2120
qed
schirmer@12854
  2121
schirmer@12854
  2122
lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
wenzelm@12937
  2123
  assumes     statM: "methd G statC sig = Some statM" and 
schirmer@12854
  2124
           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
schirmer@12854
  2125
       is_cls_statC: "is_class G statC" and
schirmer@12854
  2126
                 ws: "ws_prog G" and
schirmer@12854
  2127
         hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and
schirmer@12854
  2128
       hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
schirmer@12854
  2129
                                 dynM\<noteq>statM;
schirmer@12854
  2130
                           G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
wenzelm@12937
  2131
  shows P
schirmer@12854
  2132
proof -
schirmer@12854
  2133
  from subclseq is_cls_statC 
schirmer@12854
  2134
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
schirmer@12854
  2135
  then obtain dc where
schirmer@12854
  2136
    clsDynC: "class G dynC = Some dc" by blast
schirmer@12854
  2137
  from statM subclseq is_cls_statC ws 
schirmer@12854
  2138
  obtain dynM
schirmer@12854
  2139
    where dynM: "dynmethd G statC dynC sig = Some dynM"
schirmer@12854
  2140
    by (blast dest: methd_Some_dynmethd_Some)
schirmer@12854
  2141
  from dynM is_cls_dynC ws 
schirmer@12854
  2142
  show ?thesis
schirmer@12854
  2143
  proof (cases rule: dynmethd_Some_cases)
schirmer@12854
  2144
    case Static
schirmer@12854
  2145
    with hyp_static dynM statM show ?thesis by simp
schirmer@12854
  2146
  next
schirmer@12854
  2147
    case Overrides
schirmer@12854
  2148
    with hyp_override dynM statM show ?thesis by simp
schirmer@12854
  2149
  qed
schirmer@12854
  2150
qed
schirmer@12854
  2151
schirmer@12854
  2152
lemma ws_dynmethd:
wenzelm@12937
  2153
  assumes  statM: "methd G statC sig = Some statM" and
schirmer@12854
  2154
        subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
schirmer@12854
  2155
    is_cls_statC: "is_class G statC" and
schirmer@12854
  2156
              ws: "ws_prog G"
wenzelm@12937
  2157
  shows
wenzelm@12937
  2158
    "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
wenzelm@12937
  2159
             is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
schirmer@12854
  2160
proof - 
schirmer@12854
  2161
  from statM subclseq is_cls_statC ws
schirmer@12854
  2162
  show ?thesis
schirmer@12854
  2163
  proof (cases rule: dynmethd_cases)
schirmer@12854
  2164
    case Static
schirmer@12854
  2165
    with statM 
schirmer@12854
  2166
    show ?thesis
schirmer@12854
  2167
      by simp
schirmer@12854
  2168
  next
schirmer@12854
  2169
    case Overrides
schirmer@12854
  2170
    with ws
schirmer@12854
  2171
    show ?thesis
schirmer@12854
  2172
      by (auto dest: ws_overrides_commonD)
schirmer@12854
  2173
  qed
schirmer@12854
  2174
qed
schirmer@12854
  2175
schirmer@12854
  2176
subsection "dynlookup"
schirmer@12854
  2177
schirmer@12854
  2178
lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]:
schirmer@12854
  2179
"\<lbrakk>dynlookup G statT dynC sig = x;
schirmer@12854
  2180
           \<lbrakk>statT = NullT       ; empty sig = x                  \<rbrakk> \<Longrightarrow> P;
schirmer@12854
  2181
  \<And> I.    \<lbrakk>statT = IfaceT I    ; dynimethd G I      dynC sig = x\<rbrakk> \<Longrightarrow> P;
schirmer@12854
  2182
  \<And> statC.\<lbrakk>statT = ClassT statC; dynmethd  G statC  dynC sig = x\<rbrakk> \<Longrightarrow> P;
schirmer@12854
  2183
  \<And> ty.   \<lbrakk>statT = ArrayT ty   ; dynmethd  G Object dynC sig = x\<rbrakk> \<Longrightarrow> P
schirmer@12854
  2184
 \<rbrakk> \<Longrightarrow> P"
schirmer@12854
  2185
by (cases statT) (auto simp add: dynlookup_def)
schirmer@12854
  2186
schirmer@12854
  2187
subsection "fields"
schirmer@12854
  2188
schirmer@12854
  2189
lemma fields_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  2190
  fields G C = map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c) @  
schirmer@12854
  2191
  (if C = Object then [] else fields G (super c))"
schirmer@12854
  2192
apply (simp only: fields_def)
schirmer@12854
  2193
apply (erule class_rec [THEN trans])
schirmer@12854
  2194
apply assumption
schirmer@12854
  2195
apply clarsimp
schirmer@12854
  2196
done
schirmer@12854
  2197
schirmer@12854
  2198
(* local lemma *)
schirmer@12854
  2199
lemma fields_norec: 
schirmer@12854
  2200
"\<lbrakk>class G fd = Some c; ws_prog G;  table_of (cfields c) fn = Some f\<rbrakk> 
schirmer@12854
  2201
 \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
schirmer@12854
  2202
apply (subst fields_rec)
schirmer@12854
  2203
apply assumption+
schirmer@12854
  2204
apply (subst map_of_override [symmetric])
schirmer@12854
  2205
apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
schirmer@12854
  2206
apply (auto elim: table_of_map2_SomeI)
schirmer@12854
  2207
done
schirmer@12854
  2208
schirmer@12854
  2209
(* local lemma *)
schirmer@12854
  2210
lemma table_of_fieldsD:
schirmer@12854
  2211
"table_of (map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c)) efn = Some f
schirmer@12854
  2212
\<Longrightarrow> (declclassf efn) = C \<and> table_of (cfields c) (fname efn) = Some f"
schirmer@12854
  2213
apply (case_tac "efn")
schirmer@12854
  2214
by auto
schirmer@12854
  2215
schirmer@12854
  2216
lemma fields_declC: 
schirmer@12854
  2217
 "\<lbrakk>table_of (fields G C) efn = Some f; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>  
schirmer@12854
  2218
  (\<exists>d. class G (declclassf efn) = Some d \<and> 
schirmer@12854
  2219
                    table_of (cfields d) (fname efn)=Some f) \<and> 
schirmer@12854
  2220
  G\<turnstile>C \<preceq>\<^sub>C (declclassf efn)  \<and> table_of (fields G (declclassf efn)) efn = Some f"
schirmer@12854
  2221
apply (erule make_imp)
schirmer@12854
  2222
apply (rule ws_subcls1_induct, assumption, assumption)
schirmer@12854
  2223
apply (subst fields_rec, assumption)
schirmer@12854
  2224
apply clarify
schirmer@12854
  2225
apply (simp only: map_of_override [symmetric] del: map_of_override)
schirmer@12854
  2226
apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
schirmer@12854
  2227
apply   (force intro:rtrancl_into_rtrancl2 simp add: override_def)
schirmer@12854
  2228
schirmer@12854
  2229
apply   (frule_tac fd="Ca" in fields_norec)
schirmer@12854
  2230
apply     assumption
schirmer@12854
  2231
apply     blast
schirmer@12854
  2232
apply   (frule table_of_fieldsD)  
schirmer@12854
  2233
apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
schirmer@12854
  2234
              and  m="table_of (if Ca = Object then [] else fields G (super c))"
schirmer@12854
  2235
         in override_find_right)
schirmer@12854
  2236
apply   (case_tac "efn")
schirmer@12854
  2237
apply   (simp)
schirmer@12854
  2238
done
schirmer@12854
  2239
schirmer@12854
  2240
lemma fields_emptyI: "\<And>y. \<lbrakk>ws_prog G; class G C = Some c;cfields c = [];  
schirmer@12854
  2241
  C \<noteq> Object \<longrightarrow> class G (super c) = Some y \<and> fields G (super c) = []\<rbrakk> \<Longrightarrow>  
schirmer@12854
  2242
  fields G C = []"
schirmer@12854
  2243
apply (subst fields_rec)
schirmer@12854
  2244
apply assumption
schirmer@12854
  2245
apply auto
schirmer@12854
  2246
done
schirmer@12854
  2247
schirmer@12854
  2248
(* easier than with table_of *)
schirmer@12854
  2249
lemma fields_mono_lemma: 
schirmer@12854
  2250
"\<lbrakk>x \<in> set (fields G C); G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> 
schirmer@12854
  2251
 \<Longrightarrow> x \<in> set (fields G D)"
schirmer@12854
  2252
apply (erule make_imp)
schirmer@12854
  2253
apply (erule converse_rtrancl_induct)
schirmer@12854
  2254
apply  fast
schirmer@12854
  2255
apply (drule subcls1D)
schirmer@12854
  2256
apply clarsimp
schirmer@12854
  2257
apply (subst fields_rec)
schirmer@12854
  2258
apply   auto
schirmer@12854
  2259
done
schirmer@12854
  2260
schirmer@12854
  2261
schirmer@12854
  2262
lemma ws_unique_fields_lemma: 
schirmer@12854
  2263
 "\<lbrakk>(efn,fd)  \<in> set (fields G (super c)); fc \<in> set (cfields c); ws_prog G;  
schirmer@12854
  2264
   fname efn = fname fc; declclassf efn = C;
schirmer@12854
  2265
   class G C = Some c; C \<noteq> Object; class G (super c) = Some d\<rbrakk> \<Longrightarrow> R"
schirmer@12854
  2266
apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption)
schirmer@12854
  2267
apply (drule_tac weak_map_of_SomeI)
schirmer@12854
  2268
apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption)
schirmer@12854
  2269
apply (auto dest: fields_declC [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]])
schirmer@12854
  2270
done
schirmer@12854
  2271
schirmer@12854
  2272
lemma ws_unique_fields: "\<lbrakk>is_class G C; ws_prog G; 
schirmer@12854
  2273
       \<And>C c. \<lbrakk>class G C = Some c\<rbrakk> \<Longrightarrow> unique (cfields c) \<rbrakk> \<Longrightarrow>
schirmer@12854
  2274
      unique (fields G C)" 
schirmer@12854
  2275
apply (rule ws_subcls1_induct, assumption, assumption)
schirmer@12854
  2276
apply (subst fields_rec, assumption)            
paulson@13585
  2277
apply (auto intro!: unique_map_inj inj_onI 
paulson@13585
  2278
            elim!: unique_append ws_unique_fields_lemma fields_norec)
schirmer@12854
  2279
done
schirmer@12854
  2280
schirmer@12854
  2281
schirmer@12854
  2282
subsection "accfield"
schirmer@12854
  2283
schirmer@12854
  2284
lemma accfield_fields: 
schirmer@12854
  2285
 "accfield G S C fn = Some f 
schirmer@12854
  2286
  \<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
schirmer@12854
  2287
apply (simp only: accfield_def Let_def)
schirmer@12854
  2288
apply (rule table_of_remap_SomeD)
schirmer@12854
  2289
apply (auto dest: filter_tab_SomeD)
schirmer@12854
  2290
done
schirmer@12854
  2291
schirmer@12854
  2292
schirmer@12854
  2293
lemma accfield_declC_is_class: 
schirmer@12854
  2294
 "\<lbrakk>is_class G C; accfield G S C en = Some (fd, f); ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  2295
   is_class G fd"
schirmer@12854
  2296
apply (drule accfield_fields)
schirmer@12854
  2297
apply (drule fields_declC [THEN conjunct1], assumption)
schirmer@12854
  2298
apply auto
schirmer@12854
  2299
done
schirmer@12854
  2300
schirmer@12854
  2301
lemma accfield_accessibleD: 
schirmer@12854
  2302
  "accfield G S C fn = Some f \<Longrightarrow> G\<turnstile>Field fn f of C accessible_from S"
schirmer@12854
  2303
by (auto simp add: accfield_def Let_def)
schirmer@12854
  2304
schirmer@12854
  2305
subsection "is methd"
schirmer@12854
  2306
schirmer@12854
  2307
lemma is_methdI: 
schirmer@12854
  2308
"\<lbrakk>class G C = Some y; methd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig"
schirmer@12854
  2309
apply (unfold is_methd_def)
schirmer@12854
  2310
apply auto
schirmer@12854
  2311
done
schirmer@12854
  2312
schirmer@12854
  2313
lemma is_methdD: 
schirmer@12854
  2314
"is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> methd G C sig \<noteq> None"
schirmer@12854
  2315
apply (unfold is_methd_def)
schirmer@12854
  2316
apply auto
schirmer@12854
  2317
done
schirmer@12854
  2318
schirmer@12854
  2319
lemma finite_is_methd: 
schirmer@12854
  2320
 "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
schirmer@12854
  2321
apply (unfold is_methd_def)
schirmer@12854
  2322
apply (subst SetCompr_Sigma_eq)
schirmer@12854
  2323
apply (rule finite_is_class [THEN finite_SigmaI])
schirmer@12854
  2324
apply (simp only: mem_Collect_eq)
schirmer@12854
  2325
apply (fold dom_def)
schirmer@12854
  2326
apply (erule finite_dom_methd)
schirmer@12854
  2327
apply assumption
schirmer@12854
  2328
done
schirmer@12854
  2329
schirmer@12854
  2330
section "calculation of the superclasses of a class"
schirmer@12854
  2331
schirmer@12854
  2332
constdefs 
schirmer@12854
  2333
 superclasses:: "prog \<Rightarrow> qtname \<Rightarrow> qtname set"
schirmer@12854
  2334
 "superclasses G C \<equiv> class_rec (G,C) {} 
schirmer@12854
  2335
                       (\<lambda> C c superclss. (if C=Object 
schirmer@12854
  2336
                                            then {} 
schirmer@12854
  2337
                                            else insert (super c) superclss))"
schirmer@12854
  2338
   
schirmer@12854
  2339
lemma superclasses_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
  2340
 superclasses G C 
schirmer@12854
  2341
 = (if (C=Object) 
schirmer@12854
  2342
       then {}
schirmer@12854
  2343
       else insert (super c) (superclasses G (super c)))"
schirmer@12854
  2344
apply (unfold superclasses_def)
schirmer@12854
  2345
apply (erule class_rec [THEN trans], assumption)
schirmer@12854
  2346
apply (simp)
schirmer@12854
  2347
done
schirmer@12854
  2348
schirmer@12854
  2349
lemma superclasses_mono:
schirmer@12854
  2350
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
schirmer@12854
  2351
  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
schirmer@12854
  2352
  x\<in>superclasses G D 
schirmer@12854
  2353
\<rbrakk> \<Longrightarrow> x\<in>superclasses G C" 
schirmer@12854
  2354
proof -
schirmer@12854
  2355
  
schirmer@12854
  2356
  assume     ws: "ws_prog G"          and 
schirmer@12854
  2357
          cls_C: "class G C = Some c" and
schirmer@12854
  2358
             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
schirmer@12854
  2359
                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
schirmer@12854
  2360
  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
schirmer@12854
  2361
  thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
schirmer@12854
  2362
        x\<in>superclasses G C" (is "PROP ?P C"  
schirmer@12854
  2363
                             is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
schirmer@12854
  2364
  proof (induct ?P C  rule: converse_trancl_induct)
schirmer@12854
  2365
    fix C c
schirmer@12854
  2366
    assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D"
schirmer@12854
  2367
    with wf ws show "?SUP C"
schirmer@12854
  2368
      by (auto    intro: no_subcls1_Object 
schirmer@12854
  2369
               simp add: superclasses_rec subcls1_def)
schirmer@12854
  2370
  next
schirmer@12854
  2371
    fix C S c
schirmer@12854
  2372
    assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
schirmer@12854
  2373
       and    hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
schirmer@12854
  2374
                           \<Longrightarrow> x \<in> superclasses G S"
schirmer@12854
  2375
       and  cls_C': "class G C = Some c"
schirmer@12854
  2376
       and       x: "x \<in> superclasses G D"
schirmer@12854
  2377
    moreover note wf ws
schirmer@12854
  2378
    moreover from calculation 
schirmer@12854
  2379
    have "?SUP S" 
schirmer@12854
  2380
      by (force intro: no_subcls1_Object simp add: subcls1_def)
schirmer@12854
  2381
    moreover from calculation 
schirmer@12854
  2382
    have "super c = S" 
schirmer@12854
  2383
      by (auto intro: no_subcls1_Object simp add: subcls1_def)
schirmer@12854
  2384
    ultimately show "?SUP C" 
schirmer@12854
  2385
      by (auto intro: no_subcls1_Object simp add: superclasses_rec)
schirmer@12854
  2386
  qed
schirmer@12854
  2387
qed
schirmer@12854
  2388
schirmer@12854
  2389
lemma subclsEval:
schirmer@12854
  2390
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
schirmer@12854
  2391
  \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc 
schirmer@12854
  2392
 \<rbrakk> \<Longrightarrow> D\<in>superclasses G C" 
schirmer@12854
  2393
proof -
schirmer@12854
  2394
  note converse_trancl_induct 
schirmer@12854
  2395
       = converse_trancl_induct [consumes 1,case_names Single Step]
schirmer@12854
  2396
  assume 
schirmer@12854
  2397
             ws: "ws_prog G"          and 
schirmer@12854
  2398
          cls_C: "class G C = Some c" and
schirmer@12854
  2399
             wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
schirmer@12854
  2400
                  \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
schirmer@12854
  2401
  assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
schirmer@12854
  2402
  thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" 
schirmer@12854
  2403
    (is "PROP ?P C"  is "\<And> c. ?CLS C c  \<Longrightarrow> ?SUP C")
schirmer@12854
  2404
  proof (induct ?P C  rule: converse_trancl_induct)
schirmer@12854
  2405
    fix C c
schirmer@12854
  2406
    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c"
schirmer@12854
  2407
    with ws wf show "?SUP C"
schirmer@12854
  2408
      by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
schirmer@12854
  2409
  next
schirmer@12854
  2410
    fix C S c
schirmer@12854
  2411
    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" 
schirmer@12854
  2412
           "\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S"
schirmer@12854
  2413
           "class G C = Some c" 
schirmer@12854
  2414
    with ws wf show "?SUP C"
schirmer@12854
  2415
      by - (rule superclasses_mono,
schirmer@12854
  2416
            auto dest: no_subcls1_Object simp add: subcls1_def )
schirmer@12854
  2417
  qed
schirmer@12854
  2418
qed
schirmer@12854
  2419
schirmer@12854
  2420
end