author | wenzelm |
Wed, 17 Feb 2016 23:06:24 +0100 | |
changeset 62354 | fdd6989cc8a0 |
parent 62042 | 6c6ccf573479 |
child 63648 | f9f3006a5579 |
permissions | -rw-r--r-- |
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 |
*) |
62042 | 4 |
subsection \<open>Field, method, interface, and class declarations, whole Java programs |
5 |
\<close> |
|
12854 | 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 |
|
62042 | 12 |
text \<open> |
12854 | 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 |
|
54703 | 18 |
@{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"} |
12854 | 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} |
|
62042 | 39 |
\<close> |
12854 | 40 |
|
62042 | 41 |
subsection \<open>Modifier\<close> |
12854 | 42 |
|
62042 | 43 |
subsubsection \<open>Access modifier\<close> |
12854 | 44 |
|
58310 | 45 |
datatype acc_modi (* access modifier *) |
12854 | 46 |
= Private | Package | Protected | Public |
47 |
||
62042 | 48 |
text \<open> |
12854 | 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 |
|
62042 | 52 |
\<close> |
12854 | 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) |
|
62042 | 73 |
show "x \<le> x" \<comment> reflexivity |
12854 | 74 |
by (auto simp add: le_acc_def) |
41525 | 75 |
{ |
62042 | 76 |
assume "x \<le> y" "y \<le> z" \<comment> transitivity |
41525 | 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 |
62042 | 80 |
assume "x \<le> y" "y \<le> x" \<comment> antisymmetry |
41525 | 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 |
||
62042 | 140 |
subsubsection \<open>Static Modifier\<close> |
41778 | 141 |
type_synonym stat_modi = bool (* modifier: static *) |
12854 | 142 |
|
62042 | 143 |
subsection \<open>Declaration (base "class" for member,interface and class |
144 |
declarations\<close> |
|
12854 | 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 |
|
62042 | 153 |
subsection \<open>Member (field or method)\<close> |
12854 | 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 |
|
62042 | 161 |
subsection \<open>Field\<close> |
12854 | 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 tab-width;
wenzelm
parents:
30235
diff
changeset
|
170 |
= "vname \<times> field" |
12854 | 171 |
|
172 |
||
173 |
translations |
|
35431 | 174 |
(type) "fdecl" <= (type) "vname \<times> field" |
12854 | 175 |
|
62042 | 176 |
subsection \<open>Method\<close> |
12854 | 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 |
||
62042 | 222 |
text \<open>To be able to talk uniformaly about field and method declarations we |
12854 | 223 |
introduce the notion of a member declaration (e.g. useful to define |
62042 | 224 |
accessiblity )\<close> |
12854 | 225 |
|
58310 | 226 |
datatype memberdecl = fdecl fdecl | mdecl mdecl |
12854 | 227 |
|
58310 | 228 |
datatype memberid = fid vname | mid sig |
12854 | 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 |
||
62042 | 296 |
subsection \<open>Interface\<close> |
12854 | 297 |
|
298 |
||
62042 | 299 |
record ibody = decl + \<comment>\<open>interface body\<close> |
300 |
imethods :: "(sig \<times> mhead) list" \<comment>\<open>method heads\<close> |
|
12854 | 301 |
|
62042 | 302 |
record iface = ibody + \<comment>\<open>interface\<close> |
303 |
isuperIfs:: "qtname list" \<comment>\<open>superinterface list\<close> |
|
41778 | 304 |
type_synonym |
62042 | 305 |
idecl \<comment>\<open>interface declaration, cf. 9.1\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 |
||
62042 | 327 |
subsection \<open>Class\<close> |
328 |
record cbody = decl + \<comment>\<open>class body\<close> |
|
12854 | 329 |
cfields:: "fdecl list" |
330 |
methods:: "mdecl list" |
|
62042 | 331 |
init :: "stmt" \<comment>\<open>initializer\<close> |
12854 | 332 |
|
62042 | 333 |
record "class" = cbody + \<comment>\<open>class\<close> |
334 |
super :: "qtname" \<comment>\<open>superclass\<close> |
|
335 |
superIfs:: "qtname list" \<comment>\<open>implemented interfaces\<close> |
|
41778 | 336 |
type_synonym |
62042 | 337 |
cdecl \<comment>\<open>class declaration, cf. 8.1\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 |
||
58887 | 370 |
subsubsection "standard classes" |
12854 | 371 |
|
372 |
consts |
|
62042 | 373 |
Object_mdecls :: "mdecl list" \<comment>\<open>methods of Object\<close> |
374 |
SXcpt_mdecls :: "mdecl list" \<comment>\<open>methods of SXcpts\<close> |
|
12854 | 375 |
|
37956 | 376 |
definition |
62042 | 377 |
ObjectC :: "cdecl" \<comment>\<open>declaration of root class\<close> where |
37956 | 378 |
"ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls, |
379 |
init=Skip,super=undefined,superIfs=[]\<rparr>)" |
|
12854 | 380 |
|
37956 | 381 |
definition |
62042 | 382 |
SXcptC ::"xname \<Rightarrow> cdecl" \<comment>\<open>declarations of throwable classes\<close> where |
37956 | 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 tab-width;
wenzelm
parents:
30235
diff
changeset
|
398 |
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
399 |
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]" |
12854 | 400 |
|
401 |
||
58887 | 402 |
subsubsection "programs" |
12854 | 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 |
||
58887 | 429 |
subsubsection "is type" |
12854 | 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 |
||
58887 | 448 |
subsubsection "subinterface and subclass relation, in anticipation of TypeRel.thy" |
12854 | 449 |
|
37956 | 450 |
definition |
62042 | 451 |
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subinterface\<close> |
37956 | 452 |
where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}" |
12854 | 453 |
|
37956 | 454 |
definition |
62042 | 455 |
subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subclass\<close> |
37956 | 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 |
61989 | 459 |
subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C1_" [71,71,71] 70) |
460 |
where "G\<turnstile>C \<prec>\<^sub>C1 D == (C,D) \<in> subcls1 G" |
|
35067
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 |
61989 | 463 |
subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) |
464 |
where "G\<turnstile>C \<preceq>\<^sub>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 |
61989 | 467 |
subcls_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70) |
468 |
where "G\<turnstile>C \<prec>\<^sub>C D == (C,D) \<in>(subcls1 G)^+" |
|
12854 | 469 |
|
61989 | 470 |
notation (ASCII) |
471 |
subcls1_syntax ("_|-_<:C1_" [71,71,71] 70) and |
|
472 |
subclseq_syntax ("_|-_<=:C _"[71,71,71] 70) and |
|
473 |
subcls_syntax ("_|-_<: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 x-symbol 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 x-symbol syntax <Sigma> for dependent products
paulson
parents:
14674
diff
changeset
|
501 |
"subcls1 G = |
47455995693d
removal of x-symbol 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 |
||
58887 | 519 |
subsubsection "well-structured programs" |
12854 | 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 |
||
58887 | 565 |
subsubsection "well-foundedness" |
12854 | 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 tab-width;
wenzelm
parents:
30235
diff
changeset
|
726 |
sc: "class G (super c) = Some sc" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 tab-width;
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 tab-width;
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 tab-width;
wenzelm
parents:
30235
diff
changeset
|
763 |
by auto |
12854 | 764 |
qed |
765 |
qed |
|
766 |
qed |
|
767 |
||
58887 | 768 |
subsubsection "general recursion operators for the interface and class hiearchies" |
12854 | 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 |
|
62042 | 818 |
\<comment>\<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close> |
37956 | 819 |
"imethds G I = iface_rec G I |
12854 | 820 |
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> |
55518
1ddb2edf5ceb
folded 'Option.set' into BNF-generated 'set_option'
blanchet
parents:
54703
diff
changeset
|
821 |
(set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
822 |
|
12854 | 823 |
|
824 |
||
825 |
end |