author  wenzelm 
Wed, 03 Mar 2010 00:33:02 +0100  
changeset 35431  8758fe1fc9f8 
parent 35416  d8d7d1b785af 
child 35547  991a6af75978 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Decl.thy 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

2 
Author: David von Oheimb and Norbert Schirmer 
12854  3 
*) 
4 
header {* Field, method, interface, and class declarations, whole Java programs 

5 
*} 

6 

26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

7 
theory Decl 
27682  8 
imports Term Table (** order is significant, because of clash for "var" **) 
26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

9 
begin 
12854  10 

11 
text {* 

12 
improvements: 

13 
\begin{itemize} 

14 
\item clarification and correction of some aspects of the package/access concept 

15 
(Also submitted as bug report to the Java Bug Database: 

16 
Bug Id: 4485402 and Bug Id: 4493343 

17 
http://developer.java.sun.com/developer/bugParade/index.jshtml 

18 
) 

19 
\end{itemize} 

20 
simplifications: 

21 
\begin{itemize} 

22 
\item the only field and method modifiers are static and the access modifiers 

23 
\item no constructors, which may be simulated by new + suitable methods 

24 
\item there is just one global initializer per class, which can simulate all 

25 
others 

26 

27 
\item no throws clause 

28 
\item a void method is replaced by one that returns Unit (of dummy type Void) 

29 

30 
\item no interface fields 

31 

32 
\item every class has an explicit superclass (unused for Object) 

33 
\item the (standard) methods of Object and of standard exceptions are not 

34 
specified 

35 

36 
\item no main method 

37 
\end{itemize} 

38 
*} 

39 

40 
subsection {* Modifier*} 

41 

42 
subsubsection {* Access modifier *} 

43 

44 
datatype acc_modi (* access modifier *) 

45 
= Private  Package  Protected  Public 

46 

47 
text {* 

48 
We can define a linear order for the access modifiers. With Private yielding the 

49 
most restrictive access and public the most liberal access policy: 

50 
Private < Package < Protected < Public 

51 
*} 

52 

26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

53 
instantiation acc_modi :: linorder 
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

54 
begin 
12854  55 

26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

56 
definition 
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

57 
less_acc_def: "a < b 
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

58 
\<longleftrightarrow> (case a of 
12854  59 
Private \<Rightarrow> (b=Package \<or> b=Protected \<or> b=Public) 
60 
 Package \<Rightarrow> (b=Protected \<or> b=Public) 

61 
 Protected \<Rightarrow> (b=Public) 

62 
 Public \<Rightarrow> False)" 

63 

26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

64 
definition 
27682  65 
le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b" 
26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

66 

36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

67 
instance proof 
12854  68 
fix x y z::acc_modi 
27682  69 
show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" 
70 
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 

12854  71 
{ 
72 
show "x \<le> x" \<spacespace>\<spacespace>  reflexivity 

73 
by (auto simp add: le_acc_def) 

74 
next 

75 
assume "x \<le> y" "y \<le> z"  transitivity 

76 
thus "x \<le> z" 

77 
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 

78 
next 

79 
assume "x \<le> y" "y \<le> x"  antisymmetry 

80 
thus "x = y" 

81 
proof  

82 
have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False" 

83 
by (auto simp add: less_acc_def split add: acc_modi.split) 

84 
with prems show ?thesis 

17589  85 
by (unfold le_acc_def) iprover 
12854  86 
qed 
87 
next 

88 
fix x y:: acc_modi 

89 
show "x \<le> y \<or> y \<le> x" 

90 
by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split) 

27682  91 
} 
12854  92 
qed 
26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

93 

36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

94 
end 
12854  95 

96 
lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public" 

97 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

98 

99 
lemma acc_modi_top1 [simp, intro!]: "a \<le> Public" 

100 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

101 

102 
lemma acc_modi_le_Public: 

103 
"a \<le> Public \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public" 

104 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

105 

