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