7 header "Type relations" |
7 header "Type relations" |
8 |
8 |
9 theory TypeRel imports Decl begin |
9 theory TypeRel imports Decl begin |
10 |
10 |
11 consts |
11 consts |
12 widen :: "(ty \<times> ty ) set" --{* widening *} |
|
13 subcls1 :: "(cname \<times> cname) set" --{* subclass *} |
12 subcls1 :: "(cname \<times> cname) set" --{* subclass *} |
14 |
13 |
15 syntax (xsymbols) |
14 syntax (xsymbols) |
16 widen :: "[ty , ty ] => bool" ("_ \<preceq> _" [71,71] 70) |
|
17 subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70) |
15 subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70) |
18 subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70) |
16 subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70) |
19 syntax |
17 syntax |
20 widen :: "[ty , ty ] => bool" ("_ <= _" [71,71] 70) |
|
21 subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) |
18 subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) |
22 subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) |
19 subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) |
23 |
20 |
24 translations |
21 translations |
25 "C \<prec>C1 D" == "(C,D) \<in> subcls1" |
22 "C \<prec>C1 D" == "(C,D) \<in> subcls1" |
26 "C \<preceq>C D" == "(C,D) \<in> subcls1^*" |
23 "C \<preceq>C D" == "(C,D) \<in> subcls1^*" |
27 "S \<preceq> T" == "(S,T) \<in> widen" |
|
28 |
24 |
29 consts |
25 consts |
30 method :: "cname => (mname \<rightharpoonup> methd)" |
26 method :: "cname => (mname \<rightharpoonup> methd)" |
31 field :: "cname => (fname \<rightharpoonup> ty)" |
27 field :: "cname => (fname \<rightharpoonup> ty)" |
32 |
28 |
36 text{* Direct subclass relation *} |
32 text{* Direct subclass relation *} |
37 defs |
33 defs |
38 subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" |
34 subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" |
39 |
35 |
40 text{* Widening, viz. method invocation conversion *} |
36 text{* Widening, viz. method invocation conversion *} |
41 inductive widen intros |
37 inductive |
42 refl [intro!, simp]: "T \<preceq> T" |
38 widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70) |
43 subcls : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" |
39 where |
44 null [intro!]: "NT \<preceq> R" |
40 refl [intro!, simp]: "T \<preceq> T" |
|
41 | subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" |
|
42 | null [intro!]: "NT \<preceq> R" |
45 |
43 |
46 lemma subcls1D: |
44 lemma subcls1D: |
47 "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)" |
45 "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)" |
48 apply (unfold subcls1_def) |
46 apply (unfold subcls1_def) |
49 apply auto |
47 apply auto |