author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47176  568fdc70e565 
child 54703  499f92dc6e45 
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 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
41778
diff
changeset

8 
imports Term Table 
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
41778
diff
changeset

9 
(** order is significant, because of clash for "var" **) 
26566
36a93808642c
instantiation replacing primitive instance plus overloaded defs
haftmann
parents:
24783
diff
changeset

10 
begin 
12854  11 

12 
text {* 

13 
improvements: 

14 
\begin{itemize} 

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

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

17 
Bug Id: 4485402 and Bug Id: 4493343 

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

19 
) 

20 
\end{itemize} 

21 
simplifications: 

22 
\begin{itemize} 

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

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

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

26 
others 

27 

28 
\item no throws clause 

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

30 

31 
\item no interface fields 

32 

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

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

35 
specified 

36 

37 
\item no main method 

38 
\end{itemize} 

39 
*} 

40 

41 
subsection {* Modifier*} 

42 

43 
subsubsection {* Access modifier *} 

44 

45 
datatype acc_modi (* access modifier *) 

46 
= Private  Package  Protected  Public 

47 

48 
text {* 

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

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

51 
Private < Package < Protected < Public 

52 
*} 

53 

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

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

55 
begin 
12854  56 

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

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

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

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

62 
 Protected \<Rightarrow> (b=Public) 

63 
 Public \<Rightarrow> False)" 

64 

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

65 
definition 
27682  66 
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

67 

41525  68 
instance 
69 
proof 

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

46212  73 
show "x \<le> x"  reflexivity 
12854  74 
by (auto simp add: le_acc_def) 
41525  75 
{ 
76 
assume "x \<le> y" "y \<le> z"  transitivity 

77 
then show "x \<le> z" 

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

12854  79 
next 
41525  80 
assume "x \<le> y" "y \<le> x"  antisymmetry 
81 
moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False" 

12854  82 
by (auto simp add: less_acc_def split add: acc_modi.split) 
41525  83 
ultimately show "x = y" by (unfold le_acc_def) iprover 
12854  84 
next 
41525  85 
fix x y:: acc_modi 
86 
show "x \<le> y \<or> y \<le> x" 

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

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

90 

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

91 
end 
12854  92 

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

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

95 

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

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

98 

99 
lemma acc_modi_le_Public: 

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

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

102 

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

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

105 

106 
lemma acc_modi_Private_le: 

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

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

109 

110 
lemma acc_modi_Package_le: 

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

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

113 

114 
lemma acc_modi_le_Package: 

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

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

117 

118 
lemma acc_modi_Protected_le: 

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

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

121 

122 
lemma acc_modi_le_Protected: 

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

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

125 

126 

127 
lemmas acc_modi_le_Dests = acc_modi_top acc_modi_le_Public 

128 
acc_modi_Private_le acc_modi_bottom 

129 
acc_modi_Package_le acc_modi_le_Package 

130 
acc_modi_Protected_le acc_modi_le_Protected 

131 

47176  132 
lemma acc_modi_Package_le_cases: 
133 
assumes "Package \<le> m" 

134 
obtains (Package) "m = Package" 

135 
 (Protected) "m = Protected" 

136 
 (Public) "m = Public" 

137 
using assms by (auto dest: acc_modi_Package_le) 

12854  138 

139 

140 
subsubsection {* Static Modifier *} 

41778  141 
type_synonym stat_modi = bool (* modifier: static *) 
12854  142 

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

144 
declarations *} 

145 

146 
record decl = 

147 
access :: acc_modi 

148 

149 
translations 

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

12854  152 

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

154 
record member = decl + 

155 
static :: stat_modi 

156 

157 
translations 

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

12854  160 

161 
subsection {* Field *} 

162 

163 
record field = member + 

164 
type :: ty 

165 
translations 

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

12854  168 

41778  169 
type_synonym fdecl (* field declaration, cf. 8.3 *) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

170 
= "vname \<times> field" 
12854  171 

172 

173 
translations 

35431  174 
(type) "fdecl" <= (type) "vname \<times> field" 
12854  175 

176 
subsection {* Method *} 

177 

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

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

180 
resT ::ty (* result type *) 

181 

182 
record mbody = (* method body *) 

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

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

185 

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

187 
mbody::mbody 

188 

41778  189 
type_synonym mdecl = "sig \<times> methd" (* method declaration in a class *) 
12854  190 

191 

192 
translations 

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

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

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

205 

37956  206 
definition 
207 
mhead :: "methd \<Rightarrow> mhead" 

