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