src/HOL/Bali/DeclConcepts.thy
author Thomas Sewell <tsewell@nicta.com.au>
Fri Sep 25 19:04:18 2009 +1000 (2009-09-25)
changeset 32754 4e0256f7d219
parent 32134 ee143615019c
child 32960 69916a850301
permissions -rw-r--r--
Avoid record-inner constants in polymorphic definitions in Bali

The Bali package needs to insert a record extension into a type
class and define an associated polymorphic constant. There is no
elegant way to do this.

The existing approach was to insert every record extension into
the type class, defining the polymorphic constant at each layer
using inner operations created by the record package. Some of
those operations have been removed. They can be replaced by use
of record_name.extend if necessary, but we can also sidestep
this altogether.

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