208 
where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>" 

12854  209 

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

211 
by (simp add: mhead_def) 

212 

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

214 
by (simp add: mhead_def) 

215 

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

217 
by (simp add: mhead_def) 

218 

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

220 
by (simp add: mhead_def) 

221 

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

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

224 
accessiblity ) *} 

225 

226 
datatype memberdecl = fdecl fdecl  mdecl mdecl 

227 

228 
datatype memberid = fid vname  mid sig 

229 

35315  230 
class has_memberid = 
231 
fixes memberid :: "'a \<Rightarrow> memberid" 

12854  232 

35315  233 
instantiation memberdecl :: has_memberid 
234 
begin 

12854  235 

35315  236 
definition 
12854  237 
memberdecl_memberid_def: 
37956  238 
"memberid m = (case m of 
12854  239 
fdecl (vn,f) \<Rightarrow> fid vn 
240 
 mdecl (sig,m) \<Rightarrow> mid sig)" 

241 

35315  242 
instance .. 
243 

244 
end 

245 

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

248 

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

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

251 

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

253 
by (simp add: memberdecl_memberid_def) 

254 

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

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

257 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
35547
diff
changeset

258 
instantiation prod :: (type, has_memberid) has_memberid 
35315  259 
begin 
12854  260 

35315  261 
definition 
12854  262 
pair_memberid_def: 
37956  263 
"memberid p = memberid (snd p)" 
12854  264 

35315  265 
instance .. 
266 

267 
end 

268 

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

271 

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

273 
by (simp add: pair_memberid_def) 

274 

37956  275 
definition 
276 
is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" 

277 
where "is_field m = (\<exists> declC f. m=(declC,fdecl f))" 

12854  278 

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

280 
by (simp add: is_field_def) 

281 

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

283 
by (simp add: is_field_def) 

284 

37956  285 
definition 
286 
is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" 

287 
where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))" 

12854  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 *} 
41778  304 
type_synonym 
32960
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 

37956  317 
definition 
318 
ibody :: "iface \<Rightarrow> ibody" 

319 
where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>" 

12854  320 

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

322 
by (simp add: ibody_def) 

323 

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

325 
by (simp add: ibody_def) 

326 

327 
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

328 
record cbody = decl + {* class body *} 
12854  329 
cfields:: "fdecl list" 
330 
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

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

18551  333 
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

334 
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

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

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

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

340 
translations 

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

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

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

37956  353 
definition 
354 
cbody :: "class \<Rightarrow> cbody" 

355 
where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>" 

12854  356 

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

358 
by (simp add: cbody_def) 

359 

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

361 
by (simp add: cbody_def) 

362 

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

364 
by (simp add: cbody_def) 

365 

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

367 
by (simp add: cbody_def) 

368 

369 

370 
section "standard classes" 

371 

372 
consts 

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

12854  375 

37956  376 
definition 
377 
ObjectC :: "cdecl" {* declaration of root class *} where 

378 
"ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls, 

379 
init=Skip,super=undefined,superIfs=[]\<rparr>)" 

12854  380 

37956  381 
definition 
382 
SXcptC ::"xname \<Rightarrow> cdecl" {* declarations of throwable classes *} where 

383 
"SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 

12854  384 
init=Skip, 
385 
super=if xn = Throwable then Object 

386 
else SXcpt Throwable, 

387 
superIfs=[]\<rparr>)" 

388 

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

390 
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def) 

391 

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

17778  393 
by (simp add: SXcptC_def) 
12854  394 

37956  395 
definition 
396 
standard_classes :: "cdecl list" where 

397 
"standard_classes = [ObjectC, SXcptC Throwable, 

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

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

399 
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]" 
12854  400 

401 

402 
section "programs" 

403 

404 
record prog = 

405 
ifaces ::"idecl list" 

406 
"classes"::"cdecl list" 

407 

408 
translations 

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

12854  411 

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

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

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

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

415 

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

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

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

418 
where "class G C == table_of (classes G) C" 
12854  419 

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

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

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

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

423 

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

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

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

426 
where "is_class G C == class G C \<noteq> None" 
12854  427 

428 

429 
section "is type" 

430 

37956  431 
primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool" 
432 
and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool" 

433 
where 

434 
"is_type G (PrimT pt) = True" 

435 
 "is_type G (RefT rt) = isrtype G rt" 

436 
 "isrtype G (NullT) = True" 

437 
 "isrtype G (IfaceT tn) = is_iface G tn" 

