author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9348 | f495dba0cb07 |
child 10061 | fe82134773dc |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/TypeRel.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
The relations between Java types |
|
7 |
*) |
|
8 |
||
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
9246
diff
changeset
|
9 |
TypeRel = Decl + |
8011 | 10 |
|
11 |
consts |
|
10042 | 12 |
subcls1 :: "'c prog => (cname \\<times> cname) set" (* subclass *) |
13 |
widen :: "'c prog => (ty \\<times> ty ) set" (* widening *) |
|
14 |
cast :: "'c prog => (cname \\<times> cname) set" (* casting *) |
|
8011 | 15 |
|
16 |
syntax |
|
10042 | 17 |
subcls1 :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70) |
18 |
subcls :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _" [71,71,71] 70) |
|
19 |
widen :: "'c prog => [ty , ty ] => bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70) |
|
20 |
cast :: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70) |
|
8011 | 21 |
|
22 |
translations |
|
23 |
"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G" |
|
8106 | 24 |
"G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*" |
8011 | 25 |
"G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G" |
9348 | 26 |
"G\\<turnstile>C \\<preceq>? D" == "(C,D) \\<in> cast G" |
8011 | 27 |
|
28 |
defs |
|
29 |
||
30 |
(* direct subclass, cf. 8.1.3 *) |
|
10042 | 31 |
subcls1_def "subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}" |
8011 | 32 |
|
33 |
consts |
|
34 |
||
10042 | 35 |
method :: "'c prog \\<times> cname => ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)" |
36 |
field :: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)" |
|
37 |
fields :: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times> ty) list" |
|
8011 | 38 |
|
39 |
constdefs (* auxiliary relations for recursive definitions below *) |
|
40 |
||
41 |
subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set" |
|
10042 | 42 |
"subcls1_rel == {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}" |
8011 | 43 |
|
44 |
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
45 |
recdef method "subcls1_rel" |
10042 | 46 |
"method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty |
47 |
| Some (sc,fs,ms) => (case sc of None => empty | Some D => |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
48 |
if is_class G D then method (G,D) |
8011 | 49 |
else arbitrary) \\<oplus> |
50 |
map_of (map (\\<lambda>(s, m ). |
|
51 |
(s,(C,m))) ms)) |
|
52 |
else arbitrary)" |
|
53 |
||
54 |
(* list of fields of a class, including inherited and hidden ones *) |
|
55 |
recdef fields "subcls1_rel" |
|
10042 | 56 |
"fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary |
57 |
| Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@ |
|
58 |
(case sc of None => [] | Some D => |
|
8011 | 59 |
if is_class G D then fields (G,D) |
60 |
else arbitrary)) |
|
61 |
else arbitrary)" |
|
62 |
defs |
|
63 |
||
10042 | 64 |
field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields" |
8011 | 65 |
|
66 |
inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3 |
|
67 |
i.e. sort of syntactic subtyping *) |
|
9348 | 68 |
refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *) |
10042 | 69 |
subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D" |
9348 | 70 |
null "G\\<turnstile> NT \\<preceq> RefT R" |
8011 | 71 |
|
9246 | 72 |
inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *) |
9348 | 73 |
(* left out casts on primitve types *) |
10042 | 74 |
widen "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D" |
75 |
subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D" |
|
8011 | 76 |
|
77 |
end |