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