106 
lemma acc_modi_bottom: "a \<le> Private \<Longrightarrow> a = Private" 

107 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

108 

109 
lemma acc_modi_Private_le: 

110 
"Private \<le> a \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public" 

111 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

112 

113 
lemma acc_modi_Package_le: 

114 
"Package \<le> a \<Longrightarrow> a = Package \<or> a=Protected \<or> a=Public" 

115 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 

116 

117 
lemma acc_modi_le_Package: 

118 
"a \<le> Package \<Longrightarrow> a=Private \<or> a = Package" 

119 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

120 

121 
lemma acc_modi_Protected_le: 

122 
"Protected \<le> a \<Longrightarrow> a=Protected \<or> a=Public" 

123 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

124 

125 
lemma acc_modi_le_Protected: 

126 
"a \<le> Protected \<Longrightarrow> a=Private \<or> a = Package \<or> a = Protected" 

127 
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits) 

128 

129 

130 
lemmas acc_modi_le_Dests = acc_modi_top acc_modi_le_Public 

131 
acc_modi_Private_le acc_modi_bottom 

132 
acc_modi_Package_le acc_modi_le_Package 

133 
acc_modi_Protected_le acc_modi_le_Protected 

134 

135 
lemma acc_modi_Package_le_cases 

136 
[consumes 1,case_names Package Protected Public]: 

137 
"Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow> 

138 
(m=Public \<Longrightarrow> P m) \<Longrightarrow> P m" 

139 
by (auto dest: acc_modi_Package_le) 

140 

141 

142 
subsubsection {* Static Modifier *} 

143 
types stat_modi = bool (* modifier: static *) 

144 