438 
 "isrtype G (ClassT tn) = is_class G tn" 

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

12854  440 

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

442 
by auto 

443 

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

445 
by auto 

446 

447 

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

449 

37956  450 
definition 
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

451 
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct subinterface *} 
37956  452 
where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}" 
12854  453 

37956  454 
definition 
455 
subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct subclass *} 

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

12854  457 

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

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

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

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

461 

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

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

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

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

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

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

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

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

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

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

471 
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

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

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

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

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

477 
apply (simp add: subint1_def) 

478 
done 

479 

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

481 
apply (simp add: subcls1_def) 

482 
done 

483 

484 

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

486 
by (simp add: subint1_def) 

487 

488 
lemma subcls1D: 

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

490 
apply (simp add: subcls1_def) 

491 
apply auto 

492 
done 

493 

494 
lemma subint1_def2: 

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

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

498 
done 

499 

500 
lemma subcls1_def2: 

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

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

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

505 
done 

506 

507 
lemma subcls_is_class: 

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

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

510 

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

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

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

515 
apply (erule trancl_induct) 

516 
apply (auto intro: no_subcls1_Object) 

517 
done 

518 

519 
section "wellstructured programs" 

520 

37956  521 
definition 
522 
ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" 

523 
where "ws_idecl G I si = (\<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+)" 

12854  524 

37956  525 
definition 
526 
ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

527 
where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)" 

12854  528 

37956  529 
definition 
530 
ws_prog :: "prog \<Rightarrow> bool" where 

531 
"ws_prog G = ((\<forall>(I,i)\<in>set (ifaces G). ws_idecl G I (isuperIfs i)) \<and> 

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

12854  533 

534 

535 
lemma ws_progI: 

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

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

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

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

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

541 
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def) 

542 
apply (erule_tac conjI) 

543 
apply blast 

544 
done 

545 

546 
lemma ws_prog_ideclD: 

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

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

549 
apply (unfold ws_prog_def ws_idecl_def) 

550 
apply clarify 

551 
apply (drule_tac map_of_SomeD) 

552 
apply auto 

553 
done 

554 

555 
lemma ws_prog_cdeclD: 

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

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

558 
apply (unfold ws_prog_def ws_cdecl_def) 

559 
apply clarify 

560 
apply (drule_tac map_of_SomeD) 

561 
apply auto 

562 
done 

563 

564 

565 
section "wellfoundedness" 

566 

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

568 
apply (fold dom_def) 

569 
apply (rule_tac finite_dom_map_of) 

570 
done 

571 

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

573 
apply (fold dom_def) 

574 
apply (rule_tac finite_dom_map_of) 

575 
done 

576 

577 
lemma finite_subint1: "finite (subint1 G)" 

578 
apply (subst subint1_def2) 

579 
apply (rule finite_SigmaI) 

580 
apply (rule finite_is_iface) 

581 
apply (simp (no_asm)) 

582 
done 

583 

584 
lemma finite_subcls1: "finite (subcls1 G)" 

585 
apply (subst subcls1_def2) 

586 
apply (rule finite_SigmaI) 

587 
apply (rule finite_is_class) 

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

589 
apply auto 

590 
done 

591 

592 
lemma subint1_irrefl_lemma1: 

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

594 
apply (force dest: subint1D ws_prog_ideclD conjunct2) 

595 
done 

596 

597 
lemma subcls1_irrefl_lemma1: 

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

599 
apply (force dest: subcls1D ws_prog_cdeclD conjunct2) 

600 
done 

601 

602 
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI'] 

603 
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] 

604 

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

606 
apply (rule irrefl_trancl_rD) 

607 
apply (rule subint1_irrefl_lemma2) 

608 
apply auto 

609 
done 

610 

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

612 
apply (rule irrefl_trancl_rD) 

613 
apply (rule subcls1_irrefl_lemma2) 

614 
apply auto 

615 
done 

616 

45605  617 
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI] 
618 
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI] 

12854  619 

620 

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

622 
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic) 

623 

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

625 
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic) 

626 

627 

628 
lemma subint1_induct: 

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

630 
apply (frule wf_subint1) 

631 
apply (erule wf_induct) 

632 
apply (simp (no_asm_use) only: converse_iff) 

633 
apply blast 

634 
done 

635 

636 
lemma subcls1_induct [consumes 1]: 

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

638 
apply (frule wf_subcls1) 

639 
apply (erule wf_induct) 

640 
apply (simp (no_asm_use) only: converse_iff) 

