12857
|
1 |
(* Title: HOL/Bali/Decl.thy
|
12854
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
12858
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
12854
|
5 |
*)
|
|
6 |
header {* Field, method, interface, and class declarations, whole Java programs
|
|
7 |
*}
|
|
8 |
|
|
9 |
(** order is significant, because of clash for "var" **)
|
|
10 |
theory Decl = Term + Table:
|
|
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 |
|
12859
|
54 |
instance acc_modi:: ord ..
|
12854
|
55 |
|
|
56 |
defs (overloaded)
|
|
57 |
less_acc_def:
|
|
58 |
"a < (b::acc_modi)
|
|
59 |
\<equiv> (case a of
|
|
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 |
le_acc_def:
|
|
65 |
"a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
|
|
66 |
|
|
67 |
instance acc_modi:: order
|
12859
|
68 |
proof
|
12854
|
69 |
fix x y z::acc_modi
|
|
70 |
{
|
|
71 |
show "x \<le> x" \<spacespace>\<spacespace> -- reflexivity
|
|
72 |
by (auto simp add: le_acc_def)
|
|
73 |
next
|
|
74 |
assume "x \<le> y" "y \<le> z" -- transitivity
|
|
75 |
thus "x \<le> z"
|
|
76 |
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
|
|
77 |
next
|
|
78 |
assume "x \<le> y" "y \<le> x" -- antisymmetry
|
|
79 |
thus "x = y"
|
|
80 |
proof -
|
|
81 |
have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
|
|
82 |
by (auto simp add: less_acc_def split add: acc_modi.split)
|
|
83 |
with prems show ?thesis
|
|
84 |
by (auto simp add: le_acc_def)
|
|
85 |
qed
|
|
86 |
next
|
|
87 |
show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
|
|
88 |
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
|
|
89 |
}
|
|
90 |
qed
|
|
91 |
|
|
92 |
instance acc_modi:: linorder
|
12859
|
93 |
proof
|
12854
|
94 |
fix x y:: acc_modi
|
|
95 |
show "x \<le> y \<or> y \<le> x"
|
|
96 |
by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
|
|
97 |
qed
|
|
98 |
|
|
99 |
lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
|
|
100 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
101 |
|
|
102 |
lemma acc_modi_top1 [simp, intro!]: "a \<le> Public"
|
|
103 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
104 |
|
|
105 |
lemma acc_modi_le_Public:
|
|
106 |
"a \<le> Public \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
|
|
107 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
108 |
|
|
109 |
lemma acc_modi_bottom: "a \<le> Private \<Longrightarrow> a = Private"
|
|
110 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
111 |
|
|
112 |
lemma acc_modi_Private_le:
|
|
113 |
"Private \<le> a \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
|
|
114 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
115 |
|
|
116 |
lemma acc_modi_Package_le:
|
|
117 |
"Package \<le> a \<Longrightarrow> a = Package \<or> a=Protected \<or> a=Public"
|
|
118 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
|
|
119 |
|
|
120 |
lemma acc_modi_le_Package:
|
|
121 |
"a \<le> Package \<Longrightarrow> a=Private \<or> a = Package"
|
|
122 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
123 |
|
|
124 |
lemma acc_modi_Protected_le:
|
|
125 |
"Protected \<le> a \<Longrightarrow> a=Protected \<or> a=Public"
|
|
126 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
127 |
|
|
128 |
lemma acc_modi_le_Protected:
|
|
129 |
"a \<le> Protected \<Longrightarrow> a=Private \<or> a = Package \<or> a = Protected"
|
|
130 |
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
|
|
131 |
|
|
132 |
|
|
133 |
lemmas acc_modi_le_Dests = acc_modi_top acc_modi_le_Public
|
|
134 |
acc_modi_Private_le acc_modi_bottom
|
|
135 |
acc_modi_Package_le acc_modi_le_Package
|
|
136 |
acc_modi_Protected_le acc_modi_le_Protected
|
|
137 |
|
|
138 |
lemma acc_modi_Package_le_cases
|
|
139 |
[consumes 1,case_names Package Protected Public]:
|
|
140 |
"Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow>
|
|
141 |
(m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
|
|
142 |
by (auto dest: acc_modi_Package_le)
|
|
143 |
|
|
144 |
|
|
145 |
subsubsection {* Static Modifier *}
|
|
146 |
types stat_modi = bool (* modifier: static *)
|
|
147 |
|
|
148 |
subsection {* Declaration (base "class" for member,interface and class
|
|
149 |
declarations *}
|
|
150 |
|
|
151 |
record decl =
|
|
152 |
access :: acc_modi
|
|
153 |
|
|
154 |
translations
|
|
155 |
"decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
|
|
156 |
"decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
|
|
157 |
|
|
158 |
subsection {* Member (field or method)*}
|
|
159 |
record member = decl +
|
|
160 |
static :: stat_modi
|
|
161 |
|
|
162 |
translations
|
|
163 |
"member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
|
|
164 |
"member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
|
|
165 |
|
|
166 |
subsection {* Field *}
|
|
167 |
|
|
168 |
record field = member +
|
|
169 |
type :: ty
|
|
170 |
translations
|
|
171 |
"field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
|
|
172 |
"field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
|
|
173 |
|
|
174 |
types
|
|
175 |
fdecl (* field declaration, cf. 8.3 *)
|
|
176 |
= "vname \<times> field"
|
|
177 |
|
|
178 |
|
|
179 |
translations
|
|
180 |
"fdecl" <= (type) "vname \<times> field"
|
|
181 |
|
|
182 |
subsection {* Method *}
|
|
183 |
|
|
184 |
record mhead = member + (* method head (excluding signature) *)
|
|
185 |
pars ::"vname list" (* parameter names *)
|
|
186 |
resT ::ty (* result type *)
|
|
187 |
|
|
188 |
record mbody = (* method body *)
|
|
189 |
lcls:: "(vname \<times> ty) list" (* local variables *)
|
|
190 |
stmt:: stmt (* the body statement *)
|
|
191 |
|
|
192 |
record methd = mhead + (* method in a class *)
|
|
193 |
mbody::mbody
|
|
194 |
|
|
195 |
types mdecl = "sig \<times> methd" (* method declaration in a class *)
|
|
196 |
|
|
197 |
|
|
198 |
translations
|
|
199 |
"mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
|
|
200 |
pars::vname list, resT::ty\<rparr>"
|
|
201 |
"mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
|
|
202 |
pars::vname list, resT::ty,\<dots>::'a\<rparr>"
|
|
203 |
"mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
|
|
204 |
"mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
|
|
205 |
"methd" <= (type) "\<lparr>access::acc_modi, static::bool,
|
|
206 |
pars::vname list, resT::ty,mbody::mbody\<rparr>"
|
|
207 |
"methd" <= (type) "\<lparr>access::acc_modi, static::bool,
|
|
208 |
pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
|
|
209 |
"mdecl" <= (type) "sig \<times> methd"
|
|
210 |
|
|
211 |
|
|
212 |
constdefs
|
|
213 |
mhead::"methd \<Rightarrow> mhead"
|
|
214 |
"mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
|
|
215 |
|
|
216 |
lemma access_mhead [simp]:"access (mhead m) = access m"
|
|
217 |
by (simp add: mhead_def)
|
|
218 |
|
|
219 |
lemma static_mhead [simp]:"static (mhead m) = static m"
|
|
220 |
by (simp add: mhead_def)
|
|
221 |
|
|
222 |
lemma pars_mhead [simp]:"pars (mhead m) = pars m"
|
|
223 |
by (simp add: mhead_def)
|
|
224 |
|
|
225 |
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
|
|
226 |
by (simp add: mhead_def)
|
|
227 |
|
|
228 |
text {* To be able to talk uniformaly about field and method declarations we
|
|
229 |
introduce the notion of a member declaration (e.g. useful to define
|
|
230 |
accessiblity ) *}
|
|
231 |
|
|
232 |
datatype memberdecl = fdecl fdecl | mdecl mdecl
|
|
233 |
|
|
234 |
datatype memberid = fid vname | mid sig
|
|
235 |
|
|
236 |
axclass has_memberid < "type"
|
|
237 |
consts
|
|
238 |
memberid :: "'a::has_memberid \<Rightarrow> memberid"
|
|
239 |
|
12859
|
240 |
instance memberdecl::has_memberid ..
|
12854
|
241 |
|
|
242 |
defs (overloaded)
|
|
243 |
memberdecl_memberid_def:
|
|
244 |
"memberid m \<equiv> (case m of
|
|
245 |
fdecl (vn,f) \<Rightarrow> fid vn
|
|
246 |
| mdecl (sig,m) \<Rightarrow> mid sig)"
|
|
247 |
|
|
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 |
|
12859
|
260 |
instance * :: (type, has_memberid) has_memberid ..
|
12854
|
261 |
|
|
262 |
defs (overloaded)
|
|
263 |
pair_memberid_def:
|
|
264 |
"memberid p \<equiv> memberid (snd p)"
|
|
265 |
|
|
266 |
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
|
|
267 |
by (simp add: pair_memberid_def)
|
|
268 |
|
|
269 |
lemma memberid_pair_simp1: "memberid p = memberid (snd p)"
|
|
270 |
by (simp add: pair_memberid_def)
|
|
271 |
|
|
272 |
constdefs is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
|
|
273 |
"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
|
|
274 |
|
|
275 |
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
|
|
276 |
by (simp add: is_field_def)
|
|
277 |
|
|
278 |
lemma is_fieldI: "is_field (C,fdecl f)"
|
|
279 |
by (simp add: is_field_def)
|
|
280 |
|
|
281 |
constdefs is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
|
|
282 |
"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
|
|
283 |
|
|
284 |
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
|
|
285 |
by (simp add: is_method_def)
|
|
286 |
|
|
287 |
lemma is_methodI: "is_method (C,mdecl m)"
|
|
288 |
by (simp add: is_method_def)
|
|
289 |
|
|
290 |
|
|
291 |
subsection {* Interface *}
|
|
292 |
|
|
293 |
|
|
294 |
record ibody = decl + (* interface body *)
|
|
295 |
imethods :: "(sig \<times> mhead) list" (* method heads *)
|
|
296 |
|
|
297 |
record iface = ibody + (* interface *)
|
|
298 |
isuperIfs:: "qtname list" (* superinterface list *)
|
|
299 |
types
|
|
300 |
idecl (* interface declaration, cf. 9.1 *)
|
|
301 |
= "qtname \<times> iface"
|
|
302 |
|
|
303 |
translations
|
|
304 |
"ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
|
|
305 |
"ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
|
|
306 |
"iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
|
|
307 |
isuperIfs::qtname list\<rparr>"
|
|
308 |
"iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
|
|
309 |
isuperIfs::qtname list,\<dots>::'a\<rparr>"
|
|
310 |
"idecl" <= (type) "qtname \<times> iface"
|
|
311 |
|
|
312 |
constdefs
|
|
313 |
ibody :: "iface \<Rightarrow> ibody"
|
|
314 |
"ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
|
|
315 |
|
|
316 |
lemma access_ibody [simp]: "(access (ibody i)) = access i"
|
|
317 |
by (simp add: ibody_def)
|
|
318 |
|
|
319 |
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
|
|
320 |
by (simp add: ibody_def)
|
|
321 |
|
|
322 |
subsection {* Class *}
|
|
323 |
record cbody = decl + (* class body *)
|
|
324 |
cfields:: "fdecl list"
|
|
325 |
methods:: "mdecl list"
|
|
326 |
init :: "stmt" (* initializer *)
|
|
327 |
|
|
328 |
record class = cbody + (* class *)
|
|
329 |
super :: "qtname" (* superclass *)
|
|
330 |
superIfs:: "qtname list" (* implemented interfaces *)
|
|
331 |
types
|
|
332 |
cdecl (* class declaration, cf. 8.1 *)
|
|
333 |
= "qtname \<times> class"
|
|
334 |
|
|
335 |
translations
|
|
336 |
"cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
|
|
337 |
methods::mdecl list,init::stmt\<rparr>"
|
|
338 |
"cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
|
|
339 |
methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
|
|
340 |
"class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
|
|
341 |
methods::mdecl list,init::stmt,
|
|
342 |
super::qtname,superIfs::qtname list\<rparr>"
|
|
343 |
"class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
|
|
344 |
methods::mdecl list,init::stmt,
|
|
345 |
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
|
|
346 |
"cdecl" <= (type) "qtname \<times> class"
|
|
347 |
|
|
348 |
constdefs
|
|
349 |
cbody :: "class \<Rightarrow> cbody"
|
|
350 |
"cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
|
|
351 |
|
|
352 |
lemma access_cbody [simp]:"access (cbody c) = access c"
|
|
353 |
by (simp add: cbody_def)
|
|
354 |
|
|
355 |
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
|
|
356 |
by (simp add: cbody_def)
|
|
357 |
|
|
358 |
lemma methods_cbody [simp]:"methods (cbody c) = methods c"
|
|
359 |
by (simp add: cbody_def)
|
|
360 |
|
|
361 |
lemma init_cbody [simp]:"init (cbody c) = init c"
|
|
362 |
by (simp add: cbody_def)
|
|
363 |
|
|
364 |
|
|
365 |
section "standard classes"
|
|
366 |
|
|
367 |
consts
|
|
368 |
|
|
369 |
Object_mdecls :: "mdecl list" (* methods of Object *)
|
|
370 |
SXcpt_mdecls :: "mdecl list" (* methods of SXcpts *)
|
|
371 |
ObjectC :: "cdecl" (* declaration of root class *)
|
|
372 |
SXcptC ::"xname \<Rightarrow> cdecl" (* declarations of throwable classes *)
|
|
373 |
|
|
374 |
defs
|
|
375 |
|
|
376 |
|
|
377 |
ObjectC_def:"ObjectC \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
|
|
378 |
init=Skip,super=arbitrary,superIfs=[]\<rparr>)"
|
|
379 |
SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
|
|
380 |
init=Skip,
|
|
381 |
super=if xn = Throwable then Object
|
|
382 |
else SXcpt Throwable,
|
|
383 |
superIfs=[]\<rparr>)"
|
|
384 |
|
|
385 |
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
|
|
386 |
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
|
|
387 |
|
|
388 |
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
|
|
389 |
apply (simp add: SXcptC_def)
|
|
390 |
apply auto
|
|
391 |
done
|
|
392 |
|
|
393 |
constdefs standard_classes :: "cdecl list"
|
|
394 |
"standard_classes \<equiv> [ObjectC, SXcptC Throwable,
|
|
395 |
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
|
|
396 |
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
|
|
397 |
|
|
398 |
|
|
399 |
section "programs"
|
|
400 |
|
|
401 |
record prog =
|
|
402 |
ifaces ::"idecl list"
|
|
403 |
"classes"::"cdecl list"
|
|
404 |
|
|
405 |
translations
|
|
406 |
"prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
|
|
407 |
"prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
|
|
408 |
|
|
409 |
syntax
|
|
410 |
iface :: "prog \<Rightarrow> (qtname, iface) table"
|
|
411 |
class :: "prog \<Rightarrow> (qtname, class) table"
|
|
412 |
is_iface :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
|
|
413 |
is_class :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
|
|
414 |
|
|
415 |
translations
|
|
416 |
"iface G I" == "table_of (ifaces G) I"
|
|
417 |
"class G C" == "table_of (classes G) C"
|
|
418 |
"is_iface G I" == "iface G I \<noteq> None"
|
|
419 |
"is_class G C" == "class G C \<noteq> None"
|
|
420 |
|
|
421 |
|
|
422 |
section "is type"
|
|
423 |
|
|
424 |
consts
|
|
425 |
is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
|
|
426 |
isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
|
|
427 |
|
|
428 |
primrec "is_type G (PrimT pt) = True"
|
|
429 |
"is_type G (RefT rt) = isrtype G rt"
|
|
430 |
"isrtype G (NullT ) = True"
|
|
431 |
"isrtype G (IfaceT tn) = is_iface G tn"
|
|
432 |
"isrtype G (ClassT tn) = is_class G tn"
|
|
433 |
"isrtype G (ArrayT T ) = is_type G T"
|
|
434 |
|
|
435 |
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
|
|
436 |
by auto
|
|
437 |
|
|
438 |
lemma type_is_class: "is_type G (Class C) \<Longrightarrow> is_class G C"
|
|
439 |
by auto
|
|
440 |
|
|
441 |
|
|
442 |
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
|
|
443 |
|
|
444 |
consts
|
|
445 |
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set"
|
|
446 |
subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set"
|
|
447 |
|
|
448 |
defs
|
|
449 |
subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
|
|
450 |
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
|
|
451 |
|
|
452 |
syntax
|
|
453 |
"@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
|
|
454 |
"@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
|
|
455 |
"@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
|
|
456 |
|
|
457 |
syntax (xsymbols)
|
|
458 |
"@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)
|
|
459 |
"@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)
|
|
460 |
"@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)
|
|
461 |
|
|
462 |
translations
|
|
463 |
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
|
|
464 |
"G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
|
|
465 |
"G\<turnstile>C \<prec>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^+"
|
|
466 |
|
|
467 |
|
|
468 |
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk>
|
|
469 |
\<Longrightarrow> (I,J) \<in> subint1 G"
|
|
470 |
apply (simp add: subint1_def)
|
|
471 |
done
|
|
472 |
|
|
473 |
lemma subcls1I:"\<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,(super c)) \<in> subcls1 G"
|
|
474 |
apply (simp add: subcls1_def)
|
|
475 |
done
|
|
476 |
|
|
477 |
|
|
478 |
lemma subint1D: "(I,J)\<in>subint1 G\<Longrightarrow> \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)"
|
|
479 |
by (simp add: subint1_def)
|
|
480 |
|
|
481 |
lemma subcls1D:
|
|
482 |
"(C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c. class G C = Some c \<and> (super c = D))"
|
|
483 |
apply (simp add: subcls1_def)
|
|
484 |
apply auto
|
|
485 |
done
|
|
486 |
|
|
487 |
lemma subint1_def2:
|
|
488 |
"subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (isuperIfs (the (iface G I))))"
|
|
489 |
apply (unfold subint1_def)
|
|
490 |
apply auto
|
|
491 |
done
|
|
492 |
|
|
493 |
lemma subcls1_def2:
|
|
494 |
"subcls1 G = (\<Sigma>C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
|
|
495 |
apply (unfold subcls1_def)
|
|
496 |
apply auto
|
|
497 |
done
|
|
498 |
|
|
499 |
lemma subcls_is_class:
|
|
500 |
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D\<rbrakk> \<Longrightarrow> \<exists> c. class G C = Some c"
|
|
501 |
by (auto simp add: subcls1_def dest: tranclD)
|
|
502 |
|
|
503 |
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C\<^sub>1 D \<Longrightarrow> P"
|
|
504 |
by (auto simp add: subcls1_def)
|
|
505 |
|
|
506 |
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P"
|
|
507 |
apply (erule trancl_induct)
|
|
508 |
apply (auto intro: no_subcls1_Object)
|
|
509 |
done
|
|
510 |
|
|
511 |
section "well-structured programs"
|
|
512 |
|
|
513 |
constdefs
|
|
514 |
ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
|
|
515 |
"ws_idecl G I si \<equiv> \<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
|
|
516 |
|
|
517 |
ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
|
|
518 |
"ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
|
|
519 |
|
|
520 |
ws_prog :: "prog \<Rightarrow> bool"
|
|
521 |
"ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces G). ws_idecl G I (isuperIfs i)) \<and>
|
|
522 |
(\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
|
|
523 |
|
|
524 |
|
|
525 |
lemma ws_progI:
|
|
526 |
"\<lbrakk>\<forall>(I,i)\<in>set (ifaces G). \<forall>J\<in>set (isuperIfs i). is_iface G J \<and>
|
|
527 |
(J,I) \<notin> (subint1 G)^+;
|
|
528 |
\<forall>(C,c)\<in>set (classes G). C\<noteq>Object \<longrightarrow> is_class G (super c) \<and>
|
|
529 |
((super c),C) \<notin> (subcls1 G)^+
|
|
530 |
\<rbrakk> \<Longrightarrow> ws_prog G"
|
|
531 |
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
|
|
532 |
apply (erule_tac conjI)
|
|
533 |
apply blast
|
|
534 |
done
|
|
535 |
|
|
536 |
lemma ws_prog_ideclD:
|
|
537 |
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow>
|
|
538 |
is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
|
|
539 |
apply (unfold ws_prog_def ws_idecl_def)
|
|
540 |
apply clarify
|
|
541 |
apply (drule_tac map_of_SomeD)
|
|
542 |
apply auto
|
|
543 |
done
|
|
544 |
|
|
545 |
lemma ws_prog_cdeclD:
|
|
546 |
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>
|
|
547 |
is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+"
|
|
548 |
apply (unfold ws_prog_def ws_cdecl_def)
|
|
549 |
apply clarify
|
|
550 |
apply (drule_tac map_of_SomeD)
|
|
551 |
apply auto
|
|
552 |
done
|
|
553 |
|
|
554 |
|
|
555 |
section "well-foundedness"
|
|
556 |
|
|
557 |
lemma finite_is_iface: "finite {I. is_iface G I}"
|
|
558 |
apply (fold dom_def)
|
|
559 |
apply (rule_tac finite_dom_map_of)
|
|
560 |
done
|
|
561 |
|
|
562 |
lemma finite_is_class: "finite {C. is_class G C}"
|
|
563 |
apply (fold dom_def)
|
|
564 |
apply (rule_tac finite_dom_map_of)
|
|
565 |
done
|
|
566 |
|
|
567 |
lemma finite_subint1: "finite (subint1 G)"
|
|
568 |
apply (subst subint1_def2)
|
|
569 |
apply (rule finite_SigmaI)
|
|
570 |
apply (rule finite_is_iface)
|
|
571 |
apply (simp (no_asm))
|
|
572 |
done
|
|
573 |
|
|
574 |
lemma finite_subcls1: "finite (subcls1 G)"
|
|
575 |
apply (subst subcls1_def2)
|
|
576 |
apply (rule finite_SigmaI)
|
|
577 |
apply (rule finite_is_class)
|
|
578 |
apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
|
|
579 |
apply auto
|
|
580 |
done
|
|
581 |
|
|
582 |
lemma subint1_irrefl_lemma1:
|
|
583 |
"ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
|
|
584 |
apply (force dest: subint1D ws_prog_ideclD conjunct2)
|
|
585 |
done
|
|
586 |
|
|
587 |
lemma subcls1_irrefl_lemma1:
|
|
588 |
"ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
|
|
589 |
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
|
|
590 |
done
|
|
591 |
|
|
592 |
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
|
|
593 |
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
|
|
594 |
|
|
595 |
lemma subint1_irrefl: "\<lbrakk>(x, y) \<in> subint1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
|
|
596 |
apply (rule irrefl_trancl_rD)
|
|
597 |
apply (rule subint1_irrefl_lemma2)
|
|
598 |
apply auto
|
|
599 |
done
|
|
600 |
|
|
601 |
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
|
|
602 |
apply (rule irrefl_trancl_rD)
|
|
603 |
apply (rule subcls1_irrefl_lemma2)
|
|
604 |
apply auto
|
|
605 |
done
|
|
606 |
|
|
607 |
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
|
|
608 |
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
|
|
609 |
|
|
610 |
|
|
611 |
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
|
|
612 |
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
|
|
613 |
|
|
614 |
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)"
|
|
615 |
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
|
|
616 |
|
|
617 |
|
|
618 |
lemma subint1_induct:
|
|
619 |
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subint1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
|
|
620 |
apply (frule wf_subint1)
|
|
621 |
apply (erule wf_induct)
|
|
622 |
apply (simp (no_asm_use) only: converse_iff)
|
|
623 |
apply blast
|
|
624 |
done
|
|
625 |
|
|
626 |
lemma subcls1_induct [consumes 1]:
|
|
627 |
"\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subcls1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
|
|
628 |
apply (frule wf_subcls1)
|
|
629 |
apply (erule wf_induct)
|
|
630 |
apply (simp (no_asm_use) only: converse_iff)
|
|
631 |
apply blast
|
|
632 |
done
|
|
633 |
|
|
634 |
lemma ws_subint1_induct:
|
|
635 |
"\<lbrakk>is_iface G I; ws_prog G; \<And>I i. \<lbrakk>iface G I = Some i \<and>
|
|
636 |
(\<forall>J \<in> set (isuperIfs i). (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I
|
|
637 |
\<rbrakk> \<Longrightarrow> P I"
|
|
638 |
apply (erule make_imp)
|
|
639 |
apply (rule subint1_induct)
|
|
640 |
apply assumption
|
|
641 |
apply safe
|
|
642 |
apply (fast dest: subint1I ws_prog_ideclD)
|
|
643 |
done
|
|
644 |
|
|
645 |
|
|
646 |
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;
|
|
647 |
\<And>C c. \<lbrakk>class G C = Some c;
|
|
648 |
(C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and>
|
|
649 |
P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
|
|
650 |
\<rbrakk> \<Longrightarrow> P C"
|
|
651 |
apply (erule make_imp)
|
|
652 |
apply (rule subcls1_induct)
|
|
653 |
apply assumption
|
|
654 |
apply safe
|
|
655 |
apply (fast dest: subcls1I ws_prog_cdeclD)
|
|
656 |
done
|
|
657 |
|
|
658 |
lemma ws_class_induct [consumes 2, case_names Object Subcls]:
|
|
659 |
"\<lbrakk>class G C = Some c; ws_prog G;
|
|
660 |
\<And> co. class G Object = Some co \<Longrightarrow> P Object;
|
|
661 |
\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
|
|
662 |
\<rbrakk> \<Longrightarrow> P C"
|
|
663 |
proof -
|
|
664 |
assume clsC: "class G C = Some c"
|
|
665 |
and init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object"
|
|
666 |
and step: "\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C"
|
|
667 |
assume ws: "ws_prog G"
|
|
668 |
then have "is_class G C \<Longrightarrow> P C"
|
|
669 |
proof (induct rule: subcls1_induct)
|
|
670 |
fix C
|
|
671 |
assume hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<longrightarrow> is_class G S \<longrightarrow> P S"
|
|
672 |
and iscls:"is_class G C"
|
|
673 |
show "P C"
|
|
674 |
proof (cases "C=Object")
|
|
675 |
case True with iscls init show "P C" by auto
|
|
676 |
next
|
|
677 |
case False with ws step hyp iscls
|
|
678 |
show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
|
|
679 |
qed
|
|
680 |
qed
|
|
681 |
with clsC show ?thesis by simp
|
|
682 |
qed
|
|
683 |
|
|
684 |
lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
|
|
685 |
"\<lbrakk>is_class G C; ws_prog G;
|
|
686 |
\<And> co. class G Object = Some co \<Longrightarrow> P Object;
|
|
687 |
\<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
|
|
688 |
\<rbrakk> \<Longrightarrow> P C"
|
|
689 |
by (blast intro: ws_class_induct)
|
|
690 |
|
|
691 |
lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
|
|
692 |
"\<lbrakk>class G C = Some c; ws_prog G;
|
|
693 |
\<And> co. class G Object = Some co \<Longrightarrow> P Object co;
|
|
694 |
\<And> C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc;
|
|
695 |
C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c
|
|
696 |
\<rbrakk> \<Longrightarrow> P C c"
|
|
697 |
proof -
|
|
698 |
assume clsC: "class G C = Some c"
|
|
699 |
and init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co"
|
|
700 |
and step: "\<And> C c sc . \<lbrakk>class G C = Some c; class G (super c) = Some sc;
|
|
701 |
C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c"
|
|
702 |
assume ws: "ws_prog G"
|
|
703 |
then have "\<And> c. class G C = Some c\<Longrightarrow> P C c"
|
|
704 |
proof (induct rule: subcls1_induct)
|
|
705 |
fix C c
|
|
706 |
assume hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<longrightarrow> (\<forall> s. class G S = Some s \<longrightarrow> P S s)"
|
|
707 |
and iscls:"class G C = Some c"
|
|
708 |
show "P C c"
|
|
709 |
proof (cases "C=Object")
|
|
710 |
case True with iscls init show "P C c" by auto
|
|
711 |
next
|
|
712 |
case False
|
|
713 |
with ws iscls obtain sc where
|
|
714 |
sc: "class G (super c) = Some sc"
|
|
715 |
by (auto dest: ws_prog_cdeclD)
|
|
716 |
from iscls False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 (super c)" by (rule subcls1I)
|
|
717 |
with False ws step hyp iscls sc
|
|
718 |
show "P C c"
|
|
719 |
by (auto)
|
|
720 |
qed
|
|
721 |
qed
|
|
722 |
with clsC show "P C c" by auto
|
|
723 |
qed
|
|
724 |
|
|
725 |
lemma ws_interface_induct [consumes 2, case_names Step]:
|
|
726 |
(assumes is_if_I: "is_iface G I" and
|
|
727 |
ws: "ws_prog G" and
|
|
728 |
hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i;
|
|
729 |
\<forall> J \<in> set (isuperIfs i).
|
|
730 |
(I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
|
|
731 |
) "P I"
|
|
732 |
proof -
|
|
733 |
from is_if_I ws
|
|
734 |
show "P I"
|
|
735 |
proof (rule ws_subint1_induct)
|
|
736 |
fix I i
|
|
737 |
assume hyp: "iface G I = Some i \<and>
|
|
738 |
(\<forall>J\<in>set (isuperIfs i). (I,J) \<in>subint1 G \<and> P J \<and> is_iface G J)"
|
|
739 |
then have if_I: "iface G I = Some i"
|
|
740 |
by blast
|
|
741 |
show "P I"
|
|
742 |
proof (cases "isuperIfs i")
|
|
743 |
case Nil
|
|
744 |
with if_I hyp_sub
|
|
745 |
show "P I"
|
|
746 |
by auto
|
|
747 |
next
|
|
748 |
case (Cons hd tl)
|
|
749 |
with hyp if_I hyp_sub
|
|
750 |
show "P I"
|
|
751 |
by auto
|
|
752 |
qed
|
|
753 |
qed
|
|
754 |
qed
|
|
755 |
|
|
756 |
section "general recursion operators for the interface and class hiearchies"
|
|
757 |
|
|
758 |
consts
|
|
759 |
iface_rec :: "prog \<times> qtname \<Rightarrow> \<spacespace> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
760 |
class_rec :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
|
|
761 |
|
|
762 |
recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)"
|
|
763 |
"iface_rec (G,I) =
|
|
764 |
(\<lambda>f. case iface G I of
|
|
765 |
None \<Rightarrow> arbitrary
|
|
766 |
| Some i \<Rightarrow> if ws_prog G
|
|
767 |
then f I i
|
|
768 |
((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
|
|
769 |
else arbitrary)"
|
|
770 |
(hints recdef_wf: wf_subint1 intro: subint1I)
|
|
771 |
declare iface_rec.simps [simp del]
|
|
772 |
|
|
773 |
lemma iface_rec:
|
|
774 |
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>
|
|
775 |
iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))"
|
|
776 |
apply (subst iface_rec.simps)
|
|
777 |
apply simp
|
|
778 |
done
|
|
779 |
|
|
780 |
recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
|
|
781 |
"class_rec(G,C) =
|
|
782 |
(\<lambda>t f. case class G C of
|
|
783 |
None \<Rightarrow> arbitrary
|
|
784 |
| Some c \<Rightarrow> if ws_prog G
|
|
785 |
then f C c
|
|
786 |
(if C = Object then t
|
|
787 |
else class_rec (G,super c) t f)
|
|
788 |
else arbitrary)"
|
|
789 |
(hints recdef_wf: wf_subcls1 intro: subcls1I)
|
|
790 |
declare class_rec.simps [simp del]
|
|
791 |
|
|
792 |
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>
|
|
793 |
class_rec (G,C) t f =
|
|
794 |
f C c (if C = Object then t else class_rec (G,super c) t f)"
|
|
795 |
apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
|
|
796 |
apply simp
|
|
797 |
done
|
|
798 |
(*
|
|
799 |
lemma bar:
|
|
800 |
"[| P; !!x. P ==> Q x |] ==> Q x"
|
|
801 |
by simp
|
|
802 |
|
|
803 |
lemma metaMP: "[| A ==> B; A |] ==> B"
|
|
804 |
by blast
|
|
805 |
|
|
806 |
lemma True
|
|
807 |
proof-
|
|
808 |
presume t: "C ==> E"
|
|
809 |
thm metaMP [OF t]
|
|
810 |
|
|
811 |
presume r1: "\<And> B. P \<Longrightarrow> B"
|
|
812 |
presume r2: "\<And> C. C \<Longrightarrow> P"
|
|
813 |
thm r1 [OF r2]
|
|
814 |
|
|
815 |
thm metaMP [OF t]
|
|
816 |
|
|
817 |
lemma ws_subcls1_induct4: "\<lbrakk>is_class G C; ws_prog G;
|
|
818 |
\<And>C c. \<lbrakk>C \<noteq> Object\<longrightarrow> P (super c)\<rbrakk> \<Longrightarrow> P C
|
|
819 |
\<rbrakk> \<Longrightarrow> P C"
|
|
820 |
proof -
|
|
821 |
assume cls_C: "is_class G C"
|
|
822 |
and ws: "ws_prog G"
|
|
823 |
and hyp: "\<And>C c. \<lbrakk>C \<noteq> Object\<longrightarrow> P (super c)\<rbrakk> \<Longrightarrow> P C"
|
|
824 |
thm ws_subcls1_induct [OF cls_C ws hyp]
|
|
825 |
|
|
826 |
show
|
|
827 |
(\<And>C c. class G C = Some c \<and>
|
|
828 |
(C \<noteq> Object \<longrightarrow> G\<turnstile>C\<prec>\<^sub>C\<^sub>1super c \<and> ?P (super c) \<and> is_class G (super c)) \<Longrightarrow>
|
|
829 |
?P C) \<Longrightarrow>
|
|
830 |
?P C
|
|
831 |
show ?thesis
|
|
832 |
thm "thm ws_subcls1_induct [OF cls_C ws hyp]"
|
|
833 |
apply (rule ws_subcls1_induct)
|
|
834 |
proof (rule ws_subcls1_induct)
|
|
835 |
fix C c
|
|
836 |
assume "class G C = Some c \<and>
|
|
837 |
(C \<noteq> Object \<longrightarrow>
|
|
838 |
G\<turnstile>C\<prec>\<^sub>C\<^sub>1super c \<and> P (super c) \<and> is_class G (super c))"
|
|
839 |
show "C \<noteq> Object \<longrightarrow> P (super (?c C c))"
|
|
840 |
apply (erule ws_subcls1_induct)
|
|
841 |
apply assumption
|
|
842 |
apply (erule conjE)
|
|
843 |
apply (case_tac "C=Object")
|
|
844 |
apply blast
|
|
845 |
apply (erule impE)
|
|
846 |
apply assumption
|
|
847 |
apply (erule conjE)+
|
|
848 |
apply (rotate_tac 2)
|
|
849 |
sorry
|
|
850 |
|
|
851 |
*)
|
|
852 |
|
|
853 |
|
|
854 |
constdefs
|
|
855 |
imethds:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
|
|
856 |
(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
|
|
857 |
"imethds G I
|
|
858 |
\<equiv> iface_rec (G,I)
|
|
859 |
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
|
|
860 |
(o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
|
|
861 |
|
|
862 |
|
|
863 |
|
|
864 |
end
|