145 
subsection {* Declaration (base "class" for member,interface and class 

146 
declarations *} 

147 

148 
record decl = 

149 
access :: acc_modi 

150 

151 
translations 

35431  152 
(type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>" 
153 
(type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>" 

12854  154 

155 
subsection {* Member (field or method)*} 

156 
record member = decl + 

157 
static :: stat_modi 

158 

159 
translations 

35431  160 
(type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>" 
161 
(type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>" 

12854  162 

163 
subsection {* Field *} 

164 

165 
record field = member + 

166 
type :: ty 

167 
translations 

35431  168 
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>" 
169 
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>" 

12854  170 

171 
types 

172 
fdecl (* field declaration, cf. 8.3 *) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

173 
= "vname \<times> field" 
12854  174 

175 

176 
translations 

35431  177 
(type) "fdecl" <= (type) "vname \<times> field" 
12854  178 

179 
subsection {* Method *} 

180 

181 
record mhead = member + (* method head (excluding signature) *) 

182 
pars ::"vname list" (* parameter names *) 

183 
resT ::ty (* result type *) 

184 

185 
record mbody = (* method body *) 

186 
lcls:: "(vname \<times> ty) list" (* local variables *) 

187 
stmt:: stmt (* the body statement *) 

188 

189 
record methd = mhead + (* method in a class *) 

190 
mbody::mbody 

191 

192 
types mdecl = "sig \<times> methd" (* method declaration in a class *) 

193 

194 

195 
translations 

35431  196 
(type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854  197 
pars::vname list, resT::ty\<rparr>" 
35431  198 
(type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854  199 
pars::vname list, resT::ty,\<dots>::'a\<rparr>" 
35431  200 
(type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>" 
201 
(type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>" 

202 
(type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 

12854  203 
pars::vname list, resT::ty,mbody::mbody\<rparr>" 
35431  204 
(type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854  205 
pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>" 
35431  206 
(type) "mdecl" <= (type) "sig \<times> methd" 
12854  207 

208 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

209 
definition mhead :: "methd \<Rightarrow> mhead" where 
12854  210 
"mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>" 
211 

212 
lemma access_mhead [simp]:"access (mhead m) = access m" 

213 
by (simp add: mhead_def) 

214 

215 
lemma static_mhead [simp]:"static (mhead m) = static m" 

216 
by (simp add: mhead_def) 

217 

218 
lemma pars_mhead [simp]:"pars (mhead m) = pars m" 

219 
by (simp add: mhead_def) 

220 

221 
lemma resT_mhead [simp]:"resT (mhead m) = resT m" 

222 
by (simp add: mhead_def) 

223 

224 
text {* To be able to talk uniformaly about field and method declarations we 

225 
introduce the notion of a member declaration (e.g. useful to define 

226 
accessiblity ) *} 

227 

228 
datatype memberdecl = fdecl fdecl  mdecl mdecl 

229 

230 
datatype memberid = fid vname  mid sig 

231 

35315  232 
class has_memberid = 
233 
fixes memberid :: "'a \<Rightarrow> memberid" 

12854  234 

35315  235 
instantiation memberdecl :: has_memberid 
236 
begin 

12854  237 

35315  238 
definition 
12854  239 
memberdecl_memberid_def: 
240 
"memberid m \<equiv> (case m of 

241 
fdecl (vn,f) \<Rightarrow> fid vn 

242 
 mdecl (sig,m) \<Rightarrow> mid sig)" 

243 

35315  244 
instance .. 
245 

246 
end 

247 

12854  248 
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn" 
249 
by (simp add: memberdecl_memberid_def) 

250 

251 
lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)" 

252 
by (cases f) (simp add: memberdecl_memberid_def) 

253 

254 
lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig" 

255 
by (simp add: memberdecl_memberid_def) 

256 

257 
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)" 

258 
by (cases m) (simp add: memberdecl_memberid_def) 

259 

35315  260 
instantiation * :: (type, has_memberid) has_memberid 
261 
begin 

12854  262 

35315  263 
definition 
12854  264 
pair_memberid_def: 
265 
"memberid p \<equiv> memberid (snd p)" 

266 

35315  267 
instance .. 
268 

269 
end 

270 

12854  271 
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m" 
272 
by (simp add: pair_memberid_def) 

273 

274 
lemma memberid_pair_simp1: "memberid p = memberid (snd p)" 

275 
by (simp add: pair_memberid_def) 

276 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

277 
definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where 
12854  278 
"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)" 
279 

280 
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)" 

281 
by (simp add: is_field_def) 

282 

283 
lemma is_fieldI: "is_field (C,fdecl f)" 

284 
by (simp add: is_field_def) 

285 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

286 
definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where 
12854  287 
"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)" 
288 

289 
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)" 

290 
by (simp add: is_method_def) 

291 

292 
lemma is_methodI: "is_method (C,mdecl m)" 

293 
by (simp add: is_method_def) 

294 

295 

296 
subsection {* Interface *} 

297 

298 

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:
13601
diff
changeset

299 
record ibody = decl + {* interface body *} 
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:
13601
diff
changeset

300 
imethods :: "(sig \<times> mhead) list" {* method heads *} 
12854  301 

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:
13601
diff
changeset

302 
record iface = ibody + {* interface *} 
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:
13601
diff
changeset

303 
isuperIfs:: "qtname list" {* superinterface list *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

304 
types 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

305 
idecl {* interface declaration, cf. 9.1 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

306 
= "qtname \<times> iface" 
12854  307 

308 
translations 

35431  309 
(type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>" 
310 
(type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>" 

311 
(type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list, 

12854  312 
isuperIfs::qtname list\<rparr>" 
35431  313 
(type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list, 
12854  314 
isuperIfs::qtname list,\<dots>::'a\<rparr>" 
35431  315 
(type) "idecl" <= (type) "qtname \<times> iface" 
12854  316 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

317 
definition ibody :: "iface \<Rightarrow> ibody" where 
12854  318 
"ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>" 
319 

320 
lemma access_ibody [simp]: "(access (ibody i)) = access i" 

321 
by (simp add: ibody_def) 

322 

323 
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i" 

324 
by (simp add: ibody_def) 

325 

326 
subsection {* Class *} 

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:
13601
diff
changeset

327 
record cbody = decl + {* class body *} 
12854  328 
cfields:: "fdecl list" 
329 
methods:: "mdecl list" 

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:
13601
diff
changeset

330 
init :: "stmt" {* initializer *} 
12854  331 

18551  332 
record "class" = cbody + {* class *} 
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:
13601
diff
changeset

333 
super :: "qtname" {* superclass *} 
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:
13601
diff
changeset

334 
superIfs:: "qtname list" {* implemented interfaces *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

335 
types 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

336 
cdecl {* class declaration, cf. 8.1 *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

337 
= "qtname \<times> class" 
12854  338 

339 
translations 

35431  340 
(type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list, 
12854  341 
methods::mdecl list,init::stmt\<rparr>" 
35431  342 
(type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list, 
12854  343 
methods::mdecl list,init::stmt,\<dots>::'a\<rparr>" 
35431  344 
(type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list, 
12854  345 
methods::mdecl list,init::stmt, 
346 
super::qtname,superIfs::qtname list\<rparr>" 

35431  347 
(type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list, 
12854  348 
methods::mdecl list,init::stmt, 
349 
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>" 

35431  350 
(type) "cdecl" <= (type) "qtname \<times> class" 
12854  351 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

352 
definition cbody :: "class \<Rightarrow> cbody" where 
12854  353 
"cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>" 
354 

355 
lemma access_cbody [simp]:"access (cbody c) = access c" 

356 
by (simp add: cbody_def) 

357 

358 
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c" 

359 
by (simp add: cbody_def) 

360 

361 
lemma methods_cbody [simp]:"methods (cbody c) = methods c" 

362 
by (simp add: cbody_def) 

363 

364 
lemma init_cbody [simp]:"init (cbody c) = init c" 

365 
by (simp add: cbody_def) 

366 

367 

368 
section "standard classes" 

369 

370 
consts 

371 

14674  372 
Object_mdecls :: "mdecl list" {* methods of Object *} 
373 
SXcpt_mdecls :: "mdecl list" {* methods of SXcpts *} 

374 
ObjectC :: "cdecl" {* declaration of root class *} 

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:
13601
diff
changeset

375 
SXcptC ::"xname \<Rightarrow> cdecl" {* declarations of throwable classes *} 
12854  376 

377 
defs 

378 

379 

380 
ObjectC_def:"ObjectC \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls, 

28524  381 
init=Skip,super=undefined,superIfs=[]\<rparr>)" 
12854  382 
SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 
383 
init=Skip, 

384 
super=if xn = Throwable then Object 

385 
else SXcpt Throwable, 

386 
superIfs=[]\<rparr>)" 

387 

388 
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn" 

389 
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def) 

390 

391 
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)" 

17778  392 
by (simp add: SXcptC_def) 
12854  393 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

394 
definition standard_classes :: "cdecl list" where 
12854  395 
"standard_classes \<equiv> [ObjectC, SXcptC Throwable, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

396 
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

397 
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]" 
12854  398 

399 

400 
section "programs" 

401 

402 
record prog = 

403 
ifaces ::"idecl list" 

404 
"classes"::"cdecl list" 

405 

406 
translations 

35431  407 
(type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>" 
408 
(type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>" 

12854  409 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

410 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

411 
iface :: "prog \<Rightarrow> (qtname, iface) table" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

412 
where "iface G I == table_of (ifaces G) I" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

413 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

414 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

415 
"class" :: "prog \<Rightarrow> (qtname, class) table" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

416 
where "class G C == table_of (classes G) C" 
12854  417 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

418 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

419 
is_iface :: "prog \<Rightarrow> qtname \<Rightarrow> bool" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

420 
where "is_iface G I == iface G I \<noteq> None" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

421 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

422 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

423 
is_class :: "prog \<Rightarrow> qtname \<Rightarrow> bool" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

424 
where "is_class G C == class G C \<noteq> None" 
12854  425 

426 

427 
section "is type" 

428 

429 
consts 

430 
is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool" 

431 
isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool" 

432 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

433 
primrec "is_type G (PrimT pt) = True" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

434 
"is_type G (RefT rt) = isrtype G rt" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

435 
"isrtype G (NullT ) = True" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

436 
"isrtype G (IfaceT tn) = is_iface G tn" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

437 
"isrtype G (ClassT tn) = is_class G tn" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

438 
"isrtype G (ArrayT T ) = is_type G T" 
12854  439 

440 
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I" 

441 
by auto 

442 

443 
lemma type_is_class: "is_type G (Class C) \<Longrightarrow> is_class G C" 

444 
by auto 

445 

446 

447 
section "subinterface and subclass relation, in anticipation of TypeRel.thy" 

448 

449 
consts 

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:
13601
diff
changeset

450 
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct subinterface *} 
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:
13601
diff
changeset

451 
subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct subclass *} 
12854  452 

453 
defs 

454 
subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}" 

455 
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}" 

456 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

457 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

458 
subcls1_syntax :: "prog => [qtname, qtname] => bool" ("__<:C1_" [71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

459 
where "GC <:C1 D == (C,D) \<in> subcls1 G" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

460 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

461 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

462 
subclseq_syntax :: "prog => [qtname, qtname] => bool" ("__<=:C _"[71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

463 
where "GC <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *) 
12854  464 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

465 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

466 
subcls_syntax :: "prog => [qtname, qtname] => bool" ("__<:C _"[71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

467 
where "GC <:C D == (C,D) \<in>(subcls1 G)^+" 
12854  468 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

469 
notation (xsymbols) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

470 
subcls1_syntax ("_\<turnstile>_\<prec>\<^sub>C1_" [71,71,71] 70) and 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

471 
subclseq_syntax ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

472 
subcls_syntax ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70) 
12854  473 

474 
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 

475 
\<Longrightarrow> (I,J) \<in> subint1 G" 

476 
apply (simp add: subint1_def) 

477 
done 

478 

479 
lemma subcls1I:"\<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,(super c)) \<in> subcls1 G" 

480 
apply (simp add: subcls1_def) 

481 
done 

482 

483 

484 
lemma subint1D: "(I,J)\<in>subint1 G\<Longrightarrow> \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)" 

485 
by (simp add: subint1_def) 

486 

487 
lemma subcls1D: 

488 
"(C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c. class G C = Some c \<and> (super c = D))" 

489 
apply (simp add: subcls1_def) 

490 
apply auto 

491 
done 

492 

493 
lemma subint1_def2: 

14952
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14674
diff
changeset

494 
"subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))" 
12854  495 
apply (unfold subint1_def) 
496 
apply auto 

497 
done 

498 

499 
lemma subcls1_def2: 

14952
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14674
diff
changeset

500 
"subcls1 G = 
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14674
diff
changeset

501 
(SIGMA C: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})" 
12854  502 
apply (unfold subcls1_def) 
503 
apply auto 

504 
done 

505 

506 
lemma subcls_is_class: 

507 
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D\<rbrakk> \<Longrightarrow> \<exists> c. class G C = Some c" 

508 
by (auto simp add: subcls1_def dest: tranclD) 

509 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

510 
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C1 D \<Longrightarrow> P" 
12854  511 
by (auto simp add: subcls1_def) 
512 

513 
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P" 

514 
apply (erule trancl_induct) 

515 
apply (auto intro: no_subcls1_Object) 

516 
done 

517 

518 
section "wellstructured programs" 

519 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

520 
definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where 
12854  521 
"ws_idecl G I si \<equiv> \<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+" 
522 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

523 
definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where 
12854  524 
"ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+" 
525 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

526 
definition ws_prog :: "prog \<Rightarrow> bool" where 
12854  527 
"ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces G). ws_idecl G I (isuperIfs i)) \<and> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

528 
(\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))" 
12854  529 

530 

531 
lemma ws_progI: 

532 
"\<lbrakk>\<forall>(I,i)\<in>set (ifaces G). \<forall>J\<in>set (isuperIfs i). is_iface G J \<and> 

533 
(J,I) \<notin> (subint1 G)^+; 

534 
\<forall>(C,c)\<in>set (classes G). C\<noteq>Object \<longrightarrow> is_class G (super c) \<and> 

535 
((super c),C) \<notin> (subcls1 G)^+ 

536 
\<rbrakk> \<Longrightarrow> ws_prog G" 

537 
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def) 

538 
apply (erule_tac conjI) 

539 
apply blast 

540 
done 

541 

542 
lemma ws_prog_ideclD: 

543 
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow> 

544 
is_iface G J \<and> (J,I)\<notin>(subint1 G)^+" 

545 
apply (unfold ws_prog_def ws_idecl_def) 

546 
apply clarify 

547 
apply (drule_tac map_of_SomeD) 

548 
apply auto 

549 
done 

550 

551 
lemma ws_prog_cdeclD: 

552 
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow> 

553 
is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+" 

554 
apply (unfold ws_prog_def ws_cdecl_def) 

555 
apply clarify 

556 
apply (drule_tac map_of_SomeD) 

557 
apply auto 

558 
done 

559 

560 

561 
section "wellfoundedness" 

562 

563 
lemma finite_is_iface: "finite {I. is_iface G I}" 

564 
apply (fold dom_def) 

565 
apply (rule_tac finite_dom_map_of) 

566 
done 

567 

568 
lemma finite_is_class: "finite {C. is_class G C}" 

569 
apply (fold dom_def) 

570 
apply (rule_tac finite_dom_map_of) 

571 
done 

572 

573 
lemma finite_subint1: "finite (subint1 G)" 

574 
apply (subst subint1_def2) 

575 
apply (rule finite_SigmaI) 

576 
apply (rule finite_is_iface) 

577 
apply (simp (no_asm)) 

578 
done 

579 

580 
lemma finite_subcls1: "finite (subcls1 G)" 

581 
apply (subst subcls1_def2) 

582 
apply (rule finite_SigmaI) 

583 
apply (rule finite_is_class) 

584 
apply (rule_tac B = "{super (the (class G C))}" in finite_subset) 

585 
apply auto 

586 
done 

587 

588 
lemma subint1_irrefl_lemma1: 

589 
"ws_prog G \<Longrightarrow> (subint1 G)^1 \<inter> (subint1 G)^+ = {}" 

590 
apply (force dest: subint1D ws_prog_ideclD conjunct2) 

591 
done 

592 

593 
lemma subcls1_irrefl_lemma1: 

594 
"ws_prog G \<Longrightarrow> (subcls1 G)^1 \<inter> (subcls1 G)^+ = {}" 

595 
apply (force dest: subcls1D ws_prog_cdeclD conjunct2) 

596 
done 

597 

598 
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI'] 

599 
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] 

600 

601 
lemma subint1_irrefl: "\<lbrakk>(x, y) \<in> subint1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y" 

602 
apply (rule irrefl_trancl_rD) 

603 
apply (rule subint1_irrefl_lemma2) 

604 
apply auto 

605 
done 

606 

607 
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y" 

608 
apply (rule irrefl_trancl_rD) 

609 
apply (rule subcls1_irrefl_lemma2) 

610 
apply auto 

611 
done 

612 

613 
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard] 

614 
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard] 

615 

616 

617 
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)" 

618 
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic) 

619 

620 
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)" 

621 
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic) 

622 

623 

624 
lemma subint1_induct: 

625 
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subint1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a" 

626 
apply (frule wf_subint1) 

627 
apply (erule wf_induct) 

628 
apply (simp (no_asm_use) only: converse_iff) 

629 
apply blast 

630 
done 

631 

632 
lemma subcls1_induct [consumes 1]: 

633 
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subcls1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a" 

634 
apply (frule wf_subcls1) 

635 
apply (erule wf_induct) 

636 
apply (simp (no_asm_use) only: converse_iff) 

637 
apply blast 

638 
done 

639 

640 
lemma ws_subint1_induct: 

641 
"\<lbrakk>is_iface G I; ws_prog G; \<And>I i. \<lbrakk>iface G I = Some i \<and> 

642 
(\<forall>J \<in> set (isuperIfs i). (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I 

643 
\<rbrakk> \<Longrightarrow> P I" 

24038  644 
apply (erule rev_mp) 
12854  645 
apply (rule subint1_induct) 
646 
apply assumption 

18447  647 
apply (simp (no_asm)) 
12854  648 
apply safe 
18447  649 
apply (blast dest: subint1I ws_prog_ideclD) 
12854  650 
done 
651 

652 

653 
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G; 

654 
\<And>C c. \<lbrakk>class G C = Some c; 

655 
(C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 

656 
P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C 

657 
\<rbrakk> \<Longrightarrow> P C" 

24038  658 
apply (erule rev_mp) 
12854  659 
apply (rule subcls1_induct) 
660 
apply assumption 

18447  661 
apply (simp (no_asm)) 
12854  662 
apply safe 
663 
apply (fast dest: subcls1I ws_prog_cdeclD) 

664 
done 

665 

666 
lemma ws_class_induct [consumes 2, case_names Object Subcls]: 

667 
"\<lbrakk>class G C = Some c; ws_prog G; 

668 
\<And> co. class G Object = Some co \<Longrightarrow> P Object; 

669 
\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C 

670 
\<rbrakk> \<Longrightarrow> P C" 

671 
proof  

672 
assume clsC: "class G C = Some c" 

673 
and init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object" 

674 
and step: "\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C" 

675 
assume ws: "ws_prog G" 

676 
then have "is_class G C \<Longrightarrow> P C" 

677 
proof (induct rule: subcls1_induct) 

678 
fix C 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

679 
assume hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> is_class G S \<longrightarrow> P S" 
12854  680 
and iscls:"is_class G C" 
681 
show "P C" 

682 
proof (cases "C=Object") 

683 
case True with iscls init show "P C" by auto 

684 
next 

685 
case False with ws step hyp iscls 

18576  686 
show "P C" by (auto dest: subcls1I ws_prog_cdeclD) 
12854  687 
qed 
688 
qed 

689 
with clsC show ?thesis by simp 

690 
qed 

691 

692 
lemma ws_class_induct' [consumes 2, case_names Object Subcls]: 

693 
"\<lbrakk>is_class G C; ws_prog G; 

694 
\<And> co. class G Object = Some co \<Longrightarrow> P Object; 

695 
\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C 

696 
\<rbrakk> \<Longrightarrow> P C" 

18447  697 
by (auto intro: ws_class_induct) 
12854  698 

699 
lemma ws_class_induct'' [consumes 2, case_names Object Subcls]: 

700 
"\<lbrakk>class G C = Some c; ws_prog G; 

701 
\<And> co. class G Object = Some co \<Longrightarrow> P Object co; 

702 
\<And> C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc; 

703 
C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c 

704 
\<rbrakk> \<Longrightarrow> P C c" 

705 
proof  

706 
assume clsC: "class G C = Some c" 

707 
and init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co" 

708 
and step: "\<And> C c sc . \<lbrakk>class G C = Some c; class G (super c) = Some sc; 

709 
C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c" 

710 
assume ws: "ws_prog G" 

711 
then have "\<And> c. class G C = Some c\<Longrightarrow> P C c" 

712 
proof (induct rule: subcls1_induct) 

713 
fix C c 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

714 
assume hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> (\<forall> s. class G S = Some s \<longrightarrow> P S s)" 
12854  715 
and iscls:"class G C = Some c" 
716 
show "P C c" 

717 
proof (cases "C=Object") 

718 
case True with iscls init show "P C c" by auto 

719 
next 

720 
case False 

721 
with ws iscls obtain sc where 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

722 
sc: "class G (super c) = Some sc" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

723 
by (auto dest: ws_prog_cdeclD) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

724 
from iscls False have "G\<turnstile>C \<prec>\<^sub>C1 (super c)" by (rule subcls1I) 
12854  725 
with False ws step hyp iscls sc 
726 
show "P C c" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

727 
by (auto) 
12854  728 
qed 
729 
qed 

730 
with clsC show "P C c" by auto 

731 
qed 

732 

733 
lemma ws_interface_induct [consumes 2, case_names Step]: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

734 
assumes is_if_I: "is_iface G I" and 
12854  735 
ws: "ws_prog G" and 
736 
hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 

737 
\<forall> J \<in> set (isuperIfs i). 

738 
(I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

739 
shows "P I" 
12854  740 
proof  
741 
from is_if_I ws 

742 
show "P I" 

743 
proof (rule ws_subint1_induct) 

744 
fix I i 

745 
assume hyp: "iface G I = Some i \<and> 

746 
(\<forall>J\<in>set (isuperIfs i). (I,J) \<in>subint1 G \<and> P J \<and> is_iface G J)" 

747 
then have if_I: "iface G I = Some i" 

748 
by blast 

749 
show "P I" 

750 
proof (cases "isuperIfs i") 

751 
case Nil 

752 
with if_I hyp_sub 

753 
show "P I" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

754 
by auto 
12854  755 
next 
756 
case (Cons hd tl) 

757 
with hyp if_I hyp_sub 

758 
show "P I" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

759 
by auto 
12854  760 
qed 
761 
qed 

762 
qed 

763 

764 
section "general recursion operators for the interface and class hiearchies" 

765 

766 
consts 

767 
iface_rec :: "prog \<times> qtname \<Rightarrow> \<spacespace> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a" 

768 
class_rec :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" 

769 

770 
recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^1)" 

771 
"iface_rec (G,I) = 

772 
(\<lambda>f. case iface G I of 

28524  773 
None \<Rightarrow> undefined 
12854  774 
 Some i \<Rightarrow> if ws_prog G 
775 
then f I i 

776 
((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i)) 

28524  777 
else undefined)" 
12854  778 
(hints recdef_wf: wf_subint1 intro: subint1I) 
779 
declare iface_rec.simps [simp del] 

780 

781 
lemma iface_rec: 

782 
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 

783 
iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))" 

784 
apply (subst iface_rec.simps) 

785 
apply simp 

786 
done 

787 

788 
recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^1)" 

789 
"class_rec(G,C) = 

790 
(\<lambda>t f. case class G C of 

28524  791 
None \<Rightarrow> undefined 
12854  792 
 Some c \<Rightarrow> if ws_prog G 
793 
then f C c 

794 
(if C = Object then t 

795 
else class_rec (G,super c) t f) 

28524  796 
else undefined)" 
12854  797 
(hints recdef_wf: wf_subcls1 intro: subcls1I) 
798 
declare class_rec.simps [simp del] 

799 

800 
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow> 

801 
class_rec (G,C) t f = 

802 
f C c (if C = Object then t else class_rec (G,super c) t f)" 

803 
apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]]) 

804 
apply simp 

805 
done 

806 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35315
diff
changeset

807 
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where 
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:
13601
diff
changeset

808 
{* methods of an interface, with overriding and inheritance, cf. 9.2 *} 
12854  809 
"imethds G I 
810 
\<equiv> iface_rec (G,I) 

811 
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 

30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
28524
diff
changeset

812 
(Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

813 

12854  814 

815 

816 
end 