641 
apply blast 

642 
done 

643 

644 
lemma ws_subint1_induct: 

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

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

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

24038  648 
apply (erule rev_mp) 
12854  649 
apply (rule subint1_induct) 
650 
apply assumption 

18447  651 
apply (simp (no_asm)) 
12854  652 
apply safe 
18447  653 
apply (blast dest: subint1I ws_prog_ideclD) 
12854  654 
done 
655 

656 

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

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

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

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

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

24038  662 
apply (erule rev_mp) 
12854  663 
apply (rule subcls1_induct) 
664 
apply assumption 

18447  665 
apply (simp (no_asm)) 
12854  666 
apply safe 
667 
apply (fast dest: subcls1I ws_prog_cdeclD) 

668 
done 

669 

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

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

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

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

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

675 
proof  

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

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

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

679 
assume ws: "ws_prog G" 

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

681 
proof (induct rule: subcls1_induct) 

682 
fix C 

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

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

686 
proof (cases "C=Object") 

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

688 
next 

689 
case False with ws step hyp iscls 

18576  690 
show "P C" by (auto dest: subcls1I ws_prog_cdeclD) 
12854  691 
qed 
692 
qed 

693 
with clsC show ?thesis by simp 

694 
qed 

695 

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

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

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

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

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

18447  701 
by (auto intro: ws_class_induct) 
12854  702 

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

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

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

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

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

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

709 
proof  

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

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

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

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

714 
assume ws: "ws_prog G" 

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

716 
proof (induct rule: subcls1_induct) 

717 
fix C c 

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

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

721 
proof (cases "C=Object") 

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

723 
next 

724 
case False 

725 
with ws iscls obtain sc where 

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

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

727 
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

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

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

731 
by (auto) 
12854  732 
qed 
733 
qed 

734 
with clsC show "P C c" by auto 

735 
qed 

736 

737 
lemma ws_interface_induct [consumes 2, case_names Step]: 

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

738 
assumes is_if_I: "is_iface G I" and 
12854  739 
ws: "ws_prog G" and 
740 
hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 

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

742 
(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

743 
shows "P I" 
12854  744 
proof  
745 
from is_if_I ws 

746 
show "P I" 

747 
proof (rule ws_subint1_induct) 

748 
fix I i 

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

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

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

752 
by blast 

753 
show "P I" 

754 
proof (cases "isuperIfs i") 

755 
case Nil 

756 
with if_I hyp_sub 

757 
show "P I" 

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

758 
by auto 
12854  759 
next 
760 
case (Cons hd tl) 

761 
with hyp if_I hyp_sub 

762 
show "P I" 

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

763 
by auto 
12854  764 
qed 
765 
qed 

766 
qed 

767 

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

769 

46212  770 
function iface_rec :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a" 
35440  771 
where 
772 
[simp del]: "iface_rec G I f = 

773 
(case iface G I of 

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

35440  777 
((\<lambda>J. iface_rec G J f)`set (isuperIfs i)) 
28524  778 
else undefined)" 
35440  779 
by auto 
780 
termination 

781 
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^1)) (%(x,y,z). (x,y))") 

782 
(auto simp: wf_subint1 subint1I wf_same_fst) 

12854  783 

784 
lemma iface_rec: 

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

35440  786 
iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))" 
12854  787 
apply (subst iface_rec.simps) 
788 
apply simp 

789 
done 

790 

35440  791 

792 
function 

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

794 
where 

795 
[simp del]: "class_rec G C t f = 

796 
(case class G C of 

28524  797 
None \<Rightarrow> undefined 
12854  798 
 Some c \<Rightarrow> if ws_prog G 
799 
then f C c 

800 
(if C = Object then t 

35440  801 
else class_rec G (super c) t f) 
28524  802 
else undefined)" 
35440  803 

804 
by auto 

805 
termination 

806 
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^1)) (%(x,y,z,w). (x,y))") 

807 
(auto simp: wf_subcls1 subcls1I wf_same_fst) 

12854  808 

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

35440  810 
class_rec G C t f = 
811 
f C c (if C = Object then t else class_rec G (super c) t f)" 

812 
apply (subst class_rec.simps) 

12854  813 
apply simp 
814 
done 

815 

37956  816 
definition 
817 
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

818 
{* methods of an interface, with overriding and inheritance, cf. 9.2 *} 
37956  819 
"imethds G I = iface_rec G I 
12854  820 
(\<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

821 
(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

822 

12854  823 

824 

825 
end 