src/HOL/Bali/DeclConcepts.thy
author wenzelm
Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 12962 a24ffe84a06a
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     1
(*  Title:      HOL/Bali/DeclConcepts.thy
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     2
    ID:         $Id$
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     3
    Author:     Norbert Schirmer
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     5
*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Advanced concepts on Java declarations like overriding, inheritance,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
dynamic method lookup*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
theory DeclConcepts = TypeRel:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
"is_public G qn \<equiv> (case class G qn of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
                     None       \<Rightarrow> (case iface G qn of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
                                      None       \<Rightarrow> False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
                                    | Some iface \<Rightarrow> access iface = Public)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
                   | Some class \<Rightarrow> access class = Public)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
subsection "accessibility of types (cf. 6.6.1)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
text {* 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
Primitive types are always accessible, interfaces and classes are accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
in their package or if they are defined public, an array type is accessible if
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
its element type is accessible *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
                                      ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
       rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
                                      ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
primrec
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
"G\<turnstile>(PrimT p)   accessible_in pack  = True"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
accessible_in_RefT_simp: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
"G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
"G\<turnstile>(NullT)     accessible_in' pack = True"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
"G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
"G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
declare accessible_in_RefT_simp [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
  is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
    "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
  is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
    "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
  is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
    "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
  is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
  "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
lemma is_acc_classD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
 "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
by (simp add: is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
by (auto simp add: is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
lemma is_acc_ifaceD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
  "is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
by (simp add: is_acc_iface_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
lemma is_acc_typeD:
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
    65
 "is_acc_type  G P T \<Longrightarrow> is_type G T  \<and> G\<turnstile>T accessible_in P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
by (simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
lemma is_acc_reftypeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
"is_acc_reftype  G P T \<Longrightarrow> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
by (simp add: is_acc_reftype_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
subsection "accessibility of members"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
The accessibility of members is more involved as the accessibility of types.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
We have to distinguish several cases to model the different effects of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
accessibility during inheritance, overriding and ordinary member access 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
subsubsection {* Various technical conversion and selection functions *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
text {* overloaded selector @{text accmodi} to select the access modifier 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
out of various HOL types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
axclass has_accmodi < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
12859
wenzelm
parents: 12854
diff changeset
    87
instance acc_modi::has_accmodi ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
by (simp add: acc_modi_accmodi_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
12859
wenzelm
parents: 12854
diff changeset
    95
instance access_field_type:: ("type","type") has_accmodi ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
by (simp add: decl_acc_modi_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
12859
wenzelm
parents: 12854
diff changeset
   104
instance * :: ("type",has_accmodi) has_accmodi ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
by (simp add: pair_acc_modi_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
12859
wenzelm
parents: 12854
diff changeset
   112
instance memberdecl :: has_accmodi ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
                                          fdecl f \<Rightarrow> accmodi f
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
                                        | mdecl m \<Rightarrow> accmodi m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
lemma memberdecl_fdecl_acc_modi_simp[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
 "accmodi (fdecl m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
by (simp add: memberdecl_acc_modi_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
lemma memberdecl_mdecl_acc_modi_simp[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
 "accmodi (mdecl m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
by (simp add: memberdecl_acc_modi_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
text {* overloaded selector @{text declclass} to select the declaring class 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
out of various HOL types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
axclass has_declclass < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
12859
wenzelm
parents: 12854
diff changeset
   133
instance pid_field_type::("type","type") has_declclass ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
by (simp add: qtname_declclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
12859
wenzelm
parents: 12854
diff changeset
   141
instance * :: ("has_declclass","type") has_declclass ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
by (simp add: pair_declclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
text {* overloaded selector @{text is_static} to select the static modifier 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
out of various HOL types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
axclass has_static < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
consts is_static :: "'a::has_static \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
consts is_static :: "'a \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
12859
wenzelm
parents: 12854
diff changeset
   160
instance access_field_type :: ("type","has_static") has_static ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
decl_is_static_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
 "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
12859
wenzelm
parents: 12854
diff changeset
   166
instance static_field_type :: ("type","type") has_static ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
static_field_type_is_static_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
 "is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply (cases m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply (simp add: static_field_type_is_static_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
                 decl_is_static_def Decl.member.dest_convs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
12859
wenzelm
parents: 12854
diff changeset
   178
instance * :: ("type","has_static") has_static ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
by (simp add: pair_is_static_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
by (simp add: pair_is_static_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
12859
wenzelm
parents: 12854
diff changeset
   189
instance memberdecl:: has_static ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
memberdecl_is_static_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
 "is_static m \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
                    fdecl f \<Rightarrow> is_static f
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
                  | mdecl m \<Rightarrow> is_static m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
lemma memberdecl_is_static_fdecl_simp[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
 "is_static (fdecl f) = is_static f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
by (simp add: memberdecl_is_static_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
lemma memberdecl_is_static_mdecl_simp[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
 "is_static (mdecl m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
by (simp add: memberdecl_is_static_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
by (cases m) (simp add: mhead_def member_is_static_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
constdefs  (* some mnemotic selectors for (qtname \<times> ('a::more) decl_scheme) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
            * the first component is a class or interface name
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
            * the second component is a method, field or method head *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
(* "declclass":: "(qtname \<times> ('a::more) decl_scheme) \<Rightarrow> qtname"*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
(* "declclass \<equiv> fst" *)          (* get the class component *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
 "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
 "decliface \<equiv> fst"          (* get the interface component *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
 "member"::   "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
 "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
 "mbr \<equiv> snd"            (* get the memberdecl component *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
 "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
                           (* also used for mdecl,mhead *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
 "mthd \<equiv> snd"              (* get the method component *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
 "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
              (* also used for ((vname \<times> qtname)\<times> field) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
 "fld \<equiv> snd"               (* get the field component *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
(* "accmodi" :: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> acc_modi"*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
                           (* also used for mdecl *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
(* "accmodi \<equiv> access \<circ> snd"*)  (* get the access modifier *) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
 "is_static" ::"('b \<times> ('a::type) member_scheme) \<Rightarrow> bool" *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
                            (* also defined for emhead cf. WellType *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
 (*"is_static \<equiv> static \<circ> snd"*) (* get the static modifier *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
constdefs (* some mnemotic selectors for (vname \<times> qtname) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
 fname:: "(vname \<times> 'a) \<Rightarrow> vname" (* also used for fdecl *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
 "fname \<equiv> fst"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
 "declclassf \<equiv> snd"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
lemma declclass_simp[simp]: "declclass (C,m) = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
by (simp add: declclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
lemma decliface_simp[simp]: "decliface (I,m) = I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
by (simp add: decliface_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
lemma mbr_simp[simp]: "mbr (C,m) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
by (simp add: mbr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
by (cases m) (simp add:  mbr_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
lemma mthd_simp[simp]: "mthd (C,m) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
by (simp add: mthd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
lemma fld_simp[simp]: "fld (C,f) = f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
by (simp add: fld_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
lemma accmodi_simp[simp]: "accmodi (C,m) = access m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
by (simp )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
by (cases m) (simp add: mthd_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
by (cases f) (simp add:  fld_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
lemma is_static_simp[simp]: "is_static (C,m) = static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
by (simp add: is_static_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
by (cases m) (simp add:  mthd_def member_is_static_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
by (cases m) simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
lemma static_fld_simp[simp]: "static (fld f) = is_static f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
by (cases f) (simp add:  fld_def member_is_static_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
lemma ext_field_simp [simp]: "(declclass f,fld f) = f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
by (cases f) (simp add:  fld_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
lemma ext_method_simp [simp]: "(declclass m,mthd m) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
by (cases m) (simp add:  mthd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
by (cases m) (simp add: mbr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
lemma fname_simp[simp]:"fname (n,c) = n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
by (simp add: fname_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
lemma declclassf_simp[simp]:"declclassf (n,c) = c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
by (simp add: declclassf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
constdefs  (* some mnemotic selectors for (vname \<times> qtname) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
  "fldname \<equiv> fst"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
  "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
  "fldclass \<equiv> snd"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
lemma fldname_simp[simp]: "fldname (n,c) = n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
by (simp add: fldname_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
lemma fldclass_simp[simp]: "fldclass (n,c) = c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
by (simp add: fldclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
by (simp add: fldname_def fldclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
text {* Convert a qualified method declaration (qualified with its declaring 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
class) to a qualified member declaration:  @{text methdMembr}  *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
 "methdMembr m \<equiv> (fst m,mdecl (snd m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
by (simp add: methdMembr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
by (cases m) (simp add: methdMembr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
by (cases m) (simp add: methdMembr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
by (cases m) (simp add: methdMembr_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
text {* Convert a qualified method (qualified with its declaring 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
class) to a qualified member declaration:  @{text method}  *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
by (simp add: method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
by (simp add: method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
by (simp add: method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
by (cases m) (simp add: method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
by (simp add: mbr_def method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
  by (simp add: method_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
by (simp add: fieldm_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
by (simp add: fieldm_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
by (simp add: fieldm_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
by (cases f) (simp add: fieldm_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
by (simp add: mbr_def fieldm_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
lemma memberid_fieldm_simp[simp]:  "memberid (fieldm n f) = fid n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
by (simp add: fieldm_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
text {* Select the signature out of a qualified method declaration:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
 @{text msig} *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
"msig m \<equiv> fst (snd m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
lemma msig_simp[simp]: "msig (c,(s,m)) = s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
by (simp add: msig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
text {* Convert a qualified method (qualified with its declaring 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
class) to a qualified method declaration:  @{text qmdecl}  *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
by (simp add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
by (simp add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
by (simp add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
by (cases m) (simp add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
by (simp add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
lemma mdecl_qmdecl_simp[simp]:  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
 "mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
by (simp add: qmdecl_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
lemma methdMembr_qmdecl_simp [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
 "methdMembr (qmdecl sig old) = method sig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
by (simp add: methdMembr_def qmdecl_def method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
text {* overloaded selector @{text resTy} to select the result type 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
out of various HOL types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
axclass has_resTy < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
consts resTy:: "'a::has_resTy \<Rightarrow> ty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
12859
wenzelm
parents: 12854
diff changeset
   430
instance access_field_type :: ("type","has_resTy") has_resTy ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
decl_resTy_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
 "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
12859
wenzelm
parents: 12854
diff changeset
   436
instance static_field_type :: ("type","has_resTy") has_resTy ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
static_field_type_resTy_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
 "resTy (m::(bool,'b::has_resTy) static_field_type) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
  \<equiv> resTy (static_more m)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
12859
wenzelm
parents: 12854
diff changeset
   443
instance pars_field_type :: ("type","has_resTy") has_resTy ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
pars_field_type_resTy_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
 "resTy (m::(vname list,'b::has_resTy) pars_field_type) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
  \<equiv> resTy (pars_more m)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
12859
wenzelm
parents: 12854
diff changeset
   450
instance resT_field_type :: ("type","type") has_resTy ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
resT_field_type_resTy_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
 "resTy (m::(ty,'b::type) resT_field_type) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
  \<equiv> resT_val m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
apply (cases m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
apply (simp add: decl_resTy_def static_field_type_resTy_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
                 pars_field_type_resTy_def resT_field_type_resTy_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
                 member.dest_convs mhead.dest_convs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
by (simp add: mhead_def mhead_resTy_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
12859
wenzelm
parents: 12854
diff changeset
   467
instance * :: ("type","has_resTy") has_resTy ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
by (simp add: pair_resTy_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
by (cases m) (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
by (cases m) (simp add: mthd_def )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
subsubsection "inheritable-in"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
classes in package P if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
\begin{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
\item the declaration class of m is accessible in P and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
\item the member m is declared with protected or public access or if it is
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
      declared with default (package) access, the package of the declaration 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
      class of m is also P. If the member m is declared with private access
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
      it is not accessible for inheritance at all.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
inheritable_in:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
                  ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
"G\<turnstile>membr inheritable_in pack 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
  \<equiv> (case (accmodi membr) of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
       Private   \<Rightarrow> False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
     | Package   \<Rightarrow> (pid (declclass membr)) = pack
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
     | Protected \<Rightarrow> True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
     | Public    \<Rightarrow> True)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
Method_inheritable_in::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
                ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
Methd_inheritable_in::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
                ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
subsubsection "declared-in/undeclared-in"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
"cdeclaredmethd G C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
  \<equiv> (case class G C of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
       None \<Rightarrow> \<lambda> sig. None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
     | Some c \<Rightarrow> table_of (methods c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
    )"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
"cdeclaredfield G C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
  \<equiv> (case class G C of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
       None \<Rightarrow> \<lambda> sig. None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
     | Some c \<Rightarrow> table_of (cfields c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
    )"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
declared_in:: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
                                 ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
"G\<turnstile>m declared_in C \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
                        fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
                      | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
                                 ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
                               ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
lemma declared_in_classD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
 "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
by (cases m) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
   (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
undeclared_in:: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
                                 ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
"G\<turnstile>m undeclared_in C \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
                            fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
                          | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
lemma method_declared_inI:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
  "\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
   \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
by (auto simp add: declared_in_def cdeclaredmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
subsubsection "members"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
   the class qtname changes to the superclass in the inductive definition
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
   below
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
                           ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
 "G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
inductive "members G"  intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
             G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
            \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
text {* Note that in the case of an inherited member only the members of the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
direct superclass are concerned. If a member of a superclass of the direct
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
superclass isn't inherited in the direct superclass (not member of the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
direct superclass) than it can't be a member of the class. E.g. If a
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
member of a class A is defined with package access it isn't member of a 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
subclass S if S isn't in the same package as A. Any further subclasses 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
of S will not inherit the member, regardless if they are in the same
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
package as A or not.*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
                           ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
 "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
                           ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
 "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
                           ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
 "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
                           ("_ \<turnstile> _ inherits _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
"G\<turnstile>C inherits m 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
  \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
    (\<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)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
by (auto simp add: inherits_def intro: members.Inherited)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
                           ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
text {* A member is in a class if it is member of the class or a superclass.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
If a member is in a class we can select this member. This additional notion
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
is necessary since not all members are inherited to subclasses. So such
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
members are not member-of the subclass but member-in the subclass.*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
                           ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
 "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
                           ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
 "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
consts stat_overridesR::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
lemma member_inD: "G\<turnstile>m member_in C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
 \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
by (auto simp add: member_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
by (auto simp add: member_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
by (auto intro: member_inI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
subsubsection "overriding"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
text {* Unfortunately the static notion of overriding (used during the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
typecheck of the compiler) and the dynamic notion of overriding (used during
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
execution in the JVM) are not exactly the same. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
text {* Static overriding (used during the typecheck of the compiler) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
stat_overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
                                  ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
 "G\<turnstile>new overrides\<^sub>S  old" == "(new,old) \<in> stat_overridesR G "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
inductive "stat_overridesR G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
         G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
         G\<turnstile>Method new declared_in (declclass new);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
         G\<turnstile>Method old declared_in (declclass old); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
         G\<turnstile>Method old inheritable_in pid (declclass new);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
         G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
         G \<turnstile>Method old member_of superNew
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
           \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
text {* Dynamic overriding (used during the typecheck of the compiler) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
consts overridesR::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
  "prog  \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
overrides:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
                                  ("_ \<turnstile> _ overrides _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
 "G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
inductive "overridesR G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
         msig new = msig old; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
         G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
         G\<turnstile>Method new declared_in (declclass new);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
         G\<turnstile>Method old declared_in (declclass old);    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
         G\<turnstile>Method old inheritable_in pid (declclass new);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
         G\<turnstile>resTy new \<preceq> resTy old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
         \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
           \<Longrightarrow> G\<turnstile>new overrides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
sig_stat_overrides:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
 "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
                                  ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
 "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
                                  ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
 "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
subsubsection "Hiding"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
constdefs hides::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
                                ("_\<turnstile> _ hides _" [61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
"G\<turnstile>new hides old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
  \<equiv> is_static new \<and> msig new = msig old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
    G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
    G\<turnstile>Method new declared_in (declclass new) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
    G\<turnstile>Method old declared_in (declclass old) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
    G\<turnstile>Method old inheritable_in pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
                                  ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
 "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
lemma hidesI:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
"\<lbrakk>is_static new; msig new = msig old;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
  G\<turnstile>Method new declared_in (declclass new);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
  G\<turnstile>Method old declared_in (declclass old);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
  G\<turnstile>Method old inheritable_in pid (declclass new)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
 \<rbrakk> \<Longrightarrow> G\<turnstile>new hides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
by (auto simp add: hides_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
lemma hidesD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
  declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
  G\<turnstile>Method new declared_in (declclass new) \<and>   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
  G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
by (auto simp add: hides_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
lemma overrides_commonD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
  accmodi new \<noteq> Private \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
  msig new = msig old  \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
  G\<turnstile>Method new declared_in (declclass new) \<and>   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
  G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
by (induct set: overridesR) (auto intro: trancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
lemma ws_overrides_commonD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
"\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
  accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
  msig new = msig old  \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
  G\<turnstile>Method new declared_in (declclass new) \<and>   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
  G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
lemma stat_overrides_commonD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
  declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
  G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
  G\<turnstile>Method new declared_in (declclass new) \<and>   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
  G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
by (induct set: stat_overridesR) (auto intro: trancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
lemma overrides_eq_sigD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
 "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
by (auto dest: overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
lemma hides_eq_sigD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
 "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
by (auto simp add: hides_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
subsubsection "permits access" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
constdefs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
permits_acc:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
                   ("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
"G\<turnstile>membr in class permits_acc_to accclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
  \<equiv> (case (accmodi membr) of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
       Private   \<Rightarrow> (declclass membr = accclass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
     | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   821
     | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
                    \<or>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   823
                    (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   824
                     \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   825
     | Public    \<Rightarrow> True)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
The subcondition of the @{term "Protected"} case: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
same the other condition @{term "(pid (declclass membr) = pid accclass)"}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
holds anyway.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
*} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
text {* Like in case of overriding, the static and dynamic accessibility 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
of members is not uniform.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   836
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
\item Statically the class/interface of the member must be accessible for the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
      member to be accessible. During runtime this is not necessary. For
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
      Example, if a class is accessible and we are allowed to access a member
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
      of this class (statically) we expect that we can access this member in 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
      an arbitrary subclass (during runtime). It's not intended to restrict
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
      the access to accessible subclasses during runtime.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
\item Statically the member we want to access must be "member of" the class.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
      Dynamically it must only be "member in" the class.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
\end{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
*} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   850
accessible_fromR:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   851
 "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   852
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   855
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   856
                   ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   857
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   858
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
"G\<turnstile>membr of cls accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
 \<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
method_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
                   ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
"G\<turnstile>Method m of cls accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
 \<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
methd_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
                 ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
"G\<turnstile>Methd s m of cls accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
 \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
field_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
 "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
                 ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
"G\<turnstile>Field fn f of C accessible_from accclass"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
 \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
inductive "accessible_fromR G accclass" intros
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   890
Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
              G\<turnstile>(Class class) accessible_in (pid accclass);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
              G\<turnstile>membr in class permits_acc_to accclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
             \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   895
Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
              G\<turnstile>(Class class) accessible_in (pid accclass);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   897
              membr=(C,mdecl new);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   898
              G\<turnstile>(C,new) overrides\<^sub>S old; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   899
              G\<turnstile>class \<prec>\<^sub>C sup;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   900
              G\<turnstile>Method old of sup accessible_from accclass
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
             \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
dyn_accessible_fromR:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
 "prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times>  qtname) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
dyn_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
 "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
                   ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
"G\<turnstile>membr in C dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   914
 \<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
method_dyn_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
                 ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   920
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   921
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   922
"G\<turnstile>Method m in C dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
 \<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   925
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   926
methd_dyn_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   927
 "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   928
             ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
"G\<turnstile>Methd s m in C dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
 \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
syntax 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
field_dyn_accessible_from:: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
 "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
         ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
 \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   942
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   943
inductive "dyn_accessible_fromR G accclass" intros
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   944
Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   945
              G\<turnstile>membr in class permits_acc_to accclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
             \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   948
Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   949
              membr=(C,mdecl new);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
              G\<turnstile>(C,new) overrides old; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
              G\<turnstile>class \<prec>\<^sub>C sup;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
              G\<turnstile>Method old in sup dyn_accessible_from accclass
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
             \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
 \<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
by (auto elim: accessible_fromR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   959
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   960
lemma unique_declaration: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   961
 "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   962
  \<Longrightarrow> m = n"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   963
apply (cases m)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   964
apply (cases n,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   965
        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   966
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   967
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
lemma declared_not_undeclared:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
  "G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   972
lemma undeclared_not_declared:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   973
 "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   974
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   975
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
lemma not_undeclared_declared:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
  "\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
                                           membr_id = memberid m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
  assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
  show ?thesis (is "?P membr_id")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
  proof (cases membr_id)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
    case (fid vname)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
    with not_undecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
    obtain fld where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
      "G\<turnstile>fdecl (vname,fld) declared_in C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
      by (auto simp add: undeclared_in_def declared_in_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
                         cdeclaredfield_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
    with fid show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
    case (mid sig)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
    with not_undecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
    obtain mthd where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
      "G\<turnstile>mdecl (sig,mthd) declared_in C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
      by (auto simp add: undeclared_in_def declared_in_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
                         cdeclaredmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
    with mid show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   999
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
lemma unique_declared_in:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1004
 "\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
 \<Longrightarrow> m = n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
            split: memberdecl.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
lemma unique_member_of: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1010
  assumes n: "G\<turnstile>n member_of C" and  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
          m: "G\<turnstile>m member_of C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1012
       eqid: "memberid n = memberid m"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1013
  shows "n=m"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1014
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1015
  from n m eqid  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
  show "n=m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1017
  proof (induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
    case (Immediate C n)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1019
    assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
    assume eqid: "memberid n = memberid m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1021
    assume "G \<turnstile> m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1022
    then show "n=m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1023
    proof (cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1024
      case (Immediate _ m')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1025
      with eqid 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1026
      have "m=m'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
           "memberid n = memberid m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1028
           "G\<turnstile> mbr m declared_in C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
           "declclass m = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1030
	by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1031
      with member_n   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1032
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1033
	by (cases n, cases m) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1034
           (auto simp add: declared_in_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1035
                           cdeclaredmethd_def cdeclaredfield_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1036
                    split: memberdecl.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1037
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1038
      case (Inherited _ _ m')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1039
      then have "G\<turnstile> memberid m undeclared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1040
	by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1041
      with eqid member_n
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1042
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
	by (cases n) (auto dest: declared_not_undeclared)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
    case (Inherited C S n)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
    assume undecl: "G\<turnstile> memberid n undeclared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1048
    assume  super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
    assume    hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1050
    assume   eqid: "memberid n = memberid m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
    assume "G \<turnstile> m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1052
    then show "n=m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1053
    proof (cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
      case Immediate
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1055
      then have "G\<turnstile> mbr m declared_in C" by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1056
      with eqid undecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1057
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1058
	by (cases m) (auto dest: declared_not_undeclared)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1059
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1060
      case Inherited 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1061
      with super have "G \<turnstile> m member_of S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1062
	by (auto dest!: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
      with eqid hyp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
      show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1065
	by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
proof (induct set: members)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
  case (Immediate C m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1073
  assume "G\<turnstile> mbr m declared_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1074
  then show "is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1075
    by (cases "mbr m")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1076
       (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1077
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
  case (Inherited C S m)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
  assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
  then show "is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
    by - (rule subcls_is_class2,auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
lemma member_of_declC: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
 "G\<turnstile>m member_of C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
  \<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
by (induct set: members) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
lemma member_of_member_of_declC:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
 "G\<turnstile>m member_of C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
  \<Longrightarrow> G\<turnstile>m member_of (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
by (auto dest: member_of_declC intro: members.Immediate)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
lemma member_of_class_relation:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
  "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1096
proof (induct set: members)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1097
  case (Immediate C m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1098
  then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1100
  case (Inherited C S m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
  then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1102
    by (auto dest: r_into_rtrancl intro: rtrancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1105
lemma member_in_class_relation:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1106
  "G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
by (auto dest: member_inD member_of_class_relation
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
        intro: rtrancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
lemma member_of_Package: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1111
 "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
  \<Longrightarrow> pid (declclass m) = pid C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1113
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
  assume   member: "G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
  then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
  proof (induct rule: members.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1117
    fix C m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1118
    assume     C: "declclass m = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1119
    then show "pid (declclass m) = pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1120
      by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1121
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1122
    fix C S m  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1123
    assume inheritable: "G \<turnstile> m inheritable_in pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1124
    assume         hyp: "PROP ?P m S" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1125
           package_acc: "accmodi m = Package" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1126
    with inheritable package_acc hyp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1127
    show "pid (declclass m) = pid C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1128
      by (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1130
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1132
lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1133
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1134
  assume member_in_C:  "G\<turnstile>m member_in C"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1135
  from member_in_C
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1136
  obtain provC where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1137
    subclseq_C_provC: "G\<turnstile> C \<preceq>\<^sub>C provC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1138
     member_of_provC: "G \<turnstile> m member_of provC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1139
    by (auto simp add: member_in_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1140
  from member_of_provC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1141
  have "G \<turnstile> m member_of declclass m"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1142
    by (rule member_of_member_of_declC)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1143
  moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1144
  from member_in_C
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1145
  have "G\<turnstile>C \<preceq>\<^sub>C declclass m"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1146
    by (rule member_in_class_relation)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1147
  ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1148
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1149
    by (auto simp add: member_in_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1150
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1151
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1152
lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
 \<Longrightarrow> G\<turnstile>m member_in C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
by (auto elim: dyn_accessible_fromR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1155
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
lemma no_Private_stat_override: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1157
 "\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
by (induct set:  stat_overridesR) (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
by (induct set: overridesR) (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1163
lemma permits_acc_inheritance:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1164
 "\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1165
  \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
by (cases "accmodi m")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1167
   (auto simp add: permits_acc_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1168
            intro: subclseq_trans) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1169
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1170
lemma permits_acc_static_declC:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1171
 "\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1172
  \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1173
by (cases "accmodi m") (auto simp add: permits_acc_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1174
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1175
lemma dyn_accessible_from_static_declC: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1176
  assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1177
           static: "is_static m"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1178
  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1179
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1180
  from acc_C static
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1181
  show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1182
  proof (induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1183
    case (Immediate C m)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1184
    then show ?case 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1185
      by (auto intro!: dyn_accessible_fromR.Immediate
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1186
                 dest: member_in_declC permits_acc_static_declC) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1187
  next 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1188
    case (Overriding declCNew C m new old sup)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1189
    then have "\<not> is_static m"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1190
      by (auto dest: overrides_commonD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1191
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1192
    assume "is_static m"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1193
    ultimately show ?case 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1194
      by contradiction
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1195
  qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1196
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1197
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1198
lemma field_accessible_fromD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1199
 "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1200
  \<Longrightarrow> G\<turnstile>membr member_of C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1201
      G\<turnstile>(Class C) accessible_in (pid accC) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1202
      G\<turnstile>membr in C permits_acc_to accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1203
by (cases set: accessible_fromR)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1204
   (auto simp add: is_field_def split: memberdecl.splits) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1205
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1206
lemma field_accessible_from_permits_acc_inheritance:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1207
"\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1208
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1209
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1210
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1212
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1213
lemma accessible_Package:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1214
 "\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1215
   \<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1216
  \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1217
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1218
  assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1219
  assume "G \<turnstile> m of C accessible_from S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1220
  then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1221
    (is "?Pack m \<Longrightarrow> ?P C m")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1222
  proof (induct rule: accessible_fromR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1223
    fix C m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1224
    assume "G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1225
           "G \<turnstile> m in C permits_acc_to S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1226
           "accmodi m = Package"      
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1227
    then show "?P C m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1228
      by (auto dest: member_of_Package simp add: permits_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1229
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1230
    fix declC C new newm old Sup
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1231
    assume member_new: "G \<turnstile> new member_of C" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1232
                acc_C: "G \<turnstile> Class C accessible_in pid S" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1233
                  new: "new = (declC, mdecl newm)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1234
             override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1235
         subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1236
              acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1237
                  hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1238
          accmodi_new: "accmodi new = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1239
    from override wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1240
    have accmodi_weaken: "accmodi old \<le> accmodi newm"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1241
      by (cases old,cases newm) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1242
    from override new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1243
    have "accmodi old \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1244
      by (simp add: no_Private_stat_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1245
    with accmodi_weaken accmodi_new new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1246
    have accmodi_old: "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1247
      by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1248
    with hyp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1249
    have P_sup: "?P Sup (methdMembr old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1250
      by (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1251
    from wf override new accmodi_old accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1252
    have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1253
      by (auto dest: stat_override_Package) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1254
    from member_new accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1255
    have "pid (declclass new) = pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1256
      by (auto dest: member_of_Package)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1257
    with eq_pid_new_old P_sup show "?P C new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1258
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1259
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1260
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1261
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1262
lemma accessible_fieldD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1263
 "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1264
 \<Longrightarrow> G\<turnstile>membr member_of C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1265
     G\<turnstile>(Class C) accessible_in (pid accC) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1266
     G\<turnstile>membr in C permits_acc_to accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1267
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1268
      
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1269
(* lemmata:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1270
 Wegen  G\<turnstile>Super accessible_in (pid C) folgt:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1271
  G\<turnstile>m declared_in C; G\<turnstile>m member_of D; accmodi m = Package (G\<turnstile>D \<preceq>\<^sub>C C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1272
  \<Longrightarrow> pid C = pid D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1273
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1274
  C package
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1275
  m public in C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1276
  für alle anderen D: G\<turnstile>m undeclared_in C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1277
  m wird in alle subklassen vererbt, auch aus dem Package heraus!
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1278
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1279
  G\<turnstile>m member_of C \<Longrightarrow> \<exists> D. G\<turnstile>C \<preceq>\<^sub>C D \<and> G\<turnstile>m declared_in D
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1280
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1281
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1282
(* Begriff (C,m) overrides (D,m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1283
    3 Fälle: Direkt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1284
             Indirekt über eine Zwischenklasse (ohne weiteres override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1285
             Indirekt über override
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1286
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1287
   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1288
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1289
"G\<turnstile>m member_of C \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1290
constdefs declares_method:: "prog \<Rightarrow> sig \<Rightarrow> qtname \<Rightarrow> methd \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1291
                                 ("_,_\<turnstile> _ declares'_method _" [61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1292
"G,sig\<turnstile>C declares_method m \<equiv> cdeclaredmethd G C sig = Some m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1293
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1294
constdefs is_declared:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1295
"is_declared G sig em \<equiv> G,sig\<turnstile>declclass em declares_method mthd em"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1296
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1298
lemma member_of_Private:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1299
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1300
by (induct set: members) (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1301
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1302
lemma member_of_subclseq_declC:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1303
  "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1304
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1305
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1306
lemma member_of_inheritance:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1307
  assumes       m: "G\<turnstile>m member_of D" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1308
     subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1309
     subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1310
               ws: "ws_prog G" 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1311
  shows "G\<turnstile>m member_of C"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1312
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1313
  from m subclseq_D_C subclseq_C_m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1314
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1315
  proof (induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1316
    case (Immediate D m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1317
    assume "declclass m = D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1318
           "G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1319
    with ws have "D=C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1320
      by (auto intro: subclseq_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1321
    with Immediate 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1322
    show "G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1323
      by (auto intro: members.Immediate)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1324
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1325
    case (Inherited D S m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1326
    assume member_of_D_props: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1327
            "G \<turnstile> m inheritable_in pid D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1328
            "G\<turnstile> memberid m undeclared_in D"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1329
            "G \<turnstile> Class S accessible_in pid D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1330
            "G \<turnstile> m member_of S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1331
    assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1332
    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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1333
    assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1334
    assume "G\<turnstile>D\<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1335
    then show "G\<turnstile>m member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1336
    proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1337
      case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1338
      assume "D=C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1339
      with super member_of_D_props 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1340
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1341
	by (auto intro: members.Inherited)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1342
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1343
      case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1344
      assume "G\<turnstile>D\<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1345
      with super 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1346
      have "G\<turnstile>S\<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1347
	by (auto dest: subcls1D subcls_superD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1348
      with subclseq_C_m hyp show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1349
	by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1350
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1351
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1352
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1353
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1354
lemma member_of_subcls:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1355
  assumes     old: "G\<turnstile>old member_of C" and 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1356
              new: "G\<turnstile>new member_of D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1357
             eqid: "memberid new = memberid old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1358
     subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1359
   subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1360
               ws: "ws_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1361
  shows "G\<turnstile>D \<prec>\<^sub>C C"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1362
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1363
  from old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1364
  have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1365
    by (auto dest: member_of_subclseq_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1366
  from new 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1367
  have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1368
    by (auto dest: member_of_subclseq_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1369
  from subcls_new_old ws
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1370
  have neq_new_old: "new\<noteq>old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1371
    by (cases new,cases old) (auto dest: subcls_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1372
  from subclseq_D_new subclseq_D_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1373
  have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1374
    by (rule subcls_compareable)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1375
  then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1376
  proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1377
    assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis .
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1378
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1379
    assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1380
    with new subclseq_D_C ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1381
    have "G\<turnstile>new member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1382
      by (blast intro: member_of_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1383
    with eqid old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1384
    have "new=old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1385
      by (blast intro: unique_member_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1386
    with neq_new_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1387
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1388
      by contradiction
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1389
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1390
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1391
  proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1392
    case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1393
    assume "declclass new = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1394
    with new have "G\<turnstile>new member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1395
      by (auto dest: member_of_member_of_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1396
    with eqid old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1397
    have "new=old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1398
      by (blast intro: unique_member_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1399
    with neq_new_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1400
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1401
      by contradiction
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1402
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1403
    case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1404
    assume "G\<turnstile>declclass new\<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1405
    with subclseq_D_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1406
    show "G\<turnstile>D\<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1407
      by (rule rtrancl_trancl_trancl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1408
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1409
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1410
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1411
corollary member_of_overrides_subcls:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1412
 "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1413
   G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1414
 \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1415
by (drule overrides_commonD) (auto intro: member_of_subcls)    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1416
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1417
corollary member_of_stat_overrides_subcls:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1418
 "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1419
   G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1420
 \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1421
by (drule stat_overrides_commonD) (auto intro: member_of_subcls)    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1422
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1423
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1424
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1425
lemma inherited_field_access: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1426
  assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1427
          is_field: "is_field membr" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1428
          subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1429
  shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1430
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1431
  from stat_acc is_field subclseq 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1432
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1433
    by (auto dest: accessible_fieldD 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1434
            intro: dyn_accessible_fromR.Immediate 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1435
                   member_inI 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1436
                   permits_acc_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1437
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1438
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1439
lemma accessible_inheritance:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1440
  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1441
          subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1442
       member_dynC: "G\<turnstile>m member_of dynC" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1443
          dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1444
  shows "G\<turnstile>m of dynC accessible_from accC"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1445
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1446
  from stat_acc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1447
  have member_statC: "G\<turnstile>m member_of statC" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1448
    by (auto dest: accessible_from_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1449
  from stat_acc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1450
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1451
  proof (cases)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1452
    case Immediate
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1453
    with member_dynC member_statC subclseq dynC_acc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1454
    show ?thesis
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1455
      by (auto intro: accessible_fromR.Immediate permits_acc_inheritance)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1456
  next
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1457
    case Overriding
12854